IndisputableMonolith.Gravity.Analysis.ReggeBlochFold4DAudit

   1import IndisputableMonolith.Gravity.Analysis.ReggeBlochFold4D
   2
   3/-!
   4# Axiom audit for `ReggeBlochFold4D`
   5
   6Every public theorem must print within
   7`[propext, Classical.choice, Quot.sound]`.
   8-/
   9
  10open IndisputableMonolith.Gravity.Analysis.ReggeBlochFold4D
  11
  12#print axioms phasedClassDot_add
  13#print axioms phasedClassDot_smul
  14#print axioms phasedClassDot_zeroMomentum
  15#print axioms isT11_iff_pop
  16#print axioms factorizedBlochFold11_zeroMomentum
  17#print axioms blochFold11_eq_bilinear
  18#print axioms blochFold11Bilinear_symm
  19#print axioms blochFold11Bilinear_add_left
  20#print axioms blochFold11Bilinear_smul_left
  21#print axioms transportedSlotTerm_zeroMomentum
  22#print axioms classCoeff_axisTTPlus_mask_1
  23#print axioms classCoeff_axisTTPlus_mask_2
  24#print axioms classCoeff_axisTTPlus_mask_3
  25#print axioms slotAreaCov_support
  26#print axioms phasedClassDot_area_axis_of_masks_1_2
  27#print axioms phasedClassDot_area_axis_of_masks_2_1
  28#print axioms transportedSlotTerm_axis_seedMasks
  29#print axioms axisStarKind_count1
  30#print axioms axisStarKind_count2
  31#print axioms gaugeStarKind_count1
  32#print axioms sum_axisStarContrib
  33#print axioms sum_gaugeStarContrib
  34#print axioms classMidpointPhase_waveStar
  35#print axioms cos_quarterTurns
  36#print axioms phasedClassDot_transportedDeficit
  37#print axioms phasedA_waveStar
  38#print axioms phasedK_waveStar
  39#print axioms transportedSlotTerm_waveStar_eval
  40#print axioms slotN_axis_match
  41#print axioms slotN_gauge_match
  42#print axioms classCoeff_decoyGauge_int
  43#print axioms transportedSlotTerm_axis_waveStar
  44#print axioms transportedSlotTerm_gauge_waveStar
  45#print axioms blochFold11_axisTTPlus_waveStar
  46#print axioms blochFold11_axisTTPlus_waveStar_ne_zero
  47#print axioms blochFold11_decoyGauge_waveStar
  48#print axioms blochFold11_decoyGauge_waveStar_ne_zero
  49#print axioms blochFold4DStatus_flags
  50