IndisputableMonolith.Gravity.SevenGaps.WickActionInteriorHingeConfinementAudit

   1import IndisputableMonolith.Gravity.SevenGaps.WickActionInteriorHingeConfinement
   2
   3/-!
   4# Axiom audit: Wave C4 N3 (+ N4 fallback) WickActionInteriorHingeConfinement
   5
   6Headline theorems must print within
   7`[propext, Classical.choice, Quot.sound]`.
   8-/
   9
  10open IndisputableMonolith.Gravity.SevenGaps.WickActionInteriorHinge
  11
  12#check pentHingeCosPath_eq_moebius
  13#check pentHingeCosPath_eq_euclidCos
  14#check pentHingeCosPath_eq_lorentzCos
  15#check im_pentHingeCosPath_neg
  16#check branchRegularSum_of_causal
  17#check branchRegularSum_one
  18#check carccos_tendsto_at_cut_one
  19#check carccos_tendsto_at_cut_family
  20#check lorentzAnchor_one
  21#check rapidityPinned_one
  22#check lorentz_endpoint_not_real
  23#check wickActionInteriorHingeStatus_flags
  24
  25#print axioms pentHingeCosPath_eq_moebius
  26#print axioms im_pentHingeCosPath_neg
  27#print axioms branchRegularSum_one
  28#print axioms rapidityPinned_one
  29#print axioms lorentz_endpoint_not_real
  30#print axioms wickActionInteriorHingeStatus_flags
  31