extend_preserves_trichotomy
plain-language theorem explainer
Extending a claim universe by any forced invariant preserves the Forced/Independent/Selected trichotomy on the forcing closure. Cite this for maximal-forcing stability under carrier extension on the forced side. The proof is a one-line application of the base trichotomy theorem to the extended maximal-closure certificate obtained by adjoining the forced claim.
Claim. Let $P$ be a primitive and $U$ a claim universe with a maximal-closure certificate. If $C_0$ is forced relative to $U$'s admissibility class, then every claim $C$ in the forcing closure of the extended universe $U[C_0]$ is either forced, independent, or selected relative to the extended admissibility class.
background
A claim universe packages a realization type, an admissibility class, and a set of reality claims. The forcing closure of a primitive $P$ relative to $U$ is the set of claims in scope for maximal classification (InClosure). A maximal-closure certificate asserts that every claim in that closure falls into one of Forced, Independent, or Selected under $U$'s admissibility.
This module treats the forced half of the carrier-completeness worry: that a curated claim set might omit a physically real invariant. The structural answer is that adjoining any forced claim $C_0$ yields an extended universe that again admits a complete classifier. Classifications depend on the universe only through admissibility and realization type, both preserved in the relevant sense when the claim set is enlarged by a forced fact.
Upstream, ClaimUniverse is the carrier structure and InClosure is membership in the forcing closure. The base trichotomy on a maximal-closure certificate is what gets re-applied after extension.
proof idea
One-line term proof. From the certificate cert for $(P,U)$ and the hypothesis that $C_0$ is Forced, cert.extendForced hC0 builds a maximal-closure certificate for the extended universe. The base lemma maximal_forcing_closure_trichotomy is applied to that extended certificate, the claim $C$, and the membership hypothesis $hC$. No fresh case split is performed here.
why it matters
This is the trichotomy half of forced-side closure stability in Maximal Forcing. Paired with absorption of the forced claim itself (the sibling that places $C_0$ in Forced after extension), it answers the carrier-completeness worry for forced invariants: no forced fact can be missing in a way that breaks the classifier. The module states the consequence directly: register incompleteness, if any, can only be an undiscovered independence or selection, never an undiscovered forced invariant.
In the Recognition Science stack this is meta-level claim classification rather than a T0–T8 physical forcing step, but it underwrites that the RS register can absorb forced structure without reopening the trichotomy. No downstream uses are recorded yet; natural consumers are the sibling absorption and register-saturation results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.