canonicalBaseRatio
plain-language theorem explainer
For any nontrivial multilevel composition (a positive real sequence with at least three levels), the canonical base ratio is the first adjacent step levels(1)/levels(0). Hierarchy and φ-forcing arguments cite it as the single scale parameter of the ladder. The body is a one-line quotient of the level function.
Claim. Given a nontrivial multilevel composition $M$ (a map $\mathrm{levels}:\mathbb{N}\to\mathbb{R}$ with every value positive and at least the first three levels strictly positive), the canonical base ratio is $\mathrm{levels}(1)/\mathrm{levels}(0)\in\mathbb{R}$.
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. In that chain, T6 forces φ as the self-similar fixed point of a discrete ledger hierarchy.
A nontrivial multilevel composition packages a positive real level sequence with at least three positive rungs. Adjacent ratios of that sequence are the natural scale parameters of the hierarchy. The raw “no free scale” hypothesis asserts that every adjacent ratio equals every other; the canonical base ratio isolates the first step as the single candidate scale.
Upstream, HierarchyForcing supplies the structure (positive levels, three-level nontriviality). Downstream uniform-scale and seed-closure laws compare this ratio to φ from PhiForcing.
proof idea
Definitional one-liner: evaluate the level map at 1 and at 0 and divide. Noncomputable only because the ambient real division is noncomputable in Lean’s default setup; no lemmas are applied.
why it matters
This is the named scale parameter that the canonical uniform-scale law and growth orientation speak about. Downstream, canonical_uniform_of_no_free_scale rebuilds uniform adjacent ratios from the raw all-pairs hypothesis using this ratio; canonical_growth_iff_ratio_gt_one equates growth orientation with the ratio exceeding 1.
The φ-forcing theorems canonicalBaseRatio_eq_phi_of_uniform_seed and canonicalBaseRatio_eq_phi_of_uniformClosed_seed conclude that under uniform scale, growth, and seed closure the ratio equals φ. Admissible-orbit certificates then specialize that conclusion: an admissible orbit’s multilevel composition has canonical base ratio φ, feeding the normal-form reflection that records CanonicalUniformScaleLaw on the orbit.
In the primer landmarks this is the concrete scale object behind T6 (φ forced as self-similar fixed point) inside the complete inevitability chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.