Cost Functional Equation Law Of Logic Forces Jcost With Regularization

/-- **Theorem 1.1 (Main Result, Reformulated)**:

Let F : ℝ₊ → ℝ satisfy:
1. Reciprocity: F(x) = F(1/x)
2. Normalization: F(1) = 0
3. Composition Law: F(xy) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y)
4. Calibration: lim_{t→0} 2F(e^t)/t² = 1
5. Continuity and regularity hypotheses

Then F = J on ℝ₊, where J(x) = (x + 1/x)/2 - 1.

This theorem corresponds to Theorem 1.1 in:
  J. Washburn & M. Zlatanović, "Uniqueness of the Canonical Reciprocal Cost" -/
theorem law_of_logic_forces_jcost_with_regularization (F : ℝ → ℝ)
    (hRecip : IsReciprocalCost F)
    (hNorm : IsNormalized F)
    (hComp : SatisfiesCompositionLaw F)
    (hCalib : IsCalibrated F)
    (hCont : ContinuousOn F (Set.Ioi 0))
    -- Regularity hypotheses (from Aczél theory)
    (h_smooth : dAlembert_continuous_implies_smooth_hypothesis (H F))
    (h_ode : dAlembert_to_ODE_hypothesis (H F))
    (h_cont : ode_regularity_continuous_hypothesis (H F))
    (h_diff : ode_regularity_differentiable_hypothesis (H F))
    (h_boot : ode_linear_regularity_bootstrap_hypothesis (H F)) :
    ∀ x : ℝ, 0 < x → F x = Cost.Jcost x := by
  -- The proof follows the structure of T5_uniqueness_complete:
  -- 1. Convert composition law to CoshAddIdentity on G
  -- 2. Shift to H = G + 1 to get standard d'Alembert equation
  -- 3. Apply Aczél's theorem: continuous d'Alembert solutions are cosh
  -- 4. Calibration H''(0) = 1 selects cosh (not cos or constant)
  -- 5. Unshift: G = cosh - 1, hence F = J
  intro x hx
  -- Convert hypotheses to the required format
  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

  -- Step 1: Set up G and H
  let Gf : ℝ → ℝ := G F
  let Hf : ℝ → ℝ := H F

  -- Step 2: Derive key properties of G and H
  have h_G_even : Function.Even Gf := G_even_of_reciprocal_symmetry F hSymm
  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]
    -- Goal is F 1 + 1 = 1, and hNorm says F 1 = 0
    rw [hNorm]
    ring

  -- Step 3: G is continuous (F continuous on (0,∞), exp continuous)
  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

  -- Step 4: Convert CoshAddIdentity to d'Alembert equation for H
  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

  -- Step 5: Second derivative condition
  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
      simpa using (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

  -- Step 6: Apply d'Alembert uniqueness theorem
  have h_H_cosh : ∀ t, Hf t = Real.cosh t :=
    dAlembert_cosh_solution Hf h_H0 h_H_cont h_dAlembert h_H_d2
      h_smooth h_ode h_cont h_diff h_boot

  -- Step 7: Unshift to get G = cosh - 1
  have h_G_cosh : ∀ t, Gf t = Real.cosh t - 1 := by
    intro t
    have hH := h_H_cosh t
    have hH' : Gf t + 1 = Real.cosh t := by simpa [Hf, H, Gf] using hH
    linarith

  -- Step 8: Convert back via log parametrization
  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 simpa using hJG.symm
    _ = Cost.Jcost (Real.exp (Real.log x)) := by simp [G]
    _ = Cost.Jcost x := by simpa [ht]

/-- **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

/-- **Theorem (d'Alembert → cosh, Aczél form)**: Using only the Aczél axiom, a continuous
    solution to d'Alembert with H(0) = 1 and H''(0) = 1 must equal cosh.

    This is the clean version of `dAlembert_cosh_solution`, requiring no regularity params. -/
theorem dAlembert_cosh_solution_aczel
    [AczelSmoothnessPackage]
    (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_d2_zero : deriv (deriv H) 0 = 1) :
    ∀ t, H t = Real.cosh t := by
  have h_smooth : ContDiff ℝ ⊤ H := aczel_dAlembert_smooth H h_one h_cont h_dAlembert
  have hDiff : Differentiable ℝ H :=
    (h_smooth.of_le le_top : ContDiff ℝ 1 H).differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
  have h_even : Function.Even H := dAlembert_even H h_one h_dAlembert
  have h_H'0 : deriv H 0 = 0 := even_deriv_at_zero H h_even hDiff.differentiableAt
  have h_ode : ∀ t, deriv (deriv H) t = H t :=
    dAlembert_to_ODE_theorem H h_smooth h_dAlembert h_d2_zero
  have h_C2 : ContDiff ℝ 2 H := h_smooth.of_le le_top
  exact ode_cosh_uniqueness_contdiff H h_C2 h_ode h_one h_H'0

/-- **Theorem (d'Alembert → cosh, Aczél form)**: Using only the Aczél axiom, a continuous
    solution to d'Alembert with H(0) = 1 and H''(0) = 1 must equal cosh.

    This is the clean version of `dAlembert_cosh_solution`, requiring no regularity params. -/
theorem dAlembert_cosh_solution_aczel
    [AczelSmoothnessPackage]
    (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_d2_zero : deriv (deriv H) 0 = 1) :
    ∀ t, H t = Real.cosh t := by
  have h_smooth : ContDiff ℝ ⊤ H := aczel_dAlembert_smooth H h_one h_cont h_dAlembert
  have hDiff : Differentiable ℝ H :=
    (h_smooth.of_le le_top : ContDiff ℝ 1 H).differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
  have h_even : Function.Even H := dAlembert_even H h_one h_dAlembert
  have h_H'0 : deriv H 0 = 0 := even_deriv_at_zero H h_even hDiff.differentiableAt
  have h_ode : ∀ t, deriv (deriv H) t = H t :=
    dAlembert_to_ODE_theorem H h_smooth h_dAlembert h_d2_zero
  have h_C2 : ContDiff ℝ 2 H := h_smooth.of_le le_top
  exact ode_cosh_uniqueness_contdiff H h_C2 h_ode h_one h_H'0