Lmass0
plain-language theorem explainer
The mass-ladder layer uses the unrestricted admissibility class on the reals: every candidate yardstick is allowed. Anyone citing the forced adjacent-rung ratio φ or the independent yardstick coordinate works over this class. The definition simply takes the admissible set to be all of ℝ, with no gate or tightening.
Claim. Let $L_0$ be the admissibility class on $\mathbb{R}$ whose admissible set is $\mathbb{R}$ itself (every candidate yardstick), labeled "every candidate yardstick".
background
In the maximal-forcing mass-ladder layer, RS masses sit on a phi-ladder $m(r) = y,\varphi^r$ with free yardstick $y\in\mathbb{R}$ and dimensionless rung index $r$. An admissibility class packages a set of allowed realizations together with a label; here the realization type is $\mathbb{R}$ (candidate yardsticks).
A claim is forced on a class when it holds in every admissible realization, and independent when two admissible realizations disagree. The module separates the structural scaling identity (adjacent rungs differ by $\varphi$) from the absolute unit $y$.
Because the scaling identity is algebraic in the ladder definition, the class needs no restriction: the admissible set is the full universe of reals. Absolute yardstick choice remains free and is witnessed elsewhere by an explicit countermodel pair.
proof idea
Pure definitional construction of an AdmissibilityClass ℝ: the admissible field is Set.univ, and the label string is fixed to "every candidate yardstick". No proof obligations beyond inhabiting the structure.
why it matters
This is the ambient class for the mass-ladder claim universe. Downstream, forced_ladderRatio proves the adjacent-rung factor $\varphi$ is forced over every yardstick with no gate; yardstick_independent shows the absolute yardstick claim is independent; and mass_scaling_forced_yardstick_free packages both. The universe certificate and crown trichotomy then classify the closure as one Forced invariant plus one Independent coordinate (Selected empty).
That split is the first maximal-forcing universe whose classifier genuinely uses both branches, matching the RS mass law (yardstick times $\varphi^{\mathrm{rung}}$) and the T6 forcing of $\varphi$ as the self-similar scale. Dimensionless ladder structure is forced; absolute units stay free coordinates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.