hktKineticNormalizedRigidityStatus_flags
plain-language theorem explainer
Status certificate for gap-5 kinetic-normalized HKT rigidity: mod-vacuum rigidity is killed, FTC recovery is theorem-derived, every kinetic-normalized CanonicalMom target is ADM-plus-vacuum, and the gap-5 constraint-recovery flags are green. SevenGaps gravity auditors cite it when binding the C4/C5 ledger half. Proof is a seven-way conjunction of five definitional equalities plus two named lemmas.
Claim. The kinetic-normalized HKT rigidity status has all four boolean fields true (mod-vacuum rigidity killed, kinetic-normalized rigidity closed, FTC recovery derived, gap-5 constraint recovery), the full-theory benchmark field for gap-5 constraint recovery equals true, the bare mod-vacuum rigidity statement at $N=2$ is false, and the terminal proposition holds: every kinetic-normalized CanonicalMom target admits nonzero $c_{\mathrm{Kin}},c_{\mathrm{Grad}}$ with $c_{\mathrm{Mom}}=4\,c_{\mathrm{Kin}}c_{\mathrm{Grad}}$ and Hamiltonian density of ADM-plus-vacuum profile form.
background
Module Wave C4/C5 closes gap 5 of the SevenGaps gravity ledger in two halves. Half one kills bare mod-vacuum rigidity at $N=2$ by exhibiting a variable-kinetic CanonicalMom inhabitant outside the ADM-plus-vacuum class. Half two replaces that class by the stricter kinetic-normalized CanonicalMom targets and proves they are rigid.
A kinetic-normalized target is a CanonicalMom Hamiltonian density whose kinetic sector is already in the standard $p^2$ form. The terminal proposition asserts that every such target factors as $c_{\mathrm{Kin}},p_j^2 + c_{\mathrm{Grad}},W,(\Delta q)^2 + V$ with the momentum coefficient tied by $c_{\mathrm{Mom}}=4,c_{\mathrm{Kin}}c_{\mathrm{Grad}}$. Upstream, FTC recovery of the local profile is derived from intensivity plus $\mathrm{ContDiff},2$ and the CanonicalMom functional equation, not assumed as a class field. Gradient-sector recovery integrates the FE-forced $h_b$ off the diagonal.
The status record packages the four boolean ledger flags; the full-theory benchmark object is the cross-gap scoreboard whose gap-5 field this module is responsible for flipping.
proof idea
Term-mode proof: inhabit the seven-fold conjunction by a single anonymous constructor. The first five conjuncts are definitional equalities of boolean fields on the status record and on the full-theory benchmark object, each discharged by rfl. The sixth conjunct is the already-proved negation of bare mod-vacuum rigidity at $N=2$. The seventh is the already-proved theorem that the kinetic-normalized terminal proposition holds (every kinetic-normalized CanonicalMom target is ADM-plus-vacuum). No new analytic work occurs here; the declaration is a pure status binder.
why it matters
This is the terminal status binder for the C4/C5 gap-5 wave: mod-vacuum kill plus kinetic-normalized rigidity. The module doc ties it to the Codex bindings D-qg-hkt-modvacuum-verdict-20260723 and D-gap5-acceptance-adjudication-20260723. After both ledger halves bind green, ownership of the gap-5 constraint-recovery flip passes to Gap5ConstraintCloseStatus.
Upstream work that this certificate freezes includes FTC recovery from intensivity (no assumed conclusion-shaped field), gradient-sector recovery off the diagonal, the kinetic split of intensivity, and the inhabitant showing bare mod-vacuum rigidity fails. In the Recognition gravity program this is the discrete-Hamiltonian rigidity step that forces CanonicalMom targets, once kinetic-normalized, onto the ADM-plus-vacuum profile used by the continuum bridge. No downstream consumers are wired yet (used_by empty); the declaration exists so the ledger can read a single proved flag bundle rather than re-checking seven conjuncts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.