not_HKTRigidityModVacuumStatementN2
plain-language theorem explainer
Mod-vacuum CanonicalMom rigidity at n=2 is false: a variable-kinetic vacuum Hamiltonian density cannot be forced into rigid ADM shape with field-independent kinetic weight plus vacuum potential. Gap-5 auditors cite it as the kill of the repaired (mod-vacuum) rigidity claim. The proof instantiates the claim on a vacuum-kinetic counterexample, specializes the density identity at two momenta, and obtains the contradiction 1 = 1/2.
Claim. It is not the case that every $n=2$ Hamiltonian density in the mod-vacuum CanonicalMom class admits constants $c_{\mathrm{kin}},c_{\mathrm{grad}},c_{\mathrm{mom}}$ and a vacuum potential $V:\mathbb{R}\to\mathbb{R}$ putting the density into the rigid form $c_{\mathrm{kin}}\,p^2 + c_{\mathrm{grad}}(\text{grad term}) + V(q)$ with the CanonicalMom relation $c_{\mathrm{mom}}=4 c_{\mathrm{kin}} c_{\mathrm{grad}}$.
background
Local setting is Wave C4/C5 of the gravity seven-gaps program: after plain CanonicalMom rigidity was killed by a vacuum shift, a repaired claim restricted to mod-vacuum targets (constant vacuum sector $V\equiv 0$ allowed, but kinetic weight still forced field-independent). This module closes that repair negatively and then opens the kinetic-normalized terminal.
The counterexample is the vacuum-kinetic CanonicalMom target: its local kinetic coefficient $A(q)$ is field-dependent (explicitly $A(0)=1$ and $A(1)=1/2$), with diagonal weight and Hamiltonian density built from $A(q)p^2$ plus design terms. Mod-vacuum rigidity would still demand a single constant $c_{\mathrm{kin}}$ and some $V$ reproducing that density for all phase-space points and $\mathbb{Z}/2$ labels.
Upstream arithmetic lemmas (add_zero, mul_zero, mul_one) only discharge the elementary reductions after specialization; the mathematical content is the failed rigidity shape, not those lemmas.
proof idea
Assume the mod-vacuum rigidity statement and apply it to the vacuum-kinetic CanonicalMom target, obtaining $c_{\mathrm{kin}},c_{\mathrm{grad}},c_{\mathrm{mom}},V$ and a Hamiltonian-density identity.
Specialize at coincident-phase kinematics with discrete label $0$. After unfolding targets and cancelling gradient/cross terms (sub_self, mul_zero, diagonal weight), the identity collapses to $A(q)p^2 = c_{\mathrm{kin}} p^2 + V(q)$ for all real $q,p$.
Set $p=0$ to force $V(q)=0$. Set $p=1$ to force $A(q)=c_{\mathrm{kin}}$ for every $q$. Evaluate at $q=0$ and $q=1$: the explicit formula for $A$ yields $c_{\mathrm{kin}}=1$ and $c_{\mathrm{kin}}=1/2$, contradiction by norm_num.
why it matters
This is Part 1 of the C4/C5 gap-5 close: the four-theorem kill tower. Downstream gap5_kill_tower_scope_certificate packages it with three sibling negations as the scope certificate that stronger unconditioned $n=2$ rigidity statements are false.
Status structures read it directly: hktKineticNormalizedRigidityStatus_flags sets modVacuumRigidityKilled = true, and HKTVacuumSectorKillStatus records the C4 kill of the mod-vacuum repaired terminal. Sibling work in HKTKineticFromRecognitionCost then uses the same vacuum-kinetic inhabitant (jet not calibrated; RCL forcing field-independent weight) to motivate the kinetic-normalized replacement path rather than raw rigidity.
In the Recognition gravity ledger this clears the false positive so gap-5 constraint recovery can flip only after the kinetic-normalized half (FTC recovery derived, not assumed) also binds green. It does not itself derive $D=3$ or the eight-tick octave; those sit upstream in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.