NontrivialMultilevelComposition
plain-language theorem explainer
A structure encoding a sequence of positive real numbers with the first three terms required to be positive. Researchers deriving hierarchical scaling from zero free parameters cite this structure when stating the uniform ratio theorem. It functions as a minimal data carrier that feeds directly into constructions of uniform scale ladders and derivations of golden ratio scaling.
Claim. A structure consisting of a function $levels : ℕ → ℝ$ such that $levels(k) > 0$ for all natural numbers $k$, together with the explicit requirement that $levels(0) > 0$, $levels(1) > 0$, and $levels(2) > 0$.
background
The module treats Gap 2 of the axiom-closure plan, which derives hierarchical structure from a nontrivial zero-parameter ledger. This structure supplies the bare data package for a multilevel composition that later theorems use to force uniform adjacent ratios. Upstream results include the RealizedHierarchy structure, whose levels are generated by iterating a dynamics operator on a base state, and the theorem that all adjacent ratios in any such realized hierarchy are identical.
proof idea
This declaration is a structure definition and carries no proof body.
why it matters
It supplies the input type for the theorem that no free scale parameters forces uniform adjacent ratios. The same structure is used to construct the uniform scale ladder and to prove that the forced scaling factor equals the golden ratio. This advances the forcing chain from the Recognition Composition Law toward the self-similar fixed point and the emergence of three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.