module module moderate

`IndisputableMonolith.Gravity.Analysis.ReggeEdgeTTAttachment4D`

Algebraic layer for attaching plane-wave transverse-traceless data to Regge edges in 4D. Defines unit axis displacements, edge loads, midpoint phases, and plane-wave axis-edge perturbations on Fin 4, plus their linearity lemmas. Downstream closers and the 4D Regge edge stencil import it as the proved attachment piece of the edge TT decomposition campaign.

claimOn $\mathrm{Fin}\,4$, the module supplies unit axis displacements, the associated edge-load map, axis midpoint phases, and plane-wave axis-edge perturbations of symmetric $4\times 4$ data, together with elementary identities (evaluation on axes, additivity, scalar homogeneity, and negation/subtraction rules).

background

This sits in the QG full-theory campaign, Wave 4 / lane W4-1 (edge_tt_decomposition). The upstream module EdgeTTDecomposition4D is the linear-algebra kernel: transverse-traceless decomposition of symmetric real $4\times 4$ matrices against a nonzero Euclidean wave covector on $\mathrm{Fin},4$.

Attachment means packaging that algebraic TT split as edge-supported plane-wave data suitable for Regge calculus. The objects here are the elementary geometric ingredients: unit displacement along a coordinate axis, the load that displacement induces on an edge, a midpoint phase factor, and the combined plane-wave axis-edge perturbation. No continuum PDE analysis is claimed; the setting is finite-dimensional linear algebra over $\mathbb{R}$ with the standard Euclidean structure on four indices.

proof idea

Definition module with short algebraic lemmas, not a deep existence proof. Core defs introduce axis displacement, edge load, midpoint phase, and the plane-wave axis-edge perturbation. Supporting facts are direct unfoldings: how edge load evaluates on an axis, and that edge load and the plane-wave perturbation are additive, homogeneous under scalar multiplication, and compatible with negation and subtraction. No analytic estimates or continuum limits appear.

why it matters in Recognition Science

Named parent consumers: 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 already proved in ReggeEdgeTTAttachment4D". ReggeEdgeStencil4D is the next kernel-checked increment: 4D Freudenthal 4-cube edge-class packaging after this attachment layer. ReggeEdgeTTAttachment4DAudit records the axiom footprint (propext, Classical.choice, Quot.sound). In the campaign chain this is the bridge from pure matrix TT algebra to Regge-edge stencils used in later hinge-aware and zero-mode work.

scope and limits

Does not prove existence of a full edge TT decomposition; that lives in the closer module.
Does not construct continuum graviton modes or solve linearized Einstein equations.
Does not define the 4D Regge edge stencil or hinge-diagonal blocks.
Does not address Lorentzian signature; the upstream split is Euclidean on Fin 4.
Does not claim numerical values for physical constants or mass ladders.

used by (3)

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

IndisputableMonolith.Gravity.Analysis.EdgeTTDecompositionCloser4D module_import
IndisputableMonolith.Gravity.Analysis.ReggeEdgeStencil4D module_import
IndisputableMonolith.Gravity.Analysis.ReggeEdgeTTAttachment4DAudit module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.Analysis.EdgeTTDecomposition4D module_import

declarations in this module (44)

def axisDisp L61
def edgeLoad L66
def axisMidpointPhase L71
def planeWaveAxisEdgePert L77
theorem axisDisp_apply L82
theorem edgeLoad_axis L85
theorem edgeLoad_add L90
theorem edgeLoad_smul L95
theorem edgeLoad_neg L107
theorem edgeLoad_sub L111
theorem planeWaveAxisEdgePert_add L116
theorem planeWaveAxisEdgePert_smul L122
theorem edgeLoad_gaugePart L131
theorem edgeLoad_gaugePart_axis L181
def gaugeVertexField L193
def shiftAxis L197
def discreteLieAxis L202
def latticeDerivSymbol L206
theorem shiftAxis_dot L209
theorem sin_add_sub_sin L220
theorem discreteLieAxis_eq L230
theorem planeWaveAxisEdgePert_gaugePart L249
theorem planeWaveAxisEdgePert_gaugePart_eq_discreteLie L260
theorem edgeLoad_decomposition L275
theorem planeWaveAxisEdgePert_decomposition L286
theorem load_eq_zero_of_isTT L300
theorem gaugeVector_eq_zero_of_isTT L304
theorem gaugePart_zero L315
theorem gaugeCorrected_eq_of_isTT L320
theorem residualTrace_eq_zero_of_isTT L327
theorem ttProject_eq_of_isTT L336
def decoyTT L348
def IsGaugeDiscreteLieOnAxis L352
theorem decoyTT_edgeLoad_axis2 L356
theorem decoyTT_not_gaugeDiscreteLie_axis2 L360
theorem decoyTT_isTT L367
def witnessWave L372
def witnessH L373
def witnessBase L374
theorem witness_isTT L376
theorem witness_momentumSq L379
theorem witness_ttProject_eq L382
theorem witness_edgeLoad_tt_ne_zero L385
theorem witness_tt_edge_ne_zero L390