sum_range_sq_sinDiff
plain-language theorem explainer
For every integer N>2, the sum of squared first differences of the unit-circle samples sin(2πk/N) equals exactly 2N sin²(π/N). Gravity analysts cite it when closing the discrete quadratic energy of the fixed witness field sin(2πx) on the periodic Freudenthal lattice. The proof expands each difference via the product-to-sum identity, then kills the residual cosine sum by a telescoping vanishing lemma.
Claim. For every natural number $N>2$, $$\sum_{k=0}^{N-1}\bigl(\sin(2\pi(k+1)/N)-\sin(2\pi k/N)\bigr)^2=2N\sin^2(\pi/N).$$
background
The module develops the action-level continuum limit of the frozen quadratic Regge-Hessian energy on the canonical periodic Freudenthal family (QG Phase 2b, panel-locked Test G stage 2). The fixed nonconstant C² witness is $f(x,y,z)=\sin(2\pi x)$, sampled onto the side-$N$ torus. After the stencil collapses, the discrete energy reduces to a one-dimensional first-difference sum along the free coordinate, times an $N^2$ factor from the two frozen coordinates and the stage-1 moment entry $A_0[0,0]=1+2\sqrt{2}+\sqrt{3}$.
The companion identity sum_cos_shifted_vanishes states that $\sum_{k<N}\cos((4k+2)\pi/N)=0$ for $N>2$, proved by writing $2\sin(2\pi/N)\cos(\cdot)$ as a pure sine telescope. That vanishing is the only nontrivial input beyond elementary trig algebra. The continuum target is defined independently as $\int_{[0,1]^3}\langle\nabla f,A_0\nabla f\rangle=A_0[0,0]\cdot 2\pi^2$, so the discrete closed form must match this rate as $N\to\infty$.
proof idea
For each summand apply $\sin a-\sin b=2\cos((a+b)/2)\sin((a-b)/2)$. The half-difference collapses to $\pi/N$ and the half-sum to $(2k+1)\pi/N$, so the squared difference is $4\sin^2(\pi/N)\cos^2((2k+1)\pi/N)$. Rewrite $\cos^2$ via the double-angle formula $\cos^2\theta=1/2+\cos(2\theta)/2$ to obtain the constant term $2\sin^2(\pi/N)$ plus a cosine of argument $(4k+2)\pi/N$.
Sum over $k\in{0,\ldots,N-1}$: the constant contributes $2N\sin^2(\pi/N)$; the cosine sum is exactly the hypothesis of sum_cos_shifted_vanishes, hence vanishes. A final ring cleanup yields the claimed identity. All field simplifications are elementary; no estimates or limits appear.
why it matters
Parent theorem scaledCanonicalEnergy_witness_closed_form rewrites the $\rho(N)$-normalized canonical energy of the sampled witness as $A_0[0,0]\cdot 2N^2\sin^2(\pi/N)$ by invoking this identity after the stencil reduction. That exact closed form is the discrete half of the stage-2 rate statement: the difference from the continuum target $A_0[0,0]\cdot 2\pi^2$ is then controlled by the elementary expansion $\sin(\pi/N)=\pi/N+O(N^{-3})$, giving the explicit constant $C=A_0[0,0]\cdot(2\pi)^4/24$.
Within the Recognition gravity campaign this is pure analysis scaffolding for the tensor-first anisotropic continuum limit; it does not touch the forcing chain (T0–T8), RCL, or the phi-ladder mass formula. It does discharge the trig half of the panel-locked observable that the scaled discrete energy converges at rate $O(1/N)$ to the continuum quadratic form. The pillar-2 path-sum flag remains red and is out of scope here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.