sampledLapse
plain-language theorem explainer
Pointwise sampling of a continuum lapse $N:\mathbb{R}\to\mathbb{R}$ onto the cyclic lattice $\mathbb{Z}/n\mathbb{Z}$: site $j$ receives $N(j/n)$. Gravity continuum-limit arguments cite it to feed lattice Hamiltonians $\mathrm{HamDynN}$ from smooth data. The body is a one-line lambda, pure definitional evaluation at normalized coordinates.
Claim. For $n\in\mathbb{N}$ with $n\neq 0$ and a continuum lapse $N:\mathbb{R}\to\mathbb{R}$, the sampled lapse is the map $\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$ sending each residue class $j$ to $N\bigl((j\bmod n)/n\bigr)$.
background
This module closes Wave C2 R4 repair steps 3–4: it binds the freestanding Riemann-shape sum sampledDynamicBracketSum to the genuine lattice Poisson bracket of dynamic Hamiltonians after a periodic wrap on $\mathbb{Z}/n\mathbb{Z}$, then lands the ledger terminal continuum limit for 1-periodic $C^1$ data.
A continuum lapse $N$ is a real function of a continuous coordinate. Lattice dynamics need a discrete profile on sites ${0,\ldots,n-1}$. The sampling map evaluates $N$ at the normalized mesh points $k/n$. On the cyclic group the successor of $n-1$ wraps to $0$; for 1-periodic fields the non-periodic sample at $1$ agrees with the periodic sample at $0$, so the two mesh conventions coincide.
Sibling sampledPhasePoint does the same for phase-space coordinates $(q,p)$. Downstream, HamDynN of a sampled lapse is the lattice Hamiltonian whose bracket is compared to the continuum structure factor.
proof idea
Pure definition: the body is the lambda $j\mapsto N((j.\mathrm{val}:\mathbb{R})/n)$. No lemmas, no tactics. The NeZero n instance guarantees the denominator is admissible and that ZMod n is well-formed for the lattice carrier.
why it matters
Without a canonical continuum-to-lattice sampling of the lapse, the dynamic bracket cannot be stated on mesh data. This def is the input channel for three local parents: continuumLatticeBracket (lattice bracket on continuum samples), bracket_HamDynN_eq_periodicSampled (definitional equality of the general-$n$ dynamic bracket with the periodic sampled sum), and dirac_algebra_continuum_limit_hamDynN (the unpacked continuum-limit statement for explicit HamDynN when $n>0$).
Module doc places it in the wrap-treatment story: true structure-factor placement from bracket_HamDynN_HamDynN puts $g$ at the left split $j$, matching dynamicStructureProfile q (k/n). That equality, once the sampling is fixed, is what lets the ledger terminal dirac_algebra_continuum_limit fire for 1-periodic $C^1$ fields. In the broader Seven Gaps gravity stack this is plumbing between continuum Recognition dynamics and the discrete Dirac-algebra side, not a forcing-chain landmark itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.