periodicSampledDynamicBracketSum
plain-language theorem explainer
Defines the periodically sampled dynamic-bracket sum on an n-site mesh: each cell multiplies the discrete lapse commutator by the continuum structure factor and a wrap-aware finite-difference jump in the field, with successor of site n-1 taken at 0 rather than at 1. Continuum-limit and Dirac-algebra binding proofs in the SevenGaps gravity stack cite it as the explicit Riemann-sum shape of the lattice Poisson bracket. The body is a pure finite sum, not a derived identity.
Claim. For $n\in\mathbb{N}$ and real maps $N,M,q,p$, set $\sigma_n(k)=0$ if $k+1=n$ and $k+1$ otherwise, and $G_q(x)=1+(q(x))^2$. Then $$\sum_{k=0}^{n-1}\bigl(N(k/n)M(\sigma_n(k)/n)-M(k/n)N(\sigma_n(k)/n)\bigr)\,G_q(k/n)\,p(\sigma_n(k)/n)\bigl(q(\sigma_n(k)/n)-q(k/n)\bigr).$$
background
Module setting is Wave C2 R4 repair (Steps 3–4): bind the freestanding Riemann shape of the dynamic bracket to the genuine lattice Poisson bracket of the discrete dynamic Hamiltonians, then land the ledger terminal continuum limit for 1-periodic $C^1$ data.
The wrap-successor $\mathrm{wrapSucc},n,k$ sends $n-1\mapsto 0$ and otherwise $k\mapsto k+1$, matching successor on $\mathbb{Z}/n\mathbb{Z}$. The non-periodic mesh would sample the last cell at $1$; the periodic mesh samples at $0$. The continuum structure profile is the model shape of the concrete dynamic inverse metric along a field: $G_q(x)=1+(q(x))^2$. The ambient Poisson bracket on phase space is the standard sum of mixed $q$- and $p$-partials; structure theorems place the structure factor at the left split point of each bond, which this sum mirrors by evaluating $G_q$ at $k/n$.
proof idea
Pure definitional sum over range n. Each summand is the product of three blocks: the discrete lapse commutator $N(k/n)M(\sigma(k)/n)-M(k/n)N(\sigma(k)/n)$ with wrap-successor $\sigma$; the structure profile $G_q(k/n)$; and the momentum-weighted field jump $p(\sigma(k)/n),(q(\sigma(k)/n)-q(k/n))$. No lemmas are applied; the expression is the explicit RHS used by later unfoldings.
why it matters
This is the periodic mesh form that the binding theorems identify with the lattice bracket. Downstream, bracket_HamDynN_eq_periodicSampled states that at continuum samples the general-$n$ dynamic bracket equals this sum (definitional unfolding of the HamDynN–HamDynN bracket identity). continuumLatticeBracket_eq_periodic equates the continuum-lattice bracket wrapper to the same sum. periodicSampled_eq_sampled_of_periodic then shows that for 1-periodic data the wrap mesh agrees with the non-periodic mesh (last-cell samples at $1$ equal samples at $0$), so the freestanding Riemann shape and this periodic form coincide. Together they close Steps 3–4 toward the ledger terminal dirac_algebra_continuum_limit for 1-periodic $C^1$ data in the SevenGaps gravity stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.