IsSymmetric_add
plain-language theorem explainer
The sum of two symmetric real 4×4 matrices is again symmetric. Gravity analysts cite it when closing the Euclidean weak-field TT sector under addition before polarization of the midpoint Bloch first variation. The proof is a one-line componentwise simp from matrix addition and the two symmetry hypotheses.
Claim. Let $H,K$ be real $4\times 4$ matrices. If $H_{ij}=H_{ji}$ and $K_{ij}=K_{ji}$ for all indices $i,j$, then $(H+K)_{ij}=(H+K)_{ji}$ for all $i,j$.
background
This module derives the directional first variation of the closed 4D midpoint Bloch symbol in the Euclidean weak-field TT sector, then transports the continuum face via polarization on $H+K$ and $H-K$. Matrices live in Mat4, the 4D continuum preflight matrix type used for edge-strain and Bloch-symbol arguments.
Here symmetry is the matrix property $M_{ij}=M_{ji}$, not the scalar cost symmetry $F(x)=F(1/x)$ from the d'Alembert inevitability layer (same name, different type). The TT package later bundles symmetry with tracelessness and transversality relative to a wave covector.
Section §3 of the module records that the TT cone is closed under add and sub, so the polarization identity for the midpoint first variation stays inside the sector where the continuum Tendsto hypotheses apply.
proof idea
Term-mode tactic proof, three lines. Introduce indices $i,j$. Unfold matrix addition at $(i,j)$ via Matrix.add_apply, then rewrite each summand by the corresponding symmetry hypothesis $H_{ij}=H_{ji}$ and $K_{ij}=K_{ji}$. The resulting equality is definitional symmetry of $H+K$. No external lemmas beyond matrix API and the two assumptions.
why it matters
Parent consumer is IsTT_add, which packages this lemma with the matching traceless and transverse additivity facts to show the full TT predicate is closed under matrix addition. That closure lets the polarization identity
$$\mathrm{FV}(H,K)=\bigl(Q(H+K)-Q(H-K)\bigr)/2$$
stay inside the Euclidean weak-field TT sector where S_RS_converges_EH_4d_closed supplies the continuum face.
In the Recognition gravity stack this is bookkeeping, not a new physical law: it keeps the first-variation argument honest inside the sector the module declares as THEOREM, and does not touch Ricci focusing, null transport, or GAP1. It is a prerequisite step on the path from the midpoint Bloch symbol to a sourced response once a Freudenthal exact-$J$ metric refinement exists.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.