no_fixed_background_represents_concrete
plain-language theorem explainer
No fixed two-site background weight can equal the concrete dynamic inverse metric at every phase-space point. Gravity and Dirac-structure workers cite this as the concrete no-go separating background-weighted brackets from full ADM structure functions. The proof is a short contradiction: representation forces phase-space constancy, but the model metric is not constant.
Claim. For every fixed two-site weight $w : \mathbb{Z}/2\mathbb{Z} \to \mathbb{R}$, it is not the case that $w$ represents the concrete dynamic inverse metric $g(x,j) = 1 + (x_1(j))^2$ at every phase-space point $x$ and site $j$ (i.e., one never has $w(j) = g(x,j)$ for all $x,j$).
background
This module separates the existing background-weighted Hamiltonian bracket from the full dynamic Dirac structure function of ADM gravity. The exact lattice identity and continuum smearing results keep a site weight fixed while the phase-space point varies; full gravity needs the inverse spatial metric in that slot to depend on the canonical metric data.
FixedBackgroundRepresents w g means a fixed site weight $w$ agrees with a candidate inverse metric $g$ at every phase-space point and every site. A companion theorem states that if any such fixed $w$ represents $g$ everywhere, then $g$ is phase-space constant (same values at every phase point).
The model inverse metric is $g(x,j) = 1 + (x_1(j))^2$ on the two-site phase space. It is positive and genuinely configuration-dependent: evaluating at the zero canonical point versus a unit-configuration point already shows it is not phase-space constant.
proof idea
Assume toward contradiction that some fixed weight $w$ represents the concrete dynamic inverse metric everywhere. Apply the upstream lemma that any metric represented by a fixed background weight must be phase-space constant. That yields constancy of the concrete model metric, which directly contradicts the already-proved non-constancy witness (zero phase point versus unit configuration at site $0$). Discharge by exact on that contradiction.
why it matters
This is the concrete no-go half of Gap 5's background-weight blocker. Downstream, gap5_background_weight_blocker packages three facts: every background weight still has the exact Hamiltonian-Hamiltonian bracket identity, continuum smearing still reaches, and yet no fixed two-site weight represents the explicit positive dynamic metric at all phase points.
In the Recognition gravity stack this certifies a structural limit, not a failed computation: the weighted bracket is exact on the lattice and has continuum reach, but cannot by itself supply the phase-space-dependent inverse-metric slot required by full ADM Dirac structure. The module leaves open the separate obligations named by the phase-space-dependent Hamiltonian construction and the HKT rigidity target; no closure flag is flipped here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.