IndisputableMonolith.Gravity.Analysis.Regge4DExactActionSymbol

declarations in this module (43)

• class strains L24
• abbrev Mat4 L67
• abbrev Wave4 L68
• def cubeOffsetT11 L73
• def cubeOffsetT12 L80
• def starMemberCubeT11 L85
• def starMemberCubeT12 L92
• def transportOffset L98
• theorem transportOffset_zero L101
• def phasedDeficitDotResolvedT11 L111
• def phasedDeficitDotResolvedT12 L119
• def phasedDeficitDotCollapsed L129
• def exactDeficitDot L136
• def exactFlatCrossTermSlot L145
• def exactFlatCrossTermOrbit L152
• def exactFlatCrossTermFold L158
• def familySide L164
• def familyRealMode L166
• def finiteExactReggeSymbol L171
• def finiteExactReggeSymbolSequence L174
• def discreteBookkeepingFactor L181
• theorem discreteBookkeepingFactor_eq L183
• def discreteExactReggeSymbol L190
• def discreteExactReggeSymbolSequence L193
• theorem discreteExactReggeSymbol_eq L197
• lemma phasedDeficitDotResolvedT11_smul L205
• lemma phasedDeficitDotResolvedT12_smul L212
• lemma phasedDeficitDotCollapsed_smul L219
• lemma exactDeficitDot_smul L226
• theorem exactFlatCrossTermSlot_smul L235
• theorem exactFlatCrossTermFold_smul L244
• theorem finiteExactReggeSymbol_smul L262
• theorem discreteExactReggeSymbol_smul L269
• theorem finiteExactReggeSymbol_zero L277
• theorem phasedDeficitDotResolvedT11_zeroMomentum L283
• theorem phasedDeficitDotResolvedT12_zeroMomentum L298
• def exact_star_member_offsets_incomplete L318
• theorem exact_star_member_offsets_incomplete_closed L320
• theorem fold_retained_as_legacy_only L325
• structure ExactActionSymbolStatus L330
• def exactActionSymbolStatus L339
• theorem exactActionSymbolStatus_flags L348
• theorem exact_action_srs_still_open L361