IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4D

declarations in this module (47)

• abbrev Mat4 L37
• abbrev Wave4 L38
• def frobeniusNormSq L40
• def waveNormSq L43
• def couplingS L46
• theorem couplingS_eq_s L49
• def deltaQ L51
• def m2Coeff L54
• theorem m2Coeff_eq_m2CoeffSum L61
• def explicitM2Coeff L67
• theorem m2Coeff_eq_m2Num_div L71
• theorem m2Coeff_eq_explicitM2Coeff L75
• def closedCoeff L84
• def sym4C L91
• def sym2exC L96
• def symFull L102
• theorem closedCoeff_eq_closedCoeffZ_pointwise L108
• theorem symFull_eq_symFullZ_div L114
• theorem symFull_explicit_eq_symFull_closed L124
• def biquad L144
• theorem biquad_congr L149
• theorem sum2_mul L158
• theorem triple_double_sum_mul L164
• theorem term_expand L189
• theorem exactMidpointBlochM2_eq_biquad L217
• theorem sum6_flip_ab L245
• theorem sum6_flip_cd L252
• theorem sum4_exchange L260
• theorem sum6_exchange L277
• theorem biquad_sym4 L286
• theorem biquad_sym2ex L351
• theorem biquad_symFull L380
• def loadNormSq L389
• def quadraticForm L392
• def closedForm L395
• theorem biquad_closedCoeff_eq_closedForm L403
• theorem exactMidpointBlochM2_eq_closedForm_of_symmetric L417
• theorem closedForm_eq_neg_eighth_of_TT L432
• theorem exactMidpointBlochM2_eq_neg_eighth_frobenius_tt L445
• theorem exactMidpointBlochM2_rayleigh_eq_neg_eighth_of_TT L454
• theorem closedForm_gaugePart_eq_zero L462
• theorem exactMidpointBlochM2_eq_zero_of_gaugePart L470
• theorem exactMidpointBlochM2_gaugePart_eq_zero L477
• theorem exactMidpointBlochM2_gauge_rayleigh_eq_zero L482
• theorem exactMidpointBlochM2_faces L488
• def ExactMidpointM2TTIdentityProved L500
• theorem exactMidpointM2TTIdentityProved_true L501