maximal_forcing_closure_trichotomy
plain-language theorem explainer
Given a maximal-closure certificate for a primitive and claim universe, every claim in the forcing closure is Forced, Independent, or Selected under the universe's admissibility. Anyone citing the crown "as forced as possible" disjunction uses this form. The proof is a three-way case split on the certificate's classifier, packaging an independence witness into Independent.
Claim. Let $P$ be a primitive and $U$ a claim universe. Suppose a maximal-closure certificate exists for $(P,U)$: a classifier that assigns every claim $C$ in the forcing closure of $P$ in $U$ a claim classification. Then for every such $C$, either $C$ is forced by $U$'s admissibility, or $C$ is independent of that admissibility, or $C$ is selected by a named selection principle under that admissibility.
background
Maximal Forcing packages Recognition Science's "force everything that can be forced" program as a certificate, not a bare assertion. A claim universe $U$ carries a realization type, an admissibility class, and a set of reality claims. The forcing closure of a primitive $P$ in $U$ is the set of claims in scope for that pass; membership is written $\mathrm{InClosure},P,U,C$.
A maximal-closure certificate is a structure whose sole field is a total classifier: every claim in the closure receives a claim classification (forced, independent-via-witness, or selected). The module doc states the program goal as $\forall C\in\mathrm{ForcingClosure},P,U,,\mathrm{ClaimClassification},U,C$, with the crown theorem a projection once a real classifier is built.
Forced, Independent, and Selected are proof-carrying statuses under the universe's admissibility predicate. Independent is not a residual "maybe": it requires an explicit countermodel witness (via the independence-witness packaging lemma). Selected requires a named selection principle. The trichotomy therefore concedes no lazy contingency.
proof idea
Term-mode case analysis on the certificate. Apply cert.classifies C hC to obtain a three-way disjunction. The Forced branch injects left. The witness branch is rewritten by independent_of_witness into Independent, then injected as the middle disjunct. The Selected branch injects right. No further arithmetic or forcing lemmas are needed; the certificate already did the classification work.
why it matters
This is the crown theorem in exact disjunction form for the Maximal Forcing Closure program: the literal "as forced as possible" statement. Downstream, extend_preserves_trichotomy lifts it through universe extension by a forced invariant (new forced claim lands in Forced; prior classifications persist). The mass-ladder specialization massUniverse_trichotomy is a one-line application to the mass-ladder universe under the law-of-logic primitive, where the closure splits into one forced invariant and one independent coordinate with Selected empty.
In the broader RS forcing chain (T0–T8), this sits at the meta-level: it does not itself force $\phi$, the eight-tick octave, or $D=3$, but it is the interface that turns a concrete classifier for a claim universe into a total Forced/Independent/Selected accounting. The open work is constructing MaximalClosureCert instances for the real RS claim universes, not postulating the trichotomy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.