localHamHamCoefficient
plain-language theorem explainer
The local ham-ham coefficient at lattice site j is the product of the neighbor-q partial of the cell Hamiltonian at j with the momentum partial at the next site. Gravity workers deriving the n=2 Poisson-bracket functional equation for local Hamiltonian profiles cite this as the explicit density factor. Pure definition: multiply the two Fréchet coefficients from the smoothness package.
Claim. Given a local cell Hamiltonian profile $h:\mathbb{R}^3\to\mathbb{R}$ with Fréchet data $(h_a,h_b,h_p)$, and a phase-space point $(q,\pi)$ on the two-site lattice, the local ham-ham coefficient at site $j\in\mathbb{Z}/2\mathbb{Z}$ is $h_b(q_j,q_{j+1},\pi_j)\,h_p(q_{j+1},q_{j+2},\pi_{j+1})$.
background
The module is Wave C2 R5/R6 groundwork for the local-profile functional equation at lattice size $n=2$, mirroring the dynamical Hamiltonian sector. A local Hamiltonian profile is a map $h:\mathbb{R}\to\mathbb{R}\to\mathbb{R}\to\mathbb{R}$ assigning to neighboring configurations $q_j$, $q_{j+1}$ and momentum $\pi_j$ the cell energy density. Smoothness packages the three partials $h_a$, $h_b$, $h_p$ together with the Fréchet derivative identity on each cell.
Phase space on $n$ sites is the product of configuration and conjugate-momentum maps $\mathrm{ZMod},n\to\mathbb{R}$. The Poisson bracket of two smeared local Hamiltonians (lapses $N$ and $M$) expands into an alternating sum whose density factor is this coefficient: $\mathrm{momDensity}_j=h_b(j)\cdot h_p(j+1)$. The module reduces Dyn ham_ham for local profiles to that identity; it does not prove rigidity.
proof idea
Definition by direct product. Read the neighbor-$q$ partial $h_b$ of the smoothness package at cell $j$ (arguments $q_j$, $q_{j+1}$, $\pi_j$) and the momentum partial $h_p$ at the shifted cell $j+1$ (arguments $q_{j+1}$, $q_{j+2}$, $\pi_{j+1}$); multiply. No lemmas are applied.
why it matters
This coefficient is the density in the local-profile ham-ham form: the Poisson bracket of two profile-smeared Hamiltonians equals $\sum_j(N_j M_{j+1}-M_j N_{j+1})$ times the coefficient. That identity is re-exported as the witness that the coefficient satisfies the local-profile momentum-density identity, and is the rewrite step inside the alternating functional equation forced by CanonicalMom ham_ham at $n=2$.
Downstream, the profiled alternating FE and the fixed-profile variant instantiate lapses as $\delta_0/\delta_1$ and extract the two-point relation $h_b(a,b,p),h_p(b,a,r)-h_b(b,a,r),h_p(a,b,p)=\cdots$. The kinetic-normalized path uses the same alternating structure. Module doc is explicit: R6 attack surface; nothing here proves rigidity. Scaffolding for the SevenGaps gravity chain, not a T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.