ladderMass
plain-language theorem explainer
Defines the RS mass-ladder point as yardstick times golden ratio to the rung power: m(M0,r)=M0·φ^r. Anyone working the mass-ladder universe or dimensionless rung ratios cites this carrier. It is a one-line noncomputable definition, not a proved statement.
Claim. For a real yardstick $M_0$ and natural rung index $r$, the ladder mass is $m(M_0,r) := M_0 \cdot \varphi^r$, where $\varphi$ is the golden ratio.
background
Recognition Science places particle masses on a discrete $\varphi$-ladder. The absolute scale is a free yardstick $M_0$; the rung $r\in\mathbb{N}$ is the discrete index. The module is the mass-ladder layer of maximal forcing: it separates a forced dimensionless scaling invariant from an independent absolute yardstick.
Upstream, sector yardsticks are built as $A_s=2^{B_{\mathrm{pow}}}\cdot E_{\mathrm{coh}}\cdot\varphi^{r_0}$ (Masses.Anchor), and a unit anchor $M_0=1$ appears in RSBridge. The golden ratio $\varphi$ is the self-similar fixed point forced in the T0–T8 chain (T6). This definition is the bare carrier used by those constructions: pure geometric progression in $\varphi$, no gap or sector correction yet.
Locally the module treats every real $M_0$ as an admissible yardstick and studies claims quantified over that family.
proof idea
No proof: a noncomputable definition equal to $M_0\cdot\varphi^r$. Downstream proofs unfold it and apply pow_succ plus ring arithmetic (as in the forced adjacent-rung identity).
why it matters
This is the carrier for the fifth maximal-forcing universe (Phase 2 mass-ladder extension). The module doc states the honest split: the ratio of adjacent rungs is forced for every yardstick, while the absolute yardstick is independent.
It feeds isLadderRatioClaim (the claim that $m(M_0,r+1)=\varphi\cdot m(M_0,r)$ for all $r$) and the theorem forced_ladderRatio, which shows that claim is Forced with no gate. That is the structural half of the mass law $m(\mathrm{rung})=\mathrm{yardstick}\cdot\varphi^{\mathrm{rung}}$ from the RS primer; the absolute scale remains a free coordinate with an explicit countermodel pair elsewhere in the module.
Without this definition the classifier cannot exercise both forced and independent branches on the same universe.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.