IndisputableMonolith.CostUniqueness

   1import Mathlib
   2import IndisputableMonolith.Cost
   3import IndisputableMonolith.Cost.Convexity
   4import IndisputableMonolith.CPM.LawOfExistence
   5import IndisputableMonolith.Cost.FunctionalEquation
   6import IndisputableMonolith.Foundation.ClosedObservableFramework
   7
   8/-!
   9# Cost Uniqueness: Main Theorem T5
  10
  11This module provides the complete uniqueness theorem for J,
  12consolidating results from Convexity, Calibration, and FunctionalEquation.
  13
  14Main result: Any cost functional F satisfying symmetry, unit normalization,
  15strict convexity, and calibration must equal Jcost on ℝ₊.
  16-/
  17
  18namespace IndisputableMonolith
  19namespace CostUniqueness
  20
  21open Real Cost Set
  22
  23/-! We avoid global axioms. Functional-equation ingredients are supplied
  24    as explicit hypotheses in the theorems below. -/
  25
  26/-- Full T5 Uniqueness Theorem (with explicit functional-identity hypothesis) -/
  27theorem T5_uniqueness_complete (F : ℝ → ℝ)
  28  (hSymm : ∀ {x}, 0 < x → F x = F x⁻¹)
  29  (hUnit : F 1 = 0)
  30  (hConvex : StrictConvexOn ℝ (Set.Ioi 0) F)
  31  (hCalib : deriv (deriv (F ∘ exp)) 0 = 1)
  32  (hCont : ContinuousOn F (Ioi 0))
  33  (hCoshAdd : FunctionalEquation.CoshAddIdentity F)
  34  (h_smooth_hyp : FunctionalEquation.dAlembert_continuous_implies_smooth_hypothesis (FunctionalEquation.H F))
  35  (h_ode_hyp : FunctionalEquation.dAlembert_to_ODE_hypothesis (FunctionalEquation.H F))
  36  (h_cont_hyp : FunctionalEquation.ode_regularity_continuous_hypothesis (FunctionalEquation.H F))
  37  (h_diff_hyp : FunctionalEquation.ode_regularity_differentiable_hypothesis (FunctionalEquation.H F))
  38  (h_bootstrap_hyp : FunctionalEquation.ode_linear_regularity_bootstrap_hypothesis (FunctionalEquation.H F)) :
  39  ∀ {x : ℝ}, 0 < x → F x = Jcost x := by
  40  intro x hx
  41  -- Reduce to log coordinates and invoke d'Alembert uniqueness
  42  let Gf : ℝ → ℝ := FunctionalEquation.G F
  43  have h_even : Function.Even Gf := FunctionalEquation.G_even_of_reciprocal_symmetry F hSymm
  44  have h_G0 : Gf 0 = 0 := FunctionalEquation.G_zero_of_unit F hUnit
  45
  46  -- Gf is continuous on ℝ (F is continuous on (0,∞), exp is continuous, composition is continuous)
  47  have h_G_cont : Continuous Gf := by
  48    have h := ContinuousOn.comp_continuous hCont continuous_exp
  49    have h' : Continuous (fun t => F (Real.exp t)) :=
  50      h (by intro t; exact mem_Ioi.mpr (Real.exp_pos t))
  51    simpa [FunctionalEquation.G] using h'
  52
  53  -- Convert CoshAddIdentity F to DirectCoshAdd Gf
  54  have h_direct : FunctionalEquation.DirectCoshAdd Gf :=
  55    FunctionalEquation.CoshAddIdentity_implies_DirectCoshAdd F hCoshAdd
  56
  57  -- Apply d'Alembert uniqueness (via the shifted H := G + 1) to get Gf(t) = cosh(t) - 1.
  58  let Hf : ℝ → ℝ := FunctionalEquation.H F
  59  have h_H0 : Hf 0 = 1 := by
  60    simp [Hf, FunctionalEquation.H, FunctionalEquation.G, hUnit]
  61  have h_H_cont : Continuous Hf := by
  62    simpa [Hf, FunctionalEquation.H] using h_G_cont.add continuous_const
  63  have h_dAlembert : ∀ t u, Hf (t + u) + Hf (t - u) = 2 * Hf t * Hf u := by
  64    intro t u
  65    have hG := h_direct t u
  66    -- Convert the direct cosh-add identity for G into the d'Alembert identity for H := G + 1.
  67    -- This is pure ring algebra.
  68    -- (G(t+u)+G(t-u)) = 2(Gt·Gu) + 2(Gt+Gu)
  69    -- ⇔ (H(t+u)+H(t-u)) = 2HtHu  for H := G + 1.
  70    have h_goal :
  71        (Gf (t + u) + 1) + (Gf (t - u) + 1) = 2 * (Gf t + 1) * (Gf u + 1) := by
  72      calc
  73        (Gf (t + u) + 1) + (Gf (t - u) + 1)
  74            = (Gf (t + u) + Gf (t - u)) + 2 := by ring
  75        _ = (2 * (Gf t * Gf u) + 2 * (Gf t + Gf u)) + 2 := by simpa [hG]
  76        _ = 2 * (Gf t + 1) * (Gf u + 1) := by ring
  77    -- Discharge the original goal by unfolding Hf := H F := G F + 1 and rewriting in terms of Gf.
  78    simpa [Hf, FunctionalEquation.H, Gf] using h_goal
  79  have h_H_d2 : deriv (deriv Hf) 0 = 1 := by
  80    -- Hf = Gf + 1, so the 2nd derivative at 0 is the same as for Gf.
  81    have hG_d2 : deriv (deriv Gf) 0 = 1 := by
  82      simpa [Gf, FunctionalEquation.G] using hCalib
  83    -- `deriv (Hf)` equals `deriv (Gf)` pointwise, so their second derivatives match too.
  84    have hderiv : deriv Hf = deriv Gf := by
  85      funext t
  86      -- Unfold Hf := (fun y => Gf y + 1), then apply `deriv_add_const`.
  87      change deriv (fun y => Gf y + 1) t = deriv Gf t
  88      simpa using (deriv_add_const (f := Gf) (x := t) (c := (1 : ℝ)))
  89    have hderiv2 : deriv (deriv Hf) = deriv (deriv Gf) := congrArg deriv hderiv
  90    have hderiv2_at0 : deriv (deriv Hf) 0 = deriv (deriv Gf) 0 := congrArg (fun g => g 0) hderiv2
  91    exact hderiv2_at0.trans hG_d2
  92  have h_H_cosh : ∀ t, Hf t = Real.cosh t :=
  93    FunctionalEquation.dAlembert_cosh_solution
  94      Hf h_H0 h_H_cont h_dAlembert h_H_d2 h_smooth_hyp h_ode_hyp h_cont_hyp h_diff_hyp h_bootstrap_hyp
  95  have h_G_cosh : ∀ t, Gf t = Real.cosh t - 1 := by
  96    intro t
  97    have hH := h_H_cosh t
  98    -- Unshift: H = G + 1.
  99    have hH' : Gf t + 1 = Real.cosh t := by
 100      simpa [Hf, FunctionalEquation.H, Gf] using hH
 101    linarith
 102
 103  -- Now convert back using the log-parametrization identity for Jcost
 104  have ht : Real.exp (Real.log x) = x := Real.exp_log hx
 105  have hJG : FunctionalEquation.G Cost.Jcost (Real.log x) = Real.cosh (Real.log x) - 1 :=
 106    FunctionalEquation.Jcost_G_eq_cosh_sub_one (Real.log x)
 107  calc F x
 108      = F (Real.exp (Real.log x)) := by rw [ht]
 109    _ = Gf (Real.log x) := rfl
 110    _ = Real.cosh (Real.log x) - 1 := h_G_cosh (Real.log x)
 111    _ = FunctionalEquation.G Cost.Jcost (Real.log x) := by simpa using hJG.symm
 112    _ = Jcost (Real.exp (Real.log x)) := by simp [FunctionalEquation.G]
 113    _ = Jcost x := by simpa [ht]
 114
 115/-- Hypotheses bundle for uniqueness on ℝ₊ (non-axiomatic). -/
 116structure UniqueCostAxioms (F : ℝ → ℝ) : Prop where
 117  symmetric : ∀ {x}, 0 < x → F x = F x⁻¹
 118  unit : F 1 = 0
 119  convex : StrictConvexOn ℝ (Set.Ioi 0) F
 120  calibrated : deriv (deriv (F ∘ exp)) 0 = 1
 121  continuousOn_pos : ContinuousOn F (Ioi 0)
 122  coshAdd : FunctionalEquation.CoshAddIdentity F
 123  dAlembert_smooth : FunctionalEquation.dAlembert_continuous_implies_smooth_hypothesis (FunctionalEquation.H F)
 124  dAlembert_toODE : FunctionalEquation.dAlembert_to_ODE_hypothesis (FunctionalEquation.H F)
 125  ode_cont : FunctionalEquation.ode_regularity_continuous_hypothesis (FunctionalEquation.H F)
 126  ode_diff : FunctionalEquation.ode_regularity_differentiable_hypothesis (FunctionalEquation.H F)
 127  ode_bootstrap : FunctionalEquation.ode_linear_regularity_bootstrap_hypothesis (FunctionalEquation.H F)
 128
 129/-- Jcost is continuous on ℝ₊ -/
 130lemma Jcost_continuous_pos : ContinuousOn Jcost (Ioi 0) := by
 131  classical
 132  have h1 : ContinuousOn (fun x : ℝ => x) (Ioi 0) := continuousOn_id
 133  have h2 : ContinuousOn (fun x : ℝ => x⁻¹) (Ioi 0) := by
 134    refine ContinuousOn.inv₀ (f:=fun x : ℝ => x) (s:=Ioi 0) h1 ?hneq
 135    intro x hx; exact ne_of_gt hx
 136  have h3 : ContinuousOn (fun x : ℝ => x + x⁻¹) (Ioi 0) := h1.add h2
 137  have h4 : ContinuousOn (fun x : ℝ => (1 / 2 : ℝ) * (x + x⁻¹)) (Ioi 0) :=
 138    (continuousOn_const).mul h3
 139  have h5 : ContinuousOn (fun x : ℝ => (1 / 2 : ℝ) * (x + x⁻¹) - 1) (Ioi 0) :=
 140    h4.sub continuousOn_const
 141  simpa [Jcost, one_div, div_eq_mul_inv, mul_comm, mul_left_comm, mul_assoc, sub_eq_add_neg]
 142    using h5
 143
 144/-- `Jcost` satisfies reciprocal symmetry in the theorem-surface format. -/
 145theorem Jcost_is_reciprocal : FunctionalEquation.IsReciprocalCost Jcost :=
 146  fun x hx => Jcost_symm hx
 147
 148/-- `Jcost` is normalized at `1`. -/
 149theorem Jcost_is_normalized : FunctionalEquation.IsNormalized Jcost :=
 150  Jcost_unit0
 151
 152/-- `Jcost` satisfies the Recognition Composition Law. -/
 153theorem Jcost_satisfies_composition_law : FunctionalEquation.SatisfiesCompositionLaw Jcost :=
 154  (FunctionalEquation.composition_law_equiv_coshAdd Jcost).2 FunctionalEquation.Jcost_cosh_add_identity
 155
 156/-- `Jcost` satisfies the standard calibration condition in log coordinates. -/
 157theorem Jcost_is_calibrated : FunctionalEquation.IsCalibrated Jcost := by
 158  change deriv (deriv (fun t : ℝ => Jcost (Real.exp t))) 0 = 1
 159  exact IndisputableMonolith.CPM.LawOfExistence.RS.Jcost_log_second_deriv_normalized
 160
 161/-- Axiom-free uniqueness theorem on the paper's RCL theorem surface.
 162
 163This is the main unconditional IM-facing T5 statement: the caller supplies
 164the reciprocal, normalization, composition, calibration, continuity, and
 165explicit d'Alembert regularity hypotheses, and the conclusion is `F = Jcost`
 166on `(0, ∞)`. -/
 167theorem unique_cost_on_pos_from_rcl (F : ℝ → ℝ)
 168    (hRecip : FunctionalEquation.IsReciprocalCost F)
 169    (hNorm : FunctionalEquation.IsNormalized F)
 170    (hComp : FunctionalEquation.SatisfiesCompositionLaw F)
 171    (hCalib : FunctionalEquation.IsCalibrated F)
 172    (hCont : ContinuousOn F (Ioi 0))
 173    (h_smooth : FunctionalEquation.dAlembert_continuous_implies_smooth_hypothesis (FunctionalEquation.H F))
 174    (h_ode : FunctionalEquation.dAlembert_to_ODE_hypothesis (FunctionalEquation.H F))
 175    (h_cont : FunctionalEquation.ode_regularity_continuous_hypothesis (FunctionalEquation.H F))
 176    (h_diff : FunctionalEquation.ode_regularity_differentiable_hypothesis (FunctionalEquation.H F))
 177    (h_boot : FunctionalEquation.ode_linear_regularity_bootstrap_hypothesis (FunctionalEquation.H F)) :
 178    ∀ {x : ℝ}, 0 < x → F x = Jcost x := by
 179  intro x hx
 180  exact FunctionalEquation.washburn_uniqueness F
 181    hRecip hNorm hComp hCalib hCont h_smooth h_ode h_cont h_diff h_boot x hx
 182
 183/- Jcost satisfies the non-axiomatic hypothesis bundle (unused here)
 184 def Jcost_satisfies_axioms : UniqueCostAxioms Jcost where
 185  symmetric := fun hx => Jcost_symm hx
 186  unit := Jcost_unit0
 187  convex := Jcost_strictConvexOn_pos
 188  calibrated := by
 189    simpa using IndisputableMonolith.CPM.LawOfExistence.RS.Jcost_log_second_deriv_normalized
 190  continuousOn_pos := Jcost_continuous_pos
 191  coshAdd := FunctionalEquation.Jcost_cosh_add_identity -/
 192
 193/-- Main uniqueness statement on ℝ₊: any admissible cost equals Jcost on (0,∞). -/
 194theorem unique_cost_on_pos (F : ℝ → ℝ) (hF : UniqueCostAxioms F) :
 195  ∀ {x : ℝ}, 0 < x → F x = Jcost x :=
 196  T5_uniqueness_complete F hF.symmetric hF.unit hF.convex hF.calibrated hF.continuousOn_pos hF.coshAdd
 197    hF.dAlembert_smooth hF.dAlembert_toODE hF.ode_cont hF.ode_diff hF.ode_bootstrap
 198
 199/-! ## RegularityCert for Jcost -/
 200
 201/-- Jcost satisfies the RegularityCert requirements: continuous on (0,∞),
 202    strictly convex on (0,∞), and calibrated (second log-derivative = 1 at 0). -/
 203noncomputable def Jcost_regularity_cert :
 204    IndisputableMonolith.Foundation.ClosedFramework.RegularityCert Cost.Jcost where
 205  continuous := Jcost_continuous_pos
 206  strict_convex := Cost.Jcost_strictConvexOn_pos
 207  calibration := CPM.LawOfExistence.RS.Jcost_log_second_deriv_normalized
 208
 209end CostUniqueness
 210end IndisputableMonolith
 211