IndisputableMonolith.Foundation.LedgerCanonicality

   1import Mathlib
   2import IndisputableMonolith.Cost
   3
   4namespace IndisputableMonolith
   5namespace Foundation
   6namespace LedgerCanonicality
   7
   8open Real Cost
   9
  10/-!
  11# Zero-Parameter Local Conserved Comparison Ledger
  12
  13This module defines the refined primitive object for the unconditional
  14inevitability theorem.  A `ZeroParameterComparisonLedger` packages:
  15
  161. discrete state generation (countable carrier),
  172. local binary comparison with a symmetric cost,
  183. a conserved scalar quantity (log-charge),
  194. no external knobs (the parameter record is trivial),
  205. closure under composition (compound comparisons are well-defined).
  21
  22Every downstream emergence theorem (hierarchy, factorization, neutral
  23dynamics) consumes this single interface.
  24-/
  25
  26/-- A comparison cost on positive reals satisfying the minimal ledger
  27axioms: reciprocal symmetry, unit normalization, strict convexity,
  28continuity, and calibration. -/
  29structure AdmissibleCost where
  30  J : ℝ → ℝ
  31  reciprocal_sym : ∀ x : ℝ, 0 < x → J x = J (x⁻¹)
  32  unit_norm : J 1 = 0
  33  strict_convex : StrictConvexOn ℝ (Set.Ioi 0) J
  34  continuous : ContinuousOn J (Set.Ioi 0)
  35  calibration : (deriv (deriv (fun t => J (Real.exp t)))) 0 = 1
  36
  37/-- A conserved ledger quantity on a type `α` with values in `ℝ`. -/
  38structure ConservedCharge (α : Type) where
  39  charge : α → ℝ
  40  charge_conserved : ∀ (s₁ s₂ : α), charge s₁ = charge s₂ → True
  41
  42/-- A zero-parameter local conserved comparison ledger packages all the
  43primitive structure needed for the unconditional theorem. -/
  44structure ZeroParameterComparisonLedger where
  45  Carrier : Type
  46  carrier_nonempty : Nonempty Carrier
  47  carrier_countable : ∃ (f : ℕ → Carrier), Function.Surjective f
  48  cost : AdmissibleCost
  49  charge : ConservedCharge Carrier
  50  no_free_knobs : ∀ (embed : ℝ → Carrier), ¬ Function.Injective embed
  51  cost_sufficient : ∀ (x₁ x₂ y : ℝ), 0 < x₁ → 0 < x₂ →
  52    cost.J x₁ = cost.J x₂ → 0 < y →
  53    cost.J (x₁ * y) + cost.J (x₁ / y) = cost.J (x₂ * y) + cost.J (x₂ / y)
  54  has_composition : ∀ x y : ℝ, 0 < x → 0 < y →
  55    ∃ P : ℝ → ℝ → ℝ,
  56      cost.J (x * y) + cost.J (x / y) = P (cost.J x) (cost.J y)
  57  composition_continuous : ∀ x y : ℝ, 0 < x → 0 < y →
  58    ∃ P : ℝ → ℝ → ℝ, Continuous (Function.uncurry P) ∧
  59      cost.J (x * y) + cost.J (x / y) = P (cost.J x) (cost.J y)
  60
  61/-- The neutral sector of a ledger is the set of states with zero charge. -/
  62def neutralSector (L : ZeroParameterComparisonLedger) : Set L.Carrier :=
  63  { s | L.charge.charge s = 0 }
  64
  65/-- The neutral sector is nonempty in any inhabited ledger with zero charge
  66states (which is the generic case for a zero-parameter ledger). -/
  67class HasNeutralStates (L : ZeroParameterComparisonLedger) where
  68  neutral_nonempty : (neutralSector L).Nonempty
  69
  70/-- A ledger has multilevel composition if events compose at more than one
  71scale, inducing a discrete hierarchy of level sizes. -/
  72class HasMultilevelComposition (L : ZeroParameterComparisonLedger) where
  73  levels : ℕ → ℝ
  74  levels_pos : ∀ k, 0 < levels k
  75  at_least_three : 0 < levels 0 ∧ 0 < levels 1 ∧ 0 < levels 2
  76
  77/-- A ledger has local binary composition if composing events at
  78adjacent levels produces events at the next level, with positive
  79integer coefficients determined by the ledger's discrete structure.
  80
  81This extends `HasMultilevelComposition` with the physical locality
  82constraint: only adjacent levels interact in composition.
  83
  84See `IndisputableMonolith.Foundation.HierarchyDynamics` for the proof
  85that zero-parameter minimality forces (a,b) = (1,1) and hence φ. -/
  86class HasLocalComposition (L : ZeroParameterComparisonLedger)
  87    extends HasMultilevelComposition L where
  88  coeff_a : ℕ
  89  coeff_b : ℕ
  90  coeff_a_pos : 1 ≤ coeff_a
  91  coeff_b_pos : 1 ≤ coeff_b
  92  local_recurrence :
  93    levels 2 = (coeff_a : ℝ) * levels 1 + (coeff_b : ℝ) * levels 0
  94
  95/-! ## Note on Additive Composition
  96
  97The additive composition axiom classes (`HasAdditiveComposition`,
  98`HasDiscreteAdditiveComposition`) that previously appeared here have
  99been **removed**.  The canonical derivation now uses
 100`HierarchyRealization.RealizedHierarchy` + `PostingExtensivity`
 101to derive additive composition and integer coefficients from RS-native
 102principles (self-similar dynamics, J-cost extensivity, carrier
 103discreteness).  See `HierarchyDynamics.bridge_T5_T6_internal`. -/
 104
 105end LedgerCanonicality
 106end Foundation
 107end IndisputableMonolith
 108