24structure PublicCostLayer : Prop where 25 /-- Any admissible cost functional agrees with `Jcost` on positive reals via 26 the canonical primitive-to-uniqueness T5 route. -/ 27 unique_on_pos : 28 ∀ (F : ℝ → ℝ), 29 Cost.FunctionalEquation.PrimitiveCostHypotheses F → 30 Cost.FunctionalEquation.AczelRegularityKernel (Cost.FunctionalEquation.H F) → 31 ∀ {x : ℝ}, 0 < x → F x = Cost.Jcost x 32 /-- In logarithmic coordinates, the cost is `cosh t - 1`. -/ 33 log_closed_form : 34 ∀ t : ℝ, Cost.Jlog t = Real.cosh t - 1 35 /-- The identity ratio has zero cost. -/ 36 normalized : Cost.Jcost 1 = 0 37 /-- Reciprocal ratios have equal cost. -/ 38 reciprocal : 39 ∀ {x : ℝ}, 0 < x → Cost.Jcost x = Cost.Jcost x⁻¹ 40 /-- The cost is nonnegative on positive ratios. -/ 41 nonnegative : 42 ∀ {x : ℝ}, 0 < x → 0 ≤ Cost.Jcost x 43 /-- The unique positive zero of the cost is `x = 1`. -/ 44 zero_iff_one : 45 ∀ {x : ℝ}, 0 < x → (Cost.Jcost x = 0 ↔ x = 1) 46 /-- Near zero, the defect exceeds every prescribed bound. -/ 47 null_barrier : 48 ∀ C : ℝ, ∃ ε > 0, ∀ x : ℝ, 0 < x → x < ε → 49 C < Foundation.LawOfExistence.defect x 50 51/-- The public cost layer is available in the current public framework. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.