Pith. sign in
module module high

IndisputableMonolith.Gravity.Analysis.EdgeTTDecompositionCloser4D

show as:
view Lean formalization →

Named ledger closer for the 4D edge transverse-traceless decomposition at the algebraic-plus-attachment layer. It packages the linear-algebra TT split of symmetric 4×4 matrices and its attachment to plane-wave edge loadings into the export Prop that the continuum-recovery ledger will flip. Gravity analysts working the weak-field Regge-to-Einstein–Hilbert campaign cite it. The module is a thin assembly of already-checked kernel increments, not a new calculation.

claimThe 4D edge TT decomposition holds: every symmetric real $4\times 4$ matrix admits a unique transverse-traceless / pure-gauge / transverse-trace split against a nonzero Euclidean wave covector on $\mathbb{R}^4$, and that split attaches consistently to plane-wave loadings on axis edges of the 4-torus under the quadratic form $E\mapsto\sum_{ij}E_{ij}D^i D^j$. Decoy gauge modes coincide with the longitudinal family and are not transverse.

background

Recognition Science's quantum-gravity campaign recovers the weak-field Einstein–Hilbert quadratic action from a discrete Regge-style edge action on a 4-torus mesh. Before continuum limits, one must freeze the target, the mesh carrier, normalized TT data, and honesty decoys; that is the job of the continuum preflight. Independently, the algebraic layer decomposes symmetric $4\times 4$ real matrices against a nonzero Euclidean wave covector into transverse-traceless, pure-gauge, and transverse-trace parts.

The attachment layer then binds that split to plane-wave EDGE loadings on axis edges, using the same quadratic-form convention as the 3D chain ($\mathrm{polEdgeCoeff},E,d=\sum_{ij}E_{ij}D^i D^j$). The edge-stencil module supplies the Freudenthal 4-cube edge classes and a provisional finite quadratic. This closer sits above those four imports and does not itself prove continuum recovery.

proof idea

Assembly module, not a fresh derivation. It re-exports the algebraic uniqueness and existence statements from the 4D edge TT decomposition kernel, the plane-wave attachment identities from the edge-TT attachment layer, and the decoy-gauge comparisons (gauge equals longitudinal; gauge is not transverse). The named Prop edge_tt_decomposition / edge_tt_decomposition_holds is inhabited by composing those already kernel-checked lemmas. No continuum limit, no mesh refinement, and no curvature identities are proved here.

why it matters in Recognition Science

Feeds the ledger-facing export SRSConvergesEH4D, whose doc-comment states it is the sole place that may later inhabit the preflight names edge_tt_decomposition and S_RS_converges_EH_4d for the ledger flip. Without a closed algebraic-plus-attachment TT split on edges, the weak-field quadratic action cannot be matched mode-by-mode against the continuum EH target. In the QG full-theory campaign this is Wave 4 / lane W4-1: the smallest named closer that turns the linear-algebra and plane-wave increments into a single exportable theorem. It does not touch the eight-tick octave or the forcing chain T0–T8; its role is strictly the 4D Regge continuum-closure stack.

scope and limits

used by (1)

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

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (4)