IndisputableMonolith.Gravity.SevenGaps.Gap5ConstraintCloseStatusAudit

   1import IndisputableMonolith.Gravity.SevenGaps.Gap5ConstraintCloseStatus
   2
   3/-!
   4# Axiom audit: Wave C5 Gap5ConstraintCloseStatus
   5
   6Headline theorems must print within
   7`[propext, Classical.choice, Quot.sound]`.
   8Zero `sorryAx`.
   9-/
  10
  11open IndisputableMonolith.Gravity.SevenGaps.Gap5ConstraintCloseStatus
  12open IndisputableMonolith.Gravity.SevenGaps.HKTKineticNormalizedRigidity
  13open IndisputableMonolith.Gravity.SevenGaps.HKTVacuumSectorKill
  14open IndisputableMonolith.Gravity.SevenGaps.HKTCanonicalMomTarget
  15open IndisputableMonolith.Gravity.SevenGaps.HKTOneSiteCounterexample
  16open IndisputableMonolith.Gravity.SevenGaps.FullTheoryLedger
  17open IndisputableMonolith.Gravity.SevenGaps.CampaignLedger
  18open IndisputableMonolith.Gravity.SevenGaps.Gap5ConstraintResidualDAG
  19
  20#check hojman_pins_general_relativity_holds
  21#check gap5_constraint_recovery_both_halves
  22#check gap5_constraint_recovery_bound_to_terminals
  23#check gap5_kill_tower_scope_certificate
  24#check gap5ConstraintCloseStatus_flags
  25#check ftc_recovery_of_normalized
  26
  27#print axioms hojman_pins_general_relativity_holds
  28#print axioms gap5_constraint_recovery_both_halves
  29#print axioms gap5_constraint_recovery_bound_to_terminals
  30#print axioms gap5_kill_tower_scope_certificate
  31#print axioms ftc_recovery_of_normalized
  32#print axioms not_HKTRigidityStatement_one
  33#print axioms not_HKTRigidityStatementPointSplitDynN2Strong
  34#print axioms not_HKTRigidityStatementPointSplitDynN2Canonical
  35#print axioms not_HKTRigidityModVacuumStatementN2
  36
  37example : fullTheoryBenchmarks.gap5_constraint_recovery = true := rfl
  38example : sevenGapsCampaignStatus.gap5_continuum_algebra_hkt_open = false := rfl
  39example : gap5ResidualDAGStatus.hktRigidityOpen = false := rfl
  40example : gap5ResidualDAGStatus.packagedTargetOpen = false := rfl
  41example : gap5ResidualDAGStatus.gap5ConstraintRecovery = true := rfl
  42