mesh_step
plain-language theorem explainer
Consecutive uniform mesh abscissae on the unit interval differ by exactly the reciprocal mesh size: (k+1)/n − k/n = 1/n in ℝ. Discrete mean-value and forward-difference lemmas in the sampled Wronskian continuum limit cite this identity whenever they convert a two-point increment into a factor 1/n. The proof is a one-line rewrite of successor cast, additivity of division, and left cancellation.
Claim. For all natural numbers $n$ and $k$, the real identity $\frac{k+1}{n} - \frac{k}{n} = \frac{1}{n}$ holds (with the usual coercion of naturals into $\mathbb{R}$).
background
The module develops the continuum (rate-$h$) limit of the sampled-lapse Wronskian that appears in the dynamic structure bracket on a uniform partition of $[0,1]$. Mesh points are the rationals $k/n$ for $k=0,\ldots,n$, and every discrete difference quotient is written against the adjacent pair $k/n$ and $(k+1)/n$.
The local scaling analysis records that a $C^1$ discrete Wronskian is $O(1/n)$ per site; that $O(1/n)$ is precisely the mesh step. Downstream mean-value statements therefore need the exact algebraic identity that the abscissa gap equals $1/n$, not merely an asymptotic bound.
No deeper Recognition-Science structure (J-cost, $\phi$-ladder, eight-tick) enters here: the lemma is pure real arithmetic on the partition used by the quadrature-limit arguments.
proof idea
One-line rewrite wrapper. Coerce the successor via Nat.cast_succ so $(k+1:\mathbb{N})$ becomes $(k:\mathbb{R})+1$, split the sum in the numerator by add_div, then cancel the common $k/n$ term with add_sub_cancel_left, leaving $1/n$.
why it matters
Feeds four continuum-limit lemmas in the same module: discrete_wronskian_mvt (two mean-value applications on each mesh interval), forward_diff_mvt (scaled forward difference equals a derivative sample), forward_density_uniform (uniform control of scaled forward density versus $p\cdot q'$), and the headline wronskian_rate_h_tendsto (sampled-lapse Wronskian rate-$h$ quadrature limit).
That rate-$h$ theorem is the new content packaged into dynamic_bracket_shape_continuum_limit (Wave C2 R4). The module explicitly holds the ledger name dirac_algebra_continuum_limit free pending a general-$n$ HamDyn binding; the mesh-step identity itself is unconditional arithmetic and does not touch that honesty gap. It does not engage T0–T8, RCL, or the $\alpha$ band; it is infrastructure for the gravity seven-gaps continuum analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.