pith. machine review for the scientific record. sign in
class

HasLocalComposition

definition
show as:
view math explainer →
module
IndisputableMonolith.Foundation.LedgerCanonicality
domain
Foundation
line
86 · github
papers citing
1 paper (below)

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.LedgerCanonicality on GitHub at line 86.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  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

papers checked against this theorem (showing 1 of 1)