`uniqueness_specification`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.CostAxioms
domain: Foundation
line: 337 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.CostAxioms on GitHub at line 337.

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

 334    - Linear ODE regularity bootstrap
 335
 336    See `IndisputableMonolith.T5_uniqueness_complete` for the rigorous proof. -/
 337theorem uniqueness_specification (F : ℝ → ℝ) [CostFunctionalAxioms F]
 338    (hCont : ContinuousOn F (Set.Ioi 0))
 339    (hConvex : StrictConvexOn ℝ (Set.Ioi 0) F)
 340    -- Regularity hypotheses from Aczél's theorem on d'Alembert equations
 341    (h_smooth : Cost.FunctionalEquation.dAlembert_continuous_implies_smooth_hypothesis
 342        (Cost.FunctionalEquation.H F))
 343    (h_ode : Cost.FunctionalEquation.dAlembert_to_ODE_hypothesis
 344        (Cost.FunctionalEquation.H F))
 345    (h_cont : Cost.FunctionalEquation.ode_regularity_continuous_hypothesis
 346        (Cost.FunctionalEquation.H F))
 347    (h_diff : Cost.FunctionalEquation.ode_regularity_differentiable_hypothesis
 348        (Cost.FunctionalEquation.H F))
 349    (h_boot : Cost.FunctionalEquation.ode_linear_regularity_bootstrap_hypothesis
 350        (Cost.FunctionalEquation.H F)) :
 351    ∀ x, 0 < x → F x = J x := by
 352  intro x hx
 353  -- Bridge from CostFunctionalAxioms to T5_uniqueness_complete hypotheses
 354  -- 1. Symmetry: F(x) = F(1/x)
 355  have hSymm : ∀ {x : ℝ}, 0 < x → F x = F x⁻¹ :=
 356    Composition_Normalization_implies_symmetry F
 357  -- 2. Unit normalization: F(1) = 0
 358  have hUnit : F 1 = 0 := Normalization.unit_zero
 359  -- 3. Calibration: deriv (deriv (F ∘ exp)) 0 = 1
 360  have hCalib : deriv (deriv (F ∘ exp)) 0 = 1 := Calibration.second_deriv_at_zero
 361  -- 4. CoshAddIdentity: from Composition axiom
 362  have hCoshAdd : Cost.FunctionalEquation.CoshAddIdentity F :=
 363    Composition_implies_CoshAddIdentity F
 364  -- Apply T5_uniqueness_complete with all hypotheses
 365  unfold J
 366  exact CostUniqueness.T5_uniqueness_complete F hSymm hUnit hConvex hCalib hCont hCoshAdd
 367    h_smooth h_ode h_cont h_diff h_boot hx

papers checked against this theorem

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