vacuumKineticW_eq_design
plain-language theorem explainer
The expanded vacuum kinetic weight W(a,b) equals half of (1+a²) times the normalized kinetic kernel K(a,b). Gravity-gap and HKT rigidity proofs cite this to swap the polynomial form for the d=b−a design form before differentiating in the second argument. The proof is a one-line unfold-and-ring identity.
Claim. For all real $a,b$, the vacuum kinetic weight $W(a,b)$ equals $\frac12(1+a^2)\,K(a,b)$, where $K$ is the normalized kinetic kernel written in the lag $d=b-a$.
background
This module closes Wave C4/C5 gap5 on mod-vacuum kill and kinetic-normalized rigidity for the HKT vacuum sector. The local objects are two real bivariate polynomials that encode the vacuum kinetic contribution after the CanonicalMom normalization.
The weight $W(a,b)$ is the fully expanded sextic/quartic polynomial in the endpoint parameters $a$ and $b$. The kernel $K(a,b)$ is the same quantity rewritten in lag coordinates $d=b-a$: $K(a,b)=(1+a^2)d^2/2+(2a)d^3/3+d^4/4$.
The factor $\frac12(1+a^2)$ is the design prefactor that converts the lag form back to the expanded weight. Downstream derivative lemmas need this equality so they can differentiate the compact $K$-form rather than the expanded polynomial.
proof idea
One-line wrapper: unfold both definitions vacuumKineticW and vacuumKineticK, then close by the ring tactic. No external lemmas are required; the identity is pure polynomial algebra in $a$ and $b$ (equivalently in $a$ and $d=b-a$).
why it matters
Feeds hasDerivAt_vacuumKineticW_b, which rewrites the $s\mapsto W(a,s)$ map as $\frac12(1+a^2)K(a,s)$ by funext and this theorem, then differentiates the design form to obtain the closed Hamiltonian density derivative. That derivative step is part of the kinetic-normalized CanonicalMom intensivity field and the theorem-derived FTC recovery (ftc_recovery_of_normalized) in the gap5 terminal.
In the SevenGaps gravity ledger this is scaffolding for the C5 upgrade binding: after both ledger halves go green, Gap5ConstraintCloseStatus owns the flip of gap5_constraint_recovery. The identity itself is pure algebra, but it is the bridge that lets the normalized kinetic profile control vacuum-sector rigidity rather than an ad-hoc expanded weight.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.