yardstick_independent
plain-language theorem explainer
The absolute mass yardstick (the claim that the base mass equals 1) is independent over the full class of candidate yardsticks: two admissible realizations disagree on it. Anyone citing the mass-ladder trichotomy or the forced-vs-free split in RS units needs this. The proof is a one-line application of the independence-witness lemma to a prebuilt countermodel pair.
Claim. Over the admissibility class of every real candidate yardstick, the reality claim "$M_0 = 1$" is independent: there exist admissible realizations $R_0, R_1$ such that the claim holds at $R_0$ and fails at $R_1$.
background
In the mass-ladder layer of maximal forcing, RS masses sit on a $\varphi$-ladder $m(\mathrm{rung}) = M_0 \cdot \varphi^{\mathrm{rung}}$. The module separates two claims: the dimensionless adjacent-rung ratio equals $\varphi$ (a structural invariant), and the absolute yardstick $M_0 = 1$ (a unit choice).
Admissibility here is the unrestricted class of every real candidate yardstick. A claim is independent over an admissible class when two admissible realizations disagree on it: $\exists R_0,R_1$ both admissible with $C(R_0)$ and $\neg C(R_1)$. The yardstick claim is exactly the predicate $M_0 = 1$.
Upstream, independent_of_witness turns an explicit IndependenceWitness (yes-model, no-model, admissibility, and hold/fail certificates) into the proposition-level Independent tag. The module supplies such a witness for the yardstick.
proof idea
One-line term proof: apply independent_of_witness to the preconstructed yardstickIndepWitness. That witness packages a pair of admissible reals, one with $M_0 = 1$ and one with $M_0 \neq 1$, so the existential Independent predicate follows immediately from the witness fields.
why it matters
This is the Independent half of the mass-ladder closure, the first universe whose certificate uses both trichotomy branches. Downstream, mass_scaling_forced_yardstick_free packages it with the forced ladder-ratio claim: "Dimensionless structure is forced; absolute units are free."
In the Recognition framework this matches the mass formula on the $\varphi$-ladder (yardstick times $\varphi$ to a rung offset): ratios and gaps are structural, while the overall mass scale is a free coordinate. It shows the maximal-forcing machinery is not vacuously always-forced; it distinguishes invariants from unit choices. No open scaffold remains here; the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.