register_saturated_under_classification
plain-language theorem explainer
Any maximal-closure certificate for a claim universe remains available after adjoining a claim that already carries a classification certificate (Forced, Independent, or Selected). Carrier-completeness is therefore closed under classified extension: the register cannot omit a classifiable invariant. Cited by anyone arguing that incompleteness of the curated claim set can only be undiscovered independence or selection, never a missing forced fact. Proof is a one-line term packing the certificate's classified-extension constructor.
Claim. Fix a primitive $P$ and a claim universe $U$. Suppose $U$ carries a maximal-closure certificate relative to $P$, and let $C_0$ be a reality claim on $U$'s realization type that already admits a classification certificate in $U$ (forced, independent, or selected). Then the extended universe $U$ with $C_0$ adjoined again admits a maximal-closure certificate relative to $P$.
background
Maximal forcing packages physics claims as predicates on a realization type, collected in a claim universe: a realization type, an admissibility class, and a set of reality claims (each a labeled predicate holds). A primitive is the starting seed (object-level distinction, or a law-of-logic realization). A maximal-closure certificate asserts that the curated claim set is complete for the forcing pass: every claim in scope is classified.
Classification of a single claim is trichotomous. Forced means the claim holds in every admissible realization. Independent means two admissible realizations disagree (an independence witness). Selected (in the extended classifier used here) means a named selection principle picks it. The module's local setting is closure stability under carrier extension: adjoining a new claim must not destroy an existing complete classifier.
Upstream, ClaimUniverse is the carrier, RealityClaim is the audit-facing claim structure, and the classification inductive packages the buckets. The honest worry this module answers is that the curated set might omit a physically real invariant; the forced half of that worry is already absorbed automatically once named.
proof idea
One-line term proof. The hypothesis cert is a maximal-closure certificate on $U$; h0 is a classification certificate for $C_0$ in $U$. The certificate structure exposes a classified-extension constructor (extendClassified) that, given any such classification, rebuilds a maximal-closure certificate on the extended universe $U.\mathrm{extend},C_0$. The proof is simply the nonempty packing of that constructor application: no case split on the three buckets is needed at this layer, because the constructor already covers all classified claims.
why it matters
This is the complete structural saturation statement for the register under classified extension, covering Forced, Independent, and Selected at once. The module doc frames the consequence: no forced invariant can be "missing" in a way that breaks closure; any forced fact, once named, is absorbed while prior classifications are preserved. The residual content of the maximal-forcing program is therefore never "find the missing slot," but always "produce the classification certificate for a proposed claim."
In the Recognition Science forcing chain this sits at the foundation layer that underwrites T0–T8 uniqueness arguments: once J-uniqueness, $\varphi$, the eight-tick octave, and $D=3$ are forced, they cannot leave a hole in the carrier that the framework fails to absorb. Downstream use is presently open in the graph (no used_by edges yet); the declaration is the terminal saturation lemma of the RS closure-extension module, ready for any later completeness or audit theorem that needs nonempty maximal-closure after adjoining a classified claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.