sampledDynamicBracketSum_scaled_eq
plain-language theorem explainer
Multiplying the sampled dynamic-bracket mesh sum by the mesh cardinality n is exactly the same as inserting the forward-difference factor n·Δq into each summand. Anyone proving the rate-h continuum limit of the freestanding dynamic-bracket shape cites this identity. The proof is a one-line unfold-mul_sum-ring rearrangement.
Claim. For every natural number $n$ and every real functions $N,M,q,p$, the scaled mesh sum $n\cdot\sum_{k=0}^{n-1} W_k\,G_k\,\pi_{k+1}\Delta q_k$ equals $\sum_{k=0}^{n-1} W_k\,G_k\,\pi_{k+1}\,(n\Delta q_k)$, where $W_k=N(k/n)M((k+1)/n)-M(k/n)N((k+1)/n)$ is the discrete Wronskian, $G_k=1+(q(k/n))^2$ is the dynamic structure profile, $\pi_{k+1}=p((k+1)/n)$, and $\Delta q_k=q((k+1)/n)-q(k/n)$.
background
The module lands Wave C2 R4: the freestanding sampled-lapse Wronskian rate-$h$ residual that was left open in the weighted structure sum, packaged with the R2 lattice RHS shape and the R3 dynamic structure profile. The honest continuum object is the scaled sum $n\cdot\Sigma$, not the bare sum (which vanishes) and not an $n^2$ prefactor (which diverges).
The unscaled summand is the product of three pieces on the unit-interval mesh $k/n$: the discrete Wronskian $W_k=O(1/n)$ for $C^1$ lapses, the structure profile $G(x)=1+(q x)^2=O(1)$, and the raw momentum-flux $\pi_{k+1}\Delta q_k=O(1/n)$ for $C^1$ fields. Their product is $O(1/n^2)$ per site, so $n$ sites give a raw sum $O(1/n)$.
sampledDynamicBracketSum is the freestanding Riemann object carrying that lattice shape with non-periodic forward differences. It is deliberately not identified with bracket(HamDyn N)(HamDyn M), which exists only at $n=2$.
proof idea
Unfold the definition of the sampled sum, push the outer factor $n$ through the finite sum via mul_sum, then apply sum_congr sitewise. At each mesh index the remaining identity is pure ring arithmetic: $n\cdot(a\cdot(b\cdot\Delta q))=(a\cdot(b\cdot(n\cdot\Delta q)))$. No analytic hypotheses are used.
why it matters
This identity is the algebraic first step of dynamic_bracket_shape_continuum_limit, the true Riemann/rate-$h$ theorem that sends the scaled freestanding dynamic-bracket shape sums to $\int_0^1(NM'-MN')\cdot G\cdot(p\cdot q'),dt$ with phase-space-dependent structure $G=1+q^2$. Without moving $n$ inside the difference quotient, the summands do not match the continuum integrand's derivative factors.
In the Seven Gaps gravity program this is the honest continuum shape for the Dirac hypersurface-deformation density under dynamic structure. The ledger name dirac_algebra_continuum_limit remains free: the result does not bind the actual Hamiltonian bracket at general $n$, and it does not flip gap5_constraint_recovery (that still needs R6). The new analytic content consumed downstream is the Wronskian rate-$h$ tendsto, not a smearing-shape reach alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.