extend_claims
plain-language theorem explainer
Extending a claim universe by one reality claim updates the claim set by ordinary set insertion of that claim. Anyone working the maximal-forcing closure lemmas cites this as the bookkeeping identity for the carrier. The proof is definitional reflexivity from the definition of extend.
Claim. For any claim universe $U$ and any reality claim $C_0$ on $U$'s realization type, the claim set of the universe obtained by extending $U$ with $C_0$ equals the set-theoretic insertion of $C_0$ into $U$'s claim set: $\mathrm{claims}(U\oplus C_0)=\{C_0\}\cup\mathrm{claims}(U)$.
background
A claim universe packages a realization type, an admissibility class on that type, and a set of reality claims. A reality claim is a labeled predicate on realizations: the audit label is metadata; the mathematical content is the holds predicate.
The ambient module treats maximal forcing under carrier extension. The motivating worry is that a curated claim set might omit a physically real invariant. The forced half of that worry is answered at framework level: classification is stable when the universe is enlarged by a forced claim.
Upstream, ClaimUniverse is the structure for one maximal-forcing pass (realization, admissibility, claims). Extension is the operation that adjoins one new claim while leaving realization type and admissibility untouched. This lemma isolates the pure set-level effect of that operation on the claims field.
proof idea
One-line term proof by rfl. The equality is definitional: whatever extend is defined to put in the claims field is exactly insert C0 U.claims, so the two sides reduce to the same term and reflexivity closes the goal. Marked @[simp] so downstream rewrites unfold the extended claim set automatically.
why it matters
Bookkeeping hinge for the module's closure-stability story. The module doc states that once a forced fact is named, it is absorbed into the Forced bucket while prior classifications are preserved, because classification depends on the universe only through admissibility and realization type, both untouched by enlarging the claim set.
This identity makes that absorption literal at the set level: the extended universe's claims are the old set plus the new claim, nothing more. Sibling lemmas (extend_realization, extend_admissibility, mem_extend_self, mem_extend_of_mem, extend_preserves_trichotomy, forced_invariant_absorbed) build the full stability argument on top of this field equation. No downstream consumers are recorded yet; the lemma is infrastructure inside the RSClosureExtension pass rather than a leaf cited from physics layers.
Relative to the forcing chain (T0–T8), this is meta-framework hygiene: it ensures no forced invariant can be "missing" in a way that breaks closure. Incompleteness of the register, if any, can only be undiscovered independence or selection, never an undiscovered forced fact.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.