sampledDynamicBracketSum
plain-language theorem explainer
Defines the freestanding Riemann sum that samples the dynamic Hamiltonian-bracket RHS shape on the unit-interval mesh k/n. Each summand is a discrete Wronskian of two lapses times the structure profile G=1+q² times a forward momentum-flux increment. Gravity continuum-limit arguments cite it as the object whose n-scaled version tends to the Dirac hypersurface density. The body is a direct finite sum, not a derived identity.
Claim. For $n\in\mathbb{N}$ and real functions $N,M,q,p$, set $$S_n(N,M,q,p)=\sum_{k=0}^{n-1}\bigl(N(k/n)M((k+1)/n)-M(k/n)N((k+1)/n)\bigr)\cdot G_q(k/n)\cdot\bigl(p((k+1)/n)\,(q((k+1)/n)-q(k/n))\bigr),$$ where $G_q(x)=1+(q(x))^2$ is the continuum dynamic structure profile. This is the non-periodic forward-difference mesh sample of the dynamic bracket RHS shape.
background
Module Wave C2 R4 packages the sampled-lapse Wronskian rate-$h$ residual that was left OPEN in the weighted structure sum tendsto analysis, together with the R2 lattice RHS shape and the R3 dynamic structure profile, into a continuum shape limit.
The structure factor here is the continuum shape of the concrete dynamic inverse metric along a field profile: $G(x)=1+(q(x))^2$. The discrete summand mirrors the lattice shape of the dynamic Hamiltonian bracket: a site Wronskian $W_k$, times $G_k$, times raw momentum flux $\pi_{k+1}\Delta q_k$. For $C^1$ data one has $W_k=O(1/n)$ and $\pi\Delta q=O(1/n)$, so each site is $O(1/n^2)$ and the raw $n$-site sum is $O(1/n)$; the honest continuum object is therefore the scaled sum $n\cdot S_n$.
Honesty note from the module: this freestanding Riemann object is not identified with $\mathrm{bracket}(\mathrm{HamDyn},N,\mathrm{HamDyn},M)$ at general $n$ (that bracket exists only at $n=2$, and the non-periodic mesh leaves a wraparound term). The ledger name for a full Dirac-algebra continuum limit is held free.
proof idea
Definitional: unfold to a Finset.sum over range n. At mesh point $k/n$ multiply three factors: the forward discrete Wronskian of the two lapse samples, the dynamic structure profile $1+(q(k/n))^2$, and the forward momentum-flux increment $p((k+1)/n)\cdot(q((k+1)/n)-q(k/n))$. No lemmas are applied; downstream proofs rewrite the scaled form $n\cdot S_n$ and pass to the continuum integrand.
why it matters
This is the named freestanding sum that the shape-only continuum theorem converges. That theorem states that $n\cdot S_n(N,M,q,p)$ tends to $\int_0^1 (NM'-MN'),G_q,(p,q')$, under $C^1$ lapses and $q$ and continuous $p$ on $[0,1]$. It is explicitly not a binding of the actual dynamic Hamiltonian bracket and does not claim the ledger slot dirac_algebra_continuum_limit.
Downstream, the scaled equality lemma rewrites $n\cdot S_n$ termwise; uniform Wronskian-error control uses it in the rate-$h$ argument; the binding module equates the periodic mesh sample (and thus the continuum lattice bracket) to this sum under 1-periodicity; and Gap5 residual DAG records the typed residual as exactly the tendsto statement for this scaled sum. In the Seven Gaps gravity program it supplies the R4 shape content (Wronskian rate-$h$ plus dynamic $G=1+q^2$) without closing full constraint recovery, which still needs R6.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.