BackgroundWeightedContinuumReach
plain-language theorem explainer
A fixed background weight profile W has continuum smearing reach when every pair of continuous test profiles on [0,1] has its discrete weighted structure sums converge, as mesh N→∞, to the corresponding Riemann integral of W·Wr·S. Gravity auditors cite it as the continuum half of the Gap-5 background-weight blocker. The body is a pure Prop abbreviation of that Tendsto statement; no proof is attached here.
Claim. A real function $W$ has background-weighted continuum reach if, for every pair of functions $W_r,S$ continuous on $[0,1]$, the averages $\frac{1}{N}\sum_{k=0}^{N-1} W(k/N)\,W_r(k/N)\,S(k/N)$ tend as $N\to\infty$ to $\int_0^1 W(x)\,W_r(x)\,S(x)\,dx$.
background
The module isolates a Gap-5 obstruction in the Dirac structure-function slot of ADM gravity. Exact lattice identities such as the background-weighted Hamiltonian bracket place a site-dependent weight in that slot, and a quadrature theorem carries the smeared sums to the continuum. Both keep the weight fixed while the phase-space point varies. Full ADM instead needs the inverse spatial metric in the slot to depend on the canonical metric data.
This definition packages the continuum half of that fixed-weight story. Continuum smearing reach for a profile $W$ means: for every continuous pair of test profiles on the unit interval, the Riemann-sum style discrete weighted structure sums converge in the usual topology to the integral of the product $W\cdot W_r\cdot S$. The weight $W$ itself is treated as a fixed background, not as a dynamical field on phase space.
The surrounding file then contrasts this reach with a positive two-site dynamic inverse metric that is not phase-space constant, so no fixed background can represent it at every phase point.
proof idea
Definition only: the body is the Prop that quantifies over continuous $W_r,S$ on $[0,1]$ and asserts Filter.Tendsto of the normalized finite sums against the neighborhood filter of the definite integral. No tactics or lemmas fire at this declaration. The companion theorem background_weighted_continuum_reach later discharges the Prop for continuous $W$ by a one-line appeal to weightedStructureSum_tendsto.
why it matters
This Prop is the continuum clause inside the certified Gap-5 background-weight blocker. Downstream, background_weighted_continuum_reach proves every continuous fixed profile satisfies it; gap5_background_weight_blocker packages that reach with the exact background-weighted bracket family and the negative representation statement against concreteDynamicInverseMetric; and gap5_structure_function_blocker_certified lifts the package into the full-theory ledger.
The ledger records that every fixed background weight yields a phase-space-constant structure function and reaches the weighted continuum, yet none represents the explicit positive dynamic inverse metric. The weighted-bracket route to constraint recovery therefore needs a genuinely dynamic structure function, whose substrate derivation remains open; the closure flag stays false. The definition itself changes no flag: it only names the continuum reach that the blocker concedes to the existing background-weighted family.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.