`IndisputableMonolith.Gravity.Analysis.ReggeHinge4DStarKernelAudit`

IndisputableMonolith/Gravity/Analysis/ReggeHinge4DStarKernelAudit.lean · 32 lines · 0 declarations

Explainer status: pending

   1import IndisputableMonolith.Gravity.Analysis.ReggeHinge4DStarKernel
   2
   3/-!
   4# Axiom audit for `ReggeHinge4DStarKernel`
   5
   6Every public theorem must print within
   7`[propext, Classical.choice, Quot.sound]`.
   8-/
   9
  10open IndisputableMonolith.Gravity.Analysis.ReggeHinge4DStarKernel
  11
  12#print axioms starMembers_length
  13#print axioms starMembers_complete
  14#print axioms star_cardinality
  15#print axioms cosDihedral_opp_flat
  16#print axioms cosDihedral_orth_flat
  17#print axioms arccos_one_div_sqrt_two
  18#print axioms star_flat_angle_sum_two_pi
  19#print axioms starFlatCosines_match_orbits
  20#print axioms hasDerivAt_opp_coord
  21#print axioms hasDerivAt_orth_coord
  22#print axioms oppDeficitKernel_eq_chain
  23#print axioms orthDeficitKernel_eq_chain
  24#print axioms fullStarClassKernel_eq
  25#print axioms fullStarClassKernel_values
  26#print axioms fullStarClassKernel_zero_off
  27#print axioms fullStarClassKernel_nonvacuous
  28#print axioms fullStarClassKernel_swap23
  29#print axioms fullStar_uniformScale_decoy
  30#print axioms fullStar_homothety_stationary
  31#print axioms hinge4DStarKernelStatus_flags
  32

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