`Jcost_is_normalized`

proved

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.CostUniqueness on GitHub at line 149.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 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

papers checked against this theorem

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