IndisputableMonolith.Gravity.Analysis.Regge4DAlgebraicCloser

declarations in this module (29)

• abbrev Mat4 L66
• theorem decoy_one_orbit_m2_ne_eh_coefficient L74
• theorem plus_normalized_isTTPolarization L81
• theorem cross_normalized_isTTPolarization L86
• theorem tt_witnesses_nonvacuous L91
• theorem gauge_m2Symbol_vanishes_on_decoy L99
• theorem one_orbit_m2Symbol_axis_ne_zero L104
• theorem eh_tt_coefficient_eq L109
• def fullMomentOrbitContribution L116
• def fullMomentZeroMomentum L123
• theorem fullMomentZeroMomentum_eq_trueWeight L126
• theorem fullMomentOrbitContribution_eq_bilinear L132
• theorem fullMomentZeroMomentum_eq_bilinear L137
• theorem fullMomentZeroMomentum_axisTTPlus L143
• theorem fullMomentZeroMomentum_decoyGauge L149
• theorem fullMomentZeroMomentum_decoyTrace L155
• theorem fullMomentOrbitContribution_of_deficit_zero L161
• theorem fullMomentOrbitContribution_axisTTPlus L168
• theorem fullMomentOrbitContribution_decoyGauge L173
• def axisIntMode L188
• def Regge4DFullTTIsotropyTarget L195
• def Regge4DPureGaugeVanishesTarget L200
• def Regge4DPlusCrossAgreeTarget L205
• def Regge4DAlgebraicCloserTarget L212
• theorem fullTTIsotropyTarget_mentions_eh_coefficient L218
• structure Regge4DAlgebraicCloserStatus L225
• def regge4DAlgebraicCloserStatus L241
• theorem regge4DAlgebraicCloserStatus_flags L252
• theorem banked_does_not_flip_gap_or_isotropy L266