legitimateTightening_of_flip
plain-language theorem explainer
Smart constructor that turns an independence-to-forcing flip into a legitimate tightening of admissibility classes. Given a wider class where claim C is independent and a narrower class where C is forced, plus a named proved deeper law, it assembles the full legitimate-tightening record. Auditors of maximal-forcing steps cite it when recording a non-vacuous gate. Construction is direct field assembly: inclusion from the subset witness, non-vacuity from the flip lemma, law fields passed through.
Claim. Given admissibility classes $A$ and $B$ on realizations of type $R$, a reality claim $C$, a witness that every $B$-admissible realization is $A$-admissible, independence of $C$ over $A$, forcing of $C$ over $B$, and a named proved deeper law $\ell$, assemble a legitimate tightening from $A$ to $B$ whose subset field is the given inclusion, whose non-vacuity witness is derived from the independence-to-forcing flip, and whose deeper-law triple is $(\ell,\mathrm{proof},\mathrm{label})$.
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 adding a deeper law that reality must satisfy, or to prove independence by countermodel. This module supplies the admissibility-class machinery for that closure operator.
An admissibility class is a labeled set of realizations of an abstract type $R$ (logic models, costed realizations, or physical models, depending on phase). A claim is forced on a class when it holds in every admissible realization; it is independent when two admissible realizations disagree on it.
A legitimate tightening from $A$ to $B$ is more than the subset order $B\subseteq A$. It must also prove the gate is non-vacuous (some $A$-admissible realization is excluded by $B$) and carry a named, proved deeper law that justifies the added constraint, so the step is forced rather than chosen freely. The upstream lemma on non-vacuity states that an independence-to-forcing flip supplies exactly that witness: the $A$-admissible realization that fails the claim cannot be $B$-admissible once the claim is forced on $B$.
proof idea
One-line structure constructor. The subset field is the supplied inclusion $B\subseteq A$. The non-vacuity field is obtained by applying the flip lemma: independence of $C$ over $A$ plus forcing of $C$ over $B$ yields an $A$-admissible realization excluded by $B$. The three deeper-law fields (proposition, proof term, audit label) are passed through unchanged from the caller.
why it matters
In the Recognition foundation, maximal forcing is the discipline that closes free parameters only by deeper law, never by fiat. This constructor is the canonical way to record such a step: an independence-to-forcing flip plus a named theorem becomes a legitimate tightening that the audit trail can inspect.
It sits in the admissible-realization layer that feeds the closure operator for the forcing chain (T0–T8 landmarks: J-uniqueness, $\varphi$ as self-similar fixed point, eight-tick octave, $D=3$). No downstream theorem yet consumes it (used-by is empty), so it is infrastructure waiting on concrete tightenings that name actual RS laws.
Anyone building a forcing step that narrows the admissible set after proving a claim becomes forced will reach for this rather than hand-assembling the structure, keeping the deeper-law label attached for review.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.