IndisputableMonolith.Gravity.SevenGaps.WickActionInteriorHingeAudit

   1import IndisputableMonolith.Gravity.SevenGaps.WickActionInteriorHinge
   2
   3/-!
   4# Axiom audit: Wave C4 R2 WickActionInteriorHinge (schema + N1/N2)
   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 carccos
  14#check pentHingeCosPath
  15#check dihedralSumPath
  16#check hingeArea
  17#check wickActionPath
  18#check euclidCos
  19#check lorentzCos
  20#check lorentzRapidity
  21#check lorentzAngleRe
  22#check euclidArea
  23#check euclidAngle
  24#check WickActionContinuationCert
  25#check wick_action_continuation_4d
  26#check offArccosCut_slitPlane
  27#check continuousOn_carccos
  28#check carccos_real_eq_arccos
  29#check wickActionInteriorHingeStatus_flags
  30
  31#print axioms offArccosCut_slitPlane
  32#print axioms continuousOn_carccos
  33#print axioms carccos_real_eq_arccos
  34#print axioms wickActionInteriorHingeStatus_flags
  35