isLadderRatioClaim
plain-language theorem explainer
Packages the dimensionless mass-ladder scaling law as a RealityClaim on real yardsticks: adjacent rungs always differ by the factor φ. Anyone citing the forced-scaling theorem or the mass-universe trichotomy cites this claim object. The body is a pure predicate definition (the recurrence holds for all rungs), not a proved theorem.
Claim. The claim, over real yardsticks $M_0$, that for every natural rung $r$ one has $m(M_0,r+1)=\varphi\, m(M_0,r)$, where the ladder mass is $m(M_0,r)=M_0\varphi^r$. This is the dimensionless adjacent-rung scaling invariant, independent of the choice of yardstick.
background
In the mass-ladder layer of maximal forcing, RS masses sit on a phi-ladder $m(r)=\mathrm{yardstick}\cdot\varphi^{r}$. The module separates two questions: the dimensionless ratio of adjacent rungs, and the absolute yardstick itself. The former is structural; the latter is a free coordinate.
A RealityClaim on a carrier $R$ is a labeled predicate holds : R → Prop. Here $R=\mathbb{R}$ (candidate yardsticks). The ladder point is defined by $m(M_0,r)=M_0\varphi^r$. The admissible class is every real yardstick: no gate is needed for the ratio claim.
Upstream, independence means two admissible realizations disagree on the claim; forcedness means every admissible realization satisfies it. This definition only names the ratio claim; classification comes later.
proof idea
Definitional packaging, not a proof. The structure fields are set directly: the audit label records the recurrence in words, and holds is the predicate sending each yardstick $M_0$ to $\forall r:\mathbb{N},, m(M_0,r+1)=\varphi, m(M_0,r)$. No lemmas are applied; the mathematical content is exactly that quantified equality on the ladder.
why it matters
This claim is the forced half of the mass-ladder universe. Downstream, forced_ladderRatio shows it holds for every yardstick by unfolding $m(M_0,r)=M_0\varphi^r$, using $\varphi^{r+1}=\varphi\cdot\varphi^r$, and a one-line ring identity—no admissibility gate. It is bundled into massUniverse beside the independent yardstick claim, and the summary theorem records Forced(ratio) ∧ Independent(yardstick).
That split is the point of the Phase-2 extension: maximal forcing is not vacuously always-forced; it distinguishes structural invariants from free absolute units. In the broader RS picture this is the dimensionless skeleton of the mass law (yardstick · φ^{rung-8+gap(Z)}), with φ the self-similar fixed point from the forcing chain (T6). Absolute calibration remains open as an independent coordinate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.