PhaseSpaceDependentDiracPremise
plain-language theorem explainer
Packages the open Gap-5 Dirac premise: existence of a non-constant lattice inverse metric on phase space together with a Hamiltonian family whose exact bracket recovers that metric. ADM and RS gravity workers tracking the Seven Gaps cite it as the first conjunct of the Gap-5 target. Pure Prop definition (no proof obligation); it only names the missing construction.
Claim. For every positive integer $n$, the phase-space-dependent Dirac premise holds when there exists a map $g$ from the $n$-site phase space to site-indexed real weights that is not constant under changes of canonical data, and for which there exists a Hamiltonian construction whose exact Hamiltonian-Hamiltonian bracket produces $g$.
background
The ambient module separates the existing background-weighted bracket from full ADM dynamics. The exact identity for the weighted Hamiltonian bracket and its continuum smearing both keep the site weight fixed as the phase-space point varies. Full ADM gravity instead needs the inverse spatial metric in the Dirac structure-function slot to depend on the canonical metric data.
A lattice inverse metric is phase-space constant when its value at every site is independent of the canonical data. The open structure PhaseSpaceDependentHamiltonianConstruction asks for a differentiable Hamiltonian family whose exact bracket recovers a prescribed (possibly non-constant) $g$, including all derivative terms from that dependence. The present definition simply conjoins non-constancy of $g$ with non-emptiness of that construction.
proof idea
Definitional unpacking only: the Prop is the existential claim that some $g : \mathrm{PhaseSpace}, n \to \mathbb{Z}/n\mathbb{Z} \to \mathbb{R}$ fails phase-space constancy and admits at least one instance of the open Hamiltonian-construction structure. No tactics, no lemmas applied.
why it matters
Records the first half of Gap 5 in the Seven Gaps gravity program. Downstream, Gap5DynamicDiracAndHKTRigidityTarget is exactly this premise conjoined with an HKT rigidity statement; the module doc states that the current weighted-bracket theorem and its continuum smearing supply neither conjunct. The certified blocker already shows that no fixed background weight can represent the concrete positive dynamic inverse metric at all phase points, so a genuinely dynamic Dirac construction is obligatory. No forcing-chain landmark (T0-T8) is closed here; the declaration only keeps the open obligation named and machine-checkable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.