CanonicalUniformScaleLaw
plain-language theorem explainer
A hierarchy obeys the canonical uniform-scale law when each adjacent level is exactly the previous level times that hierarchy's own base ratio. It is the theorem-shaped stand-in for the raw all-pairs no-free-scale hypothesis. Downstream φ-forcing and admissible-orbit normal forms cite it as a certificate. The structure is a single Prop field; uniqueness is propositional (Subsingleton by rfl).
Claim. Let $M$ be a nontrivial multilevel composition (a hierarchy of levels). The canonical uniform-scale law on $M$ is the proposition that for every index $k$, the next level equals the hierarchy's canonical base ratio times the current level: $M.\mathrm{levels}(k+1) = r_M \cdot M.\mathrm{levels}(k)$, where $r_M$ is the canonical base ratio of $M$. For fixed $M$, any two such certificates are propositionally equal.
background
The module UnifiedForcingChain aims at a complete inevitability chain T-1 through T8 from the cost foundation (Recognition Composition Law, normalization, calibration). T6 is the step that forces $\varphi$ as the self-similar fixed point of a discrete ledger hierarchy.
A nontrivial multilevel composition packages a discrete ladder of positive level values. The canonical base ratio of such a hierarchy is the intrinsic scale factor associated to that ladder (the quantity later identified with $\varphi$ under growth and seed hypotheses). Cosmology-side scale ladders of the form $\varphi^k$ are the intended geometric picture, but here the ratio is still an abstract field of $M$.
The raw alternative is an all-pairs no-free-scale equation on level ratios. The present structure replaces that bulk hypothesis by a single adjacent-step law generated by one base ratio, which is easier to discharge from admissible orbits and posting data.
proof idea
This is a structure definition, not a derived theorem: one field uniform_step asserting the geometric recurrence of levels under the hierarchy's canonical base ratio. The accompanying Subsingleton instance is a one-line proof that any two inhabitants are equal by reflexivity of equality on the underlying Prop (propositional uniqueness of the certificate for fixed $M$). No upstream lemmas are applied in the definition itself; consumers construct inhabitants via canonical_uniform_of_no_free_scale or from admissible-orbit data.
why it matters
In the forcing chain this is the clean certificate that feeds T6-style $\varphi$ forcing. Downstream, uniform scale plus canonical growth and seed size yield canonicalBaseRatio_eq_phi_of_uniform_seed ($r_M = \varphi$). The same triple, or uniform+growth+posting closure, yields canonical_uniform_growth_seed_forces_phi and canonical_uniform_growth_posting_closure_forces_phi.
Admissible orbits supply the law directly (admissibleOrbit_canonical_uniform), and the admissible-orbit normal-form reflection packages it as a required field. Equivalence theorems (canonical_uniform_iff_no_free_scale, canonical_uniform_of_no_free_scale) connect it to the older all-pairs hypothesis, so the rest of the chain can quote a single named Prop instead of a free-scale jungle. Landmark link: T6 ($\varphi$ forced as self-similar fixed point) and the discrete ledger hierarchy that also underwrites the eight-tick octave and $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.