IndisputableMonolith.Gravity.SevenGaps.Gap2AntipodalBalanceBridgeAudit

   1import IndisputableMonolith.Gravity.SevenGaps.Gap2AntipodalBalanceBridge
   2
   3/-!
   4# Axiom audit: Gap2 R4 antipodal balance bridge
   5
   6Headline theorems must print within
   7`[propext, Classical.choice, Quot.sound]`.
   8-/
   9
  10open IndisputableMonolith.Gravity.SevenGaps.Gap2AntipodalBalanceBridge
  11
  12#check EventuallyTickFiberAntipodalMassBalanced
  13#check tickRoot_add_four
  14#check exactShellAmplitude_eq_zero_of_antipodalBalanced_at
  15#check eventuallyAntipodalBalanced_implies_oscillatoryTail
  16#check TailAntipodalShift
  17#check tickFiberMass_add_four_of_tailAntipodalShift
  18#check eventuallyTickFiberAntipodalMassBalanced_of_tailAntipodalShift
  19#check oscillatoryTail_of_tailAntipodalShift
  20#check nonempty_tailAntipodalShift_of_tailFiberShift
  21#check eventuallyTickFiberMassBalanced_implies_antipodal
  22#check gap2AntipodalBalanceBridgeStatus_flags
  23
  24#print axioms tickRoot_add_four
  25#print axioms exactShellAmplitude_eq_zero_of_antipodalBalanced_at
  26#print axioms eventuallyAntipodalBalanced_implies_oscillatoryTail
  27#print axioms tickFiberMass_add_four_of_tailAntipodalShift
  28#print axioms eventuallyTickFiberAntipodalMassBalanced_of_tailAntipodalShift
  29#print axioms oscillatoryTail_of_tailAntipodalShift
  30#print axioms nonempty_tailAntipodalShift_of_tailFiberShift
  31#print axioms eventuallyTickFiberMassBalanced_implies_antipodal
  32#print axioms gap2AntipodalBalanceBridgeStatus_flags
  33