vacuumKineticLocalHb
plain-language theorem explainer
The b-partial of the vacuum kinetic local Hamiltonian density is the Fréchet derivative of the packaged profile map in the (0,1,0) direction. HKT rigidity and gap-5 workers cite it when building the local functional equation, the cell-wise derivative, and the smooth local structure. The body is a one-line directional derivative of the vacuum kinetic profile; closed form is proved separately.
Claim. Define the local $b$-coefficient of the vacuum kinetic Hamiltonian profile by $H_b(a,b,p) := D_{(a,b,p)}\Phi\cdot(0,1,0)$, where $\Phi:\mathbb{R}^3\to\mathbb{R}$ packages the vacuum kinetic local profile $H(a,b,p)=A(a)\,p^2+W(a,b)$ as a map on $(a,b,p)$.
background
Wave C4/C5 gap5 studies kinetic-normalized rigidity after a mod-vacuum kill. A local Hamiltonian profile is a map $H:\mathbb{R}\to\mathbb{R}\to\mathbb{R}\to\mathbb{R}$ in coordinates $(a,b,p)$: neighboring configuration values and a momentum. The vacuum kinetic profile used here is $H(a,b,p)=A(a),p^2+W(a,b)$, with positive kinetic prefactor $A$ and interaction weight $W$.
The packaging map sends any such profile to $\Phi:\mathbb{R}\times\mathbb{R}\times\mathbb{R}\to\mathbb{R}$, $\Phi(a,b,p)=H(a,b,p)$, so Mathlib Fréchet calculus applies. Directional derivatives of $\Phi$ supply the local coefficients $H_a$, $H_b$, $H_p$ that enter the cell-wise derivative on two-site phase space and the local functional equation for the vacuum kinetic model.
proof idea
One-line definition: evaluate the Fréchet derivative of the packaged vacuum kinetic profile at $(a,b,p)$ on the unit vector $(0,1,0)$. That is $\partial H/\partial b$ whenever the profile is $C^1$. No lemmas fire at the definition site; identification with an explicit closed form is deferred to the companion equality theorem for this coefficient.
why it matters
This coefficient is the middle leg of the local smooth structure for the vacuum kinetic profile, which supplies the cell Fréchet derivative on two-site phase space. It appears in the vacuum kinetic functional equation (the off-diagonal identity relating $H_b$ and $H_p$), in the structure-momentum coefficient match, and in the diagonal decoy that the FE collapses to $0=0$ when $a=b$ (so constant kinetic is not forced on the diagonal). Together these support the kinetic-normalized half of gap5 after the mod-vacuum kill, under the C5 acceptance binding for the HKT rigidity terminal.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.