IsTransverse_sub
plain-language theorem explainer
If two 4×4 matrices are transverse to a wave covector m (each row annihilates m), their difference is transverse too. Used when closing the algebraic TT sector under linear combinations for midpoint-Bloch first-variation polarization. Proof is a short row-sum identity: the finite sum distributes over subtraction and both summands vanish.
Claim. Let $m\in\mathbb{R}^4$ and let $H,K$ be $4\times 4$ real matrices. If $\sum_j H_{ij}m_j=0$ and $\sum_j K_{ij}m_j=0$ for every row index $i$, then $\sum_j(H-K)_{ij}m_j=0$ for every $i$.
background
In the Euclidean weak-field TT sector of the closed 4D midpoint Bloch continuum face, a matrix strain is transverse when each row is orthogonal to the wave covector $m$. Concretely, transversality of $H$ to $m$ means $\forall i,;\sum_j H_{ij}m_j=0$. Algebraic TT packages three conditions: symmetry, Euclidean tracelessness, and this transversality.
The ambient module derives the directional first variation of the exact midpoint Bloch symbol, then transports the torus-normalized continuum face via banked convergence on $H+K$ and $H-K$ plus polarization. The honesty block restricts all claims to that Euclidean weak-field TT sector: not a source equation, not Ricci/null focusing, and not GAP1 closure.
Here $m$ is continuum wave data and $H,K$ are $4\times 4$ matrices (the module's Wave4/Mat4 abbreviations).
proof idea
Fix a row index $i$. Expand the $(i,j)$ entry of $H-K$ and the product with $m_j$. Distribute the finite sum over the difference via Finset.sum_sub_distrib, apply the two transverse hypotheses (each row-sum vanishes), and reduce $0-0$ to zero. Purely algebraic; no analysis or continuum input.
why it matters
Direct input to the sibling package that closes full algebraic TT under subtraction (symmetry, tracelessness, and transversality together). That linear-subspace structure is required for continuum-face polarization and the TT first-variation Tendsto argument on $H\pm K$ in the same module.
Within Recognition gravity analysis this is bookkeeping for the closed midpoint Bloch face in the Euclidean weak-field TT sector. It does not touch the forcing chain (T0–T8), RCL, or the $\varphi$-ladder mass formula. The open path flagged by the module remains a Recognition-derived Freudenthal exact-$J$ metric refinement identifying the sourced response with this midpoint variation, followed by Lorentzian null-dyad Ricci/stress transport.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.