Tightening
plain-language theorem explainer
A tightening from admissibility class A to B witnesses that every B-admissible realization is already A-admissible (B refines A). An optional strictness proposition is carried separately so the order works before strict inclusion is known. Maximal-forcing closure and the RS universe ladders (cost, alpha, gravity, hbar) cite this as the basic refinement relation. Pure structure data: two fields, no proof obligation.
Claim. A tightening from an admissibility class $A$ to a class $B$ (same realization type $R$) is a pair: a proof that every $B$-admissible realization is $A$-admissible, together with an optional proposition used as a strictness witness.
background
Maximal forcing refuses free parameters. If a claim is not forced on the current admissible class, the next move is either to tighten admissibility by adding a deeper law, or to prove independence by countermodel. This module supplies the class machinery for that closure operator.
An admissibility class packages a set of realizations of an abstract type $R$ plus a label. $R$ may be logic realizations, costed maps, physical models, or domain structures depending on phase. A claim is forced on a class when it holds in every admissible realization.
Tightening is the refinement order on those classes: moving from $A$ to $B$ means $B$'s admissible set sits inside $A$'s. Strictness is deliberately a separate propositional field so the subset order remains usable while a non-vacuity proof is still open.
proof idea
Definitional structure, not a theorem. Two fields only: subset is the inclusion of admissible sets ($B \subseteq A$), and strict_witness is an unconstrained Prop placeholder for later strictness evidence. No tactics, no lemmas applied at the definition site. Downstream constructors fill the fields (often with a trivial subset proof and True as deferred strictness).
why it matters
This is the primitive refinement arrow for the admissible-realization lattice. ForcedAfterTightening packages nonempty tightening plus forcedness on the narrower class as the promotion target from Selected to Forced. The monotonicity lemma then shows forcedness on a wider class survives any tightening.
LegitimateTightening strengthens the same subset field with a non-vacuity witness and a named deeper-law proof, so tightenings are forced by RS theorems rather than chosen freely. Concrete RS universe ladders instantiate it: cost ($L_0$ to $L_{\mathrm{cost}}$), alpha, gravity, and $\hbar$ each build a tightening record. That is how the forcing chain narrows from open candidate classes to the RS-selected laws without conceding degrees of freedom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.