IndisputableMonolith.Gravity.SevenGaps.Gap2SignatureBlockerAttackAudit

   1import IndisputableMonolith.Gravity.SevenGaps.Gap2SignatureBlockerAttack
   2
   3/-!
   4# Axiom audit: Wave C1 R4 signature Fin-8 tick blocker attack
   5
   6Headline theorems must print within
   7`[propext, Classical.choice, Quot.sound]`.
   8-/
   9
  10open IndisputableMonolith.Gravity.SevenGaps.Gap2SignatureBlockerAttack
  11
  12#check signatureMass_eq_burnside
  13#check shellMass_eq_sum_signatureMass
  14#check exactShellAmplitude_signature_fiberwise
  15#check signatureMass_cube_two
  16#check signatureMass_cube
  17#check burnsideMass_cube_eq_pow
  18#check signatureFin8OscillatoryTailBlocker_iff_signatureMassCancellation
  19#check gap2SignatureBlockerAttackStatus_flags
  20
  21#print axioms signatureMass_eq_burnside
  22#print axioms shellMass_eq_sum_signatureMass
  23#print axioms exactShellAmplitude_signature_fiberwise
  24#print axioms signatureMass_cube_two
  25#print axioms signatureMass_cube
  26#print axioms burnsideMass_cube_eq_pow
  27#print axioms signatureFin8OscillatoryTailBlocker_iff_signatureMassCancellation
  28#print axioms gap2SignatureBlockerAttackStatus_flags
  29