vacuumKineticDensity_eq_localProfile
plain-language theorem explainer
On the two-site lattice phase space, the vacuum kinetic Hamiltonian density at site j equals the local profile on configuration values at j and j+1 and momentum at j. Cite this when packaging the variable-kinetic vacuum model as a CanonicalMom inhabitant for the gap-5 mod-vacuum kill. Proof is pure definitional equality (rfl).
Claim. Let $x=(q,\pi)$ be a point of the two-site phase space $(\mathbb{Z}/2\mathbb{Z}\to\mathbb{R})\times(\mathbb{Z}/2\mathbb{Z}\to\mathbb{R})$ and let $j\in\mathbb{Z}/2\mathbb{Z}$. Then the vacuum kinetic Hamiltonian density of $x$ at site $j$ equals the local profile $A(q_j)\,\pi_j^2+W(q_j,q_{j+1})$.
background
The ambient setting is the C4/C5 gap-5 program: kill the mod-vacuum HKT rigidity claim on $N=2$ by exhibiting a variable-kinetic CanonicalMom inhabitant, then close kinetic-normalized rigidity with theorem-derived FTC recovery.
Phase space on $n$ sites is the product of configuration and conjugate momentum maps $q,\pi:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$. Here $n=2$. The local Hamiltonian profile is the quadratic-in-momentum form $A(a),p^2+W(a,b)$, with $A$ and $W$ the vacuum kinetic coefficient and interaction weight. The Hamiltonian density is defined by feeding neighboring configuration values and the on-site momentum into that profile.
Sibling definitions fix $A$ and $W$ for the vacuum kinetic model; positivity of $A$ and smoothness of the profile are handled nearby. The density identification is the bridge from those defs into the CanonicalMom structure package.
proof idea
One-line term proof by rfl. The Hamiltonian density is definitionally the local profile applied to $(q_j,q_{j+1},\pi_j)$, so the equality is by unfolding, with no algebraic rewriting or lemmas required.
why it matters
This is the density-equals-profile witness required by the CanonicalMom target for the vacuum kinetic model. Downstream, vacuumKineticCanonicalMomTarget installs the local profile bundle as ⟨profile, smoothness, this equality⟩, which is how the variable-kinetic density is shown to inhabit CanonicalMom.
That inhabitant is Part 1 of the module program: refute the mod-vacuum rigidity statement on $N=2$. Part 2 then builds kinetic-normalized CanonicalMom with theorem-derived FTC recovery rather than an assumed class field. In the SevenGaps ledger this is the gap-5 half that, once both sides bind green, flips the constraint-recovery status.
No direct T0–T8 landmark is invoked; the result is pure continuum/lattice Hamiltonian bookkeeping inside the gravity gap stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.