PhaseSpaceDependentHamiltonianConstruction
plain-language theorem explainer
Names the open interface for a Hamiltonian family whose exact Poisson brackets carry a genuinely phase-space-dependent inverse metric g. Gap-5 workers cite it when separating fixed background weights from full dynamic Dirac structure functions. It is a structure definition: supply differentiable Hamiltonians and match the point-split bracket identity with factor g(x).
Claim. A phase-space-dependent Hamiltonian construction for a map $g$ from phase space to site weights consists of a family $\mathrm{ham}_N$ of observables, one per smear $N:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$, such that each $\mathrm{ham}_N$ is differentiable on phase space and the Poisson bracket obeys $\{\mathrm{ham}_N,\mathrm{ham}_M\}(x)=\sum_j(N_j M_{j+1}-M_j N_{j+1})\,g(x)_j\,p_{j+1}(q_{j+1}-q_j)$ at every phase point $x=(q,p)$.
background
The module certifies a hard distinction in the Recognition gravity stack. The exact lattice identity for the background-weighted Hamiltonians places a site-dependent weight in the Dirac structure-function slot, and continuum smearing carries that shape forward, but the weight is held fixed as the phase-space point varies. Full ADM gravity instead needs the inverse spatial metric in that slot to depend on the canonical metric data.
Phase space is configuration-plus-momentum data on the cyclic lattice $\mathbb{Z}/n\mathbb{Z}$. The Poisson bracket is the standard sum $\sum_i(\partial_{q_i}F\partial_{p_i}G-\partial_{p_i}F\partial_{q_i}G)$; when an observable fails to be differentiable the formal derivative contributes the junk value $0$, which is why structure theorems carry explicit differentiability hypotheses.
The right-hand side of the packaged identity reuses the same point-split momentum density as the background theorem, isolating the missing piece: a differentiable Hamiltonian family whose bracket produces $g(x)_j$ including all derivative terms from the dependence of $g$ on the canonical data.
proof idea
Structure definition, not a proved theorem. Three fields must be supplied by any inhabitant: the Hamiltonian map sending each smear $N$ to an observable on phase space; a global differentiability obligation for every smear; and the exact Hamiltonian-Hamiltonian bracket identity whose structure-function factor is the phase-space-dependent $g$. No proof body and no tactics; the type itself is the obligation.
why it matters
This declaration is the named open target for Gap 5's dynamic Dirac half. Downstream, the background construction shows every fixed weighted Hamiltonian inhabits the interface only when $g$ is the constant background weight. The dynamic Dirac premise then packages existence of a nonconstant $g$ together with a nonempty inhabitant of this structure.
The module doc is explicit: no closure flag moves; this construction and the existing HKT rigidity statement remain separate remaining obligations. In the broader Recognition gravity program the point is negative but sharp: the background-weighted bracket, despite its exact lattice identity and continuum smearing reach, cannot by itself be the full dynamic Dirac structure function.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.