forced_invariant_absorbed
plain-language theorem explainer
Any claim forced over a claim universe's admissibility can be adjoined without breaking maximal-closure classification: the extended universe still carries a complete classifier certificate, and the claim stays Forced. Researchers tracking carrier-completeness on the forced side of the maximal-forcing program would cite this. The proof is a one-line term pairing the certificate extension with the original Forced witness.
Claim. Let $P$ be a primitive and $U$ a claim universe equipped with a maximal-closure certificate. If $C_0$ is a reality claim that is Forced relative to the admissibility class of $U$, then the universe obtained by adjoining $C_0$ still admits a maximal-closure certificate for $P$, and $C_0$ remains Forced under the extended admissibility predicate.
background
The maximal-forcing program classifies every reality claim into one of three buckets: Forced, Independent, or Selected. A claim universe packages a realization type, an admissibility class, and a curated claim set. A maximal-closure certificate asserts that a complete classifier exists for that universe relative to a primitive $P$.
This module treats stability of that certificate under carrier extension. The local setting is the forced half of the carrier-completeness worry: whether the curated claim set might omit a physically real invariant that the framework would have forced. Extension of a universe by a claim $C_0$ enlarges the claim set while leaving the admissibility class and realization type untouched, so prior classifications that depend only on those data are preserved.
The Forced predicate means the claim holds for every admissible realization. The theorem uses the certificate-extension construction that rebuilds a maximal-closure certificate after adjoining a Forced claim.
proof idea
Term-mode one-liner. The goal is a conjunction: a nonempty maximal-closure certificate on the extended universe, and Forced status of $C_0$ there. The second conjunct is immediate from the hypothesis that $C_0$ is Forced over $U$, since adjoining a claim does not change the admissibility predicate. The first conjunct applies the certificate method that extends a maximal-closure certificate by a Forced claim, then wraps the result as a nonempty witness. No case analysis or rewriting is required.
why it matters
This is the precise structural answer to carrier-completeness on the Forced side of the maximal-forcing register. The module states the consequence directly: no forced invariant can ever be missing in a way that breaks the closure; any forced fact, once named, is absorbed into the Forced bucket while prior classifications are preserved. Residual incompleteness of the register, if any, can only be an undiscovered independence or selection, never an undiscovered forced invariant.
The sibling theorem on register saturation under classified extension covers all three buckets at once; this declaration isolates the Forced absorption step that fuller statement builds on. Within Recognition Science foundation work it supports the claim that the curated carrier is closed under forced facts, rather than requiring an open-ended hunt for missing slots. No downstream uses are recorded yet; the declaration stands as a foundation lemma for the closure-stability story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.