edgeCoeff
plain-language theorem explainer
Affine slope of one plane-wave edge length on the periodic Freudenthal torus: polarization factor times cosine of the midpoint Bloch phase. Gravity analysts cite it whenever the Regge action profile needs a closed-form edge velocity at flat. Pure definitional product of the preflight polarization coefficient and the midpoint-phase cosine; no proof obligations.
Claim. For a strain $E:\mathbb{R}^3\to\mathbb{R}^3\to\mathbb{R}$, wavevector $k\in\mathbb{R}^3$, and positive-displacement periodic edge $e$ with displacement $d_e$, the edge coefficient is $c_e=\mathrm{pol}(E,d_e)\cdot\cos\bigl(k\cdot x_{\mathrm{mid}}(e)\bigr)$, the affine slope in the plane-wave family $\ell_e(t)=\ell^2_{\mathrm{flat}}(e)+t\,c_e$. On matched tet slots this agrees definitionally with the plane-wave tet velocity.
background
Module setting is Gate A2 of the panel-locked "Normalization-Gated Schläfli Two-Jet" protocol in the Regge TT continuum-symbol program (Crux-1(c)). The ambient geometry is the periodic Freudenthal torus: a PeriodicEdge is a base vertex plus one of seven positive cube displacements. Plane-wave edge lengths are the affine family $\ell_e(t)=\ell^2_{\mathrm{flat}}(e)+t\cdot c_d\cdot\cos(k\cdot(x+D_d/2))$, with midpoint convention fixed by the C10 probe.
Upstream, edgeMidpointPhase is exactly that Bloch phase $k\cdot(x+D_d/2)$, and polEdgeCoeff supplies the polarization factor of $E$ along the edge displacement. The first-derivative gate (ReggeTTDerivativeGate) is reused, never re-proved; this coefficient is the scalar that makes every primed edge object in the action profile an explicit closed form.
proof idea
One-line definitional product: multiply the preflight polarization coefficient of $E$ on the edge displacement by the real cosine of the midpoint Bloch phase of $(k,e)$. No tactics, no lemmas discharged.
why it matters
Supplies the scalar $c_e$ in the closed-form sqrt-hinge derivative $L'_e(t)=c_e/(2\sqrt{\ell_e(t)})$, which is the next sibling definition and the building block of hasDerivAt_planeWaveActionProfile. That derivative feeds Gate A2(a) (first variation of the true Regge action vanishes at flat) and Gate A2(b) (Schläfli-reduced second variation with no arccos second derivatives). The pathwise Schläfli kill deletes the entire $\sum_e\sqrt{\ell_e},\delta'_e$ group near $t=0$; $c_e$ is what remains in the surviving first group after flat deficits vanish. Name-collides with the unrelated free-chain coefficient in CircleWindingChain; only the gravity uses (edge sqrt derivatives, slot contributions, deficit derivatives) are in scope here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.