`Jcost_is_reciprocal`

proved

show as: view math explainer →

module: IndisputableMonolith.CostUniqueness
domain: CostUniqueness
line: 145 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.CostUniqueness on GitHub at line 145.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 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))

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.