TTBlochSymbolIs_smul
plain-language theorem explainer
The TT Bloch-symbol predicate is homogeneous of degree two under polarization rescaling: the symbol equals H on E if and only if it equals c²H on c·E, for any nonzero scalar c. Anyone citing the fixed-value continuum target −1/4 needs this equivalence to justify that the claim is not scale-ambiguous. The proof is a two-sided application of the one-direction scaling lemma, recovering the reverse arrow by rescaling with c⁻¹.
Claim. For any nonzero real scalar $c$, any $3\times 3$ real matrix $E$, any integer wavevector $m\in\mathbb{Z}^3$, and any real $H$, the continuum TT Bloch-symbol predicate holds for $(E,m,H)$ if and only if it holds for $(cE,\,m,\,c^2 H)$.
background
This module audits Gate A0 of the Normalization-Gated Schläfli Two-Jet protocol in the Regge TT continuum-symbol program. The open target asserts a fixed continuum TT Bloch-symbol value $-1/4$ on every transverse-traceless polarization. That fixed number is only meaningful if the statement cannot be rescaled into a contradiction.
The plane-wave edge family is linear in the polarization matrix $E$ through the edge-class coefficient $c_d(E)=\sum_{ij} E_{ij} D_d^i D_d^j$ (ordered-pair quadratic-form convention). Replacing $E\mapsto cE$ merely reparametrizes the same family by $t\mapsto ct$, so the second-difference quadratic form must scale by $c^2$. The predicate TTBlochSymbolIs packages that continuum symbol value; the present theorem records the exact quadratic transformation law as an equivalence.
Upstream, the one-direction companion TTBlochSymbolIs_smul_of already pushes the predicate forward under $E\mapsto cE$. Polarization structure and edge coefficients live in the preflight module (IsTTPolarization, polEdgeCoeff).
proof idea
Tactic proof by constructor on the biconditional.
Forward direction: apply the one-way lemma TTBlochSymbolIs_smul_of directly at scalar $c\neq 0$.
Reverse direction: given the predicate at $(cE,,c^2 H)$, apply the same one-way lemma at $c^{-1}\neq 0$ to the already-scaled data. Algebraic cleanup then restores the original pair: $c^{-1}\cdot(cE)=E$ by smul_smul and inv_mul_cancel₀, and $(c^{-1})^2\cdot(c^2 H)=H$ by field_simp. Rewrite those identities into the scaled hypothesis to finish.
why it matters
Gate A0 requires that the fixed-value target $-1/4$ be scaling-coherent before the continuum isotropy claim can be stated. This theorem is clause (2) of the assembled well-posedness result reggeTT_target_scaling_wellPosed: together with the Frobenius pin (frobeniusSq E = 1 on IsTTPolarization) and the polarization-class scaling law (IsTTPolarization(cE) iff $c^2=1$), it shows that quantifying a fixed symbol value over normalized TT polarizations is consistent, while an unnormalized fixed-value claim would be contradictory.
In the broader Recognition Science gravity lane this closes the normalization gate for the Regge TT continuum symbol, so later continuum-limit and isotropy work can cite a well-posed numerical target rather than a scale orbit. It does not itself evaluate the symbol or prove the $-1/4$ value; it only certifies that the target statement is not ill-posed under the polEdgeCoeff convention.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.