Cost Functional Equation

/-- **Law of Logic cost theorem**: The J-cost function is the unique
    reciprocal cost satisfying the RCL, normalization, calibration, and continuity.

    This version uses the global Aczél axiom internally and requires NO regularity
    hypothesis parameters from the caller. -/
theorem law_of_logic_forces_jcost (F : ℝ → ℝ)
    [AczelSmoothnessPackage]
    (hRecip : IsReciprocalCost F)
    (hNorm : IsNormalized F)
    (hComp : SatisfiesCompositionLaw F)
    (hCalib : IsCalibrated F)
    (hCont : ContinuousOn F (Set.Ioi 0)) :
    ∀ x : ℝ, 0 < x → F x = Cost.Jcost x := by
  intro x hx
  have hSymm : ∀ {y}, 0 < y → F y = F y⁻¹ := fun {y} hy => hRecip y hy
  have hCoshAdd : CoshAddIdentity F := composition_law_equiv_coshAdd F |>.mp hComp
  let Gf : ℝ → ℝ := G F
  let Hf : ℝ → ℝ := H F
  have h_G0 : Gf 0 = 0 := G_zero_of_unit F hNorm
  have h_H0 : Hf 0 = 1 := by
    show H F 0 = 1
    simp only [H, G, Real.exp_zero]
    rw [hNorm]; ring
  have h_G_cont : Continuous Gf := by
    have h := ContinuousOn.comp_continuous hCont continuous_exp
    have h' : Continuous (fun t => F (Real.exp t)) :=
      h (by intro t; exact Set.mem_Ioi.mpr (Real.exp_pos t))
    simp [Gf, G] at h'
    exact h'
  have h_H_cont : Continuous Hf := by
    simpa [Hf, H] using h_G_cont.add continuous_const
  have h_direct : DirectCoshAdd Gf := CoshAddIdentity_implies_DirectCoshAdd F hCoshAdd
  have h_dAlembert : ∀ t u, Hf (t + u) + Hf (t - u) = 2 * Hf t * Hf u := by
    intro t u
    have hG := h_direct t u
    have h_goal : (Gf (t + u) + 1) + (Gf (t - u) + 1) = 2 * (Gf t + 1) * (Gf u + 1) := by
      calc (Gf (t + u) + 1) + (Gf (t - u) + 1)
          = (Gf (t + u) + Gf (t - u)) + 2 := by ring
        _ = (2 * (Gf t * Gf u) + 2 * (Gf t + Gf u)) + 2 := by simp [hG]
        _ = 2 * (Gf t + 1) * (Gf u + 1) := by ring
    simp [Hf, H, Gf] at h_goal
    exact h_goal
  have h_H_d2 : deriv (deriv Hf) 0 = 1 := by
    have hG_d2 : deriv (deriv Gf) 0 = 1 := by simpa [Gf, G] using hCalib
    have hderiv : deriv Hf = deriv Gf := by
      funext t; change deriv (fun y => Gf y + 1) t = deriv Gf t
      exact (deriv_add_const (f := Gf) (x := t) (c := (1 : ℝ)))
    have hderiv2 : deriv (deriv Hf) = deriv (deriv Gf) := congrArg deriv hderiv
    exact (congrArg (fun g => g 0) hderiv2).trans hG_d2
  have h_H_cosh : ∀ t, Hf t = Real.cosh t :=
    dAlembert_cosh_solution_aczel Hf h_H0 h_H_cont h_dAlembert h_H_d2
  have h_G_cosh : ∀ t, Gf t = Real.cosh t - 1 := fun t => by
    have : Gf t + 1 = Real.cosh t := h_H_cosh t
    linarith
  have ht : Real.exp (Real.log x) = x := Real.exp_log hx
  have hJG : G Cost.Jcost (Real.log x) = Real.cosh (Real.log x) - 1 :=
    Jcost_G_eq_cosh_sub_one (Real.log x)
  calc F x
      = F (Real.exp (Real.log x)) := by rw [ht]
    _ = Gf (Real.log x) := rfl
    _ = Real.cosh (Real.log x) - 1 := h_G_cosh (Real.log x)
    _ = G Cost.Jcost (Real.log x) := by simp only [hJG]
    _ = Cost.Jcost (Real.exp (Real.log x)) := by simp [G]
    _ = Cost.Jcost x := by simp [ht]

theorem dAlembert_cosh_solution
    (H : ℝ → ℝ)
    (h_one : H 0 = 1)
    (h_cont : Continuous H)
    (h_dAlembert : ∀ t u, H (t+u) + H (t-u) = 2 * H t * H u)
    (h_deriv2_zero : deriv (deriv H) 0 = 1)
    (h_smooth_hyp : dAlembert_continuous_implies_smooth_hypothesis H)
    (h_ode_hyp : dAlembert_to_ODE_hypothesis H)
    (h_cont_hyp : ode_regularity_continuous_hypothesis H)
    (h_diff_hyp : ode_regularity_differentiable_hypothesis H)
    (h_bootstrap_hyp : ode_linear_regularity_bootstrap_hypothesis H) :
    ∀ t, H t = Real.cosh t := by
  have h_ode : ∀ t, deriv (deriv H) t = H t := h_ode_hyp h_one h_cont h_dAlembert h_deriv2_zero
  have h_even : Function.Even H := dAlembert_even H h_one h_dAlembert
  have h_deriv_zero : deriv H 0 = 0 := by
    have h_smooth := h_smooth_hyp h_one h_cont h_dAlembert
    have h_diff : DifferentiableAt ℝ H 0 := h_smooth.differentiable (by decide : (⊤ : WithTop ℕ∞) ≠ 0) |>.differentiableAt
    exact even_deriv_at_zero H h_even h_diff
  exact ode_cosh_uniqueness H h_ode h_one h_deriv_zero h_cont_hyp h_diff_hyp h_bootstrap_hyp

/-- **Key Identity**: The composition law on F is equivalent to CoshAddIdentity on G.

Specifically: F(xy) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y)
becomes: G(s+t) + G(s-t) = 2G(s)G(t) + 2G(s) + 2G(t)
via the substitution x = e^s, y = e^t. -/
theorem composition_law_equiv_coshAdd (F : ℝ → ℝ) :
    SatisfiesCompositionLaw F ↔ CoshAddIdentity F := by
  constructor
  · intro hComp t u
    have hexp_t_pos : 0 < Real.exp t := Real.exp_pos t
    have hexp_u_pos : 0 < Real.exp u := Real.exp_pos u
    have h := hComp (Real.exp t) (Real.exp u) hexp_t_pos hexp_u_pos
    -- exp(t) * exp(u) = exp(t + u)
    have h1 : Real.exp t * Real.exp u = Real.exp (t + u) := (Real.exp_add t u).symm
    -- exp(t) / exp(u) = exp(t - u)
    have h2 : Real.exp t / Real.exp u = Real.exp (t - u) := by
      rw [div_eq_mul_inv, ← Real.exp_neg u, ← Real.exp_add, sub_eq_add_neg]
    simp only [G, h1, h2] at h ⊢
    linarith
  · intro hCosh x y hx hy
    let t := Real.log x
    let u := Real.log y
    have hx_eq : x = Real.exp t := (Real.exp_log hx).symm
    have hy_eq : y = Real.exp u := (Real.exp_log hy).symm
    have h := hCosh t u
    simp only [G] at h
    rw [hx_eq, hy_eq]
    rw [← Real.exp_add, ← Real.exp_sub]
    -- h : F (exp (t + u)) + F (exp (t - u)) = 2 * (F (exp t) * F (exp u)) + 2 * (F (exp t) + F (exp u))
    -- Goal: F (exp (t + u)) + F (exp (t - u)) = 2 * F (exp t) * F (exp u) + 2 * F (exp t) + 2 * F (exp u)
    calc F (Real.exp (t + u)) + F (Real.exp (t - u))
        = 2 * (F (Real.exp t) * F (Real.exp u)) + 2 * (F (Real.exp t) + F (Real.exp u)) := h
      _ = 2 * F (Real.exp t) * F (Real.exp u) + 2 * F (Real.exp t) + 2 * F (Real.exp u) := by ring

/-- The composition law together with unit log curvature force normalization.
The composition law at `y = 1` gives `F 1 * (F x + 1) = 0`, so either `F 1 = 0`
or `F` is constantly `-1`; the constant has `H ≡ 0`, whose curvature quotient is
negative throughout a punctured neighbourhood and so cannot tend to `1`. -/
theorem logCurvature_forces_normalized (F : ℝ → ℝ)
    (hComp : SatisfiesCompositionLaw F) (hκ : HasLogCurvature (H F) 1) :
    IsNormalized F := by
  by_contra hne
  have hconst : ∀ x : ℝ, 0 < x → F x = -1 := by
    intro x hx
    have h := hComp x 1 hx one_pos
    rw [mul_one, div_one] at h
    have hquad : F 1 * (F x + 1) = 0 := by nlinarith
    rcases mul_eq_zero.mp hquad with h1 | h2
    · exact absurd h1 hne
    · linarith
  have hH : ∀ t : ℝ, H F t = 0 := by
    intro t
    have hx := hconst (Real.exp t) (Real.exp_pos t)
    simp [H, G, hx]
  have hgt : ∀ᶠ t in nhdsWithin (0 : ℝ) ({(0 : ℝ)}ᶜ),
      (1 / 2 : ℝ) < 2 * (H F t - 1) / t ^ 2 :=
    hκ.eventually (eventually_gt_nhds (by norm_num))
  have hne0 : ∀ᶠ t in nhdsWithin (0 : ℝ) ({(0 : ℝ)}ᶜ), t ≠ 0 := by
    filter_upwards [self_mem_nhdsWithin] with t ht using ht
  obtain ⟨t, hgt', ht0⟩ := (hgt.and hne0).exists
  have ht2 : 0 < t ^ 2 := by positivity
  have hneg : 2 * (H F t - 1) / t ^ 2 < 0 := by
    rw [hH t]
    exact div_neg_of_neg_of_pos (by norm_num) ht2
  linarith