sample_mem_Icc
plain-language theorem explainer
For naturals k ≤ n, the mesh sample k/n lies in the closed unit interval [0,1]. Continuum quadrature and density-control lemmas in the Dirac-algebra rate-h module cite it to keep sample points inside the domain of continuous fields. The proof is a short case split on n = 0 versus n > 0, using mesh nonnegativity and div_le_one.
Claim. For natural numbers $k \le n$, the real sample $\frac{k}{n}$ belongs to the closed unit interval $[0,1]$.
background
The module builds the Wave C2 R4 continuum limit for the sampled-lapse Wronskian rate-$h$ residual of the dynamic structure bracket. Lattice points are the uniform mesh ratios $k/n$ on the unit interval, and continuous fields ($N$, $M$, $F$, $p$, $q$) are evaluated only on $\mathrm{Icc},0,1$.
The sole upstream fact is mesh nonnegativity: $0 \le k/n$ for all naturals $n,k$, from nonnegativity of casts under division. That supplies the lower endpoint of the closed interval; the upper endpoint $k/n \le 1$ is the content of this lemma under the hypothesis $k \le n$.
Local scaling context: discrete Wronskian and momentum-flux factors are each $O(1/n)$ for $C^1$ data, so the honest continuum object is the scaled sum $n\cdot\Sigma$, converging to an integral over $[0,1]$. Sample membership in that interval is therefore a standing domain obligation.
proof idea
Term-mode proof. The closed-interval membership is a pair of inequalities. The lower bound $0 \le k/n$ is exactly the sibling lemma mesh_nonneg. For the upper bound, case on $n$: if $n = 0$, substitute and simplify (both sides collapse); if $n > 0$, apply div_le_one at the positive cast of $n$, reducing to $k \le n$ after exact_mod_cast.
why it matters
Keeps every mesh abscissa inside the domain of the continuous structure and momentum profiles used by the rate-$h$ analysis. Downstream it is applied by the strict variant sample_mem_Icc_lt (for $k < n$), by the uniform forward-density control comparing scaled increments $n\Delta q$ to $p\cdot q'$, and by the main theorem wronskian_rate_h_tendsto (sampled-lapse Wronskian rate-$h$ quadrature limit).
That rate-$h$ limit is the new content packaged into dynamic_bracket_shape_continuum_limit. The freestanding ledger name dirac_algebra_continuum_limit remains held free pending a general-$n$ HamDynN binding and periodic wrap treatment; this lemma only discharges the elementary domain step on the unit mesh, not the open HamDyn identification or gap-5 recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.