tightening_does_work
plain-language theorem explainer
If a reality claim is independent over a wider admissibility class but forced over a narrower one, some wider-admissible realization is excluded by the narrower class. Maximal-forcing auditors cite this to certify that a tightening is non-vacuous rather than a no-op. The proof unpacks the independence countermodel and feeds it to the forcing hypothesis.
Claim. Let $A$ and $B$ be admissibility classes of realizations of type $R$, and let $C$ be a reality claim on $R$. If $C$ is independent over the admissible set of $A$ and forced over the admissible set of $B$, then there exists a realization $r\in R$ that is $A$-admissible and not $B$-admissible.
background
Maximal forcing never leaves a free parameter idle: if a claim is not forced on the current admissible class, the next move is either to tighten admissibility by a deeper law, or to prove independence by countermodel. This module supplies the admissibility-class machinery for that closure operator.
An admissibility class packages a set of allowed realizations of an abstract type $R$ (logical models, costed structures, or physical models) together with an audit label. Tightening from $A$ to $B$ means every $B$-admissible realization is $A$-admissible; non-vacuity of that cut is a separate obligation.
Independence of a claim $C$ over a set means both a satisfying and a failing admissible realization exist. Forcing means every admissible realization satisfies $C$. The doc-comment states the bridge: if $C$ is independent over $A$ but forced over $B$, the $A$-admissible failure of $C$ cannot be $B$-admissible.
proof idea
Term-mode, two steps. Unpack the independence hypothesis: it yields (among other data) an $A$-admissible realization $r_1$ that fails the claim $C$. Suppose for contradiction $r_1$ were $B$-admissible. Forcing of $C$ over $B$ would then imply $C$ holds at $r_1$, contradicting the independence witness. Therefore $r_1$ is $A$-admissible and not $B$-admissible. No external lemmas are required beyond the meanings of Independent and Forced.
why it matters
Legitimate tightenings in this module must carry a discharged non-vacuity proof, not a stored triviality. Downstream, the smart constructor legitimateTightening_of_flip builds a LegitimateTightening from a subset relation, an independence-to-forcing flip, and a named deeper-law certificate; its does_work field is exactly the existence proved here.
That design matches the module thesis: every added gate must both be justified by a deeper RS law and actually shrink the admissible set. In the broader forcing chain (T0–T8), this is the local certificate that a step from a wider class to a narrower one is a real cut, not a relabeling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.