ttWitnessPolarization
plain-language theorem explainer
Pins the standard TT witness polarization matrix E = diag(1,-1,0)/√2 used by the sympy Regge diagnostic and by every Gate C-A3 witness-level theorem. Gravity analysts cite it whenever they evaluate hinge or assembled constant blocks at the reported TT mode with k = e_z. Pure definition by cases on the nine matrix entries; no proof obligation.
Claim. The reported transverse-traceless witness polarization is the real $3\times 3$ matrix $E$ with $E_{00} = 1/\sqrt{2}$, $E_{11} = -1/\sqrt{2}$, and all other entries zero; equivalently $E = \mathrm{diag}(1,-1,0)/\sqrt{2}$.
background
Gate C-A3 of the QG full-theory campaign (Paper C / Pillar 1, Lane C) closes the hinge-aware zero mode for the Regge TT symbol. The same-day sympy diagnostic found that the stencil-only constant block does not vanish under TT: its residual at the reported witness is $-\pi(\sqrt{2}+4)/8$. The assembled quadratic does vanish, because the hinge contribution equals that residual and enters with a relative minus sign.
The witness itself is the pair $(E,k)$ with polarization $E=\mathrm{diag}(1,-1,0)/\sqrt{2}$ and wave vector $k=e_z$. Downstream lemmas check that $E$ is symmetric, traceless, transverse to $k$, and Frobenius-normalized (a genuine TT polarization), then evaluate the seven edge-class coefficients $c_d(E)$ that feed the hinge/edge-diagonal block.
This definition is the concrete matrix that every such evaluation plugs in; it matches the diagnostic report verbatim so that kernel statements and external numerics refer to the same object.
proof idea
Definition by exhaustive pattern match on $(i,j)\in\mathrm{Fin},3\times\mathrm{Fin},3$. The diagonal entries $(0,0)$ and $(1,1)$ receive $\pm 1/\sqrt{2}$; every off-diagonal and the $(2,2)$ slot is zero. No lemmas, no tactics.
why it matters
This is the fixed witness that makes Gate C-A3 checkable in the kernel. Four local theorems consume it: ttWitness_isTT certifies it is a genuine TT polarization for $k=e_z$; ttWitness_polEdgeCoeff evaluates the seven edge-class coefficients exactly as $(1/\sqrt{2},-1/\sqrt{2},0,0,1/\sqrt{2},-1/\sqrt{2},0)$; hinge_cancels_recorded_residual shows the hinge/edge-diagonal block at this $E$ equals the recorded stencil-only residual $-\pi(\sqrt{2}+4)/8$; and assembled_witness_split pins the assembly convention $\mathrm{assembled}(E_w)=\mathrm{hinge}(E_w)-\mathrm{stencilOnlyConstantWitnessResidual}$ with both sides zero.
Without a single named matrix, those equalities could silently drift from the diagnostic. The definition therefore anchors the zero-mode headline (assembled constant block vanishes at the TT witness) to the external report.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.