backgroundHamiltonianConstruction
plain-language theorem explainer
Any fixed background weight w yields a Hamiltonian construction whose exact HH bracket recovers the constant inverse-metric field g(x)=w. Gravity and ADM structure-function work cite it to place the existing weighted lattice Hamiltonian inside the dynamic target interface without claiming genuine phase-space dependence. The body is a one-line packaging of the known differentiability and exact bracket identities for HamW.
Claim. For any fixed site weight $w:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$, the background-weighted Hamiltonian family $H_w$ is a phase-space-dependent Hamiltonian construction for the constant inverse-metric field $g(x)=w$. Explicitly: $H_w[N]$ is differentiable in phase space for every lapse $N$, and $\{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 isolates a gap between the existing background-weighted hypersurface bracket and full ADM dynamics. On the periodic lattice phase space $(q,\pi):(\mathbb{Z}/n\mathbb{Z}\to\mathbb{R})^2$, the Poisson bracket is the standard sum of $\partial_q F,\partial_\pi G-\partial_\pi F,\partial_q G$ terms. The weighted Hamiltonian $H_w[N]$ produces, via the exact identity bracket_HamW_HamW, a D-type generator whose structure-function slot is filled by the fixed weight $w_j$ times the point-split momentum density $\pi_{j+1}(q_{j+1}-q_j)$.
Full ADM gravity instead needs that slot occupied by a genuinely phase-space-dependent inverse spatial metric $g(x)$. The open target structure PhaseSpaceDependentHamiltonianConstruction packages exactly that demand: a differentiable Hamiltonian family whose HH bracket equals the same Wronskian times $g(x)_j$ times the point-split density, including all derivative terms from $g$'s dependence on canonical data. The present definition only inhabits that structure when $g$ is the constant field $x\mapsto w$.
proof idea
One-line structure inhabitant. Set the Hamiltonian field to the existing background family $H_w$. Differentiability is differentiable_HamW w. The HH bracket identity is discharged by applying bracket_HamW_HamW w at each triple of lapses and phase point, which matches the structure's right-hand side once $g(x)$ is constantly $w$.
why it matters
This definition is the positive half of the dynamic structure-function blocker: it shows the background-weighted construction does sit inside the dynamic target interface, but only for phase-space-constant metrics. Downstream siblings (e.g. the fixed-background representation lemmas and the concrete nonconstant inverse-metric witness) then prove that no fixed $w$ can represent a truly dynamic $g$. The module doc is explicit that no closure flag flips: the missing dynamic Dirac premise remains open, recorded alongside HKT rigidity as a separate Gap-5 obligation. In the Recognition gravity ledger this separates an exact lattice identity (and its continuum smearing reach) from the full ADM structure function required for dynamic spatial geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.