dynamic_weighted_continuum_reach
plain-language theorem explainer
Every continuous field profile q on [0,1] induces a continuum smearing reach: h-scaled lattice sums of G·(Wr·S) converge to the matching integral, with G = 1+(q x)². Gravity and continuum-limit workers cite it when discharging the dynamic half of gap-5 residual R3. The proof is a one-line reduction to the banked fixed-background quadrature after composing through the dynamic structure profile.
Claim. If $q:\mathbb{R}\to\mathbb{R}$ is continuous on $[0,1]$, then for every pair of continuous weight and source profiles $W_r,S$ on $[0,1]$, $$\frac1N\sum_{k=0}^{N-1} G\!\Bigl(\tfrac kN\Bigr)\,W_r\!\Bigl(\tfrac kN\Bigr)\,S\!\Bigl(\tfrac kN\Bigr)\;\xrightarrow{N\to\infty}\;\int_0^1 G(x)\,W_r(x)\,S(x)\,dx,$$ where $G(x)=1+(q(x))^2$ is the field-induced structure profile.
background
Wave C2 R3 extends the banked fixed-background continuum reach so the structure-function profile is induced by a continuum field profile $q$ through the same law that inhabits the dynamic lattice bracket: $G(x)=1+(q x)^2$. That $G$ is the continuum shape of the concrete dynamic inverse metric along $q$, and the package is witnessed by the HamDyn family (phase-space-dependent Hamiltonian construction on that metric).
DynamicWeightedContinuumReach q packages the statement that $h$-scaled lattice sums of $G\cdot(W_r\cdot S)$ tend to the integral on $[0,1]$, with $G$ named as a function of the field data through $1+q^2$. The admissible class is continuity of $q$ on the closed unit interval; global continuity is not required.
The fixed-background sibling already supplies the quadrature for an arbitrary continuous structure profile. This declaration only specialises that banked reach to the dynamic family.
proof idea
One-line term proof. Introduce continuous $W_r$ and $S$, then apply the banked fixed-background continuum reach to the composed profile dynamicStructureProfile q, feeding continuity of that profile from continuousOn_dynamicStructureProfile q hq. No new analytic work: the dynamic law is just the named specialisation $G=1+q^2$.
why it matters
Feeds the R3 headline residual typedResidual_gap5_dynamic_continuum_smearing, which packages three witnesses: this continuum reach for every continuous $q$, the pointwise identification of the concrete dynamic inverse metric with the structure profile, and the two-site dynamic bracket residual. That residual is the smearing half of the continuum story for gap 5.
Module honesty is explicit: this does not flip gap5_constraint_recovery, and the sampled-lapse Wronskian rate-$h$ limit remains open inside the ledger terminal R4 (dirac_algebra_continuum_limit). A sibling decoy certificate shows why a fixed-background weight alone cannot discharge R3: constant field profiles $q\equiv 0$ and $q\equiv 1$ induce distinct structure profiles ($G\equiv 1$ vs $G\equiv 2$ at $x=0$), so no single fixed $W$ covers the dynamic family.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.