isYardstickClaim
plain-language theorem explainer
Packages the absolute-unit choice "yardstick equals one" as a RealityClaim on real realizations. Mass-ladder and maximal-forcing work cites it as the independent coordinate opposite the forced φ-ratio. The body is a one-line predicate definition: holds at M0 iff M0 = 1.
Claim. The yardstick claim is the assertion, on real realizations $M_0$, that $M_0 = 1$ (absolute mass unit fixed to one).
background
In the mass-ladder layer, RS places masses on a $\varphi$-ladder $m(\mathrm{rung}) = \mathrm{yardstick}\cdot\varphi^{\mathrm{rung}}$. Dimensionless adjacent-rung ratios are structural; the absolute yardstick is a free coordinate (unit choice).
A RealityClaim on a type $R$ is audit metadata plus a predicate holds : R → Prop. Here $R = \mathbb{R}$ and the realization is the yardstick $M_0$. The module is the fifth maximal-forcing instantiation and the first whose closure uses both trichotomy branches: one forced claim (ladder ratio $\varphi$) and one independent claim (this yardstick).
Upstream, independence witnesses and claim-universe machinery treat such predicates as the theorem content; the label "M0 = 1" is only audit-facing.
proof idea
Definition, not a proof. Instantiates RealityClaim ℝ with label "M0 = 1" and holds := fun M0 => M0 = 1. No lemmas or tactics; the predicate is the entire content.
why it matters
This is the independent half of the mass-ladder claim universe. It sits in massUniverse beside the forced ladder-ratio claim, and is the subject of yardstickIndepWitness (models $1$ and $2$ both admissible, disagreeing on $M_0=1$) and yardstick_independent.
Downstream summary mass_scaling_forced_yardstick_free records Forced(ladder ratio) ∧ Independent(yardstick): dimensionless structure forced, absolute units free. That mixed classifier is the first certificate exercising both forced and independent, so the machinery is not vacuously always-forced.
Framework-wise it matches the RS mass formula (yardstick times $\varphi$ to a rung offset) and the primer's absolute-unit freedom versus forced $\varphi$-ladder scaling (T6).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.