deficit_planeWave_zero
plain-language theorem explainer
Along any plane-wave edge-length family, every hinge deficit vanishes at amplitude zero. Gravity analysts cite this when killing the first-variation integrand of the Regge action at flat. The proof is a two-line reduction: zero amplitude is the flat edge field, and flat fields have zero deficit by the Stage-1 kernel theorem.
Claim. For any polarization matrix $E:\mathbb{R}^{3\times 3}$, wavevector $k\in\mathbb{R}^3$, and periodic edge $e$ on the $N^3$ Freudenthal torus, the hinge deficit of the plane-wave edge-length field at amplitude $t=0$ is zero: $\delta_e\bigl(\ell^{\mathrm{pw}}(E,k;0)\bigr)=0$.
background
This module is Gate A2 of the Normalization-Gated Schläfli Two-Jet protocol in the Regge TT continuum-symbol program. It studies the true Regge action profile $S(t)$ along plane-wave edge-length deformations of a flat periodic triangulation, aiming to show the first variation vanishes at flat and to extract a Schläfli-reduced second variation with no arccos second derivatives.
A PeriodicEdge is a positive-displacement edge on the $N\times N\times N$ Freudenthal torus (base vertex plus one of seven cube displacements). The deficit at a hinge is the classical angular defect $2\pi-\sum\theta$. The map deficitOfField evaluates that defect on every edge of a length assignment. The plane-wave family planeWaveEdgeField N E k t deforms edge lengths by a polarized plane wave of amplitude $t$; at $t=0$ it collapses to the flat (constant) edge field.
Upstream, Stage-1 already proved that every deficit of the flat edge field is zero (deficitOfField_flatEdgeField). The present statement merely threads that kernel fact through the plane-wave family at zero amplitude.
proof idea
Two-step rewrite. First apply planeWaveEdgeField_zero_amplitude, which identifies the plane-wave edge field at amplitude $0$ with the flat edge field. Then invoke deficitOfField_flatEdgeField N e, the Stage-1 kernel theorem that every hinge deficit of the flat assignment vanishes. No geometry is re-proved here; the family is only specialized at $t=0$.
why it matters
Gate A2(a) needs the first variation of the plane-wave Regge profile to vanish at flat. The first-variation integrand splits into a deficit group $\sum (\ell'_e/(2\sqrt{\ell_e}))\delta_e$ and a Schläfli group $\sum\sqrt{\ell_e},\delta'_e$. This lemma kills every $\delta_e$ factor at $t=0$, so the deficit group dies; the Schläfli group dies separately by the pathwise Schläfli identity.
Immediate parents are firstVariationIntegrand_zero (the full integrand vanishes at flat because both groups die) and hasDerivAt_reducedFirstVariation_flat (when differentiating the reduced first variation, product-rule terms carrying the flat deficit drop out, leaving only $\sum \ell'_e(0),\delta'_e(0)$). Together these feed trueReggeAction_firstVariation_flat_eq_zero and the Schläfli-reduced second-variation formula of Gate A2(b). In the broader RS gravity lane this is the discrete flat-background kernel step before continuum-symbol extraction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.