exists_fixed_background_iff_phaseSpaceConstant
plain-language theorem explainer
A lattice inverse metric on phase space admits a single fixed site-weight representation at every phase point if and only if the metric is constant across phase space. Gravity and ADM structure-function work cites this as the exact obstruction separating background-weighted brackets from fully dynamic Dirac structure functions. The proof is a two-direction constructor: one side applies the one-way constancy lemma; the other exhibits the constant slice as the representing weight.
Claim. For any candidate inverse metric $g$ on the $n$-site phase space, there exists a fixed site weight $w$ such that $w(j)=g(x,j)$ for every phase point $x$ and every site $j$ if and only if $g$ is phase-space constant: $g(x,j)=g(y,j)$ for all phase points $x,y$ and sites $j$.
background
This module sits inside the Gravity SevenGaps development that separates background-weighted Dirac brackets from a fully dynamic ADM structure function. The exact lattice identity bracket_HamW_HamW and the continuum smearing result keep a site 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.
Two local predicates make the distinction precise. Phase-space constancy means changing the canonical data never changes the value of $g$ at any site. A fixed background representation means a single site weight $w$ agrees with $g$ at every phase point and every site. The one-way lemma already shows that any such representation forces constancy; the present result upgrades that to an exact characterization.
Phase space here is the product of configuration and momentum data on the cyclic lattice $\mathbb{Z}/n\mathbb{Z}$. The two-site positive example developed later in the file is the concrete witness that non-constant metrics exist and therefore cannot be represented by any fixed background weight.
proof idea
Term-mode constructor on the biconditional.
Left-to-right: unpack an existential witness $w$ with FixedBackgroundRepresents w g, then apply the already-proved one-way lemma fixed_background_represents_only_constant.
Right-to-left: assume phase-space constancy. Pick the zero configuration-momentum point $x_0$ and take the candidate weight to be the slice $w:=g(x_0,\cdot)$. For arbitrary phase point $x$ and site $j$, constancy gives $g(x_0,j)=g(x,j)$, which is exactly the representation identity.
why it matters
This is the exact characterization that turns the one-way constancy obstruction into an iff, so later blocker theorems can reason both directions. Its sole recorded consumer is gap5_background_weight_blocker, which certifies that the present background-weighted family keeps its exact bracket and continuum reach, yet no fixed two-site weight can represent the explicit positive dynamic metric at all phase points.
In the Recognition gravity program this closes the logical gap between "weighted structure functions with fixed background" and "dynamic inverse-metric structure functions required by ADM." The module doc is explicit that no closure flag moves: PhaseSpaceDependentHamiltonianConstruction still names the missing Hamiltonian construction, and Gap5DynamicDiracAndHKTRigidityTarget records that construction and HKT rigidity as separate remaining obligations. The result is therefore a certified blocker, not a completion of Gap 5.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.