IsTransverse_add
plain-language theorem explainer
Transversality of two 4×4 matrix strains against a fixed wave mode is preserved under matrix addition. Anyone assembling the TT (transverse-traceless) cone for the Euclidean weak-field first variation of the closed 4D midpoint Bloch symbol cites this. The proof is a four-line expansion: distribute the defining sum, apply both hypotheses, and cancel with add_zero.
Claim. Let $m$ be a 4D wave mode and let $H,K$ be $4\times 4$ real matrices. If $H$ is transverse to $m$ and $K$ is transverse to $m$, then $H+K$ is transverse to $m$.
background
The ambient module studies the directional first variation of the closed 4D midpoint Bloch symbol in the Euclidean weak-field TT sector. Matrices are Mat4 (4×4 continuum preflight matrices) and modes are Wave4 (4D wave data from the same preflight layer).
Transversality (IsTransverse m M) is the algebraic TT gauge condition on a matrix strain $M$ relative to mode $m$: for each index $i$, a finite sum of entries of $M$ contracted against $m$ vanishes. It is one of the three legs of the TT predicate (alongside symmetry and tracelessness), imported from the edge TT decomposition layer.
The local honesty bound is strict: results here live only in the Euclidean weak-field TT sector of the closed midpoint Bloch continuum face. They are not source equations, not Ricci/null focusing, and not GAP1 closure.
proof idea
Fix an index $i$. Unfold matrix addition on entries and distribute multiplication over addition (Matrix.add_apply, add_mul). Split the defining finite sum with Finset.sum_add_distrib. Each summand is zero by the corresponding transversality hypothesis at $i$, so the total is $0+0$, finished by add_zero.
why it matters
This is the transverse leg of TT-cone closure under addition. The sole direct consumer is IsTT_add, which packages symmetry, tracelessness, and transversality into a single TT-sum rule:
IsTT_add := ⟨IsSymmetric_add, IsTraceless_add, IsTransverse_add⟩.
That sum rule is bookkeeping for the polarization identity used when transporting the torus-normalized continuum face of the midpoint Bloch first variation along the banked S_RS_converges_EH_4d_closed Tendsto on $H+K$ and $H-K$. In the broader RS gravity stack it supports the Euclidean weak-field TT analysis only; the module doc explicitly defers the Recognition-derived Freudenthal exact-$J$ metric refinement and Lorentzian null-dyad transport as future work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.