hamDynDensity
plain-language theorem explainer
Local energy density of the campaign dynamic Hamiltonian on the two-site phase space: half of kinetic momentum squared plus a configuration-weighted nearest-neighbor gradient term. Gravity workers building HKT point-split targets, smearing identities, or kinetic nondegeneracy witnesses cite it. Pure definitional unpack of the summand inside HamDyn; no proof content.
Claim. For phase-space data $(q,p)$ on $\mathbb{Z}/2\mathbb{Z}$, the dynamic Hamiltonian density at site $j$ is $\rho_H(q,p;j)=\tfrac12\bigl(p_j^2+(1+q_j^2)(q_{j+1}-q_j)^2\bigr)$. Smearing against a lapse $N$ recovers the full dynamic Hamiltonian: $\sum_j N_j\,\rho_H(q,p;j)=H_{\mathrm{Dyn}}[N](q,p)$.
background
This module repairs the Hojman–Kuchař–Teitelboim dynamic target after the unsplit momentum–Hamiltonian field proved uninhabitable for honest nearest-neighbor profiles against the frozen quadratic Hamiltonian. At $n=2$, $-1=1$ on $\mathbb{Z}/2\mathbb{Z}$, so the generator-symmetric packaging vanishes and the repaired API uses smeared point-split source/target advection densities instead.
PhaseSpace 2 is a pair of real fields on the two sites: configuration $q=x.1$ and conjugate momentum $p=x.2$. The campaign dynamic Hamiltonian HamDyn (from DynamicStructureBracket) is the $N$-weighted sum of the same local expression that this density isolates:
$$H_{\mathrm{Dyn}}N=\sum_i\frac{N_i}{2}\bigl(p_i^2+(1+q_i^2)(q_{i+1}-q_i)^2\bigr).$$
The density is that summand without the lapse factor, so Frechet calculus and pointwise nondegeneracy checks can run sitewise.
proof idea
Definitional abbreviation only: the body is the algebraic summand of HamDyn with the lapse factor stripped, evaluated at a single site $j\in\mathbb{Z}/2\mathbb{Z}$. No tactics, no lemmas. Downstream equalities such as the smearing identity recover HamDyn by funext, unfold, and ring.
why it matters
Load-bearing density for the honest HamDyn inhabitant of the repaired point-split Dyn target. It is installed as hamDensity in hamDynPointSplitTarget, and the smearing theorem identifies $\sum_j N_j,\mathrm{hamDynDensity},x,j$ with HamDyn N.
Downstream uses include: equality to the local-profile form (hamDynDensity_eq_localProfile); kinetic nondegeneracy of the total energy (hamDyn_kinetic_regular_witness, hamDynDensity_nondeg); the open unsplit advection identity UnsplitMomHamForProfileDyn (stated against this density, not the frozen quadratic); and the vacuum-sector split HamVac_eq_HamDyn_add_Vac.
In the SevenGaps gravity campaign this is the concrete energy density against which point-split HKT structure and the open HamDyn-level unsplit no-go are measured. No rigidity theorem and no ledger flag are claimed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.