wronskian_cell_error_abs
plain-language theorem explainer
On each mesh cell the absolute gap between the discrete two-point Wronskian of lapses N,M and the scaled continuum density (N M'-M N')/n equals (1/n) times the absolute derivative-mismatch remainder at the mean-value points. Anyone proving the rate-h quadrature limit for sampled-lapse Wronskians cites this identity. The proof is pure algebra: substitute the cell mean-value hypothesis, expand the continuum Wronskian, and factor the positive mesh scale out of the absolute value.
Claim. Let $N,M:\mathbb{R}\to\mathbb{R}$, $n,k\in\mathbb{N}$ with $n>0$, and $c,d\in\mathbb{R}$. Suppose the discrete cell Wronskian equals the mean-value form $$N(k/n)M((k+1)/n)-M(k/n)N((k+1)/n)=(1/n)\bigl(N(k/n)M'(c)-M(k/n)N'(d)\bigr).$$ Then $$\bigl|\text{discrete Wronskian}-(1/n)\,W(N,M)(k/n)\bigr|=(1/n)\bigl|N(k/n)(M'(c)-M'(k/n))-M(k/n)(N'(d)-N'(k/n))\bigr|,$$ where $W(N,M)=NM'-MN'$ is the continuum Wronskian density.
background
The module closes Wave C2 R4: the sampled-lapse Wronskian rate-$h$ residual left open by weightedStructureSum_tendsto, packaged with the R2 lattice RHS shape and R3 dynamic structure profile. Scaling analysis shows each discrete Wronskian cell is $O(1/n)$ for $C^1$ lapses, so the honest continuum object is $n\cdot\sum$ converging to $\int (NM'-MN'),G,(p,q')$.
The continuum density used here is $W(N,M)(t)=N(t)M'(t)-M(t)N'(t)$. On the uniform mesh of width $1/n$, the two-point discrete Wronskian at site $k$ is compared to $(1/n)W(N,M)(k/n)$. The hypothesis is the mean-value rewriting of that discrete cell: increments of $M$ and $N$ are replaced by derivatives at intermediate points $c,d$.
Local mesh facts in the same file (nonnegativity of the step, sample points in $[0,1]$, etc.) support the surrounding rate-$h$ argument; this lemma isolates the absolute cell error once the mean-value form is granted.
proof idea
Two short steps. First form the signed cell error and rewrite it via the given mean-value equality hEq; unfold the continuum Wronskian definition and cancel by ring to obtain
$$\text{error}=(1/n)\bigl(N(k/n)(M'(c)-M'(k/n))-M(k/n)(N'(d)-N'(k/n))\bigr).$$
Second, take absolute values: cast $n>0$ to $\mathbb{R}$, apply abs_mul, and drop the absolute value on the positive factor $1/n$ by abs_of_pos. No analytic estimates enter; the identity is purely algebraic once the cell mean-value form is assumed.
why it matters
Feeds directly into THEOREM (A) of the module, wronskian_rate_h_tendsto: the sampled-lapse Wronskian rate-$h$ quadrature limit. That theorem is the new content of the dynamic-bracket shape continuum package; R3 smearing-shape reach alone does not contain it.
In the Recognition gravity chain this cell-error identity is the bookkeeping step that turns mean-value remainders into an $O(1/n)$ summand suitable for a Riemann-sum limit. The honest scaled object is $n\cdot\sum$ of discrete Wronskians times structure and momentum-flux factors, converging to the continuum integrand $\int W(N,M),G,(p q')$. The freestanding ledger name dirac_algebra_continuum_limit remains held free (HamDyn exists only at $n=2$; wraparound undischarged), but the rate-$h$ analysis itself is real and is consumed by the renamed shape theorem. Does not flip gap5_constraint_recovery (needs R6 as well).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.