`CostAlgebraData`

definition

show as: view math explainer →

module: IndisputableMonolith.Algebra.CostAlgebra
domain: Algebra
line: 589 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Algebra.CostAlgebra on GitHub at line 589.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 586    - Involution: x ↦ 1/x preserving J
 587
 588    From this single structure, all of RS is derived. -/
 589structure CostAlgebraData where
 590  /-- The cost function -/
 591  cost : ℝ → ℝ
 592  /-- Satisfies the Recognition Composition Law -/
 593  rcl : SatisfiesRCL cost
 594  /-- Normalization: cost at identity is zero -/
 595  normalized : cost 1 = 0
 596  /-- Reciprocal symmetry -/
 597  symmetric : ∀ x : ℝ, 0 < x → cost x = cost x⁻¹
 598  /-- Non-negativity on ℝ₊ -/
 599  nonneg : ∀ x : ℝ, 0 < x → 0 ≤ cost x
 600
 601/-- **THEOREM: J provides the canonical CostAlgebraData.** -/
 602noncomputable def canonicalCostAlgebra : CostAlgebraData where
 603  cost := J
 604  rcl := RCL_holds
 605  normalized := J_at_one
 606  symmetric := J_reciprocal
 607  nonneg := J_nonneg
 608
 609/-- **THEOREM: The canonical cost algebra is unique.**
 610    Any CostAlgebraData with the same axioms + calibration J''(1)=1
 611    must have cost = J. (This is T5 in the forcing chain.) -/
 612theorem cost_algebra_unique (C : CostAlgebraData)
 613    (hCalib : deriv (deriv (fun t => C.cost (Real.exp t))) 0 = 1)
 614    (hCont : ContinuousOn C.cost (Set.Ioi 0))
 615    (hSmooth : dAlembert_continuous_implies_smooth_hypothesis (IndisputableMonolith.Cost.FunctionalEquation.H C.cost))
 616    (hODE : dAlembert_to_ODE_hypothesis (IndisputableMonolith.Cost.FunctionalEquation.H C.cost))
 617    (hContReg : ode_regularity_continuous_hypothesis (IndisputableMonolith.Cost.FunctionalEquation.H C.cost))
 618    (hDiffReg : ode_regularity_differentiable_hypothesis (IndisputableMonolith.Cost.FunctionalEquation.H C.cost))
 619    (hBoot : ode_linear_regularity_bootstrap_hypothesis (IndisputableMonolith.Cost.FunctionalEquation.H C.cost)) :

papers checked against this theorem

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