vacuumKinetic_profile_contDiff
plain-language theorem explainer
The vacuum kinetic local Hamiltonian profile, viewed as a real map on triples (a,b,p), is C². HKT kinetic-normalized rigidity proofs cite this to justify Fréchet derivatives and closed-form partials of the cell Hamiltonian. The argument rewrites the packaged profile as A(a)p² plus the polynomial W(a,b), then adds the two pre-proved ContDiff lemmas for those summands.
Claim. The map $(a,b,p)\mapsto A(a)\,p^{2}+W(a,b)$ from $\mathbb{R}^{3}$ to $\mathbb{R}$ is twice continuously differentiable, where $A(a)=(1+a^{2})^{-1}$ and $W$ is the fixed polynomial potential of the vacuum kinetic local profile.
background
This module closes Wave C4/C5 gap5 on the HKT side: a mod-vacuum kill plus kinetic-normalized rigidity. The local object is a three-argument Hamiltonian density on neighboring configuration coordinates and a conjugate momentum. The vacuum kinetic choice uses amplitude weight $A(a)=(1+a^{2})^{-1}$ times $p^{2}$, plus a fixed polynomial $W(a,b)$ in the two configuration slots.
profileMap packages any such local profile as a single map $\mathbb{R}\times\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ by reading the triple as $(a,b,p)$. Smoothness is stated in Mathlib's ContDiff at order 2, which is the regularity needed for first derivatives everywhere and for matching closed-form partials.
Upstream, the kinetic summand $A(a)p^{2}$ and the $W$ summand are already known to be $C^{2}$ as maps on triples (by composition/multiplication for $A$ and projections, and by direct fun_prop after unfolding $W$).
proof idea
Pointwise, the packaged profile equals the sum of the kinetic term $t\mapsto A(t_{1}),(t_{2,2})^{2}$ and the $W$ term $t\mapsto W(t_{1},t_{2,1})$. After a funext identity and rewrite, the claim is the sum of two maps already proved $C^{2}$: contDiff_vacuumKinetic_kinTerm and contDiff_vacuumKinetic_wTerm. ContDiff is closed under addition, so one add finishes the proof.
why it matters
This is the smoothness certificate for the vacuum kinetic local profile inside the kinetic-normalized CanonicalMom story. It discharges the local $C^{2}$ obligation (vacuumKineticLocalProfile_contDiff2) and supplies the ContDiff hypothesis used when extracting Fréchet derivatives at a phase-space point (hasFDerivAt_vacuumKineticLocalCell).
Closed-form partial identities for the $b$- and $p$-derivatives (vacuumKineticLocalHb_eq_closed, vacuumKineticLocalHp_eq_closed) start from this theorem: drop order from 2 to 1, take differentiability, and read off hasFDerivAt. That chain is how the module turns an explicit density into theorem-derived FTC recovery rather than an assumed class field, which is the C5 half of the gap5 binding after the mod-vacuum kill.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.