pith. machine review for the scientific record. sign in
theorem proved term proof

uniqueness_specification

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 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

proof body

Term-mode proof.

 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
 368
 369end CostAxioms
 370end Foundation
 371end IndisputableMonolith

depends on (26)

Lean names referenced from this declaration's body.