HamW
plain-language theorem explainer
Defines the background-weighted smeared Hamiltonian on the periodic lattice: kinetic term unweighted, stiffness term multiplied by a fixed site weight w. Gravity and constraint-algebra workers cite it as the generator whose Poisson bracket recovers w as the discrete Dirac structure function. The body is a direct finite sum over lattice sites; no proof obligations.
Claim. For a fixed background weight $w: \mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$ and lapse $N$, the smeared Hamiltonian on phase space $(q,\pi)$ is $$H_w[N](q,\pi)=\sum_i\frac{N_i}{2}\bigl(\pi_i^2+w_i(q_{i+1}-q_i)^2\bigr).$$ The weight multiplies only the discrete gradient-squared (stiffness) slot; the kinetic slot is unweighted. $w$ depends on the lattice site alone, never on $(q,\pi)$.
background
This module sits in the QG Seven-Gaps campaign, Pillar 1 (constraint algebra), panel-locked bet C10: a weighted structure function on the lattice. It generalizes the frozen-1 hypersurface-deformation generator of HypersurfaceDeformation by inserting a fixed background weight into the stiffness slot.
Phase space is the product of configuration and conjugate momentum on the periodic $n$-site lattice: pairs $(q,\pi)$ with both maps $\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$. The continuum reading (interpretive, not proved here) treats $w$ as a sampled inverse spatial metric $h^{xx}(x)$, or local sound-speed squared, of a static background line element.
Honesty bound from the module doc: this is a BACKGROUND-$w$ object. The weight never depends on the phase-space point. The genuinely dynamic inverse metric $g^{ab}[q]$ demanded by full Dirac algebra and GR recovery remains open; HKT rigidity is untouched.
proof idea
Pure definition: a finite sum over $i\in\mathbb{Z}/n\mathbb{Z}$ of $(N_i/2)$ times kinetic $\pi_i^2$ plus $w_i$ times the squared nearest-neighbor difference $(q_{i+1}-q_i)^2$. No tactics, no lemmas, no sorry. Downstream differentiability and bracket theorems expand this sum and differentiate termwise with respect to the $q$ and $\pi$ coordinates.
why it matters
This is the model object for the weighted hypersurface bracket. The headline theorem bracket_HamW_HamW shows two such generators close on a D-type (shift) generator whose smearing is the discrete lapse Wronskian times $w$, so the structure function of the bracket is exactly the background weight (linear in $w$, not $w^2$, because only the stiffness slot is weighted).
Downstream, DynamicStructureFunctionBlocker packages every fixed HamW as a PhaseSpaceDependentHamiltonianConstruction only for the phase-space-constant metric $g\equiv w$, and records the exact bracket identity as HamWHasBackgroundStructureFunction. The same blocker proves no fixed two-site background weight can represent a concrete dynamic inverse metric at every phase-space point, and leaves open PhaseSpaceDependentDiracPremise: a nonconstant $g$ together with a Hamiltonian whose exact bracket produces it. That open premise is the remaining gap toward gap5 constraint recovery; this definition supplies the background side of the comparison, not the dynamic side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.