forward_diff_mvt
plain-language theorem explainer
On each unit-interval mesh bin $[k/n,(k+1)/n]$, a $C^1$ scalar $q$ has an interior point where the scaled forward increment $n\,(q_{k+1}-q_k)$ equals $q'$. Analysts of the rate-$h$ continuum bracket and forward-density control cite it as the local MVT bridge from discrete increments to derivatives. The proof is classical slope-equals-derivative plus the mesh step identity $b-a=1/n$.
Claim. Let $q:\mathbb{R}\to\mathbb{R}$ be continuously differentiable of order one. For integers $n>0$ and $0\le k<n$, there exists $c\in\bigl(\frac{k}{n},\frac{k+1}{n}\bigr)$ such that $n\bigl(q\bigl(\frac{k+1}{n}\bigr)-q\bigl(\frac{k}{n}\bigr)\bigr)=q'(c)$.
background
The module lands the sampled-lapse Wronskian rate-$h$ residual for the dynamic bracket shape continuum. Lattice summands of the discrete Dirac/HamDyn bracket scale as $O(1/n^2)$ per site; the honest continuum object is therefore the scaled sum $n\cdot\Sigma$, converging to an integral of continuum Wronskian times structure profile times momentum flux $p\cdot q'$.
Local mesh facts fix the partition of $[0,1]$ into bins of width $1/n$: left endpoint $k/n$ is nonnegative, right endpoint $(k+1)/n\le 1$ when $k<n$, and the open bin is strictly ordered. The continuum Wronskian density is $N M'-M N'$. Forward increments of a $C^1$ field $q$ must be rewritten as derivatives before comparing discrete flux $p_{k+1},n\Delta q_k$ to the continuum density $p,q'$.
Upstream mesh lemmas supply $a<b$, $b-a=1/n$, and the closed-bin inclusion in $[0,1]$. The classical mean-value identity (slope equals derivative on an open subinterval) is then available once $q$ is known differentiable and continuous on the closed bin.
proof idea
Name the bin endpoints $a=k/n$ and $b=(k+1)/n$. Strict inequality $a<b$ is mesh_lt. The closed interval $[a,b]$ sits inside $[0,1]$ by chaining mesh_nonneg and mesh_le_one through le_trans. ContDiff order one yields global differentiability and continuous-on-$[a,b]$; restrict to DifferentiableOn the open bin.
Apply Mathlib exists_deriv_eq_slope to obtain $c\in(a,b)$ with $q'(c)=(q(b)-q(a))/(b-a)$. Substitute mesh_step, which gives $b-a=1/n$, and clear the reciprocal by field simplification using $n\neq 0$. The displayed identity is exactly the scaled forward difference.
why it matters
This is the local analytic step behind uniform forward-density control: forward_density_uniform compares $p((k+1)/n)\cdot n\Delta q_k$ to $p(k/n),q'(k/n)$ and needs the MVT representation of the scaled increment on every bin. The same identity feeds the explicit decoy frozen_continuum_density_differs_from_dynamic, which separates the dynamic $G=1+q^2$ continuum density from a frozen-structure integrand.
In the module honesty note, the rate-$h$ analysis (Wronskian tendsto plus forward-density control) is the real content retained while the ledger name dirac_algebra_continuum_limit stays free pending general-$n$ HamDyn binding. The theorem does not touch gap5 constraint recovery or the eight-tick/T8 dimension chain; it is pure real-analysis scaffolding for the gravity SevenGaps continuum shape limit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.