IndisputableMonolith.Gravity.SevenGaps.GaugeHistoryMeasureAudit

   1import IndisputableMonolith.Gravity.SevenGaps.GaugeHistoryMeasure
   2
   3/-!
   4# Axiom audit: Wave C1 R5 gauge-history measure (post-critic repair)
   5
   6Headline theorems must print within
   7`[propext, Classical.choice, Quot.sound]`.
   8-/
   9
  10open IndisputableMonolith.Gravity.SevenGaps.GaugeHistoryMeasure
  11
  12#check PostedBoundedHistory
  13#check canonicalHistory
  14#check CanonicalHistory
  15#check CanonicalHistory.fiber_unique
  16#check CanonicalHistory.equivUnderlying
  17#check HistoryRelabel
  18#check HistoryRelabel.toRelabel
  19#check HistoryRelabel.ofRelabel
  20#check historyRelabel_equiv_relabel
  21#check historyRelabel_equiv_relabel_canonical
  22#check historyOrbitCardClass
  23#check historyPairCountClass
  24#check GaugeHistoryEnrichment
  25#check nuBuild
  26#check nuBuild_def_history_only
  27#check history_class_equiv_orbit
  28#check historyOrbitCardClass_eq_orbitCardClass
  29#check history_pair_equiv_pair
  30#check historyPairCountClass_eq_pairCountClass
  31#check nuBuild_gaugeCounting
  32#check nuBuild_eq_gaugeOrbitMass
  33#check gap2_gauge_counting_from_history_discharged
  34#check TypedResidual_gap2_gauge_counting_from_history
  35#check typedResidual_gap2_gauge_counting_from_history_closed
  36#check TypedResidual_gap2_gauge_counting_from_history_closed
  37#check circularNu
  38#check circularNu_def_is_gaugeOrbitMass
  39#check circularNu_satisfies_gaugeCounting
  40#check decoy_uniformClassMass_not_gaugeCounting
  41#check gap2_history_measure_decoy_anchors
  42
  43#print axioms CanonicalHistory.fiber_unique
  44#print axioms historyRelabel_equiv_relabel
  45#print axioms nuBuild_def_history_only
  46#print axioms historyOrbitCardClass_eq_orbitCardClass
  47#print axioms historyPairCountClass_eq_pairCountClass
  48#print axioms nuBuild_gaugeCounting
  49#print axioms nuBuild_eq_gaugeOrbitMass
  50#print axioms gap2_gauge_counting_from_history_discharged
  51#print axioms typedResidual_gap2_gauge_counting_from_history_closed
  52#print axioms TypedResidual_gap2_gauge_counting_from_history_closed
  53#print axioms circularNu_def_is_gaugeOrbitMass
  54#print axioms circularNu_satisfies_gaugeCounting
  55#print axioms decoy_uniformClassMass_not_gaugeCounting
  56#print axioms gap2_history_measure_decoy_anchors
  57