Pith. sign in
module module high

IndisputableMonolith.Gravity.Analysis.EdgeTTDecomposition4D

show as:
view Lean formalization →

Defines the algebraic transverse-traceless (TT) sector for real 4×4 matrices: symmetric, Euclidean-traceless, and transverse to a momentum. Supplies projectors, gauge pieces, and Frobenius-style inner products used throughout the 4D Regge continuum campaign. Downstream closers and preflight modules import this layer as the frozen TT data model. The module is definitional infrastructure rather than a single theorem.

claimOn real $4\times 4$ matrices, a mode $h$ is algebraically TT when it is symmetric ($h=h^{\mathsf T}$), Euclidean-traceless ($\mathrm{tr}\,h=0$), and transverse to a momentum $p$ ($h\,p=0$). The module packages the Euclidean trace, outer-square and transverse projectors, gauge (longitudinal) part, momentum square, and the Frobenius load/dot products that isolate the TT subspace.

background

In linearized gravity and Regge calculus, physical graviton polarizations live in the transverse-traceless sector. In four Euclidean dimensions one works with real $4\times 4$ matrices $h_{\mu\nu}$. Symmetry removes antisymmetric junk; vanishing Euclidean trace removes the conformal scalar; transversality $h_{\mu\nu}p^{\nu}=0$ kills the longitudinal gauge orbit for a chosen momentum $p$.

This module freezes that algebraic language for the Recognition Science 4D continuum campaign. Sibling names indicate the standard toolkit: Mat4 carriers, predicates for symmetry, tracelessness, transversality and full TT, plus momentumSq, gaugePart, outerSq, transverseProjector, and Frobenius load/dot. No continuum limit or curvature identity is claimed here; only the linear-algebraic TT model.

The setting is the Gravity analysis stack that feeds Regge edge attachment, second-variation, and Option-C Bloch bridges on the Freudenthal 4-torus mesh.

proof idea

This is a definition module: it introduces matrix types, TT predicates, projectors, and inner-product helpers. There is no single top-level theorem to walk. Downstream modules compose these definitions into existence statements (algebraic TT decomposition), normalized plus/cross witnesses, and pure-gauge decoys. Expect elementary linear-algebra proofs (symmetry of projectors, kernel characterizations, orthogonality of gauge vs TT parts) rather than analytic estimates.

why it matters in Recognition Science

The module is the shared TT vocabulary for the 4D Regge full-theory campaign. EdgeTTDecompositionCloser4D inhabits the preflight Prop edge_tt_decomposition by composing algebraic TT decomposition, Frobenius-normalized plus/cross witnesses, a pure-gauge non-transverse decoy, and plane-wave edge attachment. Regge4DContinuumPreflight freezes normalized TT data and honesty decoys before any continuum recovery claim. Algebraic closers (Regge4DAlgebraicCloser, tensor/transported variants), flat second-variation status, and the Recognition-mesh exact-J bridge all import this layer so that TT, gauge, and isotropy targets speak one matrix language. An axiom audit module checks the public theorems stay within the expected classical footprint. Without this frozen algebraic TT model, the continuum preflight and named closers would not have a common carrier.

scope and limits

used by (12)

From the project-wide theorem graph. These declarations reference this one in their body.

declarations in this module (56)