ForcingClosure
plain-language theorem explainer
For a forcing primitive and a claim universe, the forcing closure is the set of reality claims whose forced/independent/selected status is under classification. It is the execution interface for one maximal-forcing pass: today it simply exposes the universe's claim set. Downstream membership (`InClosure`) and any later constructive closure from syntax or semantics cite this definition.
Claim. Given a primitive $P$ (object-level distinction, or law-of-logic after a non-vacuous floor) and a claim universe $U$ (realization type, admissibility class, and a set of reality claims), the forcing closure of $P$ in $U$ is the set of reality claims on $U$'s realization that are currently targeted for status classification. At present this equals the claim set of $U$.
background
Maximal forcing aims to classify every reality claim relative to a primitive starting point: forced, independent, or selected by a named principle scheduled for tightening. A claim universe packages one pass: a realization type, an admissibility class on that type, and a set of reality claims about those realizations.
Primitives are kept as two constructors (object-level distinction versus law-of-logic) so later modules can prove equivalence rather than identify them silently. Reality claims are the propositions whose status the closure is meant to settle.
The module treats the closure as an execution interface. Later phases are expected to build the claim set constructively from syntax or semantics; the present definition only names the set being closed.
proof idea
Definitional, not a proof. The primitive argument is unused (placeholder for a future constructive operator). The body is the projection that returns the claim set field of the claim universe. No lemmas are applied.
why it matters
This is the named claim set for one maximal-forcing pass. Membership in the closure is exactly InClosure, the predicate that marks a claim as in scope for classification from a given primitive.
The module program is complete only when every claim in this set is forced, independent, or selected with a named principle. The definition therefore anchors the bookkeeping layer of maximal forcing in the Foundation stack, even while the operator remains non-constructive. It does not itself invoke T5–T8, the RCL, or the mass ladder; those enter only when concrete claims inside the universe are discharged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.