`IndisputableMonolith.Gravity.SevenGaps.Gap2CertifiedFin8PhaseCloseAudit`

IndisputableMonolith/Gravity/SevenGaps/Gap2CertifiedFin8PhaseCloseAudit.lean · 23 lines · 0 declarations

Explainer status: pending

   1import IndisputableMonolith.Gravity.SevenGaps.Gap2CertifiedFin8PhaseClose
   2
   3/-!
   4# Axiom audit: Gap2 certified Fin-8 phase close API
   5
   6Headline theorems must print within
   7`[propext, Classical.choice, Quot.sound]`.
   8-/
   9
  10open IndisputableMonolith.Gravity.SevenGaps.Gap2CertifiedFin8PhaseClose
  11
  12#check CertifiedTickRecipeKind
  13#check CertifiedTickRecipe
  14#check CertifiedGap2Fin8PhaseClose
  15#check TypedResidual_certified_fin8_phase_close
  16#check typedResidual_continuum_substrate_oscillatoryTail_of_certified_fin8
  17#check bare_r5_of_certified_fin8_phase_close
  18#check gap2CertifiedFin8PhaseCloseStatus_flags
  19
  20#print axioms typedResidual_continuum_substrate_oscillatoryTail_of_certified_fin8
  21#print axioms bare_r5_of_certified_fin8_phase_close
  22#print axioms gap2CertifiedFin8PhaseCloseStatus_flags
  23

source mirrored from github.com/jonwashburn/shape-of-logic