HasMultilevelComposition
A ZeroParameterComparisonLedger carries multilevel composition when it supplies a strictly positive real function on natural numbers with the first three values positive. Researchers deriving hierarchy emergence and the phi fixed point from the zero-parameter ledger cite this interface. The declaration is a direct class definition with no proof body or lemmas.
claimLet $L$ be a zero-parameter comparison ledger. Then $L$ has multilevel composition if there exists a function $levels : ℕ → ℝ$ such that $levels(k) > 0$ for all $k ∈ ℕ$, and in particular $levels(0) > 0$, $levels(1) > 0$, and $levels(2) > 0$.
background
The module defines the ZeroParameterComparisonLedger as the single primitive interface for the unconditional inevitability theorem. It consists of a nonempty countable carrier, an admissible cost obeying the J-cost symmetry identity, a conserved charge, and the requirement that no real embedding is injective, together with closure under composition. The doc-comment states that multilevel composition means events compose at more than one scale and induce a discrete hierarchy of level sizes. Upstream, IntegrationGap.A fixes the active edge count per tick at 1, while MagnitudeOfMismatch.forces guarantees single-valued comparisons on any carrier and cost.
proof idea
This declaration is a pure class definition with zero proof lines. It directly encodes the doc-comment content without applying any lemmas or tactics.
why it matters in Recognition Science
HasLocalComposition extends this class by adding adjacent-level locality and positive integer coefficients, which HierarchyDynamics then shows are forced to (1,1) and hence phi. The interface therefore sits between the basic ledger axioms and the forcing chain steps that produce the eight-tick octave and D=3. It supplies the discrete scale structure required for the mass formula on the phi-ladder.
scope and limits
- Does not assert existence of any ledger satisfying the class.
- Does not relate the levels function to the cost or charge data.
- Does not constrain the growth rate or functional form of levels.
- Does not derive the coefficients (1,1) or the value phi.
formal statement (Lean)
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 φ. -/