unitStructureHamHamRHS
plain-language theorem explainer
Defines the lattice ham–ham right-hand side with structure function frozen at unity: a nearest-neighbor lapse–shift wedge times momentum density. Gravity workers comparing the classical HKT constraint algebra to the widened dynamic-structure target cite it as the unit-structure baseline. The body is an explicit finite sum; no proof content.
Claim. Given a momentum-density map $\mathrm{mom}$ from lattice phase space to site values, site functions $N,M:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$, and a phase-space point $x$, set $\mathrm{RHS}_{\mathrm{unit}}(\mathrm{mom},N,M,x)=\sum_{j}(N_j M_{j+1}-M_j N_{j+1})\cdot 1\cdot \mathrm{mom}(x)_j$, summed over the periodic lattice $\mathbb{Z}/n\mathbb{Z}$.
background
The ambient setting is Wave C2 R5/R6 groundwork for a widened Hojman–Kuchař–Teitelboim (HKT) target. The classical HKT rigidity claim is false already at one site, so the module keeps an explicit structure-function slot rather than folding a constant into the momentum density and calling that GR.
Phase space here is the canonical lattice wave field: configuration $q:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$ and conjugate momentum $\pi:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$ on a periodic $n$-site ring. The ham–ham Poisson bracket of two smeared Hamiltonian constraints is expected to close on a spatial diffeomorphism generated by a wedge of the two smearing fields times a structure function; the unit case freezes that structure function at $1$.
The module records the classical unsplit advection form as a falsification-adjacent baseline. Separate no-go results already show that no Fréchet-smooth nearest-neighbor local momentum profile can satisfy the unsplit equation against a frozen quadratic Hamiltonian at $n=2$.
proof idea
Pure definition: the right-hand side is written as the finite sum over lattice sites $j$ of the discrete wedge $(N_j M_{j+1}-M_j N_{j+1})$ multiplied by the constant structure value $1$ and by the momentum density at $(x,j)$. No lemmas, tactics, or rewriting are involved.
why it matters
This is the unit-structure baseline inside the dynamic HKT target module. The immediate consumer is the recovery theorem showing that inserting the constant $1$ reproduces the original unsmeared ham–ham right-hand side (the sum without an explicit structure factor). That recovery pins the relationship between the frozen classical algebra and the widened target that carries a non-constant structure-function slot.
In the broader Seven Gaps gravity program, the definition keeps the classical unsplit advection form on the books while the load-bearing work moves to dynamic and point-split strong targets. It does not itself close HKT rigidity; it only names the unit case against which non-constant structure and the open unsplit no-go propositions are compared.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.