IndisputableMonolith.Gravity.SevenGaps.WickActionEuclidSchlaefliAudit

   1import IndisputableMonolith.Gravity.SevenGaps.WickActionEuclidSchlaefli
   2
   3/-!
   4# Axiom audit: Wave C4 R4 WickActionEuclidSchlaefli
   5
   6Headline theorems must print within
   7`[propext, Classical.choice, Quot.sound]`.
   8-/
   9
  10open IndisputableMonolith.Gravity.SevenGaps.WickActionInteriorHinge
  11open IndisputableMonolith.Gravity.SevenGaps.FullTheoryLedger
  12
  13#check euclidCos_mem_Ioo
  14#check hasDerivAt_euclidCos
  15#check hasDerivAt_euclidArea
  16#check euclidAngleDeriv
  17#check hasDerivAt_euclidAngle
  18#check wickActionPath_re_eq_euclidRegge
  19#check hasDerivAt_euclidAngleWeightedArea
  20#check euclid_angle_deriv_term_ne_zero_at_one
  21#check euclidSchlaefli_holds
  22#check euclidSchlaefli_field_inhabited
  23#check euclidSchlaefli_field_inhabited_one
  24#check wickActionEuclidSchlaefliStatus_flags
  25
  26#print axioms euclidCos_mem_Ioo
  27#print axioms hasDerivAt_euclidCos
  28#print axioms hasDerivAt_euclidAngle
  29#print axioms euclidSchlaefli_holds
  30#print axioms euclidSchlaefli_field_inhabited
  31#print axioms euclid_angle_deriv_term_ne_zero_at_one
  32#print axioms wickActionEuclidSchlaefliStatus_flags
  33