forward_density_uniform
plain-language theorem explainer
On the unit interval, the mesh-scaled forward difference of a C¹ field q, weighted by a continuous momentum density p at the right endpoint, converges uniformly in the mesh index to p·q'. Anyone proving Riemann-sum continuum limits for dynamic Dirac brackets cites this. The argument is a mean-value rewrite plus uniform continuity of p and q' on the compact interval, with a two-term absolute-value split.
Claim. Let $q:\mathbb{R}\to\mathbb{R}$ be $C^1$ and let $p$ be continuous on $[0,1]$. Then for every $\varepsilon>0$ there exists $N_0\in\mathbb{N}$ such that for all $n\ge N_0$ and all $k<n$, $$\bigl|p\bigl(\tfrac{k+1}{n}\bigr)\,n\bigl(q\bigl(\tfrac{k+1}{n}\bigr)-q\bigl(\tfrac{k}{n}\bigr)\bigr)-p\bigl(\tfrac{k}{n}\bigr)\,q'\bigl(\tfrac{k}{n}\bigr)\bigr|<\varepsilon.$$
background
This module closes Wave C2 R4: the rate-$h$ continuum shape of the freestanding sampled dynamic bracket. The honest scaled object is $n\cdot\Sigma$ of lattice summands $W_k G_k(\pi_{k+1}\Delta q_k)$, converging to $\int(NM'-MN')\cdot G\cdot(p\cdot q')$ with structure $G=1+q^2$. The ledger name dirac_algebra_continuum_limit is held free; only the shape/rate analysis is claimed.
The forward density is the local factor $p\cdot q'$ appearing in that continuum integrand (via continuum momentum flux). On a uniform mesh of width $1/n$, the natural discrete stand-in is the right-endpoint weight $p((k+1)/n)$ times the scaled forward difference $n(q((k+1)/n)-q(k/n))$. Uniform control of the pointwise error is needed before summing $n$ sites.
Upstream, forward_diff_mvt supplies a mean-value identity equating the scaled forward difference to $q'(c)$ for some $c$ in the open mesh interval. Compactness of $[0,1]$ gives uniform bounds on $|p|$ and $|q'|$ (exists_norm_bound_on_Icc) and uniform continuity of both $p$ and $q'$.
proof idea
Fix $\varepsilon>0$. Bound $|p|$ by $B_P$ and $|q'|$ by $B_{q'}$ on $[0,1]$. Set $\varepsilon':=\varepsilon/(2(B_P+B_{q'}+1))$. Uniform continuity of $p$ and of $q'$ on the compact interval yields moduli $\delta_p,\delta_q$; take $\delta=\min(\delta_p,\delta_q)$ and choose $N_0$ large enough that the mesh $1/n\le\delta$ for $n\ge N_0$.
For each site $k$, apply forward_diff_mvt to write $n(q_{k+1}-q_k)=q'(c)$. Algebraic rearrangement splits the error into
$(p_{k+1}-p_k)q'(c)+p_k(q'(c)-q'k)$.
Distance estimates put both $|c-k/n|$ and $|(k+1)/n-k/n|$ under the moduli, so each factor difference is $\le\varepsilon'$. Absolute values and the product bounds give total error $\le\varepsilon'B{q'}+B_P\varepsilon'<\varepsilon$.
why it matters
This is the local analytic engine behind the rate-$h$ continuum limit. Downstream, dynamic_bracket_shape_continuum_limit multiplies the sampled dynamic-bracket sum by $n$ and passes to the integral of the continuum Dirac density; without uniform forward-density control the Riemann sum for $p\cdot q'$ would not close. The companion decoy frozen_continuum_density_differs_from_dynamic uses the same continuum density language to show the dynamic $G=1+q^2$ integrand is not the frozen-1 integrand (explicit mismatch $2\neq 1$ at $t=1$ for $q=\mathrm{id}$).
In the Seven Gaps gravity program this sits inside the Dirac hypersurface-deformation algebra continuum analysis: it justifies replacing discrete momentum-flux factors by $p q'$ under mesh refinement, which is the continuum content of the R2/R3 shape package. It does not bind bracket(HamDyn N)(HamDyn M) (still only at $n=2$) and does not flip gap-5 constraint recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.