yardstickIndepWitness
plain-language theorem explainer
Explicit independence witness for the absolute mass yardstick in the mass-ladder claim universe: the reals 1 and 2 are both admissible, and the claim "M0 = 1" holds at 1 while failing at 2. Anyone classifying claims in the RS mass-ladder layer cites this pair. The body is a direct structure instance; the no-model branch is a one-line numerical contradiction.
Claim. There is an independence witness for the claim $M_0 = 1$ over the mass-ladder universe: the admissible real realizations $1$ and $2$ satisfy that the claim holds at $1$ and fails at $2$. Hence the absolute yardstick is a free coordinate, not a forced invariant.
background
The RS mass law places masses on a phi-ladder, $m(\mathrm{rung}) = \mathrm{yardstick}\cdot\varphi^{\mathrm{rung}}$. This module is the Phase-2 mass-ladder layer of maximal forcing: it separates the dimensionless scaling invariant (adjacent-rung ratio equals $\varphi$, forced over every yardstick) from the absolute yardstick (independent free coordinate).
An IndependenceWitness is an explicit countermodel pair for a claim over an admissible class: two realizations, both admissible, one at which the claim holds and one at which it fails. Here the realization type is $\mathbb{R}$ and the claim is the absolute-unit choice "$M_0 = 1$" (holds means equality to one). The ambient universe packages that claim together with the forced ladder-ratio claim under a single admissibility predicate on reals.
proof idea
Direct structure instance of the independence-witness record. The yes-model is $1$ and the no-model is $2$. Both admissibility obligations are discharged by trivial (every real is admissible in this universe). The yes-holds field is rfl ($1=1$). The no-fails field assumes $2=1$ from the claim and finishes by norm_num, a pure numerical contradiction. No upstream lemmas beyond the witness structure and the claim/universe defs are required.
why it matters
Feeds yardstick_independent, which lifts the witness to a Prop-level independence statement, and through that the mixed classifier massUniverse_classifier: every claim in the mass-ladder closure is classified, scaling as forced and yardstick as independent. Downstream doc: this is "the first universe whose certificate uses both branches," proving the maximal-forcing machinery is not trivially always-forced.
In the broader RS picture this matches the mass formula (yardstick times a $\varphi$-power on the ladder): ratios and rung structure are forced by the self-similar fixed point $\varphi$ (T6) and the composition law, while the overall scale remains a free coordinate. The witness is the machine-checked countermodel pair that makes that separation honest.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.