canonical_uniform_iff_no_free_scale
plain-language theorem explainer
For any nontrivial multilevel hierarchy, the canonical uniform-scale law (every adjacent step multiplies by the hierarchy's own base ratio) is equivalent to the raw no-free-scale condition that all adjacent level ratios agree. Hierarchy and T5–T6 bridge arguments cite this to swap between the two formulations. The proof is a two-line iff constructor from the two one-sided lemmas.
Claim. Let $M$ be a nontrivial multilevel composition (positive real levels $M_k$ with at least three levels). Then $M$ obeys the canonical uniform-scale law—every adjacent step satisfies $M_{k+1} = r_M \, M_k$ for the hierarchy's canonical base ratio $r_M$—if and only if all adjacent ratios agree: $M_{j+1}/M_j = M_{k+1}/M_k$ for every $j,k$.
background
The Unified Forcing Chain module shows T0–T8 as forced from the cost foundation (Recognition Composition Law plus normalization and calibration). The T5→T6 step needs self-similarity on a discrete ledger hierarchy: once $J$ is unique, a closed scale forces $\varphi$ as the self-similar fixed point.
A NontrivialMultilevelComposition is a positive real sequence of levels with at least three entries. The raw no-free-scale condition says every adjacent ratio $M_{k+1}/M_k$ is the same number—no free scale parameter between rungs. CanonicalUniformScaleLaw is the theorem-shaped replacement: every step is generated by the hierarchy's own canonical base ratio, $M_{k+1} = r_M M_k$.
Upstream, the one-sided lemmas already prove each direction separately (canonical_uniform_of_no_free_scale and no_free_scale_of_canonical_uniform). This declaration packages them as a single equivalence used by the T5–T6 bridge.
proof idea
Term-mode constructor on the biconditional. The forward direction applies no_free_scale_of_canonical_uniform M: if every step multiplies by the canonical base ratio, then all adjacent ratios equal that same ratio, hence equal each other. The reverse applies canonical_uniform_of_no_free_scale M: if all adjacent ratios agree, that common value is the canonical base ratio and the uniform-step law holds. No further algebra is done here.
why it matters
This equivalence is the clean interface between the older raw no-free-scale hypothesis and the canonical uniform-scale certificate used in the forcing chain. Downstream, t5_to_t6_bridge_holds records that the T5-to-T6 self-similarity bridge is theorem-backed; that bridge needs a closed, parameter-free scale on the hierarchy so that self-similarity pins $\varphi$ (T6) once $J$ is unique (T5).
In the primer landmarks, T5 is $J$-uniqueness ($J(x)=\cosh(\log x)-1$) and T6 is $\varphi$ as the self-similar fixed point. Replacing an ad-hoc all-pairs ratio hypothesis with a unique canonical certificate keeps the hierarchy step propositionally tidy (subsingleton certificates) and feeds the complete inevitability chain from cost foundation through T6.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.