HamW_has_background_structure_function
plain-language theorem explainer
For any fixed site weight w, the weighted Hamiltonian family HamW has w as its Dirac structure function in the Hamiltonian-Hamiltonian bracket. Gap-5 and discrete hypersurface-deformation arguments cite this packaging. The proof is a one-line application of the exact weighted bracket identity.
Claim. For every background weight $w:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$, the $w$-weighted Hamiltonian deformations satisfy $\{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))$ at every phase-space point $x$. Equivalently, $H_w$ has fixed background structure function $w$.
background
The module isolates a Gap-5 obstruction in discrete ADM-style gravity. The exact lattice identity for the background-weighted hypersurface bracket places a site-dependent weight in the Dirac structure-function slot, and a companion continuum-smearing result carries that shape to the continuum. Both keep the weight fixed while the phase-space point varies. Full ADM gravity instead needs the inverse spatial metric in that slot to depend on the canonical metric data.
Here $H_w[N]$ is the Hamiltonian deformation smeared by lapse $N$ with fixed background weight $w$. Phase space carries configuration $q$ and momentum $\pi$ on the cyclic lattice $\mathbb{Z}/n\mathbb{Z}$. The upstream headline theorem states that ${H_w[N],H_w[M]}$ equals the discrete lapse Wronskian times $w_j$ times the point-split momentum density $\pi_{j+1}(q_{j+1}-q_j)$. The proposition packaged here is exactly that identity, quantified over all lapses and phase points.
proof idea
One-line term-mode wrapper: apply the exact discrete weighted hypersurface bracket theorem to the given weight $w$. That theorem already supplies the full quantified identity that defines the fixed-background structure-function proposition, so no further rewriting is required.
why it matters
This declaration turns the existing exact bracket into a named proposition that the Gap-5 blocker can quantify over. Downstream, the certified blocker asserts three conjuncts: every two-site weight has this fixed-background structure function; every continuous background profile has continuum smearing reach; and no fixed weight represents the explicit positive dynamic inverse metric at all phase points. The first conjunct is discharged by this theorem.
In the Recognition gravity ledger this marks a clean separation: the background-weighted bracket is exact and continuum-reachable, yet cannot by itself be the full dynamic Dirac structure function. The module leaves the missing phase-space-dependent Hamiltonian construction and the HKT rigidity obligation as separate open targets; no closure flag is flipped.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.