LocalHamFromProfile
plain-language theorem explainer
Smeared local Hamiltonian on the two-site lattice: sum of lapse times a three-argument density profile evaluated on neighboring configurations and on-site momentum. Gravity workers attacking the n=2 ham_ham functional equation use it as the standard packing of local profiles into a global Hamiltonian. The body is the direct finite sum over Z/2Z.
Claim. Given a local Hamiltonian profile $h:\mathbb{R}\times\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ and a lapse $N:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$, the smeared Hamiltonian at phase-space point $(q,\pi)$ is $\sum_{j\in\mathbb{Z}/2\mathbb{Z}} N(j)\, h(q_j,q_{j+1},\pi_j)$.
background
Module setting is Wave C2 R5/R6 groundwork for the local-profile functional equation at lattice size $n=2$ (mirroring HamDyn). The aim is to reduce the dynamical ham_ham identity for local profiles to a product form on momentum density; nothing in this module yet proves rigidity.
A local Hamiltonian profile is simply a map $h:\mathbb{R}^3\to\mathbb{R}$, read as depending on configuration at site $j$, configuration at the neighbor $j+1$, and conjugate momentum at $j$. Phase space at $n=2$ is the product of configuration and momentum fields on the periodic two-site lattice: $(q,\pi)$ with $q,\pi:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$.
The lapse $N$ is a real weight on the two sites. Smearing multiplies the local density by $N(j)$ and sums, producing the global Hamiltonian functional used in Poisson-bracket identities.
proof idea
Pure definition: evaluate the three-argument profile at $(q_j,q_{j+1},\pi_j)$, multiply by the lapse component $N(j)$, and sum over the two residues of $\mathbb{Z}/2\mathbb{Z}$. No lemmas, no tactics.
why it matters
Standard packing that lets every downstream n=2 rigidity argument treat a local profile as a global Hamiltonian. Downstream, hamDensity_smear_eq_LocalHamFromProfile identifies the smeared target density with this packing under a pointwise density hypothesis. profiled_ham_ham_alternating_FE and alternating_FE_of_profile derive the alternating functional equation forced by CanonicalMom ham_ham at n=2 from such profiles. vacuumKineticHam_eq_LocalHamFromProfile and ham_ham_vacuumKinetic specialize the packing to the vacuum-kinetic witness. canonicalMom_excludes_balanced_quartic uses the same profile language to rule out a strong falsifier. In the SevenGaps gravity program this is R6 attack surface: the definition itself proves nothing, but every local-profile FE and kinetic-normalized rigidity theorem routes through it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.