IndisputableMonolith.Gravity.Analysis.ReggeHinge4DStarKernel22Audit

   1import IndisputableMonolith.Gravity.Analysis.ReggeHinge4DStarKernel22
   2
   3/-!
   4# Axiom audit for `ReggeHinge4DStarKernel22`
   5
   6Every public theorem must print within
   7`[propext, Classical.choice, Quot.sound]`.
   8-/
   9
  10open IndisputableMonolith.Gravity.Analysis.ReggeHinge4DStarKernel22
  11
  12#print axioms starMembers_length
  13#print axioms starMembers_complete
  14#print axioms star_cardinality
  15#print axioms only_origin_corner_contains_hinge
  16#print axioms hingeGramDet_t22
  17#print axioms apexDotNum_t22
  18#print axioms apex3NormSqNum_t22
  19#print axioms apex4NormSqNum_t22
  20#print axioms cosDihedral_t22_flat
  21#print axioms flatAngleT22_eq
  22#print axioms star_flat_angle_sum_two_pi
  23#print axioms starFlatCosines_match_orbit
  24#print axioms hasDerivAt_t22_slot0
  25#print axioms hasDerivAt_t22_slot1
  26#print axioms hasDerivAt_t22_slot2
  27#print axioms hasDerivAt_t22_slot3
  28#print axioms hasDerivAt_t22_slot4
  29#print axioms hasDerivAt_t22_slot5
  30#print axioms hasDerivAt_t22_slot6
  31#print axioms hasDerivAt_t22_slot7
  32#print axioms hasDerivAt_t22_slot8
  33#print axioms hasDerivAt_t22_slot9
  34#print axioms hasDerivAt_t22_coord
  35#print axioms t22DeficitKernel_eq_chain
  36#print axioms fullStarClassKernel_eq
  37#print axioms fullStarClassKernel_values
  38#print axioms swap01Mask_bounds
  39#print axioms fullStarClassKernel_nonvacuous
  40#print axioms fullStarClassKernel_swap01
  41#print axioms fullStarClassKernel_swap23
  42#print axioms fullStar_uniformScale_decoy
  43#print axioms fullStar_homothety_stationary
  44#print axioms hinge4DStarKernel22Status_flags
  45