IndisputableMonolith.Gravity.SevenGaps.WickActionCutLimitFamilyAudit

   1import IndisputableMonolith.Gravity.SevenGaps.WickActionCutLimitFamily
   2
   3/-!
   4# Axiom audit: Wave C4 F1 WickActionCutLimitFamily
   5
   6Headline theorems must print within
   7`[propext, Classical.choice, Quot.sound]`.
   8-/
   9
  10open IndisputableMonolith.Gravity.SevenGaps.WickActionInteriorHinge
  11
  12#check lorentzK_gt_one
  13#check lorentzCos_eq_neg_lorentzK
  14#check rapidityPinned_of_causal
  15#check tendsto_pentHingeCosPath_of_causal
  16#check tendsto_csqrt_sq_sub_one_of_causal
  17#check eventually_carccos_log_arg_eq_of_causal
  18#check eventually_im_log_arg_nonneg_of_causal
  19#check carccos_tendsto_at_cut_of_causal
  20#check carccos_tendsto_at_cut_family_holds
  21#check lorentzAnchor_of_causal
  22#check continuousOn_wickActionPath_Ioc_of_causal
  23#check wickActionCutLimitFamilyStatus_flags
  24
  25#print axioms rapidityPinned_of_causal
  26#print axioms carccos_tendsto_at_cut_of_causal
  27#print axioms lorentzAnchor_of_causal
  28#print axioms continuousOn_wickActionPath_Ioc_of_causal
  29#print axioms carccos_tendsto_at_cut_family_holds
  30#print axioms wickActionCutLimitFamilyStatus_flags
  31