IndisputableMonolith.Gravity.SevenGaps.Gap2PostingCocycleCarrierAudit

   1import IndisputableMonolith.Gravity.SevenGaps.Gap2PostingCocycleCarrier
   2
   3/-!
   4# Axiom audit: Gap2 posting-cocycle carrier (STOP A)
   5
   6Headline theorems must print within
   7`[propext, Classical.choice, Quot.sound]`.
   8-/
   9
  10open IndisputableMonolith.Gravity.SevenGaps.Gap2PostingCocycleCarrier
  11
  12#check PostingEnrichedPathClass
  13#check forgetPostingPhase
  14#check postingPhase
  15#check FactorsThroughPostingForget
  16#check carrier_forgets_posting_phase
  17#check postingPhase_not_factors_through_forget
  18#check PostingEnrichedExactHistory
  19#check exact_carrier_forgets_posting_phase
  20#check exact_postingPhase_not_factors_through_forget
  21#check TypedResidual_carrier_forgets_posting_phase
  22#check typedResidual_carrier_forgets_posting_phase
  23#check PostingCocycleExactPathBridge
  24#check TypedResidual_posting_cocycle_bridge
  25#check certifiedRecipe_of_bridge
  26#check gap2PostingCocycleCarrierStatus_flags
  27
  28#print axioms carrier_forgets_posting_phase
  29#print axioms postingPhase_not_factors_through_forget
  30#print axioms exact_carrier_forgets_posting_phase
  31#print axioms exact_postingPhase_not_factors_through_forget
  32#print axioms typedResidual_carrier_forgets_posting_phase
  33#print axioms gap2PostingCocycleCarrierStatus_flags
  34