IndisputableMonolith.Gravity.Analysis.ReggeBlochFold4D

declarations in this module (82)

• def maskCoord L69
• def hingeBase L72
• def phasedClassDot L75
• theorem phasedClassDot_add L78
• theorem phasedClassDot_smul L85
• theorem phasedClassDot_zeroMomentum L93
• def isT11 L102
• theorem isT11_iff_pop L108
• def factorizedSlotTerm L119
• def factorizedBlochFold11 L127
• lemma t11_count_nat L130
• lemma t11_count_real L145
• theorem factorizedBlochFold11_zeroMomentum L156
• def transportPermOfDiff L185
• def permClass L201
• def transportedDeficit L208
• def slotTransportPerm L214
• def slotAreaCov L217
• def slotDeficitKer L223
• def transportedSlotTerm L226
• def blochFold11 L234
• def blochFold11Bilinear L237
• theorem blochFold11_eq_bilinear L247
• theorem blochFold11Bilinear_symm L270
• theorem blochFold11Bilinear_add_left L279
• theorem blochFold11Bilinear_smul_left L293
• theorem transportedSlotTerm_zeroMomentum L319
• theorem classCoeff_axisTTPlus_mask_1 L330
• theorem classCoeff_axisTTPlus_mask_2 L336
• theorem classCoeff_axisTTPlus_mask_3 L342
• theorem slotAreaCov_support L348
• theorem phasedClassDot_area_axis_of_masks_1_2 L357
• theorem phasedClassDot_area_axis_of_masks_2_1 L382
• theorem transportedSlotTerm_axis_seedMasks L407
• def waveStar L425
• def axisStarKind L431
• def axisStarContrib L440
• def gaugeStarKind L445
• def gaugeStarContrib L448
• theorem axisStarKind_count1 L451
• theorem axisStarKind_count2 L456
• theorem gaugeStarKind_count1 L461
• theorem sum_axisStarContrib L467
• theorem sum_gaugeStarContrib L502
• def baseTurns L529
• def dispTurns L535
• def quarterTurns L541
• def cosC1 L545
• def cosC2 L551
• lemma waveStar_dot_maskCoord L558
• lemma waveStar_dot_classDisp L569
• theorem classMidpointPhase_waveStar L579
• theorem cos_quarterTurns L588
• def slotAreaCovZ4 L627
• lemma slotAreaCov_eq_cast L632
• def slotA1 L638
• def slotA2 L643
• def slotK1 L648
• def slotK2 L654
• def slotN1 L660
• def slotN2 L666
• theorem phasedClassDot_transportedDeficit L673
• theorem phasedA_waveStar L696
• theorem phasedK_waveStar L711
• theorem transportedSlotTerm_waveStar_eval L727
• def axisCertN1 L746
• def axisCertN2 L750
• def gaugeCertN1 L755
• def gaugeCertN2 L759
• theorem slotN_axis_match L766
• def decoyGaugeCoeffZ L773
• theorem classCoeff_decoyGauge_int L775
• theorem slotN_gauge_match L785
• theorem transportedSlotTerm_axis_waveStar L793
• theorem transportedSlotTerm_gauge_waveStar L807
• theorem blochFold11_axisTTPlus_waveStar L821
• theorem blochFold11_axisTTPlus_waveStar_ne_zero L828
• theorem blochFold11_decoyGauge_waveStar L835
• theorem blochFold11_decoyGauge_waveStar_ne_zero L841
• structure BlochFold4DStatus L852

… and 2 more