bracket_HamW_HamW_one
plain-language theorem explainer
When the background weight is identically one, the Poisson bracket of two weighted smeared Hamiltonians equals the frozen-1 lattice identity: a discrete lapse Wronskian times the point-split density. Anyone citing the weighted hypersurface bracket as a true generalization of the unweighted deformation algebra needs this recovery. The proof is a three-rewrite: unit-weight collapse of each generator, then the existing frozen-1 bracket theorem.
Claim. For lapse smearings $N,M:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$ and phase-space point $x=(q,\pi)$, the Poisson bracket of the two unit-weight background-weighted Hamiltonians satisfies $\{H_{w\equiv 1}[N],H_{w\equiv 1}[M]\}(x)=\sum_j(N_j M_{j+1}-M_j N_{j+1})\,\pi_{j+1}(q_{j+1}-q_j)$.
background
This module sits in the QG Seven-Gaps campaign, Pillar 1 (constraint algebra), panel C10: a background-weighted structure function on the periodic lattice. The weighted smeared Hamiltonian is $H_w[N]=\sum_i(N_i/2)\bigl(\pi_i^2+w_i(q_{i+1}-q_i)^2\bigr)$, with fixed site weight $w$ only in the stiffness slot; the kinetic slot is unweighted. Continuum reading (interpretive): $w$ samples a static inverse spatial metric $h^{xx}$.
The sanity anchor states that at unit weight the weighted generator equals the frozen-1 generator of HypersurfaceDeformation as functions on phase space. The headline weighted bracket then closes two $w$-weighted Hamiltonian deformations on a D-type generator whose smearing is the discrete lapse Wronskian times $w$ (structure function linear in $w$, not $w^2$).
The present result is the frozen-1 recovery: substituting $w\equiv 1$ must literally reproduce the already-proved unweighted identity, so the weighted theorem is an honest generalization rather than a parallel construction. Panel-lock honesty: $w$ is never phase-space dependent; full Dirac $g^{ab}[q]$ and HKT rigidity remain open.
proof idea
One-line rewrite proof. First apply the unit-weight sanity anchor twice, replacing each HamW (fun _ => 1) · by the frozen-1 generator Ham. The goal is then exactly the statement of the existing unweighted hypersurface-deformation bracket theorem, which is applied directly. No new algebraic expansion is performed here; all Kronecker collapse and Frechet work lives upstream in the frozen-1 proof and in the weighted headline bracket.
why it matters
Closes the honesty loop for panel C10: the weighted structure function is a true extension of the frozen-1 hypersurface-deformation algebra, not a rebranded twin. Downstream, the continuum smearing limit weightedStructureSum_tendsto consumes the weighted bracket shape (background weight profile $W$, continuum lapse-Wronskian $Wr$, closure density $S$) and sends the $h$-scaled lattice sums to $\int_0^1 W\cdot(Wr\cdot S)$ via the quadrature toolkit. That consumer needs the discrete identity family to be coherent at $w=1$ with the already-audited frozen-1 theorem.
Framework place: constraint-algebra side of gravity recovery on the lattice, toward but not flipping gap5_constraint_recovery. No Hojman–Kuchař–Teitelboim target is inhabited; phase-space-dependent structure functions stay open. The result is pure algebraic bookkeeping that keeps the weighted pillar continuous with the unweighted one.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.