planeWaveEdgeField_smul
plain-language theorem explainer
Rescaling a TT polarization matrix E by a real factor c leaves the plane-wave edge-field family unchanged up to amplitude reparametrization t ↦ c·t. Anyone auditing Gate A0 of the Normalization-Gated Schläfli Two-Jet protocol cites this to show polarization and amplitude normalizations are the same gauge. The proof is a one-line pointwise reduction through the linear scaling of the edge-class coefficient.
Claim. For every real scalar $c$, every $3\times 3$ real matrix $E$, every wavevector $k\in\mathbb{R}^3$, and every amplitude $t\in\mathbb{R}$, the plane-wave edge field built from the rescaled polarization $c\cdot E$ at amplitude $t$ equals the plane-wave edge field built from $E$ at amplitude $c\,t$: $\ell_e(c\cdot E,k,t)=\ell_e(E,k,c\,t)$ for every edge $e$.
background
This module audits scaling well-posedness of the fixed continuum TT Bloch-symbol target $-1/4$ (Crux-1(c), Gate A0 of the Normalization-Gated Schläfli Two-Jet protocol). The open claim ReggeTTContinuumIsotropyTarget assigns that fixed value on every TT polarization; a fixed number is meaningful only if rescaling the polarization cannot manufacture a contradiction.
The plane-wave family is $\ell_e(t)=\ell^2_{\mathrm{flat}}(e)+t,c_d(E),\cos(k\cdot x_{\mathrm{mid}})$, linear in the polarization matrix $E$ through the edge-class coefficient $c_d(E)=\sum_{ij}E_{ij}D_d^i D_d^j$ (the standard quadratic form $D^T E D$). Upstream, planeWaveEdgeField packages exactly that family, and polEdgeCoeff_smul records the elementary identity $c_d(c\cdot E)=c,c_d(E)$.
The module's convention audit confirms that both the edge coefficient and the Frobenius pin $\sum_{ij}E_{ij}^2=1$ sum over all ordered pairs, so the double-counting conventions are consistent; the scaling chain below then makes the fixed-value statement well-posed.
proof idea
Pointwise on edges via funext. Unfold the definition of the plane-wave edge field and rewrite the coefficient of the cosine by polEdgeCoeff_smul, which supplies $c_d(c\cdot E)=c,c_d(E)$. The remaining scalar identity $t\cdot(c,c_d(E))=(c,t)\cdot c_d(E)$ is discharged by ring. No geometric or lattice facts are needed beyond the already-proved linearity of the edge-class coefficient.
why it matters
This is step (b) of the Gate A0 scaling audit: it shows that polarization normalization and amplitude normalization are literally the same gauge. The immediate parent is planeWaveActionProfile_smul, the corollary that the Regge action profile of $c\cdot E$ at amplitude $t$ equals the original profile at amplitude $c,t$. That feeds the second-difference quadratic-form scaling by $c^2$ and ultimately TTBlochSymbolIs_smul, which records that the continuum TT Bloch symbol itself scales by $c^2$ under $E\mapsto c\cdot E$.
Together with the Frobenius pin in IsTTPolarization (only $c^2=1$ preserves the hypothesis class), the fixed numerical target $-1/4$ becomes a well-posed statement rather than a rescaling contradiction. In the broader QG full-theory campaign this closes the normalization gate before the continuum isotropy claim is attacked; it does not itself prove the $-1/4$ value.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.