IndisputableMonolith.Gravity.Analysis.EdgeTTDecomposition4D

declarations in this module (56)

• abbrev Mat4 L40
• def IsSymmetric L42
• def euclideanTrace L45
• def IsTraceless L48
• def IsTransverse L51
• def IsTT L55
• def momentumSq L58
• def gaugePart L61
• def outerSq L64
• def transverseProjector L67
• def load L70
• def dot L73
• def gaugeVector L76
• def gaugeCorrected L82
• def residualTrace L85
• def ttProject L88
• theorem gaugePart_symmetric L93
• theorem outerSq_symmetric L97
• theorem transverseProjector_symmetric L101
• theorem load_gaugePart L111
• theorem load_smul L126
• theorem load_sub L132
• theorem load_one L136
• theorem load_outerSq L147
• theorem load_transverseProjector L156
• theorem dot_gaugeVector L165
• theorem load_gaugePart_gaugeVector L211
• theorem gaugeCorrected_transverse L226
• theorem gaugeCorrected_symmetric L233
• theorem euclideanTrace_smul L242
• theorem euclideanTrace_sub L248
• theorem euclideanTrace_one L252
• theorem euclideanTrace_outerSq L258
• theorem euclideanTrace_transverseProjector L261
• theorem ttProject_symmetric L269
• theorem ttProject_transverse L277
• theorem ttProject_traceless L287
• theorem ttProject_isTT L295
• theorem exists_edgeTTDecomposition L304
• theorem exists_edgeTTDecomposition' L312
• def axisWave L322
• theorem axisWave_momentumSq L328
• def axisTTPlus L333
• def axisTTCross L340
• theorem axisTTPlus_isTT L346
• theorem axisTTCross_isTT L354
• theorem axisTTPlus_ne_zero L362
• theorem axisTTCross_ne_zero L367
• theorem axisTT_independent L372
• def decoyLongitudinal L382
• theorem decoyLongitudinal_symmetric L385
• theorem decoyLongitudinal_not_transverse L388
• theorem decoy_ttProject_isTT L394
• theorem decoy_projection_restores_transverse L399
• theorem zero_wave_momentumSq L403
• theorem decomposition_hypothesis_fails_at_zero L407