LegitimateTightening
plain-language theorem explainer
A legitimate tightening from admissibility class A to B is a proper subset refinement of realizations, justified by a named, proved deeper Recognition Science law rather than an arbitrary cut. Maximal-forcing closure work cites it when promoting Selected claims to Forced after the gate actually excludes something. The structure packages inclusion, a non-vacuity witness, and a discharged deeper-law proof (replacing a stored True).
Claim. A legitimate tightening from admissibility class $A$ to class $B$ (on an abstract realization type $R$) consists of: (i) every $B$-admissible realization is $A$-admissible; (ii) there exists an $A$-admissible realization excluded by $B$; (iii) a named proposition (the deeper law) together with a proof of that proposition. Every such object forgets to an ordinary tightening by using the deeper law as the strictness witness.
background
Maximal forcing, in this module, 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 reality must satisfy, or to prove independence by countermodel. An admissibility class is a labeled set of realizations of an abstract type $R$ (logic models, costed models, physical models, etc.).
A plain tightening from $A$ to $B$ is only the subset relation $B.admissible \subseteq A.admissible$, with an optional strictness witness proposition. That witness can be the trivial True, so ordinary tightening does not yet certify that the cut is forced or non-vacuous.
Legitimacy upgrades the witness: the cut must exclude at least one formerly admissible realization, and the justification must be an actual proved deeper law with an audit label. The conversion to ordinary tightening stores that deeper law as the strictness witness.
proof idea
This is a structure definition, not a proved theorem. The fields are the mathematical content: subset inclusion, an existential non-vacuity witness (does_work), a proposition deeper_law with its proof, and a string label for audits.
The companion forgetful map toTightening is a one-line field packing: copy subset, and set strict_witness to the stored deeper law. No lemmas are applied; the point is to replace strict_witness := True with a discharged obligation.
why it matters
In the Recognition forcing workflow, tightening is how independence becomes force: add a deeper law, shrink the admissible class, then re-check the claim. Legitimate tightening is the audited form of that step, so the gate is neither vacuous nor free choice.
The sole immediate consumer is the smart constructor legitimateTightening_of_flip, which builds one from a genuine independence-to-forcing flip plus a named proved law. That sits inside the admissibility-class machinery for the maximal-forcing closure operator (module doc): either tighten by a deeper law or exhibit a countermodel.
Framework-wise this is infrastructure for the T0–T8 forcing chain style of argument (J-uniqueness, $\varphi$, eight-tick octave, $D=3$), not a physics identity itself. It records that each admissibility cut carries a discharged RS theorem, not a placeholder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.