vacuumKineticHamDensity
plain-language theorem explainer
Defines the sitewise Hamiltonian density of the variable-kinetic vacuum counterexample on the two-site phase space: at lattice site j it evaluates the local profile on (q_j, q_{j+1}, π_j). Gravity and HKT-rigidity workers cite it as the concrete density that inhabits CanonicalMom yet breaks mod-vacuum shape. The body is a one-line specialization of the local profile to phase-space coordinates.
Claim. On the two-site canonical phase space $(q,\pi)\in(\mathbb{Z}/2\mathbb{Z}\to\mathbb{R})^2$, the vacuum-kinetic Hamiltonian density at site $j$ is the local profile value $A(q_j)\,\pi_j^2+W(q_j,q_{j+1})$, where $A$ and $W$ are the fixed vacuum-kinetic amplitude and interaction weight.
background
The ambient setting is Wave C4/C5 gap5: kill mod-vacuum HKT rigidity and close kinetic-normalized rigidity. Phase space on $n$ sites is the product of configuration $q:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$ and conjugate momentum $\pi:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$ on the periodic lattice; here $n=2$.
The upstream local profile is the pure function $(a,b,p)\mapsto A(a),p^2+W(a,b)$. It packages a configuration-dependent kinetic coefficient $A$ times squared momentum, plus a nearest-neighbor weight $W$. The density defined here simply feeds site $j$ and its successor into that profile.
This density is the Hamiltonian building block for the variable-kinetic CanonicalMom inhabitant used against the mod-vacuum rigidity statement on $N=2$.
proof idea
Definitional one-liner: apply the local vacuum-kinetic profile to the triple (configuration at $j$, configuration at $j+1$, momentum at $j$). No tactics; the equality to the profile is definitional (rfl downstream).
why it matters
This density is the concrete counterexample object for gap5 Part 1. Downstream it feeds differentiability of the smeared Hamiltonian, the ham-ham Poisson bracket identity, the mom-ham split, and the equality-to-local-profile lemma. Those assemble into not_HKTRigidityModVacuumStatementN2 (mod-vacuum CanonicalMom rigidity is false) and into vacuumKinetic_fails_modVacuum_hamShape, which records that the same density refuses the constant-coefficient mod-vacuum ham shape.
In the Recognition gravity ledger this is the variable-kinetic witness that forces the upgrade from bare mod-vacuum rigidity to kinetic-normalized CanonicalMom (intensivity field, FTC recovery theorem-derived). It sits inside the SevenGaps HKT chain rather than the T0-T8 forcing spine, but it is the explicit kill that lets gap5 close after both ledger halves bind green.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.