massUniverse
plain-language theorem explainer
Defines the mass-ladder claim universe: realizations are real yardsticks, every yardstick is admissible, and the claim set is exactly the dimensionless adjacent-rung ratio identity plus the absolute-unit choice M0 = 1. Anyone citing the mixed Forced/Independent mass-ladder closure uses this package. Assembly is a three-field structure instance, not a proof.
Claim. The mass-ladder claim universe has realization type $\mathbb{R}$ (candidate yardsticks), admissibility class equal to the full set of reals (every yardstick allowed), and claim set $\{$adjacent rungs scale by $\varphi$, yardstick equals $1$ $\}$.
background
Recognition Science places particle masses on a $\varphi$-ladder: $m(r) = M_0 \cdot \varphi^r$ for rung $r$ and free yardstick $M_0$. The module is the Phase-2 maximal-forcing layer that separates what the ladder forces from what remains a coordinate choice.
A claim universe packages three pieces: a type of realizations, an admissibility class on that type, and a finite set of reality claims. Here the realization type is $\mathbb{R}$, and the admissibility class is the universal class (label: every candidate yardstick), so no gate tightens the domain before classification.
The two claims are: (i) the structural identity $\mathrm{ladderMass}(M_0,r+1)=\varphi\cdot\mathrm{ladderMass}(M_0,r)$ for all $r$, independent of $M_0$; (ii) the absolute-unit assertion $M_0=1$. Upstream, the generic ClaimUniverse structure is the carrier for one maximal-forcing pass; the ladder-ratio and yardstick claims are the concrete RealityClaim instances plugged into that carrier.
proof idea
Definitional assembly, not a tactic proof. Realization is set to $\mathbb{R}$; admissibility is the universal class on yardsticks; claims is the two-element set containing the ladder-ratio claim and the yardstick claim. No lemmas are applied beyond naming those three components.
why it matters
This is the fifth concrete maximal-forcing instantiation and the first whose closure genuinely uses both Forced and Independent branches of the trichotomy. Downstream, the mixed classifier routes every closed claim through this universe; the independence witness for the yardstick claim reads its claim set; the maximal-closure certificate and the crown trichotomy theorem are indexed on it.
In framework terms it records the honest split predicted by the RS mass law: dimensionless $\varphi$-scaling on the ladder is forced with no gate (a structural identity), while the absolute yardstick remains a free coordinate with an explicit countermodel pair. That split shows the forcing machinery is not vacuously always-forced. It sits under the broader forcing chain (T6 $\varphi$ as self-similar fixed point; mass formula yardstick $\cdot\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$) as the layer that classifies which mass-ladder statements are invariants versus coordinates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.