vacuumKineticLocalHa
plain-language theorem explainer
Defines the a-component of the vacuum kinetic local Hamiltonian density as the Fréchet derivative of the packaged three-argument profile at (a,b,p) in the direction (1,0,0). Anyone assembling the LocalHamSmooth witness for the kinetic-normalized vacuum profile cites it. The body is pure definitional packaging: no proof obligations.
Claim. Let $H_{\mathrm{vac}}(a,b,p)=A(a)\,p^{2}+W(a,b)$ be the vacuum kinetic local Hamiltonian density, packaged as a map $\mathbb{R}^{3}\to\mathbb{R}$. The $a$-partial profile is $H_{a}(a,b,p):=D\widehat{H}_{\mathrm{vac}}(a,b,p)\cdot(1,0,0)$, i.e. the directional derivative of that map in the first coordinate.
background
In the SevenGaps HKT stack a local Hamiltonian profile is simply a smooth map $H:\mathbb{R}^{3}\to\mathbb{R}$ with arguments $(a,b,p)$ (adjacent configuration coordinates and a conjugate momentum). The vacuum kinetic profile used here is $H_{\mathrm{vac}}(a,b,p)=A(a),p^{2}+W(a,b)$, with $A$ a positive kinetic prefactor and $W$ the two-site interaction term.
profileMap repackages any such $H$ as a single map on $\mathbb{R}\times\mathbb{R}\times\mathbb{R}$, so that Mathlib Fréchet calculus applies directly. The ambient module closes Wave C4/C5 gap5: after the mod-vacuum kill, the remaining work is kinetic-normalized CanonicalMom rigidity, with FTC recovery theorem-derived rather than assumed as a class field.
proof idea
Definitional one-liner. Apply Mathlib fderiv to profileMap vacuumKineticLocalProfile at the point $(a,b,p)$ in the coordinate direction $(1,0,0)$. No lemmas are invoked; the value is exactly the partial of the packaged vacuum kinetic density with respect to its first argument.
why it matters
Supplies the ha field of vacuumKineticLocalSmooth, the LocalHamSmooth structure on the vacuum kinetic profile. That structure is the differentiability half of the kinetic-normalized rigidity terminal for gap5: the companion lemma hasFDerivAt_vacuumKineticLocalCell expands the cell-wise Fréchet derivative as a linear combination of coordinate covectors weighted by $H_a$, $H_b$, and $H_p$. Together with the mod-vacuum kill half, this feeds the green binding of Gap5ConstraintCloseStatus and the flip of gap5_constraint_recovery under the C5 adjudication.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.