LocalProfileMomDensityIdentity
plain-language theorem explainer
Defines the local-profile momentum-density identity at two lattice sites: the Poisson bracket of two local Hamiltonians built from a smooth profile h and lapses N, M equals a sum of antisymmetrized lapse products times a candidate momentum density. Gravity workers attacking the HKT ham-ham coefficient reduction cite it. Pure Prop packaging; no proof content.
Claim. For a local Hamiltonian profile $h:\mathbb{R}^3\to\mathbb{R}$ with a smoothness witness $S$, and a candidate momentum density $\mu:\mathrm{PhaseSpace}(2)\to(\mathbb{Z}/2\mathbb{Z}\to\mathbb{R})$, the identity asserts that for all lapses $N,M:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$ and all phase-space points $x$, $\{H_h[N],H_h[M]\}(x)=\sum_{j\in\mathbb{Z}/2\mathbb{Z}}(N_j M_{j+1}-M_j N_{j+1})\,\mu(x)_j$, where $H_h[N]=\sum_j N_j\,h(q_j,q_{j+1},p_j)$.
background
Module Wave C2 R5/R6 groundwork fixes the local-profile functional equation at $n=2$ (mirroring HamDyn). The goal is to reduce the dynamical ham-ham bracket for local profiles to the coefficient form $\mathrm{momDensity}_j=h_b(j),h_p(j+1)$. Nothing here proves rigidity.
A local Hamiltonian profile is a map $h:\mathbb{R}\to\mathbb{R}\to\mathbb{R}\to\mathbb{R}$ of neighbouring configuration coordinates and the on-site momentum. LocalHamFromProfile builds the smeared Hamiltonian $H_hN=\sum_j N_j,h(q_j,q_{j+1},p_j)$. Smoothness packages the three partials $h_a,h_b,h_p$ together with a Fréchet derivative witness on each cell.
Phase space is the product of configuration and momentum fields on the periodic lattice $\mathbb{Z}/n\mathbb{Z}$. The Poisson bracket is the standard sum ${F,G}=\sum_i(\partial_{q_i}F,\partial_{p_i}G-\partial_{p_i}F,\partial_{q_i}G)$, with the usual caveat that nondifferentiable observables inject the junk value $0$.
proof idea
Definitional packaging only: the body is the universal quantification over lapses $N,M$ and phase-space points $x$ equating the Poisson bracket of the two profile Hamiltonians to the indicated bilinear form in $N,M$ contracted against momDensity. No tactics, no lemmas applied. Downstream theorems discharge the Prop by supplying a concrete coefficient and invoking the local-profile ham-ham form lemma.
why it matters
This Prop is the attack surface for R6 in the Seven Gaps gravity stack. The parent theorem localHamHamCoefficient_witnesses_identity shows that the concrete coefficient extracted from the smooth profile (essentially $h_b,h_p$ on neighbouring cells) satisfies the identity, via the local-profile ham-ham form computation.
In the broader Recognition Science gravity program this is the $n=2$ local-profile reduction of the hypersurface-deformation ham-ham relation. It sits downstream of the Poisson-bracket model on lattice phase space and upstream of any rigidity claim that would force the profile shape. The module doc is explicit: nothing here proves rigidity; the identity only names the coefficient that must match momentum density.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.