IndisputableMonolith.Gravity.SevenGaps.Gap2EnrichedCarrierPhaseAudit

   1import IndisputableMonolith.Gravity.SevenGaps.Gap2EnrichedCarrierPhase
   2
   3/-!
   4# Axiom audit: Wave C R5 enriched-carrier phase terminal
   5
   6Headline theorems must print within
   7`[propext, Classical.choice, Quot.sound]`.
   8-/
   9
  10open IndisputableMonolith.Gravity.SevenGaps.Gap2EnrichedCarrierPhase
  11
  12#check descendedTick
  13#check GlobalEquivalentInvariant
  14#check selfLoopCount_congr
  15#check selfLoopTick_invariant
  16#check selfLoopClassTick_not_ShellSigTick
  17#check oscillatoryTail_of_enriched_eventual_balance
  18#check oscillatoryTail_of_enriched_identically_zero
  19#check TypedResidual_enriched_carrier_oscillatoryTail
  20#check bare_r5_of_enriched_carrier_oscillatoryTail
  21#check typedResidual_continuum_substrate_oscillatoryTail_of_enriched
  22#check enrichedCarrierPhaseSubstrate_nonempty
  23#check signatureBlocker_iff_no_shellSig_oscillatoryTail
  24#check gap2EnrichedCarrierPhaseStatus_flags
  25
  26#print axioms selfLoopCount_congr
  27#print axioms selfLoopTick_invariant
  28#print axioms selfLoopClassTick_not_ShellSigTick
  29#print axioms oscillatoryTail_of_enriched_eventual_balance
  30#print axioms oscillatoryTail_of_enriched_identically_zero
  31#print axioms bare_r5_of_enriched_carrier_oscillatoryTail
  32#print axioms typedResidual_continuum_substrate_oscillatoryTail_of_enriched
  33#print axioms enrichedCarrierPhaseSubstrate_nonempty
  34#print axioms gap2EnrichedCarrierPhaseStatus_flags
  35