IndisputableMonolith.Gravity.SevenGaps.WickActionCutLimitAudit

   1import IndisputableMonolith.Gravity.SevenGaps.WickActionCutLimit
   2
   3/-!
   4# Axiom audit: Wave C4 N4 WickActionCutLimit
   5
   6Headline theorems must print within
   7`[propext, Classical.choice, Quot.sound]`.
   8-/
   9
  10open IndisputableMonolith.Gravity.SevenGaps.WickActionInteriorHinge
  11
  12#check csqrt_of_im_neg
  13#check tendsto_pentHingeCosPath_one
  14#check tendsto_csqrt_sq_sub_one_one
  15#check eventually_carccos_log_arg_eq
  16#check eventually_im_log_arg_nonneg
  17#check carccos_tendsto_at_cut_one_holds
  18#check carccos_tendsto_at_cut_one_inhabited
  19#check lorentzAnchor_one_holds
  20#check lorentzAnchor_one_inhabited
  21#check wickActionCutLimitStatus_flags
  22
  23#print axioms csqrt_of_im_neg
  24#print axioms tendsto_pentHingeCosPath_one
  25#print axioms tendsto_csqrt_sq_sub_one_one
  26#print axioms carccos_tendsto_at_cut_one_holds
  27#print axioms lorentzAnchor_one_holds
  28#print axioms wickActionCutLimitStatus_flags
  29