mesh_le_one
plain-language theorem explainer
On the uniform mesh of n bins, the right endpoint of bin k satisfies (k+1)/n ≤ 1 whenever k < n. Mean-value and interval-inclusion arguments for discrete Wronskians and forward differences cite this bound to keep sample points inside [0,1]. The proof is a one-line cast of Nat.succ_le_of_lt through div_le_one.
Claim. For natural numbers $n$ and $k$ with $k < n$, the real quotient satisfies $\frac{k+1}{n} \le 1$.
background
The module develops the continuum (rate-$h$) limit of the sampled-lapse Wronskian residual that appears in the dynamic structure bracket on a uniform partition of $[0,1]$. Sample points are $k/n$ and $(k+1)/n$ for $k \in {0,\ldots,n-1}$. Mean-value theorems place intermediate points in the open mesh intervals $((k/n),((k+1)/n))$, which must sit inside the closed unit interval where the continuum fields $N,M,q$ and the structure weight $G$ are controlled.
This lemma is the elementary right-endpoint bound: under the standing index hypothesis $k < n$, the upper mesh node never exceeds $1$. Sibling facts supply nonnegativity of the left node and the open-interval inclusion $I_{oo}(k/n,(k+1)/n)\subseteq I_{cc}(0,1)$. The module doc stresses that the honest scaled object is $n\cdot\sum$, converging to an integral involving $(NM'-MN')\cdot G\cdot(p\cdot q')$; keeping the mesh inside $[0,1]$ is prerequisite bookkeeping for those MVT applications.
proof idea
From $k < n$ one gets $0 < n$ after casting to $\mathbb{R}$. Then $\mathrm{div_le_one}$ reduces the claim to $k+1 \le n$, which is $\mathrm{Nat.succ_le_of_lt},hk$ transported by $\mathrm{exact_mod_cast}$. Pure arithmetic; no analysis lemmas.
why it matters
Feeds three local consumers: Ioo_mesh_subset_Icc (open mesh cell sits in $[0,1]$), discrete_wronskian_mvt (two MVTs for the discrete Wronskian of $C^1$ lapses), and forward_diff_mvt (scaled forward difference equals a derivative sample). Those lemmas underwrite wronskian_rate_h_tendsto, the rate-$h$ quadrature limit that the module packages into the dynamic-bracket shape continuum theorem.
In the Seven Gaps gravity program this is scaffolding arithmetic, not a physics claim: it keeps the lattice nodes inside the continuum domain so the $O(1/n)$ Wronskian and momentum-flux scalings are well-posed. It does not discharge the held-free ledger name dirac_algebra_continuum_limit (still blocked on general-$n$ HamDynN and periodic wrap).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.