PhaseSpaceConstant
plain-language theorem explainer
A lattice inverse metric is phase-space constant when its value at every site is independent of the canonical phase-space data. Gravity researchers in the Seven Gaps Dirac-structure program cite this predicate to separate fixed-background weights from truly dynamic inverse metrics. Pure definition: universal equality of site values across all phase points.
Claim. A map $g$ from phase space and lattice sites into the reals is phase-space constant when, for all phase-space points $x,y$ and every site $j$, one has $g(x,j)=g(y,j)$.
background
In the lattice Dirac program, the structure-function slot of the Hamiltonian bracket is filled by a site weight. The existing background-weighted identity keeps that 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.
Phase space here is the discrete canonical configuration space used by the hypersurface-deformation module: points carry the lattice metric (and conjugate) data. A candidate inverse metric is a real-valued function of a phase-space point and a site index in $\mathbb{Z}/n\mathbb{Z}$.
This module isolates the distinction. Fixed background weights can match a candidate at every phase point only when that candidate does not actually depend on the phase point.
proof idea
Definition, not a theorem. The body is the Prop that $g$ takes the same real value at every phase-space point for each fixed site index. No lemmas are applied.
why it matters
This predicate is the hinge of the dynamic structure-function blocker. Downstream, a fixed background weight represents a candidate at every phase point only if the candidate is phase-space constant (one direction is immediate rewriting; the converse builds the constant weight from any phase point). The concrete two-site positive example is then shown not constant, so no background weight represents it.
That separation feeds the open premise requiring a nonconstant inverse metric together with a Hamiltonian construction whose exact bracket produces it. Module-level, Gap 5 still needs that dynamic Dirac construction separately from HKT rigidity; this definition only names the constancy obstruction that blocks treating the existing background-weighted bracket as the full dynamic structure function. No T0–T8 forcing step is discharged here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.