ForcedAfterTightening
plain-language theorem explainer
Predicate recording that a reality claim is forced on a tightened admissibility class: some tightening from A to B exists, and the claim holds on every B-admissible realization. Maximal-forcing and closure-operator work cites it as the promotion target from Selected to Forced. Body is a two-conjunct Prop abbreviation, not a proved theorem.
Claim. For admissibility classes $A,B$ on a realization type $R$ and a reality claim $C$, say $C$ is forced after tightening from $A$ to $B$ when there exists a tightening $A\to B$ (every $B$-admissible realization is $A$-admissible) and $C$ holds in every realization in the admissible set of $B$.
background
Maximal forcing refuses to leave free parameters idle. If a claim is not forced on the current admissible class, the next move is either to tighten admissibility by imposing a deeper law reality must satisfy, or to prove independence by countermodel. This module supplies the admissibility-class machinery for that closure operator.
An admissibility class on an abstract realization type $R$ is a labeled set of allowed realizations; $R$ may later be instantiated by strict logic models, costed realizations, or physical structures. A tightening from $A$ to $B$ is a witness that every $B$-admissible realization is already $A$-admissible (with an optional strictness field kept separate so the order remains usable before strictness is known). Upstream, a claim is forced on an admissible set precisely when it holds in every member of that set.
proof idea
Definitional abbreviation, not a proof. The predicate is the conjunction of two Props: nonemptiness of the type of tightenings from $A$ to $B$, and the primitive forcedness predicate applied to $B$'s admissible set and the claim $C$. No tactics, no lemmas discharged.
why it matters
Gives the typed promotion target in the maximal-forcing admissible-realization layer: once a tightening $A\to B$ is exhibited and the claim is forced on $B$, the claim is a candidate to move from Selected to Forced. The module doc frames this as the non-lazy branch of the closure operator (tighten, or prove independence). No downstream consumers are registered yet, so the declaration is infrastructure rather than a leaf theorem. It supports the broader forcing program (T0–T8 style uniqueness of laws) by naming the intermediate state after a deeper admissibility constraint is imposed, without yet committing to a concrete physical law or dimension count.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.