IsTraceless_add
plain-language theorem explainer
The Euclidean trace vanishes on the sum of two traceless 4×4 matrices. Analysts in the Euclidean weak-field TT sector of the midpoint Bloch first variation cite this when closing the TT cone under addition. The proof unfolds the trace, distributes the entrywise sum, and cancels the two zero traces.
Claim. Let $H,K$ be $4\times 4$ real matrices. If the Euclidean trace of $H$ is zero and the Euclidean trace of $K$ is zero, then the Euclidean trace of $H+K$ is zero.
background
This module works in the Euclidean weak-field transverse-traceless (TT) sector of the closed 4D midpoint Bloch continuum face. Matrices are Mat4, the standard $4\times 4$ continuum matrix type used for edge strain and polarization in the Regge/continuum preflight layer.
Tracelessness is the vanishing of the Euclidean trace (sum of diagonal entries). Together with symmetry and transversality to a wave covector, it defines the TT cone on which the directional first variation of the exact midpoint Bloch symbol is derived. The honesty block of the module restricts all theorems here to that Euclidean weak-field TT sector: not a source equation, not Ricci/null focusing, and not GAP1 closure.
Upstream, the Euclidean trace is the linear functional used in the edge TT decomposition; additivity of matrix addition on entries is the only algebraic input needed for this lemma.
proof idea
Tactic proof. Unfold IsTraceless and euclideanTrace on both hypotheses and the goal, so the claim is that the sum of diagonal entries of $H+K$ is zero. Simplify with entrywise matrix addition. Rewrite by distributing the finite sum over addition (Finset.sum_add_distrib), substitute the two zero-trace hypotheses, and finish with add_zero.
why it matters
Feeds IsTT_add in the same module, which packages symmetry, tracelessness, and transversality into closure of the TT predicate under matrix addition: IsTT m (H+K) from IsTT m H and IsTT m K. That closure is needed so the TT sector stays a linear space when the first-variation argument polarizes on $H+K$ and $H-K$ and transports the torus-normalized continuum face via the banked S_RS_converges_EH_4d_closed Tendsto.
In the broader Recognition gravity stack this is bookkeeping inside the Euclidean weak-field TT analysis of the midpoint Bloch symbol, not a forcing-chain step (T0–T8) and not a claim about sourced Einstein response. The module’s honesty clause still flags the missing future object: a Recognition-derived Freudenthal exact-$J$ metric refinement identifying the sourced response with this midpoint variation, then Lorentzian null-dyad transport.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.