zeroPhasePoint
plain-language theorem explainer
Names the origin of the two-site canonical phase space: vanishing configuration and momentum at every site. Gravity auditors cite it as one of two explicit test points that separate a phase-dependent inverse metric from any fixed background weight. The body is a pair of constantly-zero maps.
Claim. Let the two-site phase space consist of pairs of real-valued configuration and momentum fields on $\mathbb{Z}/2\mathbb{Z}$. The zero phase point is the pair in which both fields are identically zero.
background
This module sits in the Seven Gaps gravity stack. The exact lattice identity bracket_HamW_HamW and the continuum smearing limit put a site-dependent weight in the Dirac structure-function slot, but keep 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.
PhaseSpace n is the product of configuration and momentum fields on an $n$-site lattice (here $n=2$). A weight represents a candidate inverse metric at every phase point only if that metric is phase-space constant. The module builds a positive two-site counterexample metric and evaluates it at explicit points to break constancy.
The zero phase point is the canonical origin used for those evaluations: configuration zero and momentum zero everywhere.
proof idea
Definitional pair: both the configuration map and the momentum map send every site of $\mathbb{Z}/2\mathbb{Z}$ to $0$. No lemmas are applied; the term is the pair of constantly-zero functions.
why it matters
Feeds the two witness theorems that close the dynamic-structure-function blocker. concreteDynamicInverseMetric_witness evaluates the concrete inverse-metric candidate at this point and at the unit-configuration point, obtaining the values $1$ and $2$ on site $0$. From that inequality, concreteDynamicInverseMetric_not_constant concludes the candidate is not phase-space constant, so no fixed background weight can represent it everywhere.
That distinction is the module's main claim: the existing background-weighted bracket, despite its exact lattice identity and continuum reach, cannot by itself be the full dynamic Dirac structure function of ADM gravity. The remaining obligations stay open under PhaseSpaceDependentHamiltonianConstruction and Gap5DynamicDiracAndHKTRigidityTarget; this definition only supplies a concrete test point for the blocker, not a closure of Gap 5.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.