fixed_background_represents_only_constant
plain-language theorem explainer
A fixed site weight that matches a candidate inverse metric at every phase-space point forces that metric to be independent of the canonical data. Gravity and ADM structure-function work cite this as the one-direction half of the fixed-background characterization. The proof is a two-line rewrite: equality through the common weight at two phase points.
Claim. Let $w: \mathbb{Z}/n\mathbb{Z} \to \mathbb{R}$ be a fixed site weight and $g$ a map from phase space to site-valued reals. If $w(j) = g(x,j)$ for every phase-space point $x$ and every site $j$, then $g(x,j) = g(y,j)$ for all phase points $x,y$ and all sites $j$.
background
This module sits in the Seven Gaps gravity stack. The exact lattice identity for the background-weighted Hamiltonian bracket and its continuum smearing both keep a site weight fixed while 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.
PhaseSpaceConstant g means changing the canonical data never changes $g$ at any lattice site: $\forall x,y,j., g(x,j)=g(y,j)$. FixedBackgroundRepresents w g means a single weight $w$ agrees with $g$ at every phase point and site: $\forall x,j., w(j)=g(x,j)$. Phase space here is the lattice canonical data type from the hypersurface-deformation development.
The local goal is a certified distinction: fixed background weights can represent only phase-space-constant inverse metrics, so they cannot stand in for a genuinely dynamic Dirac structure function.
proof idea
Term-mode proof by unfolding the two predicates. Fix arbitrary phase points $x,y$ and site $j$. From the representation hypothesis, $w(j)=g(x,j)$ and $w(j)=g(y,j)$. Rewrite both sides of the desired equality $g(x,j)=g(y,j)$ via those two identities; the common weight cancels and the claim is immediate. No external lemmas are required beyond the definitions of the two predicates.
why it matters
This is the forward half of the exact characterization exists_fixed_background_iff_phaseSpaceConstant: a candidate inverse metric admits one fixed background representation at all phase points exactly when it is phase-space constant. Downstream, no_fixed_background_represents_concrete applies it to the positive two-site example concreteDynamicInverseMetric, which is not constant, yielding a concrete no-go.
That no-go feeds the certified blocker gap5_background_weight_blocker: the present background-weighted family keeps its exact bracket and continuum reach, yet no fixed two-site weight represents the explicit dynamic metric at all phase points. In the Recognition gravity program this separates the existing background-weighted bracket from the missing phase-space-dependent Hamiltonian construction named by PhaseSpaceDependentHamiltonianConstruction, and records that Gap 5 (dynamic Dirac structure plus HKT rigidity) remains an open obligation rather than a closed flag.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.