triUniverseCert
plain-language theorem explainer
Packages a maximal-closure certificate for the law-of-logic primitive over the three-branch claim universe. Anyone checking that maximal forcing is non-degenerate cites it: one closure realizes Forced, Selected, and Independent with proofs. The body is a one-field structure instance wiring in the existing three-universe classifier.
Claim. There is a maximal-closure certificate for the law-of-logic primitive on the three-branch claim universe: every reality claim in the closure is assigned a classification (Forced, Selected, or Independent) by the three-universe classifier.
background
Maximal forcing starts from a Primitive: either bare distinction or a law-of-logic realization once the floor is non-vacuous. A claim universe collects reality claims over a realization; a maximal-closure certificate is a structure whose single field is a classifier map sending every claim in the closure to a ClaimClassification (Forced / Selected / Independent).
This module's setting is Phase 4 of maximal forcing: the Forced branch (cost, $\varphi$, dimension, $\alpha$) and the Independent branch (mass yardstick) are exercised elsewhere. Here the third tag, Selected, is shown honestly via the golden class $L_{\mathrm{golden}}$ of ratios with $r^2=r+1$ but no positivity: $r=\varphi$ is not forced because the conjugate $\psi=(1-\sqrt{5})/2$ also solves the constraint, yet positivity selects the expanding root and drains Selected into Forced under the tightened class.
The three-branch universe is the concrete claim universe that simultaneously hosts one Forced, one Selected, and one Independent claim, so the classifier cannot collapse to a single tag.
proof idea
Definitional packaging, not a tactic proof. The certificate is the structure MaximalClosureCert at primitive lawOfLogic and universe triUniverse, with the classifies field set equal to the already-constructed triUniverse_classifier. No further lemmas are applied at this site; soundness lives in that classifier and in the sibling proofs that tag the three sample claims.
why it matters
Closes the non-degeneracy check for the maximal-forcing stack: a single certified closure exhibits all three trichotomy branches with proofs, ruling out a secretly always-Forced or always-Independent classifier. That matches the module claim that Selected is a real interim tag with an explicit drainage path (positivity promoting $L_{\mathrm{golden}}$ to the Forced is-$\varphi$ result), not a dumping ground.
In the broader Recognition forcing chain this sits under foundation-level reality closure rather than a numbered T0–T8 step; it underwrites that later Forced results (J-uniqueness, $\varphi$, eight-tick, $D=3$) and Independent ones (yardstick) are classified by a machinery that can also host Selected claims. No downstream consumers are wired yet; the declaration is the completeness witness for the example universe itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.