quarticHamDensity2
plain-language theorem explainer
Quartic kinetic density on the two-site lattice phase space: at site j the density equals the fourth power of the conjugate momentum. Model builders of the point-split HKT Hamiltonian cite it when summing weighted site densities and when constructing the zero-momentum decoy. The body is a one-line projection of the momentum coordinate raised to the fourth power.
Claim. For a phase-space point $x=(q,\pi)$ on the two-site periodic lattice and a site index $j\in\mathbb{Z}/2\mathbb{Z}$, the quartic kinetic density is $h_j(x)=\pi_j^4$.
background
The ambient 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$, so $x.2$ is the momentum field and $x.2,j$ is the value $\pi_j$ at site $j$.
This module repairs the weak point-split HKT target after an adversarial pass showed that a pure quartic zero-momentum model inhabits the weak schema. The strong class adds load-bearing momentum, Mom–Ham advection, and kinetic regularity; the quartic density is the kinetic building block used both for the honest inhabitant and for the explicit decoy that the strong gate must reject.
Upstream, the phase-space abbreviation fixes the coordinate convention used throughout the SevenGaps HKT stack. Downstream weighted sums of this density define the full Hamiltonian functional on two sites.
proof idea
Pure definition: extract the momentum component of the phase-space pair and raise the value at site $j$ to the fourth power. No lemmas or tactics; the body is the term $(x.2,j)^4$.
why it matters
Supplies the sitewise kinetic density for the two-site quartic Hamiltonian used throughout the point-split strong module and the CanonicalMom target. Downstream, the weighted sum defines the full Hamiltonian; Fréchet differentiability of that sum is proved by differentiating each site term; nondegeneracy and the zero-momentum decoy are stated directly in terms of this density. In CanonicalMom it appears inside balanced-quartic bracket identities and the weak-schema inhabitant that falsifies strong-class rigidity. Within the SevenGaps gravity stack it is the concrete kinetic model that separates the decoy (vanishing momentum) from load-bearing dynamics after the Wave C2 adjudication.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.