mesh_nonneg
plain-language theorem explainer
Mesh sample points k/n on the unit interval are nonnegative as reals. Sampling and mean-value lemmas in the Dirac-algebra continuum module cite it to place lattice nodes inside Icc 0 1. The proof is a one-line wrapper of div_nonneg on the two Nat.cast nonnegativity facts.
Claim. For all natural numbers $n$ and $k$, the real quotient satisfies $0 \le k/n$.
background
This module develops the continuum (rate-$h$) limit of the sampled-lapse Wronskian residual that appears in the dynamic structure bracket. Lattice sites are the uniform mesh points $k/n$ for $k < n$, and continuum comparison is on the closed unit interval $[0,1]$.
Nonnegativity of those sample abscissae is the lower half of membership in $\mathrm{Icc},0,1$. Sibling facts supply the matching upper bound and the open-interval nesting used by mean-value arguments. The module's honesty note keeps the freestanding ledger name for a full Dirac-algebra continuum limit free; the rate-$h$ analysis itself is real and consumes these mesh lemmas.
proof idea
One-line wrapper: apply div_nonneg to Nat.cast_nonneg on the numerator cast and on the denominator cast. No case split on $n=0$ is needed; the real division convention makes the inequality hold uniformly.
why it matters
Local plumbing for the Wave C2 R4 continuum package. Downstream, sample_mem_Icc and Ioo_mesh_subset_Icc use it to keep mesh nodes and MVT intermediate points inside $[0,1]$. Those feed discrete_wronskian_mvt (discrete Wronskian via two mean-value applications) and forward_diff_mvt, which underwrite the sampled-lapse Wronskian rate-$h$ quadrature limit wronskian_rate_h_tendsto and the renamed shape theorem dynamic_bracket_shape_continuum_limit.
It does not close the held-free ledger name dirac_algebra_continuum_limit (still needs general-$n$ HamDyn binding and periodic wrap). It is pure real-arithmetic support for the gravity seven-gaps continuum track, not a Recognition forcing-chain step (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.