InClosure
plain-language theorem explainer
Membership predicate: a reality claim sits in the forcing closure of a primitive relative to a fixed claim universe. Downstream certificates and crown theorems quantify only over claims that satisfy this. The body is pure set membership in the current closure operator (presently the universe's claim set).
Claim. For a primitive $P$, a claim universe $U$, and a reality claim $C$ on the realizations of $U$, write $\mathrm{InClosure}(P,U,C)$ when $C$ belongs to the forcing closure of $P$ in $U$ (presently: when $C$ is one of the claims listed by $U$).
background
Maximal forcing packages a single pass over a chosen universe of realizations. A ClaimUniverse carries a realization type, an admissibility class, and a set of reality claims. Each reality claim is a labeled predicate on realizations; the theorem content is the holds field.
A primitive is the starting seed of the pass: either object-level distinction (exists x y, x ≠ y) or a Law-of-Logic realization after the floor is non-vacuous. The two constructors stay distinct so later modules can prove equivalence rather than identify them silently.
The module treats ForcingClosure as the execution interface for the set of claims whose status is under closure. The module doc states the program is complete only when every claim in that set is classified as forced, independent, or selected with a named principle scheduled for tightening. At present the operator simply returns the universe's claim set; later phases are expected to build it constructively from syntax or semantics.
proof idea
Definitional abbreviation, not a proof. Unfolding yields set membership of the claim in ForcingClosure P U, which itself currently equals U.claims. No lemmas or tactics are involved; downstream proofs typically discharge it by Set.mem_singleton or direct membership in the universe's claim set.
why it matters
This is the gate predicate for the entire maximal-forcing stack. ForcedInvariant packages a claim together with an InClosure witness and a forcedness proof. MaximalClosureCert requires a classifier for every claim in the closure; the conditional crown theorems maximal_forcing_closure and maximal_forcing_closure_trichotomy then conclude that every in-closure claim is Forced, Independent, or Selected.
Concrete use appears in the alpha-layer universe: isAlphaWindowClaim_in_closure places the fine-structure window claim in scope, and alphaUniverse_classifier classifies every in-closure claim there. Extension lemmas (mem_extend_of_mem, extend_preserves_trichotomy) preserve membership under universe growth. In the Recognition forcing program this is the bookkeeping hinge between the primitive seed and the T0–T8 style classification of what reality must fix.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.