`IndisputableMonolith.Gravity.SevenGaps.HKTDynamicTargetAudit`

IndisputableMonolith/Gravity/SevenGaps/HKTDynamicTargetAudit.lean · 14 lines · 0 declarations

Explainer status: pending

   1import IndisputableMonolith.Gravity.SevenGaps.HKTDynamicTarget
   2
   3open IndisputableMonolith.Gravity.SevenGaps.HKTDynamicTarget
   4
   5#check HojmanKucharTeitelboimTargetDyn
   6#check HKTRigidityStatementDyn
   7#check unitStructure_recovers_original_ham_ham_RHS
   8#check unitStructure_is_phaseSpaceConstant
   9#check hktDynamicTargetStatus_flags
  10
  11#print axioms unitStructure_recovers_original_ham_ham_RHS
  12#print axioms unitStructure_is_phaseSpaceConstant
  13#print axioms hktDynamicTargetStatus_flags
  14

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