canonical_uniform_of_no_free_scale
plain-language theorem explainer
If every adjacent ratio of a multilevel hierarchy is the same, the hierarchy obeys the canonical uniform-scale law: each level equals the base ratio times the previous level. Hierarchy and closed-scale realization proofs cite this to replace a raw all-pairs ratio hypothesis with a single generator. The argument is a short field calculation identifying the common ratio with the base ratio levels(1)/levels(0).
Claim. Let $M$ be a nontrivial multilevel composition (positive real levels with at least three levels). If for all $j,k$ one has $M.\mathrm{levels}(j+1)/M.\mathrm{levels}(j)=M.\mathrm{levels}(k+1)/M.\mathrm{levels}(k)$, then $M$ satisfies the canonical uniform-scale law: for every $k$, $M.\mathrm{levels}(k+1)=r_M\, M.\mathrm{levels}(k)$, where $r_M$ is the hierarchy's own base ratio.
background
The Unified Forcing Chain module aims to force T0–T8 from the cost foundation (Recognition Composition Law plus normalization and calibration). Hierarchy structure sits between discreteness/ledger forcing and the self-similar $\varphi$ step (T6): multilevel compositions package a positive sequence of scale levels with a nontriviality lower bound of three levels.
The raw no-free-scale condition says every adjacent ratio equals every other adjacent ratio. That is an all-pairs statement. The structure CanonicalUniformScaleLaw is the theorem-shaped replacement: adjacent levels are generated by a single canonical base ratio of the hierarchy (the ratio of level 1 to level 0). Propositional uniqueness of such certificates is recorded separately by a subsingleton instance.
Upstream, NontrivialMultilevelComposition supplies positivity of every level, which is what makes the ratios well-defined and the field simplifications legal. Downstream wrappers apply this lemma once a concrete realization (admissible orbit, realized hierarchy, or closed-scale model) has already produced equal adjacent ratios.
proof idea
Tactic proof of the single field uniform_step. Fix level index $k$. Positivity of levels gives $M.\mathrm{levels},k\neq 0$. Instantiate the no-free-scale hypothesis at $(k,0)$ so the adjacent ratio at $k$ equals the adjacent ratio at $0$. Unfold the canonical base ratio (level 1 over level 0). Then rewrite
$M.\mathrm{levels}(k+1)=(M.\mathrm{levels}(k+1)/M.\mathrm{levels},k)\cdot M.\mathrm{levels},k$
by field simplification, and replace the ratio by the base ratio via the $(k,0)$ equality. No deeper lemmas are needed beyond positivity and the base-ratio definition.
why it matters
This lemma is the one-direction bridge from the older raw no-free-scale hypothesis to the canonical uniform-scale certificate used throughout the forcing chain. Its immediate parent is the biconditional canonical_uniform_iff_no_free_scale, which packages both directions.
Three realization theorems apply it as a one-line discharge: realizedHierarchy_canonical_uniform, realizedClosedScale_canonical_uniform, and admissibleOrbit_canonical_uniform. Each builds a multilevel composition from a closed observable framework (realized hierarchy, closed-scale model, or admissible orbit) and feeds the resulting equal-ratio fact into this constructor.
In framework terms, uniform adjacent scaling is the discrete self-similarity ingredient that later pins $\varphi$ as the unique self-similar fixed point (T6) on the ledger hierarchy. Without a single generator for every step, free scale parameters would remain and the $\varphi$-ladder mass and constant derivations would not be forced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.