gap5ConstraintCloseStatus
plain-language theorem explainer
Status record that gap-5 constraint recovery is closed: Dirac continuum half and HKT kinetic-normalized half both closed, residual open bits cleared, kill tower banked. Gravity campaign ledgers and the flags theorem cite it as the binding receipt. The body is a pure structure inhabitant with hardcoded Booleans, not a proof.
Claim. The gap-5 constraint-close status is the record with recovery flag true, continuum-algebra/HKT open flag false, HKT rigidity open flag false, packaged-target open flag false, Dirac half closed true, HKT half closed true, and kill-tower banked true.
background
Wave C5 of the Seven Gaps gravity campaign tracks whether the gap-5 residual (constraint recovery) has been closed. Gap 5 asks that the continuum Dirac algebra of hypersurface deformations, together with an HKT (Hojman–Kuchař–Teitelboim) kinetic-normalized rigidity pin, recover the Einstein constraints rather than a wider class of ultralocal theories.
The structure Gap5ConstraintCloseStatus packages seven Booleans: the full-theory recovery flip, three residual/campaign open bits that must clear, two half-closed certificates (Dirac continuum binding; Hojman pin of GR via kinetic-normalized $n=2$ rigidity), and a kill-tower bank flag. The kill tower records that stronger unconditioned $n=2$ HKT statements fail (one-site, point-split dynamical, canonical-momentum, vacuum-sector variants).
This module sits downstream of FullTheoryLedger and both named closers so ledger Bool flips cannot create import cycles. Adjudication reference: D-gap5-acceptance-adjudication-20260723.
proof idea
Definitional structure inhabitant, not a tactic proof. Each field of Gap5ConstraintCloseStatus is assigned a literal Boolean matching the adjudicated green conjunction: recovery true; the three open bits false; both halves closed true; kill tower banked true. No lemmas are applied at this site; the mathematical content lives in the upstream closers (dirac_algebra_continuum_limit, hojman_pins_general_relativity_holds) and the kill-tower counterexamples that this record merely flags as banked.
why it matters
Binding receipt that lets the full-theory and campaign ledgers flip gap-5 without cyclic imports. Downstream, gap5ConstraintCloseStatus_flags re-exports the seven equalities as a single conjunction for consumers that need a theorem rather than a def. Parent narrative: Dirac half plus HKT half yield gap5_constraint_recovery_both_halves, which is the adjudicated content behind the recovery Bool. In the RS gravity stack this closes the constraint-recovery residual on the path from discrete recognition dynamics toward continuum GR (ADM/HKT shape rigidity at $n=2$), while the banked kill tower scopes the claim so no stronger unconditioned $n=2$ rigidity is asserted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.