contDiff_vacuumKinetic_wTerm
plain-language theorem explainer
The vacuum kinetic W-term, read as a map on R^3 by projecting to the first two coordinates, is C^2. Anyone assembling C^2 regularity of the kinetic-normalized local profile cites this lemma. The proof unfolds the explicit polynomial and hands the goal to Mathlib's fun_prop automation; composition-based ContDiff proofs time out in whnf.
Claim. Let $W:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ be the vacuum kinetic $W$-term (the explicit degree-6 polynomial in two real variables used in the kinetic-normalized vacuum sector). Then the map $(x,y,z)\mapsto W(x,y)$ is of class $C^2$ on $\mathbb{R}^3$.
background
This module closes Wave C4/C5 gap5 in the HKT gravity sector: mod-vacuum kill plus kinetic-normalized rigidity. Part 2 introduces a kinetic-normalized canonical-momentum intensivity field whose FTC recovery is theorem-derived rather than an assumed class field.
The vacuum kinetic density splits into an $A$-factor times a squared momentum coordinate plus a residual $W$-term. The $W$-term is the explicit real polynomial $W(a,b)=a^6/24+7a^4/24-a^3b^3/6-a^3b/2+a^2b^4/8+a^2b^2/4+a^2/4-ab^3/6-ab/2+b^4/8+b^2/4$.
The ambient profile lives on triples $(a,b,p)\in\mathbb{R}^3$. ContDiff statements are therefore stated for maps out of that product, with $W$ depending only on the first two coordinates.
proof idea
One-line automation after definitional expansion. Unfold vacuumKineticW to expose the polynomial combination of powers, products, and scalar multiplications. Then fun_prop discharges $C^2$ from Mathlib's ContDiff rules for arithmetic operations on $\mathbb{R}$. The doc-comment notes that a .comp-based ContDiff proof of the two-site $W$ times out in whnf, so the direct unfold path is intentional.
why it matters
Feeds vacuumKinetic_profile_contDiff, which rewrites the local profile map as $A(a),p^2+W(a,b)$ and needs $C^2$ of each summand. That profile regularity is infrastructure for the kinetic-normalized CanonicalMom intensivity field and the theorem-derived FTC recovery on the gap5 ledger half.
In the SevenGaps gravity program this is bookkeeping, not a new physical law: it certifies that the vacuum kinetic design polynomial is smooth enough for the rigidity PDE and mean-value arguments imported from Mathlib. It sits under the C5 upgrade binding (D-gap5-acceptance-adjudication-20260723) after the mod-vacuum kill half is already green. No T0–T8 forcing step is at stake; the landmark is gap-closure hygiene in the HKT vacuum sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.