vacuumKineticLocalHp
plain-language theorem explainer
Defines the momentum partial of the vacuum-kinetic local Hamiltonian profile as the Fréchet derivative of that profile in the pure-p direction. Gravity and HKT-rigidity arguments cite it as the local p-coefficient in the two-site functional equation and structure-momentum identities. The body is a three-line packaging of fderiv along (0,0,1).
Claim. Let $H(a,b,p)=A(a)\,p^{2}+W(a,b)$ be the vacuum-kinetic local Hamiltonian profile. Define the momentum coefficient $H_{p}(a,b,p)$ to be the directional Fréchet derivative of $(a,b,p)\mapsto H(a,b,p)$ at $(a,b,p)$ in the direction $(0,0,1)$. Thus $H_{p}$ is again a map $\mathbb{R}^{3}\to\mathbb{R}$.
background
This module closes Wave C4/C5 gap5: a mod-vacuum kill together with kinetic-normalized rigidity for the HKT (Hamiltonian kinetic torsion) sector. Local Hamiltonian profiles are bare maps $\mathbb{R}\to\mathbb{R}\to\mathbb{R}\to\mathbb{R}$, written $H(a,b,p)$ with configuration pair $(a,b)$ and momentum $p$.
profileMap repackages such a profile as a single map $\mathbb{R}^{3}\to\mathbb{R}$, so ordinary Fréchet calculus applies. The vacuum-kinetic profile used here is $H(a,b,p)=A(a),p^{2}+W(a,b)$, a quadratic-in-$p$ density with configuration-dependent kinetic prefactor $A$ and potential $W$. The three partials $H_{a}$, $H_{b}$, $H_{p}$ are the directional derivatives of that map along the standard basis; this declaration is the pure-$p$ slot.
Those coefficients feed the two-site functional equation that tests whether a CanonicalMom inhabitant can be kinetic-normalized, and they appear in the structure-momentum density identities on the two-site phase space.
proof idea
Pure definition, not a proof. The body applies fderiv ℝ to profileMap vacuumKineticLocalProfile at the point $(a,b,p)$ in the direction $(0,0,1)$. That is exactly the partial derivative of the vacuum-kinetic profile with respect to its third (momentum) argument. No lemmas are invoked at the definition site; closed-form evaluation is deferred to the sibling identity that equates this fderiv to an explicit algebraic expression in $A$ and $p$.
why it matters
Supplies the local $p$-coefficient used throughout the kinetic-normalized rigidity half of gap5. Downstream, the functional equation vacuumKinetic_FE multiplies $H_{b}$ against $H_{p}$ on swapped sites and recovers a nonzero factor proportional to $(b-a)$; the diagonal special case is the decoy fe_diagonal_trivial ($0=0$, no constant-kinetic force). The same coefficient appears in hasFDerivAt_vacuumKineticLocalCell as the weight on the momentum coordinate, in vacuumKinetic_localCoeff_eq_structure_mom matching structure times momentum density, and in the kinetic-regularity witness and the final vacuumKinetic_not_kineticNormalized verdict.
Together with the closed-form rewrite vacuumKineticLocalHp_eq_closed, it lets the ledger flip gap5 after both the mod-vacuum kill and the kinetic-normalized rigidity halves bind. Framework role is local to the SevenGaps gravity chain rather than the T0–T8 forcing spine, but it is the concrete obstruction that rules out kinetic-normalized CanonicalMom inhabitants in this vacuum sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.