vacuumKineticHam_eq_LocalHamFromProfile
plain-language theorem explainer
The vacuum kinetic Hamiltonian, written as a weighted sum of site densities on two-site phase space, coincides with the local Hamiltonian built from the vacuum kinetic profile. Anyone proving differentiability or Poisson-bracket identities for this kinetic model cites the equality to reuse the generic local-profile calculus. The proof is pure definitional unfolding: function extensionality plus reflexivity.
Claim. For every weight function $N:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$, the map $y\mapsto\sum_{j\in\mathbb{Z}/2\mathbb{Z}} N(j)\,\rho_{\mathrm{kin}}(y,j)$ equals the local Hamiltonian obtained by feeding the vacuum kinetic local profile into the standard profile-to-Hamiltonian constructor (with the same weights $N$).
background
The module closes Wave C4/C5 gap5 on kinetic-normalized HKT rigidity: after killing the mod-vacuum claim, one works with a kinetic-normalized canonical-momentum intensivity field whose FTC recovery is theorem-derived rather than axiomatic.
A local Hamiltonian profile is a smooth map $(a,b,p)\mapsto h(a,b,p)$ of neighboring configuration values and a momentum. The vacuum kinetic profile is $h(a,b,p)=A(a),p^{2}+W(a,b)$, with positive kinetic coefficient $A$ and interaction $W$. The associated density at site $j$ evaluates that profile on the two-site phase-space coordinates $(q_j,q_{j+1},p_j)$.
LocalHamFromProfile assembles any such profile into a global Hamiltonian by the weighted sum $\sum_j N(j),h(q_j,q_{j+1},p_j)$. The vacuum kinetic Hamiltonian is written the same way with the kinetic density; the present equality records that the two writings are identical.
proof idea
One-line definitional proof. After funext on the phase-space argument, both sides reduce by unfolding: the left-hand density is defined as the vacuum kinetic profile evaluated on neighboring coordinates, and LocalHamFromProfile is exactly the weighted sum of those evaluations. Reflexivity closes the goal; no lemmas are invoked.
why it matters
The equality is the bridge that lets the vacuum kinetic model inherit the generic local-profile toolkit instead of re-proving calculus facts by hand. Downstream, differentiable_vacuumKineticHam rewrites through it and applies differentiable_LocalHamFromProfile with the vacuum kinetic smoothness witness. The Poisson-bracket identity ham_ham_vacuumKinetic likewise treats the kinetic Hamiltonian as a local-profile Hamiltonian, obtaining the structure-dynamics form of the bracket on two-site phase space.
In the gap5 ledger this sits on the kinetic-normalized rigidity half: once the Hamiltonian is identified with a local profile object, intensivity, FTC recovery, and bracket computations become available without extra scaffolding. It does not itself discharge the mod-vacuum kill or the final Gap5ConstraintCloseStatus flip; those are sibling obligations in the same wave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.