pith. machine review for the scientific record. sign in
class definition def or abbrev

HasLocalComposition

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  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

depends on (18)

Lean names referenced from this declaration's body.