IndisputableMonolith.Gravity.SevenGaps.Gap2TailAutFiberParityBlockerAudit

   1import IndisputableMonolith.Gravity.SevenGaps.Gap2TailAutFiberParityBlocker
   2
   3/-!
   4# Axiom audit: Gap2 R4 Aut-fiber parity blocker
   5
   6Headline theorems must print within
   7`[propext, Classical.choice, Quot.sound]`.
   8-/
   9
  10open IndisputableMonolith.Gravity.SevenGaps.Gap2TailAutFiberParityBlocker
  11
  12#check AutFiberBucket
  13#check TailAutFiberEven
  14#check TailAutFiberParityBlocker
  15#check classMu_eq_one_div_shellAutCard
  16#check shellAutCard_eq_of_classMu_eq
  17#check even_card_of_tick_add_four
  18#check tailAutFiberEven_of_tailAntipodalShift
  19#check no_tailAntipodalShift_of_parityBlocker
  20#check BareR5DecoyCertificate
  21#check bareR5DecoyCertificate
  22#check bareR5DecoyCertificate_banked
  23#check gap2TailAutFiberParityBlockerStatus_flags
  24
  25#print axioms classMu_eq_one_div_shellAutCard
  26#print axioms shellAutCard_eq_of_classMu_eq
  27#print axioms even_card_of_tick_add_four
  28#print axioms tailAutFiberEven_of_tailAntipodalShift
  29#print axioms no_tailAntipodalShift_of_parityBlocker
  30#print axioms bareR5DecoyCertificate_banked
  31#print axioms gap2TailAutFiberParityBlockerStatus_flags
  32