mem_extend_of_mem
plain-language theorem explainer
If a reality claim already sits in the closure of a claim universe, it remains in the closure after adjoining any new claim. Maximal-forcing and carrier-completeness arguments cite this when enlarging the register. The proof is a one-line appeal to set-insert membership.
Claim. Fix a primitive $P$ and a claim universe $U$. Let $C_0$ and $C$ be reality claims on the realization type of $U$. If $C$ lies in the $P$-closure of $U$, then $C$ also lies in the $P$-closure of the universe obtained by adjoining $C_0$ to $U$.
background
This module treats maximal forcing as stability of a complete classifier under carrier extension. A claim universe packages a realization type, an admissibility class, and a curated set of reality claims. The $P$-closure predicate records which claims are already registered in that set for a given primitive $P$.
Extension adjoins one new claim $C_0$ by inserting it into the claim set while leaving the realization type and admissibility class fixed. That is the only structural change: classifications and forcedness are indexed by admissibility and realization, not by the size of the claim set.
Upstream, claims are classified by a trichotomy (forced, independent with an explicit countermodel witness, or selected by a named principle). The module's goal is to show that once a complete classifier exists for $U$, adjoining a classifiable claim yields a complete classifier for the extended universe, with old claims retaining membership and classification.
proof idea
One-line wrapper. Closure membership is ordinary set membership in the curated claim set of $U$. Extension is defined by inserting $C_0$ into that set, so the standard lemma that membership is preserved under insert applies directly to the hypothesis that $C$ was already in the closure.
why it matters
This is the membership half of extension stability: old claims never fall out of the register when a new claim is named. The module doc states the structural payoff: no forced invariant can be "missing" in a way that breaks closure; once named, it is absorbed while prior classifications survive because classification depends on $U$ only through admissibility and realization, both untouched by enlarging the claim set.
Sibling constructions build on the same insert geometry: transporting a classification along extension, and rebuilding a maximal-closure certificate after adjoining a forced, independent, or selected claim. Together they answer the forced half of the carrier-completeness worry in the Recognition foundation stack (the forcing-chain setting that pins $J$, $\varphi$, the eight-tick octave, and $D=3$). The remaining barrier is producing the classification certificate itself, never re-proving that old claims still belong.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.