IndisputableMonolith.Gravity.SevenGaps.Gap2TailFiberShiftBridgeAudit

   1import IndisputableMonolith.Gravity.SevenGaps.Gap2TailFiberShiftBridge
   2
   3/-!
   4# Axiom audit: Wave C1 R4 conditional TailFiberShift bridge
   5
   6Headline theorems must print within
   7`[propext, Classical.choice, Quot.sound]`.
   8-/
   9
  10open IndisputableMonolith.Gravity.SevenGaps.Gap2TailFiberShiftBridge
  11
  12#check TailFiberShift
  13#check tickFiberMass_succ_of_tailFiberShift
  14#check eventuallyTickFiberMassBalanced_of_tailFiberShift
  15#check oscillatoryTail_of_tailFiberShift
  16#check oscillatoryTail_of_labeled_tailFiberShift
  17#check tick_shift_excludes_fixed_point
  18#check fixed_class_blocks_tick_shift
  19#check endpointReversal_fixes_allLoops
  20#check tetSlotRotation_fixes_constTet
  21#check endpointReversal_no_tailFiberShift
  22#check tetSlotRotation_no_tailFiberShift
  23#check endpointReversalThenTetSlotRotation_no_tailFiberShift
  24#check gap2TailFiberShiftBridgeStatus_flags
  25
  26#print axioms eventuallyTickFiberMassBalanced_of_tailFiberShift
  27#print axioms oscillatoryTail_of_tailFiberShift
  28#print axioms oscillatoryTail_of_labeled_tailFiberShift
  29#print axioms tick_shift_excludes_fixed_point
  30#print axioms fixed_class_blocks_tick_shift
  31#print axioms endpointReversal_no_tailFiberShift
  32#print axioms tetSlotRotation_no_tailFiberShift
  33#print axioms endpointReversalThenTetSlotRotation_no_tailFiberShift
  34#print axioms gap2TailFiberShiftBridgeStatus_flags
  35