module module moderate

`IndisputableMonolith.Gravity.Analysis.EdgeTTDecompositionLorentz4D`

Algebraic layer for the Lorentzian transverse-traceless (TT) decomposition of symmetric 4×4 matrices in signature (−,+,+,+). Defines Minkowski raise/trace/dot, traceless and transverse predicates, and the gauge outer-product pieces that split a symmetric tensor into TT plus pure-gauge. Gravity analysts cite it when matching local Clausius balances to Einstein form. Structure is definition-heavy linear algebra over ℝ⁴ with predicate lemmas.

claimOn $\mathbb{R}^{4}$ with Minkowski metric $\eta=\mathrm{diag}(-1,1,1,1)$, equip $\mathrm{Mat}_{4}(\mathbb{R})$ with index raising (negate the time component), Minkowski contraction and trace, and the predicates Lorentz-traceless, Lorentz-transverse, and Lorentz-TT. Introduce the gauge pieces built from symmetrized outer products so that a symmetric tensor decomposes into a TT part plus pure-gauge terms.

background

Jacobson's thermodynamic route to Einstein's equation reduces, at the algebraic hinge, to comparing two symmetric quadratic forms on every Minkowski-null direction. The upstream Clausius–Einstein bridge isolates that finite-dimensional fact: equality on all null vectors fixes the difference only up to a multiple of the metric, so a local all-null Clausius balance has the shape of Einstein's equation with the metric term free.

This module supplies the 4D Lorentzian toolkit for that hinge. Matrices are plain $4\times 4$ real arrays. Index raising for $(-,+,+,+)$ negates the time component. Minkowski dot and trace are the $\eta$-contractions. A symmetric matrix is Lorentz-traceless if its $\eta$-trace vanishes, Lorentz-transverse if it annihilates a chosen null (or timelike) direction after raising, and Lorentz-TT if both hold. Gauge pieces are built from outer squares and symmetrized outer products of vectors, the algebraic pure-gauge directions one must quotient by to reach the TT sector.

proof idea

Definition module with supporting predicate lemmas, not a single deep theorem. It introduces Mat4, symmetry, raise, Minkowski dot/trace, $\eta$, and the three Lorentz predicates (traceless, transverse, TT), then the gauge constructors (outer square, symmetrized outer, gauge part). Proofs are routine matrix algebra: unfolding definitions, component arithmetic under signature $(-,+,+,+)$, and verifying that gauge pieces are symmetric and that TT means the residual after subtracting gauge. No analytic estimates or continuum limits.

why it matters in Recognition Science

Feeds the axiom-audit module EdgeTTDecompositionLorentz4DAudit, which #print axioms every public theorem of this Lorentzian 4D TT layer and expects only [propext, Classical.choice, Quot.sound]. In the broader gravity stack it is the algebraic substrate under the Clausius–Einstein bridge: once null-direction balance is known up to a metric multiple, one still needs a clean TT-versus-gauge split of symmetric tensors to identify the curvature side with the Einstein tensor's TT content. Without this layer, the finite-dimensional hinge stays informal. It does not itself derive Einstein's equation or fix $G$; it only makes the 4D Lorentzian decomposition machine-checkable for downstream thermodynamic and Recognition-gravity arguments.

scope and limits

Does not derive Einstein's equation or fix Newton's constant.
Does not treat curved manifolds, only flat algebraic $\mathbb{R}^{4}$ matrices.
Does not include continuum or distributional GR identities.
Does not claim uniqueness of the gauge split beyond the predicates defined here.
Does not address signature $(+,+,+,−)$ or dimensions other than 4.

used by (1)

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

IndisputableMonolith.Gravity.Analysis.EdgeTTDecompositionLorentz4DAudit module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.ClausiusEinsteinBridge module_import

declarations in this module (118)

abbrev Mat4 L57
def IsSymmetric L59
def raise L63
def minkowskiDot L67
def minkowskiTrace L71
def IsLorentzTraceless L74
def IsLorentzTransverse L78
def IsLorentzTT L82
def minkowskiEta L85
def gaugePart L87
def outerSq L90
def symmetrizedOuter L93
def lorentzLoad L97
theorem lorentzLoad_eq L100
theorem IsLorentzTransverse_iff_lorentzLoad L106
theorem minkowskiDot_eq_sum L112
theorem minkowskiDot_comm L117
theorem minkowskiTrace_eq_sum L121
theorem gaugePart_symmetric L128
theorem outerSq_symmetric L132
theorem symmetrizedOuter_symmetric L136
theorem raise_raise L140
theorem lorentzLoad_smul L147
theorem lorentzLoad_sub L153
theorem lorentzLoad_eta L157
theorem lorentzLoad_outerSq L163
theorem lorentzLoad_symmetrizedOuter L173
theorem lorentzLoad_symmetrizedOuter_l L190
theorem lorentzLoad_gaugePart L207
theorem minkowskiTrace_smul L224
theorem minkowskiTrace_sub L230
theorem minkowskiTrace_add L236
theorem minkowskiTrace_eta L242
theorem minkowskiTrace_outerSq L246
theorem minkowskiTrace_symmetrizedOuter L250
theorem minkowskiDot_eq_MinkowskiNull L254
def transverseProjector L261
def gaugeVector L264
def gaugeCorrected L270
def residualTrace L273
def ttProject L276
theorem minkowskiEta_symmetric L279
theorem transverseProjector_symmetric L286
theorem lorentzLoad_transverseProjector L293
theorem minkowskiDot_gaugeVector L300
theorem lorentzLoad_gaugePart_gaugeVector L348
theorem gaugeCorrected_transverse L363
theorem gaugeCorrected_symmetric L370
theorem minkowskiTrace_transverseProjector L377
theorem ttProject_symmetric L385
theorem ttProject_transverse L393
theorem ttProject_traceless L403
theorem ttProject_isLorentzTT L411
theorem exists_lorentzTTDecomposition L420
theorem exists_lorentzTTDecomposition' L428
def nullProjector L439
def nullSMixed L442
def kron L445
def nullPMixed L447
def nullPhp L451
def nullBilinear L456
def nullMGaugeVector L460
def nullLGaugeVector L463
def nullGap L467
def nullTraceCoeff L472
def nullTTProject L475
theorem nullProjector_symmetric L478
theorem nullProjector_minkowskiTrace L485
theorem lorentzLoad_nullProjector_m L493
theorem lorentzLoad_nullProjector_l L502
theorem sum_kron_left L511
theorem sum_kron_right L520
theorem nullPhp_expand_algebra L529
theorem sum_kron_H_kron L549
theorem sum_S_H_kron L561
theorem sum_kron_H_S L571
theorem nullPhp_entry L582
theorem sum_nullSMixed_H_col L592
theorem sum_H_nullSMixed_row L612
theorem nullGap_entry L628

… and 38 more