extend_realization
plain-language theorem explainer
Extending a claim universe by any reality claim leaves the underlying realization type unchanged. Anyone working the maximal-forcing closure or classifier-stability lemmas cites this as the carrier-invariance fact. The proof is pure definitional equality (`rfl`) from the structure of the extension operator.
Claim. For any claim universe $U$ and any reality claim $C_0$ on $U$'s realization type, the realization type of the extended universe $U.extend(C_0)$ equals the realization type of $U$.
background
A claim universe packages three pieces: a realization type (the carrier of admissible worlds), an admissibility class on that carrier, and a set of reality claims. A reality claim is a labeled predicate holds on realizations; the label is audit metadata, the predicate is the mathematical content.
The module treats carrier-completeness under maximal forcing: whether omitting a physically real invariant could break the classifier. Extension of a universe by a claim $C_0$ enlarges only the claim set. By design, admissibility and the realization type stay fixed, so classification (which depends on those two) is stable under naming new forced facts.
Upstream, ClaimUniverse is the structure for one maximal-forcing pass, and RealityClaim supplies the predicate form of each claim. The present lemma isolates the realization half of that invariance.
proof idea
One-line definitional proof. The extension constructor is defined so that the Realization field of the extended universe is copied from the original; equality is therefore rfl. No lemmas are applied.
why it matters
This is the carrier half of the module's stability thesis: "ClaimClassification depends on the universe only through its admissibility class and realization type, both untouched by enlarging the claim set." Together with the companion facts on admissibility and claim-set membership, it underwrites that any forced invariant, once named, is absorbed into the Forced bucket without disturbing prior classifications.
In the broader Recognition forcing picture this closes the "missing forced invariant" worry at the framework level. The only remaining incompleteness of a register is undiscovered independence or selection, never an undiscovered forced fact. No downstream consumers are recorded yet; siblings such as extend_admissibility, extend_preserves_trichotomy, and forced_invariant_absorbed sit in the same closure package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.