no_free_scale_of_canonical_uniform
plain-language theorem explainer
Any multilevel hierarchy obeying the canonical uniform-scale law has identical adjacent ratios at every index: the step ratio is independent of level. Hierarchy and self-similarity arguments cite this to replace the raw all-pairs no-free-scale hypothesis with a single base-ratio certificate. The proof rewrites both ratios by the uniform step and cancels positives.
Claim. Let $M$ be a nontrivial multilevel composition (positive real level sizes $M.\mathrm{levels}:\mathbb{N}\to\mathbb{R}$, at least three levels). If every adjacent step is generated by $M$'s canonical base ratio $r_M$, i.e. $M.\mathrm{levels}(k+1)=r_M\cdot M.\mathrm{levels}(k)$ for all $k$, then for all indices $j,k$, $$\frac{M.\mathrm{levels}(j+1)}{M.\mathrm{levels}(j)}=\frac{M.\mathrm{levels}(k+1)}{M.\mathrm{levels}(k)}.$$
background
In the Unified Forcing Chain, T0–T8 are forced from the Recognition Composition Law plus normalization and calibration. The T5→T6 bridge needs self-similarity on a discrete ledger hierarchy: no free scale parameters may sit between levels.
A NontrivialMultilevelComposition is a positive real sequence of level sizes with at least three levels. The structure CanonicalUniformScaleLaw is the theorem-shaped certificate that every adjacent step is multiplication by one fixed canonical base ratio of that hierarchy (the replacement for a raw all-pairs hypothesis).
The raw no-free-scale equation asserts that every pair of adjacent ratios coincides. This lemma is the easy direction: uniform generation by a single base ratio immediately yields that all-pairs equality. The converse direction and the full equivalence live in the sibling canonical_uniform_iff_no_free_scale.
proof idea
Term-style tactic proof, three steps. Fix arbitrary indices $j$ and $k$. Rewrite $M.\mathrm{levels}(j+1)$ and $M.\mathrm{levels}(k+1)$ via the uniform-step field of the canonical law, so each side becomes $(r_M\cdot \ell_j)/\ell_j$ and $(r_M\cdot \ell_k)/\ell_k$. Then field_simp with positivity of levels (from levels_pos) cancels the nonzero denominators and equates both sides to $r_M$. No external lemmas beyond the structure fields.
why it matters
This is the export arrow from the canonical uniform-scale certificate to the older all-pairs no-free-scale language used throughout hierarchy forcing. Downstream, canonical_uniform_iff_no_free_scale packages both directions; hierarchy_forced_ratio_eq_canonical_base identifies the forced hierarchy ratio with the canonical base once uniformity and growth hold.
On the φ side it feeds the posting-closure packages: canonical_uniform_posting_closure_forces_phi, canonical_uniform_growth_posting_closure_forces_phi, and the seed variants that force φ from uniform scale plus growth/posting data. Those close the T5→T6 self-similarity bridge (t5_to_t6_bridge_holds, T5_To_T6_SelfSimilarity_Bridge): unique J (T5) plus discrete self-similar hierarchy forces the golden ratio fixed point (T6).
Within the primer landmarks, this is pure hierarchy hygiene for T6, not a claim about J-uniqueness, eight-tick, or $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.