polEdgeCoeff_mul_left
plain-language theorem explainer
The edge-class coefficient of a polarization matrix is homogeneous of degree one under entrywise scaling: replacing each entry of E by c times that entry multiplies the coefficient by c. Continuum TT Bloch-symbol scaling arguments cite this as the first link in the Gate A0 chain. The proof unfolds the defining double sum and factors the scalar through both Finset sums by ring.
Claim. For any real scalar $c$, any real $3\times 3$ matrix $E$, and any edge-class index $d\in\{0,\ldots,6\}$, the edge-class coefficient satisfies $c_d\bigl((i,j)\mapsto c\,E_{ij}\bigr)=c\,c_d(E)$, where $c_d(E)=\sum_{i,j}E_{ij}D_d^i D_d^j$.
background
This module audits scaling well-posedness of the fixed continuum TT Bloch-symbol target $-1/4$ (Gate A0 of the Normalization-Gated Schläfli Two-Jet protocol in the Regge TT continuum-symbol program). The plane-wave edge family is linear in the polarization matrix $E$ through the edge-class coefficient, so $E\mapsto c\cdot E$ merely reparametrizes the same family.
The edge-class coefficient is defined by $c_d(E)=\sum_{i,j}E_{ij}D_d^i D_d^j$: it measures how a metric perturbation $E$ loads the squared length of displacement class $d$. The double sum runs over all ordered index pairs (the standard quadratic-form convention $D^T E D$), matching the Frobenius pin used in the TT-polarization predicate.
Upstream, the coefficient is the preflight definition that packages the displacement components $D_d$ against $E$. The present lemma isolates the entrywise-scaling form of its linearity before the scalar-action (•) packaging.
proof idea
Term-mode proof by unfolding the double-sum definition of the edge-class coefficient. Apply Finset.mul_sum to pull $c$ out of the outer sum, then again for the inner sum, with Finset.sum_congr at each level to reduce to the summand. The remaining identity $c\cdot(E_{ij}D_d^i D_d^j)=(c,E_{ij})D_d^i D_d^j$ is discharged by ring.
why it matters
First algebraic step of the Gate A0 scaling chain that makes the fixed-value continuum TT isotropy target well-posed. Downstream, the scalar-action form of the same identity is obtained by rewriting $c\bullet E$ as entrywise multiplication and applying this lemma; that form then feeds the plane-wave profile, second-difference, and Bloch-symbol scaling theorems (TTBlochSymbolIs_smul), which together show the symbol scales as $c^2$ under $E\mapsto c\cdot E$.
Combined with the Frobenius pin on TT polarizations (only $c^2=1$ preserves the hypothesis class), a fixed numerical value such as $-1/4$ is therefore coherent rather than contradictory. The module records that the double-counting conventions in the coefficient and the Frobenius norm are mutually consistent, so the lane proceeds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.