FixedBackgroundRepresents
plain-language theorem explainer
A fixed site weight represents a phase-space-dependent inverse metric everywhere precisely when the two agree at every phase point and lattice site. Gravity workers on the Gap 5 Dirac structure-function blocker cite this as the representation relation. It is a pure Prop definition: pointwise equality, no proof content.
Claim. A fixed site weight $w:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$ represents a candidate inverse metric $g$ (a map from phase space to site-valued reals) at every phase-space point when $w(j)=g(x,j)$ for all phase points $x$ and all sites $j$.
background
The module isolates a Gap 5 obstruction for background-weighted brackets in lattice gravity. The exact identity bracket_HamW_HamW and the continuum smearing result weightedStructureSum_tendsto both keep a site-dependent weight fixed while the phase-space point varies. Full ADM gravity instead needs the inverse spatial metric in that structure-function slot to depend on the canonical metric data.
Phase space here is the product of configuration and conjugate momentum, each a real-valued field on the periodic lattice with $n$ sites. A candidate inverse metric is then a map from that phase space to site-indexed reals. A fixed background weight is merely a site-indexed real function, independent of phase.
The definition records when such a fixed weight can stand in for the full phase-dependent object: only by agreeing with it at every phase point and every site.
proof idea
Definitional, not a theorem. The body is the Prop that for every phase-space point $x$ and every site $j$, the fixed weight at $j$ equals the candidate inverse metric evaluated at $(x,j)$. No lemmas or tactics.
why it matters
This is the representation relation that turns the fixed-vs-dynamic distinction into a Lean predicate. Downstream, fixed_background_represents_only_constant shows any $g$ so represented must be phase-space constant; exists_fixed_background_iff_phaseSpaceConstant gives the exact characterization. The concrete no-go no_fixed_background_represents_concrete then applies it to the positive two-site example concreteDynamicInverseMetric, and gap5_background_weight_blocker packages the certified blocker: background weights have exact brackets and continuum reach, yet none represents that dynamic metric.
The FullTheoryLedger theorem gap5_structure_function_blocker_certified lifts the same fact into the ledger: the weighted-bracket route to constraint recovery needs a genuinely dynamic structure function, whose substrate derivation remains open and the closure flag stays false. No T0–T8 landmark is discharged here; the contribution is the Gap 5 structure-function separation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.