wrapSucc
plain-language theorem explainer
Wrap-successor on the discrete circle {0,…,n−1} sends the last index to 0 and every other index to its ordinary successor. Gravity continuum-binding proofs cite it to sample 1-periodic fields at the ZMod-n successor rather than at the non-periodic mesh point 1. The body is a one-line if-then definition.
Claim. For natural numbers $n$ and $k$, the wrap-successor is $0$ when $k+1=n$, and $k+1$ otherwise. On the index set $\{0,\ldots,n-1\}$ this is the map $n-1\mapsto 0$ and $k\mapsto k+1$ for $k<n-1$.
background
The module repairs Steps 3–4 of the Wave C2 R4 continuum binding: it equates the freestanding Riemann-shape sum sampledDynamicBracketSum with the genuine lattice bracket of two HamDynN Hamiltonians after a periodic wrap treatment, then lands the ledger terminal for 1-periodic $C^1$ data.
On $\mathrm{ZMod},n$, site $n-1$ has successor $0$. A non-periodic mesh would sample the last cell at $(k+1)/n=1$; the periodic mesh samples at $0$. For 1-periodic fields those two evaluations agree, so the periodic sampled dynamic bracket sum equals the ordinary sampled sum. Wrap-successor is the pure index arithmetic that implements that last-cell wrap.
True structure-factor placement from the HamDynN bracket identity puts the structure profile $g$ at the left split point $j$, matching the dynamic structure profile at $k/n$.
proof idea
Pure definitional if-then: if $k+1=n$ return $0$, else return $k+1$. No lemmas are applied; downstream lemmas unfold this definition and case-split on the same equality.
why it matters
This index map is the sole wrap primitive for the periodic sampled RHS. It is used definitionally inside the periodic sampled dynamic bracket sum (last cell samples at $0$, not $1$), and is the target of the comparison lemmas that relate wrap-successor to $\mathrm{ZMod},n$ successor valuation and prove it stays strictly below $n$.
Those facts feed the theorem that, at continuum samples, the general-$n$ dynamic bracket equals the periodic sampled sum by definitional unfolding of the HamDynN bracket identity. That equality is the bridge from freestanding Riemann shape to genuine lattice bracket, closing the continuum-binding step that lands the Dirac-algebra continuum-limit terminal for 1-periodic $C^1$ data in the Seven Gaps gravity stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.