mem_extend_self
plain-language theorem explainer
Adjoining a reality claim to a claim universe places that claim in the extended forcing closure. Researchers tracking maximal-forcing register stability under carrier extension cite this membership fact. The proof is a one-line application of set-insert membership.
Claim. For any primitive $P$, claim universe $U$, and reality claim $C_0$ on the realization type of $U$, the claim $C_0$ lies in the forcing closure of $P$ relative to the universe obtained by adjoining $C_0$ to $U$.
background
A claim universe packages a realization type, an admissibility class on that type, and a set of reality claims (each a labeled predicate on realizations). The forcing closure of a primitive $P$ on such a universe is the set of claims treated as in-scope for the maximal-forcing pass; membership is written as the predicate InClosure.
Primitives are the two starting points of maximal forcing: object-level distinction, or a law-of-logic realization after the floor is non-vacuous. Extending a universe by a claim $C_0$ enlarges the claim set (classically by insert) while leaving realization type and admissibility untouched.
This module addresses carrier-completeness: whether a curated claim set can omit a physically real forced invariant. The local setting is stability of the maximal-forcing classification under extension by a forced claim.
proof idea
One-line term proof. The extended universe is built so its claim set is the old set with $C_0$ inserted. Membership of $C_0$ in that set is exactly Set.mem_insert, which discharges InClosure on the extension.
why it matters
This is the self-membership half of closure stability under carrier extension. The module doc states the structural consequence: no forced invariant can be "missing" in a way that breaks closure; once named, it is absorbed while prior classifications stay intact. Together with the sibling that old claims remain in the extended closure, it underwrites the claim that incompleteness of the register can only be undiscovered independence or selection, never an undiscovered forced fact.
No downstream dependents are recorded yet; the lemma is infrastructure for the extension theorems in the same module (preservation of trichotomy, absorption of forced invariants, saturation of the register under classification). It sits in the Foundation maximal-forcing layer rather than in the T0–T8 forcing chain, but it protects the integrity of that chain's claim register when new forced invariants are named.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.