quadraticHamDensity
plain-language theorem explainer
Defines the frozen quadratic Hamiltonian density on the two-site periodic lattice: half the sum of squared momentum and squared nearest-neighbor configuration difference at each site. Gravity and HKT-target work cite it as the local energy density against which unsplit versus point-split momentum advection is tested. The body is a direct algebraic formula on phase-space coordinates.
Claim. On the two-site phase space $(q,\pi)$ with $q,\pi:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$, the frozen quadratic Hamiltonian density at site $j$ is $\frac{1}{2}\bigl(\pi_j^2 + (q_{j+1}-q_j)^2\bigr)$.
background
The ambient setting is the Wave C2 R5 repair of the Hojman–Kuchař–Teitelboim dynamic target. The unsplit Dyn target keeps a single mom_ham field that is uninhabitable for honest nearest-neighbor local momentum profiles against a frozen quadratic Hamiltonian: at $n=2$, unsplit advection forces a singular identity when $p_0+p_1=0$. This module supplies the repaired, point-split sibling.
Phase space is the product of configuration and conjugate momentum maps on the periodic lattice: $\mathrm{PhaseSpace}(n)=( \mathbb{Z}/n\mathbb{Z}\to\mathbb{R})\times(\mathbb{Z}/n\mathbb{Z}\to\mathbb{R})$. Here $n=2$, so indices live in $\mathbb{Z}/2\mathbb{Z}$ and nearest-neighbor differences wrap around the two sites.
The density is the local integrand of the frozen quadratic Hamiltonian used throughout the SevenGaps gravity campaign: kinetic $\pi_j^2$ plus discrete gradient squared of $q$.
proof idea
Pure definition: no proof obligations. The right-hand side reads the momentum component $x.2$ and the configuration component $x.1$ at site $j$ and its successor $j+1$, squares each contribution, adds, and divides by two. Downstream lemmas unfold this formula and cancel by ring arithmetic.
why it matters
This density is the frozen energy density against which the module adjudicates unsplit versus point-split momentum sectors. Smearing it recovers the global Hamiltonian: $\sum_j N_j,\mathrm{quadraticHamDensity}(x,j)=\mathrm{Ham},N$. The unsplit advection identity UnsplitMomHamForProfile equates the Poisson bracket of a local momentum profile with $\mathrm{Ham},N$ to a weighted sum of these densities. The no-go theorem unsplit_RHS_delta0_unsplitNoGo evaluates that right-hand side on a singular witness phase point and obtains a nonzero linear form in $N$, showing unsplit advection cannot hold smoothly.
No rigidity theorem is proved here, and no ledger flag is flipped. The load-bearing repaired class is the strong point-split Dyn target; the weak schema and the unsplit Dyn target remain as falsification-adjacent records. Framework contact is the discrete hypersurface-deformation algebra underlying RS gravity, not the T0–T8 forcing chain directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.