hierarchy_forced_ratio_eq_canonical_base
plain-language theorem explainer
Under a canonical uniform-scale law and growth (base ratio > 1), the unique uniform ladder ratio forced by zero free scale equals the hierarchy's own base ratio levels₁/levels₀. Hierarchy and T5–T6 bridge arguments cite this to pin the self-similar scale to the data rather than an external parameter. The proof is a one-line application of ratio uniqueness to the uniform-step certificate.
Claim. Let $M$ be a multilevel composition with positive levels and at least three levels. Suppose every adjacent step satisfies $M.\mathrm{levels}(k+1)=r_M\,M.\mathrm{levels}(k)$ where $r_M=M.\mathrm{levels}(1)/M.\mathrm{levels}(0)$, and suppose $1<r_M$. Then the uniform scale ladder constructed from the induced no-free-scale data has ladder ratio exactly $r_M$.
background
The Unified Forcing Chain module aims to derive T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. The T5→T6 step needs a discrete self-similar hierarchy whose single scale ratio is forced, not chosen.
A nontrivial multilevel composition is a positive real sequence of levels with at least three entries. The canonical base ratio is simply the first adjacent quotient $r_M=\mathrm{levels}(1)/\mathrm{levels}(0)$. The canonical uniform-scale law is the theorem-shaped stand-in for raw all-pairs no-free-scale: every step is multiplication by that same $r_M$.
Upstream, hierarchy_forced builds a uniform scale ladder from any no-free-scale certificate and a growth hypothesis $1<\mathrm{levels}(1)/\mathrm{levels}(0)$. The companion uniqueness result states that this constructed ladder has the only possible uniform ratio compatible with those data.
proof idea
Term-mode one-liner. Feed hierarchy_forced_ratio_unique the multilevel $M$, the no-free-scale certificate obtained by specializing the canonical uniform law (no_free_scale_of_canonical_uniform), the growth hypothesis $1<r_M$, and the uniform-step field of the canonical law. Uniqueness then identifies the forced ladder ratio with $r_M$.
why it matters
This closes the identification between "the ratio the hierarchy forces" and "the hierarchy's own base ratio" once uniform scaling is stated canonically. Downstream it supports t5_to_t6_bridge_holds, whose doc-comment records that the T5-to-T6 self-similarity bridge is theorem-backed: unique $J$ plus an internal closed scale forces $\varphi$ as the self-similar fixed point (forcing-chain landmark T6).
Without this equality, the ladder ratio could float as an abstract uniform constant rather than the concrete $r_M$ read off the levels. The result is local glue inside the complete inevitability chain, not a new physical constant derivation by itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.