uniform_scale_ratio_unique
plain-language theorem explainer
In any positive multilevel composition, a uniform geometric scale factor is unique: if every adjacent level multiplies by σ and also by τ, then σ = τ. Hierarchy and φ-ladder arguments cite this to pin the single free ratio once zero free-scale is imposed. The proof evaluates the two recurrences at level 0 and cancels the strictly positive base value.
Claim. Let $M$ be a nontrivial multilevel composition (a sequence of strictly positive real levels with at least three levels). If $\sigma,\tau\in\mathbb{R}$ satisfy $M_{k+1}=\sigma\,M_k$ and $M_{k+1}=\tau\,M_k$ for every $k\in\mathbb{N}$, then $\sigma=\tau$.
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. Hierarchy structure sits between ledger discreteness and the self-similar fixed point that forces φ (T6).
A nontrivial multilevel composition is a map $k\mapsto M_k\in\mathbb{R}$ with $M_k>0$ for all $k$ and at least three positive levels. Uniform scaling means a single real ratio multiplies every adjacent pair: $M_{k+1}=\sigma M_k$. Cosmology-side ladders use the same geometric pattern (e.g. $\varphi^k$), so uniqueness of that ratio is the algebraic backbone of “no free scale.”
Upstream hierarchy forcing already packages the positive-level data; this lemma isolates the pure cancellation fact needed before one identifies the forced ratio with φ.
proof idea
Short tactic proof. From positivity of levels, $M_0\neq 0$. Instantiate both uniform-scaling hypotheses at $k=0$ to get $M_1=\sigma M_0$ and $M_1=\tau M_0$, hence $\sigma M_0=\tau M_0$. Right-cancel the nonzero factor $M_0$ (mul_right_cancel₀) to conclude $\sigma=\tau$. No hierarchy-specific lemmas beyond the structure’s positivity field.
why it matters
Feeds directly into hierarchy_forced_ratio_unique, which states that the canonical hierarchy from zero-free-scale data has the unique possible uniform scale ratio. That step is the uniqueness half of the hierarchy construction on the path to T6 (φ forced as the self-similar fixed point of the discrete ledger).
Without uniqueness, “no free scale parameters forces uniform adjacent ratios” would leave an equivalence class of generators rather than a single ratio. With it, the forcing chain can identify the geometric step with the unique self-similar scale and proceed toward the eight-tick octave and $D=3$. The lemma is elementary but closes the equivalence loophole in the canonical hierarchy story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.