maximal_forcing_closure
plain-language theorem explainer
Given a maximal closure certificate for a primitive and claim universe, every reality claim in the forcing closure is classified as forced, independent, or selected. Foundation workers cite this as the conditional crown of the Maximal Forcing program. The proof is a one-line projection of the certificate's classifier field; the real work is building the certificate, not asserting the crown bare.
Claim. Let $P$ be a primitive and $U$ a claim universe. If a maximal closure certificate for $(P,U)$ exists, then every reality claim $C$ on the realization of $U$ that lies in the forcing closure of $P$ and $U$ admits a claim classification: either forced (true in every admissible realization), independent (two admissible realizations disagree, with an explicit witness), or selected (by a named selection principle).
background
The Maximal Forcing Closure program packages "as forced as possible" physics as a certificate rather than a bare assertion. A claim universe carries a realization type, an admissibility predicate, and a roster of reality claims. The forcing closure of a primitive $P$ relative to $U$ is the set of those claims the forcing process reaches (InClosure).
Classification of one claim is the inductive proposition ClaimClassification: forced (holds under every admissible realization), independent (an explicit countermodel pair), or selected (a named selection principle). Upstream, that inductive lives in ForcedInvariant; claim universes and closure membership live in ForcingClosure.
This module states the exact certificate shape whose construction will be the real theorem. Once every claim in the closure is classified, the crown statement is just a projection from that certificate. The program keeps the crown deliberately conditional: build the certificate for the actual RS universe, do not postulate totality.
proof idea
One-line term proof. The structure MaximalClosureCert P U packages exactly the universal classifier
$\forall C,; \mathrm{InClosure}, P, U, C \to \mathrm{ClaimClassification}, U, C$
as its field classifies. The theorem is the projection cert.classifies, with no extra reasoning, lemmas, or case splits.
why it matters
Crown-theorem interface for Maximal Forcing. Downstream, costUniverse_classifier shows the cost-layer universe is fully classified (its single claim, the J-cost identity, is forced), discharging a transitional certificate over that thin universe. The broader program is to construct such a certificate for the full RS claim universe, tying into the forcing chain T0–T8 (J-uniqueness, $\varphi$ as self-similar fixed point, eight-tick octave, $D=3$).
The companion comment on the trichotomy form stresses that Independent and Selected are themselves proof obligations (countermodel witness; named selection principle), so the disjunction concedes no contingency lazily. Sibling maximal_forcing_closure_trichotomy restates the same fact in explicit three-way form. Open work is the real-universe certificate, not this projection.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.