polEdgeCoeff_smul
plain-language theorem explainer
The edge-class coefficient of a 3x3 polarization is homogeneous of degree one under real scalar multiplication of the matrix. Gravity analysts auditing Gate A0 of the Normalization-Gated Schläfli Two-Jet protocol cite it to start the scaling chain that makes a fixed continuum TT Bloch value well-posed. The proof rewrites the scalar action pointwise and hands off to the already-proved left-multiplication identity.
Claim. For every real scalar $c$, every real $3\times 3$ matrix $E$, and every edge-class index $d\in\{0,\ldots,6\}$, if $c_d(E)=\sum_{i,j} E_{ij} D_d^i D_d^j$ denotes the edge-class coefficient of $E$, then $c_d(c\cdot E)=c\, c_d(E)$.
background
In the Regge TT continuum-symbol program the polarization matrix $E$ loads each of seven lattice edge-displacement classes through the quadratic form
$c_d(E)=\sum_{i,j} E_{ij} D_d^i D_d^j$
(the standard $D^\top E D$ convention, summing over all ordered pairs). That coefficient is exactly polEdgeCoeff from the preflight module.
This audit module is Gate A0 of the panel-locked protocol "Normalization-Gated Schläfli Two-Jet". The open target claims a fixed continuum TT Bloch value $-1/4$ on every TT polarization. A fixed number is meaningful only if rescaling $E\mapsto c\cdot E$ does not produce a contradictory family of plane-wave edge fields; the first algebraic fact needed is that $c_d$ itself scales linearly.
The sibling lemma already records the same identity written with pointwise multiplication rather than the • scalar action. The present statement is the • packaging used by the plane-wave family constructors.
proof idea
Term-mode, three steps. First observe that the scalar action on matrices is definitionally pointwise multiplication: $(c\bullet E){ij}=c,E{ij}$. Rewrite the goal with that identity. The resulting equality is exactly the sibling left-multiplication lemma polEdgeCoeff_mul_left, which is applied directly. No summation or displacement arithmetic is reopened.
why it matters
This is clause (a) of the Gate A0 scaling audit. It is the first link in the chain that shows the plane-wave edge-field family is merely reparametrized under $E\mapsto c\cdot E$ (amplitude $t\mapsto c,t$), so polarization normalization and amplitude normalization are the same gauge.
The sole recorded consumer is planeWaveEdgeField_smul, whose doc-comment states that rescaling the polarization "reparametrizes the SAME plane-wave edge-field family by $t\mapsto c\cdot t$". That fact, together with quadratic scaling of the second-difference form and the Frobenius pin in IsTTPolarization, makes the fixed-value claim $-1/4$ on the continuum TT Bloch symbol well-posed rather than contradictory. It sits inside the QG full-theory Crux-1(c) lane, not the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.