IndisputableMonolith.Foundation.DimensionalConstraints.CostLayer

   1import Mathlib
   2import IndisputableMonolith.Cost
   3import IndisputableMonolith.Cost.AczelClassification
   4import IndisputableMonolith.Foundation.LawOfExistence
   5
   6/-!
   7# Dimensional Constraints: Cost Layer
   8
   9This file packages the public cost-theoretic core used in the dimensional
  10constraints rebuttal.
  11
  12It exposes the statements needed in the paper in a compact, paper-specific
  13namespace without importing confidential parts of the full development.
  14-/
  15
  16namespace IndisputableMonolith
  17namespace Foundation
  18namespace DimensionalConstraints
  19namespace CostLayer
  20
  21open Real
  22
  23/-- Public cost layer used in the dimensional-constraints rebuttal. -/
  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. -/
  52theorem public_cost_layer : PublicCostLayer := by
  53  refine
  54    { unique_on_pos := ?_
  55      log_closed_form := Cost.Jlog_as_cosh
  56      normalized := Cost.Jcost_unit0
  57      reciprocal := ?_
  58      nonnegative := ?_
  59      zero_iff_one := ?_
  60      null_barrier := Foundation.LawOfExistence.nothing_cannot_exist }
  61  · intro F hF hKernel x hx
  62    exact Cost.FunctionalEquation.primitive_to_uniqueness_of_kernel F hF hKernel x hx
  63  · intro x hx
  64    exact Cost.Jcost_symm hx
  65  · intro x hx
  66    exact Cost.Jcost_nonneg hx
  67  · intro x hx
  68    exact Cost.Jcost_eq_zero_iff x hx
  69
  70end CostLayer
  71end DimensionalConstraints
  72end Foundation
  73end IndisputableMonolith
  74