LocalProfileHamHamFormGeneral
plain-language theorem explainer
Packages, for any lattice size n≥1, the Poisson-bracket identity that local Hamiltonian profiles must satisfy: the bracket of two N- and M-weighted cell sums of a profile h equals a cyclic sum of (N_j M_{j+1}-M_j N_{j+1}) times a product of two auxiliary profiles h_b and h_p on neighboring cells. Gravity workers attacking the HKT local functional equation (R6) cite this Prop as the general-n target shape. It is a pure definition, not a proof.
Claim. For $n\ge 1$, a local Hamiltonian profile $h:\mathbb{R}^3\to\mathbb{R}$, and auxiliary profiles $h_b,h_p$, the following holds: for all weight functions $N,M:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$ and all phase-space points $x=(q,\pi)$, the Poisson bracket of the two observables $y\mapsto\sum_j N_j\,h(q_j,q_{j+1},\pi_j)$ and $y\mapsto\sum_j M_j\,h(q_j,q_{j+1},\pi_j)$ equals $\sum_j(N_j M_{j+1}-M_j N_{j+1})\,h_b(q_j,q_{j+1},\pi_j)\,h_p(q_{j+1},q_{j+2},\pi_{j+1})$.
background
The module supplies Wave C2 groundwork for the local-profile functional equation on the periodic lattice, landed first at $n=2$ (mirroring HamDyn). The goal is to reduce the dynamical ham–ham bracket identity for local profiles to the momentum-density factorization $\mathrm{momDensity}_j=h_b(j),h_p(j+1)$. That is the R6 attack surface; the module itself proves no rigidity.
A local Hamiltonian profile is simply a real function of three arguments $(q_j,q_{j+1},\pi_j)$. Phase space is the product of configuration and conjugate momentum fields on $\mathbb{Z}/n\mathbb{Z}$. The Poisson bracket is the standard lattice sum ${F,G}(x)=\sum_i(\partial_{q_i}F,\partial_{\pi_i}G-\partial_{\pi_i}F,\partial_{q_i}G)$, with the usual caveat that nondifferentiable observables inject the junk value $0$ from fderiv.
The $n=2$ theorem already proved in this file is the concrete instance; the present declaration only packages the same shape for general $n$.
proof idea
No proof: the declaration is a Prop-valued definition. It literally writes the universal quantification over weight functions $N,M$ and phase-space points $x$, equating the Poisson bracket of the two $h$-weighted cell sums to the cyclic structure-constant sum involving $h_b$ and $h_p$. The body is the statement itself, not a derivation.
why it matters
In the Seven Gaps gravity program this Prop is the general-$n$ packaging of the local ham–ham functional equation that R6 must eventually discharge. The module doc states the reduction target: Dyn ham_ham for local profiles collapses to $\mathrm{momDensity}_j=h_b(j),h_p(j+1)$. The proved $n=2$ form sits immediately above; this definition freezes the same algebraic shape so later lattice-size generalizations can cite one name.
No downstream theorems yet use it (used_by is empty). It does not itself force uniqueness of $h$, $h_b$, or $h_p$, nor does it touch the Recognition forcing chain (T5–T8) or the global constants. It is scaffolding for the HKT local analysis, not a closed physical claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.