extend_admissibility
plain-language theorem explainer
Extending a claim universe by any reality claim leaves its admissibility class definitionally unchanged. Maximal-forcing and register-closure arguments cite this to know classifications still see the same admissible class after naming a new claim. The proof is pure reflexivity from the definition of extension.
Claim. For any claim universe $U$ and any reality claim $C_0$ on the realization type of $U$, the admissibility class of the universe obtained by adjoining $C_0$ equals the admissibility class of $U$: $(U.\mathrm{extend}\, C_0).\mathrm{admissibility} = U.\mathrm{admissibility}$.
background
A claim universe packages one realization type, an admissibility class on that type, and a set of reality claims (each a labeled predicate on realizations). A reality claim is forced on an admissibility class when it holds in every admissible realization.
This module treats closure stability under carrier extension: the worry that a curated claim set might omit a physically real invariant. The forced half of that worry is answered at framework level: adjoining a forced claim yields again a complete classifier, with the new claim marked Forced, while prior classifications stay intact.
Classification depends on the universe only through its admissibility class and realization type. Extension enlarges the claim set; it is designed not to touch those two fields. This lemma records the admissibility half of that design.
proof idea
One-line wrapper: the goal is definitional equality, discharged by rfl. By construction, extend rebuilds the claim universe with the same realization type and the same admissibility class, only the claim set enlarged by $C_0$. No lemmas are applied.
why it matters
Module doc states the structural consequence: no forced invariant can be "missing" in a way that breaks closure, because any forced fact, once named, is absorbed into Forced while every prior classification is preserved verbatim. That preservation rests on admissibility (and realization type) being untouched when the claim set grows.
This simp fact is the admissibility leg of that invariance. Sibling results in the same file handle realization, claim-set membership, trichotomy preservation, and absorption of forced invariants. Together they underwrite the register claim that incompleteness, if any, can only be undiscovered independence or selection, never an undiscovered forced invariant.
No downstream uses are recorded yet; the lemma is infrastructure for the maximal-forcing closure narrative rather than a leaf physics identity (T5–T8, RCL, mass ladder).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.