exists_edgeTTDecomposition'
plain-language theorem explainer
Every symmetric real 4×4 matrix admits a transverse-traceless (TT) plus gauge plus residual-trace decomposition against any nonzero Euclidean wave covector. Gravity and continuum-limit workers cite this existential packaging of the algebraic edge-TT layer. The proof is a one-line term that witnesses the three summands from the constructive projector theorem.
Claim. Let $H$ be a symmetric $4\times 4$ real matrix and $m\in\mathbb{R}^4$ a covector with $m\cdot m\neq 0$. Then there exist a matrix $H_{\mathrm{TT}}$, a vector $v\in\mathbb{R}^4$, and a scalar $\beta\in\mathbb{R}$ such that $H=H_{\mathrm{TT}}+\mathrm{gauge}(m,v)+\beta\,P_\perp(m)$ and $H_{\mathrm{TT}}$ is TT: symmetric, Euclidean-traceless, and transverse to $m$.
background
This module is the algebraic layer of the ledger name edge_tt_decomposition (QG campaign Wave 4 / W4-1). It lifts the 3D Euclidean TT conventions (symmetry, Euclidean trace zero, transversality to a wave covector) to Fin 4, with no Frobenius pin and no Minkowski specialization yet.
Mat4 is simply Matrix (Fin 4) (Fin 4) ℝ. Symmetry is entrywise $H_{ij}=H_{ji}$. Algebraic TT means the conjunction of symmetry, vanishing Euclidean trace, and transversality $H m = 0$ (in the module's Euclidean sense). The gauge piece and the transverse projector are the standard linear-algebra corrections that absorb longitudinal and pure-trace contamination along $m$.
The constructive sibling states the same identity with explicit projectors: $H=\mathrm{ttProject}(m,H)+\mathrm{gaugePart}(m,\mathrm{gaugeVector}(m,H))+\mathrm{residualTrace}(m,H),\mathrm{transverseProjector}(m)$, and proves the projected piece is TT whenever $m\cdot m\neq 0$.
proof idea
Pure term-mode packaging of the constructive theorem. The existential is witnessed by the triple $(\mathrm{ttProject},m,H,,\mathrm{gaugeVector},m,H,,\mathrm{residualTrace},m,H)$. The conjunction (decomposition identity and TT property of the first summand) is exactly the conclusion of exists_edgeTTDecomposition, applied to the same $m$, $H$, symmetry hypothesis, and nondegeneracy $m\cdot m\neq 0$. No extra algebra is performed.
why it matters
This is the existential interface to the algebraic edge_tt_decomposition kernel increment. Downstream continuum or Regge arguments that only need existence of a TT remainder (rather than the explicit projectors) can cite this form without unfolding the gauge vector or residual trace.
Per the module contract it does not yet decompose Regge EDGE perturbations on a 4D lattice, does not prove $S_{\mathrm{RS}}$ converges to Einstein-Hilbert in 4D, and does not flip gap_action_recovery. Minkowski/null specialization and the "two independent unnormalized TT polarizations" nondegeneracy section that follows are separate steps. No used_by edges are recorded yet; the declaration is the public existence face of the already-proved constructive decomposition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.