HamWHasBackgroundStructureFunction
plain-language theorem explainer
Packages the fixed-background structure-function property for weighted hypersurface Hamiltonians: their mutual Poisson bracket equals the discrete two-site form with weight w frozen, independent of phase-space variation. Gravity auditors cite it when separating background-weighted brackets from full ADM dynamics. Pure Prop alias of the identity already proved by the exact weighted Ham–Ham bracket theorem; no new proof content.
Claim. For a fixed lattice weight $w:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$, the weighted Hamiltonians have background structure function $w$ when, for all smearings $N,M$ and every phase point $x=(q,\pi)$, $\{H_w[N],H_w[M]\}(x)=\sum_j(N_j M_{j+1}-M_j N_{j+1})\,w_j\,\pi_{j+1}(q_{j+1}-q_j)$.
background
The module certifies a structural gap in the gravity lane. The exact lattice identity for the background-weighted bracket places a site-dependent weight in the Dirac structure-function slot, and the companion continuum smearing result carries that same fixed weight to the continuum. Full ADM gravity instead needs the inverse spatial metric in that slot to vary with the canonical metric data.
Phase space is the product of configuration $q$ and conjugate momentum $\pi$ on the periodic $n$-site lattice. The Poisson bracket is the standard sum over sites of mixed $q$- and $p$-partials (with the usual caveat that nondifferentiable observables contribute the junk value $0$). The weighted Hamiltonian $H_w[N]$ is the hypersurface Hamiltonian smeared by $N$ against a frozen weight profile $w$.
Upstream, the exact HamW–HamW bracket theorem supplies the lattice identity that this proposition records. The continuum companion then shows that fixed background profiles still reach a weighted continuum limit under mild regularity.
proof idea
Definitional packaging only. The body is the universal quantification over smearings $N,M$ and phase points $x$ of the exact weighted Hamiltonian–Hamiltonian bracket identity. No tactics or lemmas fire here. The companion theorem discharges the proposition in one line by applying the existing exact bracket theorem for the weighted family.
why it matters
Names the background property used by the certified Gap 5 blocker. Downstream, gap5_background_weight_blocker asserts three facts together: every fixed weight satisfies this proposition; continuous profiles retain continuum reach; yet no fixed two-site weight represents the explicit positive dynamic inverse metric at all phase points. The ledger theorem gap5_structure_function_blocker_certified lifts the same triple, keeps the gap5 closure flag false, and records that a genuinely phase-space-dependent structure function (with its Hamiltonian substrate) remains open.
In the Recognition gravity program this separates what is already proved (exact lattice identity plus continuum smearing for frozen weights) from what full constraint recovery still needs: a dynamic Dirac structure function whose inverse-metric slot tracks the canonical data. The module explicitly leaves PhaseSpaceDependentHamiltonianConstruction and the HKT-rigidity target as separate remaining obligations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.