IndisputableMonolith.Gravity.Analysis.ReggeBlochM2Symbol4D

declarations in this module (42)

• def symbolDir L43
• def foldAlong L48
• def phaseScale L51
• theorem classMidpointPhase_symbolDir L55
• theorem phasedClassDot_symbolDir L69
• theorem foldAlong_neg L77
• theorem foldAlong_even L92
• theorem foldAlong_odd_deriv_at_zero L99
• def slotKerDotZ L104
• theorem slotKerDotZ_axis L110
• theorem slotKerDotZ_gauge L116
• lemma classDot_slotDeficit_reindex L120
• theorem classDot_slotDeficitKer_axis L147
• theorem classDot_slotDeficitKer_gauge L154
• theorem transportedSlotTerm_axis_zeroMomentum L161
• theorem transportedSlotTerm_gauge_zeroMomentum L166
• lemma zero_smul_symbolDir L171
• theorem foldAlong_axis_zero L175
• theorem foldAlong_gauge_zero L180
• def m2SlotCoeff L185
• def m2Symbol L194
• def phase2Nat L197
• lemma slotAreaCov_eq_cast L202
• theorem phaseScale_eq_phase2Nat L207
• def slotA0Z4 L227
• def slotKppZ L230
• def m2SlotCertZ L235
• theorem m2SlotCoeff_eq_cert L238
• theorem sum_m2SlotCertZ_axis L290
• theorem sum_m2SlotCertZ_gauge L297
• lemma sum_div_const L302
• theorem m2Symbol_axisTTPlus L307
• theorem m2Symbol_decoyGauge L318
• theorem m2Symbol_axisTTPlus_ne_zero L329
• def FoldAlongM2Tendsto L334
• def FoldAlongM2Tendsto_axisTTPlus L338
• def FoldAlongM2Tendsto_decoyGauge L342
• theorem FoldAlongM2Tendsto_axis_iff L346
• theorem FoldAlongM2Tendsto_gauge_iff L352
• structure BlochM2Symbol4DStatus L358
• def blochM2Symbol4DStatus L369
• theorem blochM2Symbol4DStatus_flags L379