background_weighted_continuum_reach
plain-language theorem explainer
Every continuous fixed background weight W on [0,1] has full continuum smearing reach: the discrete weighted structure sums converge to the integral of W·Wr·S. Gravity and continuum-limit workers cite it when packaging the background-weighted bracket's reach. The proof is a one-line wrapper of the existing quadrature theorem weightedStructureSum_tendsto.
Claim. Let $W:[0,1]\to\mathbb{R}$ be continuous. Then for every pair of continuous test profiles $W_r,S$ on $[0,1]$, $$\frac1N\sum_{k=0}^{N-1} W\!\left(\frac kN\right) W_r\!\left(\frac kN\right) S\!\left(\frac kN\right)\ \to\ \int_0^1 W(x)\,W_r(x)\,S(x)\,dx$$ as $N\to\infty$.
background
This module separates two layers of the Dirac structure function in Recognition gravity. The exact lattice identity bracket_HamW_HamW places a site-dependent weight in the structure-function slot, and a quadrature result carries that smearing shape to the continuum. Both keep the 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.
BackgroundWeightedContinuumReach W packages the continuum claim for a single fixed profile $W$: every continuous pair of smearing functions $W_r,S$ on the unit interval has discrete weighted sums converging in the usual Riemann-sum topology to $\int_0^1 W,W_r,S$. Continuity of $W$ on the compact interval $[0,1]$ is the only hypothesis on the background.
The local setting is Gap 5 of the seven gravity gaps: certify that fixed-background weighting, despite exact lattice identity and continuum reach, cannot by itself be the full dynamic Dirac structure function.
proof idea
One-line wrapper. After introducing the two continuous smearing profiles $W_r$ and $S$, the goal is exactly the conclusion of weightedStructureSum_tendsto applied to $W,W_r,S$ with the three continuity hypotheses. No extra algebraic work.
why it matters
Feeds the certified blocker gap5_background_weight_blocker, whose conjunction records three facts: every two-site weight has the background structure-function identity; every continuous continuum profile $W$ has continuum smearing reach (this theorem); and no fixed two-site weight represents the explicit positive dynamic inverse metric concreteDynamicInverseMetric at all phase points.
Together those clauses pin the module thesis: the existing background-weighted bracket has exact lattice identity and continuum reach, yet cannot serve as the full dynamic Dirac structure function of ADM gravity. The open obligations named in the module (PhaseSpaceDependentHamiltonianConstruction and the separate HKT rigidity target) remain; this result only closes the continuum-reach half of the background side. No T0–T8 forcing step is discharged here; the contribution is a gravity-gap blocker, not a foundation landmark.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.