IsSymmetric_sub
plain-language theorem explainer
The difference of two symmetric 4×4 matrices is again symmetric. Gravity analysts cite it when closing the Euclidean weak-field TT sector under linear combinations for the midpoint Bloch first variation. The argument is a two-line componentwise simplification: unfold symmetry on H−K and rewrite entries via matrix subtraction plus the two symmetry hypotheses.
Claim. Let $H,K$ be $4\times 4$ real matrices. If $H_{ij}=H_{ji}$ and $K_{ij}=K_{ji}$ for all indices $i,j\in\{0,1,2,3\}$, then $(H-K)_{ij}=(H-K)_{ji}$ for all $i,j$.
background
This module works in the Euclidean weak-field transverse-traceless (TT) sector of the closed 4D midpoint Bloch continuum face. The honesty block is explicit: results here are not source equations, not Ricci/null focusing, and not GAP1 closure.
Mat4 is the 4×4 continuum matrix type used for edge-strain and TT data. In this gravity analysis layer, matrix symmetry means entrywise equality under index swap: $H_{ij}=H_{ji}$ for all $i,j:\mathrm{Fin},4$. (A separate functional-equation notion of symmetry, $F(x)=F(1/x)$, appears in the d'Alembert cost algebra and is not the predicate used here.)
The TT package on a wave mode is the conjunction of symmetry, tracelessness, and transversality. Closure of that package under subtraction needs each conjunct separately; this lemma is the symmetry conjunct.
proof idea
Term/tactic hybrid, essentially mechanical. Unfold the goal IsSymmetric (H−K) to a quantified entry equality, introduce indices i j, then simp only with Matrix.sub_apply and the two hypotheses applied at (i,j). Componentwise, $(H-K){ij}=H{ij}-K_{ij}=H_{ji}-K_{ji}=(H-K)_{ji}$. No external lemmas beyond matrix subtraction and the given symmetries.
why it matters
Feeds IsTT_sub in the same module, which packages symmetry, tracelessness, and transversality so that if $H$ and $K$ are TT relative to a wave mode then so is $H-K$. That closure is required for continuum-face polarization: the first-variation analysis transports a torus-normalized continuum face via the banked S_RS_converges_EH_4d_closed Tendsto on both $H+K$ and $H-K$.
Within Recognition Science gravity, this is scaffolding for the Euclidean TT directional first variation of the exact midpoint Bloch symbol, not a claim about sourced Einstein response. The module’s missing future object remains a Recognition-derived Freudenthal exact-$J$ metric refinement that would identify the sourced response with this midpoint variation, then Lorentzian null-dyad Ricci/stress transport. Do not read this as GAP1 or as a null-field equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.