IsTraceless_sub
plain-language theorem explainer
Difference of two traceless Euclidean 4×4 strain matrices remains traceless. Gravity analysts in the weak-field TT sector of the midpoint Bloch continuum face cite this when closing the TT class under linear combinations used for polarization. The proof is a short diagonal-sum argument: Euclidean trace is linear, so the two zero traces cancel.
Claim. If $H,K\in\mathrm{Mat}_4(\mathbb{R})$ satisfy $\mathrm{tr}_E(H)=0$ and $\mathrm{tr}_E(K)=0$, where the Euclidean trace is $\mathrm{tr}_E(M)=\sum_{i=0}^{3}M_{ii}$, then $\mathrm{tr}_E(H-K)=0$.
background
In the Euclidean weak-field TT sector of the closed 4D midpoint Bloch continuum face, strain data are 4×4 real matrices (Mat4). The Euclidean trace is the plain sum of diagonal entries. A matrix is traceless when that sum is zero. Tracelessness is one of the three TT ingredients (with symmetry and transversality) used throughout the first-variation analysis.
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 closed 4D RS-to-EH Tendsto on the combinations $H+K$ and $H-K$ plus polarization. Algebraic closure of the traceless condition under subtraction is a small prerequisite for those polarized combinations.
Upstream, IsTraceless is exactly euclideanTrace H = 0 with euclideanTrace H = ∑ i, H i i. Name collisions with cost-algebra H and bridge-ratio K in the dependency graph are binder noise, not content.
proof idea
Unfold the traceless predicate and the Euclidean-trace definition on both hypotheses and the goal, reducing everything to diagonal-sum equalities. Simplify matrix subtraction entrywise. Rewrite the sum of entrywise differences via Finset.sum_sub_distrib, obtaining a difference of two diagonal sums. Each sum is zero by hypothesis, so the difference is zero.
why it matters
Directly feeds IsTT_sub in the same module, which packages symmetry, tracelessness, and transversality:
⟨IsSymmetric_sub …, IsTraceless_sub …, IsTransverse_sub …⟩.
That full TT closure under subtraction is what lets the continuum-face polarization and TT first-variation Tendsto arguments treat $H-K$ as still TT whenever $H$ and $K$ are.
The module honesty block is binding: the surrounding development is a theorem only in the Euclidean weak-field TT sector of the closed midpoint Bloch continuum face. 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 / pullback identifying the sourced response with this midpoint variation, followed by Lorentzian null-dyad Ricci / stress transport.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.