DynamicWeightedContinuumReach
plain-language theorem explainer
Defines continuum smearing reach for a field-induced structure profile: Riemann sums of G·(Wr·S) on the unit interval converge to the corresponding integral, with G(x)=1+(q(x))². Gravity workers cite it when packaging Gap-5 dynamic continuum smearing against the banked fixed-background quadrature. The body is a pure Prop abbreviation, not a proved statement.
Claim. For a real field profile $q$, the dynamic weighted continuum reach holds when, for every pair of weight and source profiles $W_r,S$ continuous on $[0,1]$, the mesh-$1/N$ Riemann sums of $G_q(k/N)\,W_r(k/N)\,S(k/N)$ tend as $N\to\infty$ to $\int_0^1 G_q(x)\,W_r(x)\,S(x)\,dx$, where $G_q(x)=1+(q(x))^2$.
background
Module Wave C2 R3 lifts the banked fixed-background continuum reach so the structure-function profile is induced by a continuum field $q$ rather than held fixed. The continuum law is the same shape that inhabits the dynamic lattice bracket: $G(x)=1+(q(x))^2$, i.e. the continuum form of the concrete dynamic inverse metric along $q$.
The named profile dynamicStructureProfile is exactly that map $x\mapsto 1+(q x)^2$. Continuity of $G$ on $[0,1]$ follows from continuity of $q$ on the same interval; the admissible class is ContinuousOn on the closed unit interval, not global continuity.
The predicate packages the smearing half of the continuum story: $h$-scaled lattice sums of $G\cdot(W_r\cdot S)$ must tend to the integral. It deliberately does not touch the sampled-lapse Wronskian rate-$h$ limit (still open in ledger terminal R4) and does not flip gap5_constraint_recovery.
proof idea
No proof: this is a Prop-valued definition. The body is the universal quantification over continuous weight and source profiles of the standard Riemann-sum-to-integral Tendsto statement, with the structure factor specialized to dynamicStructureProfile q. Downstream, the companion theorem discharges the predicate by feeding that profile into the already-banked fixed-background continuum-reach lemma.
why it matters
This is the interface Prop for Gap-5 dynamic continuum smearing. The companion theorem dynamic_weighted_continuum_reach shows every continuous-on-$[0,1]$ field profile satisfies it, by reducing to the banked fixed-background quadrature after composing through $1+q^2$.
The typed residual TypedResidual_gap5_dynamic_continuum_smearing conjoins three pieces: (1) reach for every admissible $q$ (this predicate), (2) binding of the continuum law to the concrete dynamic inverse metric on sampled phase points, and (3) the already-banked Hamiltonian inhabitant from the HamDyn family. Together they witness the smearing half of the continuum story without claiming the open Wronskian rate-$h$ limit or constraint recovery.
In the Seven Gaps gravity ladder this is the continuum-smearing rung that lets field-dependent structure profiles inherit quadrature convergence from the fixed-background case.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.