forced_of_forced_under_tightening
plain-language theorem explainer
A reality claim forced on a wider admissibility class stays forced after any tightening to a narrower class. Maximal-forcing arguments cite this when a deeper law shrinks the admissible set and previously forced content must be retained. The proof is a one-line subset transfer: every B-admissible realization is A-admissible, so the original forcing hypothesis applies unchanged.
Claim. Let $A$ and $B$ be admissibility classes of realizations of type $R$, and let $C$ be a reality claim on $R$. If $B$ is a tightening of $A$ (every $B$-admissible realization is $A$-admissible) and $C$ is forced on the admissible set of $A$, then $C$ is forced on the admissible set of $B$.
background
Maximal forcing never leaves a free parameter idle. When a claim is not yet forced on the current admissible class, the next move is either to tighten admissibility by adding a deeper law, or to exhibit independence by countermodel. This module supplies the admissibility-class machinery for that closure operator.
An admissibility class packages a set of realizations of an abstract type $R$ (logic models, costed realizations, physical models, etc.) with a label. A tightening from $A$ to $B$ is a subset witness: every $B$-admissible realization is $A$-admissible, with an optional strictness field kept separate so the order remains usable before strictness is known.
Forcing of a reality claim on a set means every realization in that set satisfies the claim. The present lemma is the elementary monotonicity of that predicate under shrinking the admissible set.
proof idea
Term-style tactic proof in two steps. Introduce an arbitrary $B$-admissible realization $r$. Apply the tightening's subset field to place $r$ in $A$'s admissible set, then discharge the goal by the hypothesis that $C$ is already forced on $A$. No auxiliary lemmas are required; the argument is pure set inclusion.
why it matters
This is the retention half of the maximal-forcing step: when admissibility is tightened by a deeper law, every claim already forced on the wider class remains forced on the narrower one. Sibling definitions (ForcedAfterTightening, tightening_does_work, LegitimateTightening) build the promotion path from Selected to Forced and the obligation that a tightening do real work rather than free selection.
In the Recognition Science forcing chain, this supports the discipline that degrees of freedom are closed only by law, not by choice (the same stance that drives T5 J-uniqueness through T8 dimension forcing). No downstream consumers are wired yet (used_by is empty); the lemma is infrastructure for the closure operator rather than a leaf physics identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.