IndisputableMonolith.Gravity.SevenGaps.HKTGroundworkAudit

   1import IndisputableMonolith.Gravity.SevenGaps.HKTOneSiteCounterexample
   2import IndisputableMonolith.Gravity.SevenGaps.HKTDynamicTarget
   3import IndisputableMonolith.Gravity.SevenGaps.HKTLocalFunctionalEquation
   4
   5/-!
   6# Axiom audit: Wave C2 R5/R6 HKT groundwork
   7-/
   8
   9open IndisputableMonolith.Gravity.SevenGaps.HKTOneSiteCounterexample
  10open IndisputableMonolith.Gravity.SevenGaps.HKTDynamicTarget
  11open IndisputableMonolith.Gravity.SevenGaps.HKTLocalFunctionalEquation
  12
  13#check quarticOneSiteHKT
  14#check one_site_wronskians_vacuous
  15#check not_HKTRigidityStatement_one
  16#check HojmanKucharTeitelboimTargetDyn
  17#check HKTRigidityStatementDyn
  18#check unitStructure_recovers_original_ham_ham_RHS
  19#check unitStructure_is_phaseSpaceConstant
  20#check hktDynamicTargetStatus_flags
  21#check local_profile_ham_ham_form
  22#check localHamHamCoefficient_witnesses_identity
  23
  24#print axioms one_site_wronskians_vacuous
  25#print axioms not_HKTRigidityStatement_one
  26#print axioms unitStructure_recovers_original_ham_ham_RHS
  27#print axioms unitStructure_is_phaseSpaceConstant
  28#print axioms hktDynamicTargetStatus_flags
  29#print axioms local_profile_ham_ham_form
  30#print axioms localHamHamCoefficient_witnesses_identity
  31#print axioms bracket_quarticHam_quarticHam
  32