IndisputableMonolith.Gravity.Analysis.ReggeHinge4DStarKernel13Audit

   1import IndisputableMonolith.Gravity.Analysis.ReggeHinge4DStarKernel13
   2
   3/-!
   4# Axiom audit for `ReggeHinge4DStarKernel13`
   5
   6Under the worktree shared-`.lake` symlink, `lake build` may no-op and new
   7modules do not emit oleans.  The binding axiom audit is therefore the
   8`#print axioms` block at the end of
   9`ReggeHinge4DStarKernel13.lean`, verified by
  10
  11```
  12lake env lean IndisputableMonolith/Gravity/Analysis/ReggeHinge4DStarKernel13.lean
  13```
  14
  15Every public theorem must print within
  16`[propext, Classical.choice, Quot.sound]`.
  17
  18When an olean is available (non-symlink build), the block below is the
  19standalone audit surface.
  20-/
  21
  22open IndisputableMonolith.Gravity.Analysis.ReggeHinge4DStarKernel13
  23
  24#print axioms cubeContainsHinge_origin
  25#print axioms star_cube_cardinality
  26#print axioms only_origin_contains_hinge
  27#print axioms starMembers_length
  28#print axioms starMembers_complete
  29#print axioms star_cardinality
  30#print axioms cosDihedral_t13_flat
  31#print axioms arccos_one_half
  32#print axioms star_flat_angle_sum_two_pi
  33#print axioms starFlatCosines_match
  34#print axioms hasDerivAt_t13_coord
  35#print axioms chainT13_eq
  36#print axioms t13DeficitKernel_eq_chain
  37#print axioms swap12Class_eq_table
  38#print axioms fullStarClassKernel_eq
  39#print axioms fullStarClassKernel_values
  40#print axioms fullStarClassKernel_zero_off
  41#print axioms fullStarClassKernel_nonvacuous
  42#print axioms fullStarClassKernel_swap12
  43#print axioms fullStar_uniformScale_decoy
  44#print axioms fullStar_homothety_stationary
  45#print axioms hinge4DStarKernel13Status_flags
  46