`IndisputableMonolith.Gravity.Analysis.ReggeHinge4DStarKernel12Audit`

IndisputableMonolith/Gravity/Analysis/ReggeHinge4DStarKernel12Audit.lean · 30 lines · 0 declarations

Explainer status: pending

   1import IndisputableMonolith.Gravity.Analysis.ReggeHinge4DStarKernel12
   2
   3/-!
   4# Axiom audit for `ReggeHinge4DStarKernel12`
   5
   6Every public theorem must print within
   7`[propext, Classical.choice, Quot.sound]`.
   8-/
   9
  10open IndisputableMonolith.Gravity.Analysis.ReggeHinge4DStarKernel12
  11
  12#print axioms starMembers_length
  13#print axioms starMembers_complete
  14#print axioms star_cardinality
  15#print axioms cosDihedral_near_flat
  16#print axioms cosDihedral_far_flat
  17#print axioms star_flat_angle_sum_two_pi
  18#print axioms starFlatCosines_match_orbits
  19#print axioms hasDerivAt_near_coord
  20#print axioms hasDerivAt_far_coord
  21#print axioms nearDeficitKernel_eq_chain
  22#print axioms farDeficitKernel_eq_chain
  23#print axioms fullStarClassKernel_eq
  24#print axioms fullStarClassKernel_values
  25#print axioms fullStarClassKernel_nonvacuous
  26#print axioms fullStarClassKernel_swap12
  27#print axioms fullStar_uniformScale_decoy
  28#print axioms fullStar_homothety_stationary
  29#print axioms hinge4DStarKernel12Status_flags
  30

source mirrored from github.com/jonwashburn/shape-of-logic