IndisputableMonolith.Gravity.SevenGaps.WickActionCertAssemblyAudit

   1import IndisputableMonolith.Gravity.SevenGaps.WickActionCertAssembly
   2
   3/-!
   4# Axiom audit: Wave C4 R5 WickActionCertAssembly
   5
   6Headline theorems must print within
   7`[propext, Classical.choice, Quot.sound]`.
   8Zero `sorryAx`.
   9-/
  10
  11open IndisputableMonolith.Gravity.SevenGaps.WickActionInteriorHinge
  12
  13#check carccos_at_lorentz_cut_one
  14#check carccos_value_ne_cut_limit_one
  15#check contAction_not_satisfiable_at_one
  16#check continuousOn_wickActionPath_Ioc_one
  17#check wickActionContinuationCertV2_one
  18#check wick_action_continuation_v2_at_one_holds
  19#check decoy_euclidean_only_falsified
  20#check decoy_interior_nhds_not_cutLimit_filter
  21#check wickActionCertAssemblyStatus_flags
  22
  23#print axioms carccos_at_lorentz_cut_one
  24#print axioms carccos_value_ne_cut_limit_one
  25#print axioms contAction_not_satisfiable_at_one
  26#print axioms continuousOn_wickActionPath_Ioc_one
  27#print axioms wickActionContinuationCertV2_one
  28#print axioms wick_action_continuation_v2_at_one_holds
  29#print axioms decoy_euclidean_only_falsified
  30#print axioms wickActionCertAssemblyStatus_flags
  31