IndisputableMonolith.Gravity.Analysis.ReggeEdgeTTAttachment4D

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