hierarchy_forced_ratio_unique
plain-language theorem explainer
Any uniform scale factor that generates the level sequence of a nontrivial multilevel composition must equal the ratio of the canonical hierarchy built from zero-free-scale data. Hierarchy and self-similarity arguments cite this when identifying the forced ladder ratio with a concrete generator σ. The proof is a two-hypothesis application of uniform scale-ratio uniqueness.
Claim. Let $M$ be a nontrivial multilevel composition (positive levels, at least three). Suppose adjacent ratios are free-scale free: $M.\mathrm{levels}(j+1)/M.\mathrm{levels}(j)$ is independent of $j$, and $1 < M.\mathrm{levels}(1)/M.\mathrm{levels}(0)$. If $\sigma\in\mathbb{R}$ satisfies $M.\mathrm{levels}(k+1)=\sigma\, M.\mathrm{levels}(k)$ for all $k$, then the ratio of the forced uniform-scale ladder equals $\sigma$.
background
The Unified Forcing Chain module derives 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 rungs. Zero free scale means every adjacent ratio equals every other; together with growth above 1 this data builds the canonical uniform-scale ladder via hierarchy_forced.
Upstream, uniform_scale_ratio_unique already states that if two reals each generate the same level sequence by uniform scaling, they coincide. The present result specializes that uniqueness to the ratio field of the forced ladder.
proof idea
One-line wrapper around uniform_scale_ratio_unique. Feed it the multilevel composition $M$, take the first generator to be the forced ladder's own uniform-scaling law (from hierarchy_forced), and take the second generator to be the hypothesized $\sigma$-scaling $h\sigma$. Uniqueness yields equality of the two ratios.
why it matters
Pins the forced hierarchy ratio to any concrete uniform generator, so later identifications are not up to an undetermined constant. Downstream, hierarchy_forced_ratio_eq_canonical_base uses it to match the forced ratio to the canonical base whenever the canonical uniform-scale law and growth hold. That identification feeds t5_to_t6_bridge_holds, the theorem-backed T5→T6 self-similarity bridge: unique $J$ plus a forced closed scale forces $\varphi$ as the self-similar fixed point (primer T5–T6). Without ratio uniqueness the ladder could drift by an arbitrary factor and $\varphi$-forcing would not close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.