forced_ladderRatio
plain-language theorem explainer
Adjacent rungs on the RS mass ladder always differ by the factor φ, for every real yardstick. The dimensionless scaling invariant is forced on the full admissibility class (no gate). Cite this when separating forced ladder structure from free absolute units. Proof is a short algebraic identity: unfold the ladder, apply pow_succ, and ring.
Claim. Let $\mathrm{ladderMass}(M_0,r)=M_0\cdot\varphi^r$. On the admissibility class of every candidate yardstick $M_0\in\mathbb{R}$, the claim $\forall r\in\mathbb{N},\;\mathrm{ladderMass}(M_0,r+1)=\varphi\cdot\mathrm{ladderMass}(M_0,r)$ holds. In the maximal-forcing sense, this reality claim is forced: it is true in every admissible realization.
background
This module is the mass-ladder layer of maximal forcing. The RS mass law places masses on a phi-ladder $m(\mathrm{rung})=\mathrm{yardstick}\cdot\varphi^{\mathrm{rung}}$. The module separates two claims: the dimensionless adjacent-rung ratio is forced for every yardstick, while the absolute yardstick itself is independent (a free coordinate with an explicit countermodel pair).
Here $\mathrm{ladderMass}(M_0,r)=M_0\cdot\varphi^r$ is a point on that ladder. The claim under study asserts $\mathrm{ladderMass}(M_0,r+1)=\varphi\cdot\mathrm{ladderMass}(M_0,r)$ for all natural $r$. The admissibility class is the universe of all real yardsticks; no further gate is imposed.
Upstream, Forced means the claim holds in every admissible realization. The claim object packages exactly the forall-rung ratio identity. Phi enters as the self-similar fixed point of the forcing chain (T6), so the ratio $\varphi$ is the structural step of the ladder, not an empirical fit.
proof idea
Term/tactic hybrid, essentially an algebraic one-liner. Introduce an arbitrary yardstick $M_0$ (membership in the full class is vacuous) and a rung $r$. Reduce the goal to $\mathrm{ladderMass}(M_0,r+1)=\varphi\cdot\mathrm{ladderMass}(M_0,r)$. Unfold the ladder definition to $M_0\cdot\varphi^{r+1}$ versus $\varphi\cdot(M_0\cdot\varphi^r)$. Rewrite with $\mathrm{pow_succ}$ and finish by ring. No external lemmas beyond the ladder definition and ordinary power arithmetic are required.
why it matters
This is the forced half of the mass-ladder universe's honest split: dimensionless structure forced, absolute units free. It feeds mass_scaling_forced_yardstick_free, which packages Forced(ladder ratio) ∧ Independent(yardstick), and massUniverse_classifier, the first mixed classifier that exercises both ClaimClassification.forced and .independent branches.
In the Recognition framework this pins the mass formula's phi-ladder step (yardstick · φ^(rung−8+gap(Z))) as a structural identity rather than a calibrated slope. It aligns with T6 (φ forced as self-similar fixed point): once masses live on powers of φ, adjacent-rung ratios cannot be anything else. The result shows the maximal-forcing machinery is not trivially always-forced; the companion Independent claim on the yardstick is what makes the trichotomy nontrivial.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.