IsTT_sub
plain-language theorem explainer
If two 4×4 matrices are transverse-traceless (TT) relative to the same wave mode, their difference is TT. Gravity analysts cite this when polarizing the midpoint Bloch first variation on H+K and H−K in the Euclidean weak-field sector. The proof is a three-field constructor applying the component closures under subtraction.
Claim. Let $m$ be a 4D wave mode and let $H,K$ be $4\times 4$ real matrices. If $H$ and $K$ are each symmetric, traceless, and transverse to $m$, then $H-K$ is likewise symmetric, traceless, and transverse to $m$.
background
The module works in the Euclidean weak-field TT sector of the closed 4D midpoint Bloch continuum face. Matrices live in Mat4 and modes in Wave4 (both aliases of the Regge 4D continuum preflight types). A matrix is TT relative to a mode when it is simultaneously symmetric, traceless, and transverse to that mode; those three predicates are the fields of the TT structure used here.
The ambient goal is the directional first variation of the exact midpoint Bloch symbol, transported to the torus-normalized continuum face via the banked SRS-to-EH convergence on sums and differences, then polarized. Componentwise algebraic closure of the TT cone under linear operations is therefore a prerequisite, not a dynamical claim.
Upstream cost and bridge constants (H, dimensionless $K=\varphi^{1/2}$, etc.) appear in the import graph of the gravity stack but are not used in this lemma; the argument is pure linear algebra on the TT triple.
proof idea
Term-mode proof: build the TT triple for $H-K$ by applying three sibling closures to the corresponding projections of the hypotheses.
- Symmetry:
IsSymmetric_subon the first fields ofhHandhK. - Tracelessness:
IsTraceless_subon the nested second fields. - Transversality:
IsTransverse_subon the remaining fields.
No rewriting or analysis; just the structure constructor.
why it matters
Feeds the headline continuum result continuumTTFirstVariation_closed: the torus-normalized midpoint first variation tends to $-\tfrac14$ times the Frobenius pairing, under TT hypotheses on both $H$ and $K$. That theorem needs TT on $H-K$ (and on $H+K$) so the banked S_RS_converges_EH_4d_closed Tendsto can be applied to the polarized pair and the cross term extracted.
In the Recognition gravity program this is scaffolding for the Euclidean weak-field TT face only. Module honesty forbids reading it as a source equation, Ricci/null focusing, or GAP1 closure; the missing future object remains a Recognition-derived Freudenthal exact-$J$ metric refinement identifying the sourced response with this midpoint variation, then Lorentzian null-dyad transport. No appeal to PixelAreaModel, LocalNullPatch, or the mesh exact-$J$ model is licensed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.