dynamic_bracket_shape_continuum_limit
plain-language theorem explainer
Scaled freestanding dynamic-bracket shape sums converge, as mesh size 1/n → 0, to the continuum Dirac hypersurface-deformation density with structure factor G = 1 + q². Anyone citing the Gap-5 continuum Dirac algebra or the Wave C2 R4 residual closure needs this rate-h Riemann limit. The proof splits the scaled sum into a Wronskian rate-h main term plus a uniformly controlled density error that vanishes in the limit.
Claim. Let $N,M,q:\mathbb{R}\to\mathbb{R}$ be $C^1$ and let $p$ be continuous on $[0,1]$. Then $n$ times the sampled dynamic-bracket shape sum over the uniform $n$-mesh tends, as $n\to\infty$, to $\int_0^1 (N M'-M N')\,G(q)\,(p q')\,dt$, where $G(q)=1+q^2$ is the dynamic structure profile and the integrand is the continuum Dirac density.
background
Wave C2 R4 packages the sampled-lapse Wronskian rate-$h$ residual that was left open in the weighted structure-sum analysis. The freestanding object is the mesh sum whose summands have the lattice shape of the dynamic Hamiltonian bracket: discrete Wronskian $W_k=N(k/n)M((k+1)/n)-M(k/n)N((k+1)/n)$, structure $G_k=1+q(k/n)^2$, and raw momentum flux $\pi_{k+1}\Delta q_k$. For $C^1$ data each factor scales so the product per site is $O(1/n^2)$; $n$ sites give a raw sum $O(1/n)$, so the honest continuum object is $n\cdot\Sigma$, not a bare or $n^2$-scaled sum.
The continuum target is the interval integral of the continuum Dirac density: continuum Wronskian $(NM'-MN')$ times dynamic structure profile times continuum momentum flux $p q'$. Continuity of the structure profile on $[0,1]$ follows from $C^1$ of $q$; the product with momentum flux is continuous on the compact interval once $p$ is continuous and $q$ is $C^1$.
Honesty note from the module: this freestanding Riemann object is not identified with bracket(HamDyn N, HamDyn M) at general $n$ (that binding exists only at $n=2$, and non-periodic mesh leaves a wrap term). The ledger name for the full Dirac-algebra continuum limit is held free pending periodic general-$n$ binding.
proof idea
Establish continuity on $[0,1]$ of the dynamic structure profile and of its product with continuum momentum flux. Apply the upstream Wronskian rate-$h$ theorem to that continuous weight, obtaining convergence of the main scaled sum to $\int W\cdot G\cdot(p q')$.
Define a per-cell density error (forward difference flux minus continuum flux) and the structure-weighted error. Bound the structure profile on $[0,1]$, then invoke forward-density uniform control to show the weighted errors are uniformly small for large $n$. Feed that uniform error into the Wronskian-times-uniform-error vanishing lemma.
Algebraically rewrite the scaled sampled shape sum as main weighted Wronskian sum plus error sum (ring after unfolding the scaled-sum identity). Add the two Tendsto statements and match the limit integral to the continuum Dirac density by interval-integral congruence (definitional after unfolding density abbreviations).
why it matters
Closes the Wave C2 R4 freestanding shape residual in the Gap-5 constraint residual DAG: the typed residual for dynamic bracket shape continuum is discharged by direct application of this theorem. Downstream, the repaired ledger terminal dirac_algebra_continuum_limit is proved by Step-3 HamDynN binding, periodicity, and this shape limit; the scaled continuum lattice bracket equals the scaled freestanding sum under 1-periodicity, so the shape theorem is the analytic core of the binding.
Also feeds the explicit decoy that frozen continuum density differs from the dynamic $G=1+q^2$ integrand (e.g. value 2 vs 1 at a standard test point), separating dynamic structure from frozen-1 smearing. Does not by itself flip full gap-5 constraint recovery (needs R6 as well). In the Recognition gravity stack this is the continuum Dirac hypersurface-deformation density limit for dynamic structure, not a claim about Newton's $G$ or the forcing chain T0–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.