HKTKineticNormalizedRigidityStatus
plain-language theorem explainer
Status ledger for the C4/C5 gap5 terminal on Holst–Kibble–Thiemann kinetic rigidity. It packages four booleans: mod-vacuum rigidity killed, kinetic-normalized rigidity closed, FTC recovery derived (not assumed), and gap5 constraint recovery. Gravity auditors cite it when reading the green ledger flip. The declaration is a plain structure; the inhabited value sets every flag true.
Claim. A status record with four boolean fields: (i) whether the mod-vacuum rigidity claim has been killed by a variable-kinetic counterexample; (ii) whether kinetic-normalized canonical-momentum rigidity is closed; (iii) whether fundamental-theorem-of-calculus recovery is theorem-derived rather than an assumed class field; (iv) whether the gap5 constraint-recovery flag is green.
background
This module closes Wave C4/C5 gap5 in the HKT (Holst–Kibble–Thiemann) gravity sector: first kill mod-vacuum rigidity by exhibiting a variable-kinetic CanonicalMom inhabitant, then lock the kinetic-normalized intensivity class.
Kinetic-normalized canonical momentum means a local Hamiltonian profile $h$ with a $C^2$ smooth witness $S$ and a nonzero constant $c_{\mathrm{Kin}}$ such that the momentum slot satisfies $S.h_p(a,b,p)=2 c_{\mathrm{Kin}} p$ (ultralocal intensivity) and the target Hamiltonian density is assembled from $h$. The older assumed ftc_recovery field is discharged as a derived theorem once that normalization holds.
The vacuum kinetic profile is deliberately not of that form: its $A$-factor is nonconstant ($A(0)=1$, $A(1)=1/2$), so it cannot inhabit the normalized class. That exclusion is the load-bearing counterexample behind the first flag.
proof idea
No proof body: this is a four-field structure definition (boolean ledger type). Downstream, a single definition inhabits it by setting every field to true, recording that the mod-vacuum kill, kinetic-normalized closure, derived FTC recovery, and gap5 constraint recovery have all been established in the surrounding module.
why it matters
Gap5 is the kinetic half of the SevenGaps gravity ledger. The module binding notes (D-qg-hkt-modvacuum-verdict-20260723, D-gap5-acceptance-adjudication-20260723) require both: (1) $\neg$ mod-vacuum rigidity via the variable-kinetic inhabitant, and (2) closure of the kinetic-normalized class with FTC recovery theorem-derived rather than postulated.
The concrete value hktKineticNormalizedRigidityStatus sets all four flags true, so parent gap-close status objects can flip gap5_constraint_recovery once the companion ledger half is also green. Without this status type, the C5 adjudication has nowhere to record the terminal verdict.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.