  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

papers checked against this theorem

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