IsTT_add
plain-language theorem explainer
The sum of two algebraic TT matrices relative to the same wave vector remains algebraic TT (symmetric, Euclidean-traceless, and transverse). Anyone proving continuum first-variation identities under H+K / H-K polarization cites this closure. The proof is a three-field constructor from the component additivity lemmas.
Claim. Let $m$ be a 4-wave vector and let $H,K$ be $4\times 4$ real matrices. If both $H$ and $K$ are algebraic TT relative to $m$ (symmetric, Euclidean-traceless, and transverse to $m$), then $H+K$ is algebraic TT relative to $m$.
background
In the Euclidean weak-field TT sector of the closed 4D midpoint Bloch continuum face, strain matrices live in Mat4 and couple to a wave vector of type Wave4. Algebraic TT means the conjunction of three linear conditions: symmetry of the matrix, vanishing Euclidean trace, and transversality to the wave vector $m$ (the product $H m$ vanishes in the appropriate sense).
The module derives the genuine cross-term / directional first variation of the exact midpoint Bloch symbol, then transports its torus-normalized continuum face via the banked SRS-to-EH convergence on $H+K$ and $H-K$ plus polarization. Additivity of the TT predicate is the elementary linear-algebra fact needed before those polarized continuum statements can be stated for sums.
Upstream, IsTT is defined exactly as the triple of properties; the three component lemmas IsSymmetric_add, IsTraceless_add, and IsTransverse_add already close each conjunct under matrix addition.
proof idea
Term-mode proof: unpack the two IsTT hypotheses into their three conjuncts, apply the corresponding additivity lemmas (IsSymmetric_add, IsTraceless_add, IsTransverse_add), and repack the resulting triple as IsTT m (H+K). No further calculation.
why it matters
Feeds the headline continuum theorem continuumTTFirstVariation_closed, whose hypotheses require both $H$ and $K$ to be algebraic TT and whose polarized transport runs on $H+K$ and $H-K$. Without TT-closure under addition, the Tendsto statement for the torus-normalized midpoint first variation (limit $-\tfrac14$ Frobenius pairing) cannot even be typed for the polarized pair.
Locally this sits inside the Euclidean weak-field TT sector analysis of the closed midpoint Bloch face. Per the module honesty clause it is not a source equation, not Ricci/null focusing, and not GAP1 closure; the missing future object remains a Recognition-derived Freudenthal exact-$J$ metric refinement identifying the sourced response with this midpoint variation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.