massUniverse_classifier
plain-language theorem explainer
Every claim in the mass-ladder forcing closure is classified: the dimensionless adjacent-rung ratio equals φ (forced), while the absolute mass yardstick is independent. Anyone separating RS mass-law invariants from free coordinates cites this. The proof is a two-case membership split on a two-element claim set, feeding each ClaimClassification constructor.
Claim. For every reality claim $C$ about the mass-ladder universe, if $C$ lies in the forcing closure generated from the law-of-logic primitive, then $C$ is classified: either forced (true in every admissible realization) or independent (two admissible realizations disagree on $C$). Concretely the closure holds the φ-ladder ratio claim as forced and the absolute yardstick claim as independent.
background
The module is the fifth concrete maximal-forcing universe and the first whose closure genuinely uses both trichotomy branches. Recognition Science places masses on a φ-ladder: $m(\mathrm{rung})=\mathrm{yardstick}\cdot\varphi^{\mathrm{rung}}$. The dimensionless scaling invariant (adjacent-rung ratio equals $\varphi$) is a structural property of the ladder and is forced over every yardstick with no gate. The absolute yardstick is a free coordinate, witnessed by an explicit countermodel pair.
ClaimClassification is the inductive verdict on one claim in one universe: either forced (holds under every admissible realization) or independent (an independence witness of two disagreeing admissible realizations). InClosure means the claim belongs to the forcing closure of a chosen primitive (here law-of-logic) inside the mass-ladder claim universe. Upstream, forced_ladderRatio supplies the forced branch and yardstickIndepWitness the independent branch.
proof idea
Introduce the claim $C$ and the closure hypothesis. The hypothesis immediately gives membership of $C$ in the universe's finite claim set. Unfold the mass-universe definition and simplify membership to a disjunction of two singleton equalities. Case-split:
- On the ladder-ratio claim, substitute and apply the
forcedconstructor with the already-provedforced_ladderRatiolemma. - On the yardstick claim, substitute and apply the
independentconstructor withyardstickIndepWitness.
No further arithmetic: the work is pure case analysis on a two-element set.
why it matters
This is the mixed classifier that makes the mass-ladder universe the first certificate to exercise both forced and independent branches, proving the maximal-forcing machinery is not trivially always-forced. Downstream, massUniverseCert packages it as the classifies field of a real MaximalClosureCert for law-of-logic over the mass universe; the crown trichotomy on that universe then records one forced invariant, one independent coordinate, and an empty selected set.
In the broader RS chain this realizes the honest separation predicted for the mass formula (yardstick times $\varphi$ to a rung power): φ itself is the T6 self-similar fixed point, and the ladder ratio is the dimensionless structural content, while the yardstick remains a free coordinate. It closes Phase-2 scaffolding that the forcing layer can distinguish invariants from coordinates in machine-checked form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.