`IndisputableMonolith.Gravity.SevenGaps.HKTOneSiteCounterexampleAudit`

IndisputableMonolith/Gravity/SevenGaps/HKTOneSiteCounterexampleAudit.lean · 16 lines · 0 declarations

Explainer status: pending

   1import IndisputableMonolith.Gravity.SevenGaps.HKTOneSiteCounterexample
   2
   3/-!
   4# Axiom audit: HKT one-site rigidity falsification
   5-/
   6
   7open IndisputableMonolith.Gravity.SevenGaps.HKTOneSiteCounterexample
   8
   9#check one_site_wronskians_vacuous
  10#check quarticOneSiteHKT
  11#check not_HKTRigidityStatement_one
  12
  13#print axioms one_site_wronskians_vacuous
  14#print axioms not_HKTRigidityStatement_one
  15#print axioms bracket_quarticHam_quarticHam
  16

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