IndisputableMonolith.Gravity.SevenGaps.Gap2TickPhaseTailBlockerAudit

   1import IndisputableMonolith.Gravity.SevenGaps.Gap2TickPhaseTailBlocker
   2
   3/-!
   4# Axiom audit: Wave C1 R4 gap2 tick-phase tail blocker
   5
   6Headline theorems must print within
   7`[propext, Classical.choice, Quot.sound]`.
   8-/
   9
  10open IndisputableMonolith.Gravity.SevenGaps.Gap2TickPhaseTailBlocker
  11
  12#check exactPathClass_zero_subsingleton
  13#check exactPathClass_zero_subsingleton_or_the_precise_finite_head_fact
  14#check tickFiberMass_shell_zero
  15#check no_tickFiberMassBalanced
  16#check exactShellAmplitude_eq_zero_of_massBalanced_at
  17#check tickFiberMassBalanced_implies_exactShellTailCancellation
  18#check tickFiberMassBalanced_implies_oscillatoryTail
  19#check exactShellTailCancellation_of_identically_zero_amplitudes
  20#check EventuallyTickFiberMassBalanced
  21#check eventuallyTickFiberMassBalanced_implies_oscillatoryTail
  22#check eventuallyTickFiberMassBalanced_implies_exactShellTailCancellation
  23#check ShellSigTick
  24#check SignatureFin8OscillatoryTailBlocker
  25#check gap2TickPhaseTailBlockerStatus_flags
  26
  27#print axioms exactPathClass_zero_subsingleton
  28#print axioms exactPathClass_zero_subsingleton_or_the_precise_finite_head_fact
  29#print axioms tickFiberMass_shell_zero
  30#print axioms no_tickFiberMassBalanced
  31#print axioms exactShellAmplitude_eq_zero_of_massBalanced_at
  32#print axioms tickFiberMassBalanced_implies_exactShellTailCancellation
  33#print axioms tickFiberMassBalanced_implies_oscillatoryTail
  34#print axioms exactShellTailCancellation_of_identically_zero_amplitudes
  35#print axioms eventuallyTickFiberMassBalanced_implies_oscillatoryTail
  36#print axioms eventuallyTickFiberMassBalanced_implies_exactShellTailCancellation
  37#print axioms gap2TickPhaseTailBlockerStatus_flags
  38