`unique_cost_on_pos`

proved

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.CostUniqueness on GitHub at line 194.

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

 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

papers checked against this theorem

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