HasMultilevelComposition
plain-language theorem explainer
ZeroParameterComparisonLedger instances admit multilevel composition when equipped with a strictly positive real function on natural numbers that is positive on the first three values. Hierarchy emergence arguments cite this interface when extending to local composition axioms. The declaration is a bare class definition introducing the levels map and its three positivity axioms.
Claim. A ledger $L$ has multilevel composition if it is equipped with a function $l : ℕ → ℝ$ satisfying $l(k) > 0$ for every natural number $k$, together with the explicit positivity conditions $l(0) > 0$, $l(1) > 0$ and $l(2) > 0$.
background
The ZeroParameterComparisonLedger packages a countable carrier, an admissible cost whose J-cost obeys the Recognition Composition Law, a conserved charge, and the absence of free parameters. This class adds the requirement of a discrete hierarchy of positive level sizes so that events can compose across multiple scales. The module states that every downstream emergence theorem on hierarchy and factorization consumes this single interface. Upstream results include the active edge count per fundamental tick and the magnitude-of-mismatch forcing of symmetry.
proof idea
This declaration is a class definition. It directly introduces the levels field as a map from naturals to reals and asserts the three positivity properties without invoking lemmas or tactics.
why it matters
This interface is extended by HasLocalComposition, which adds adjacent-level coefficients and feeds the argument that zero-parameter minimality forces coefficients (1,1) and hence phi. It supports the chain from J-uniqueness through the self-similar fixed point to the eight-tick octave and three spatial dimensions. The module doc notes that every emergence theorem consumes this single interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.