Pith. sign in

IndisputableMonolith.Gravity.Analysis.ReggeHinge4DOrbitClassificationAudit

IndisputableMonolith/Gravity/Analysis/ReggeHinge4DOrbitClassificationAudit.lean · 45 lines · 0 declarations

show as:
view math explainer →

open module explainer GitHub source

Explainer status: pending

   1import IndisputableMonolith.Gravity.Analysis.ReggeHinge4DOrbitClassification
   2
   3/-!
   4# Axiom audit: `ReggeHinge4DOrbitClassification`
   5
   6`#print axioms` for every public theorem of the 4D triangle-hinge orbit
   7classification.  Expected footprint:
   8`[propext, Classical.choice, Quot.sound]`.
   9-/
  10
  11open IndisputableMonolith.Gravity.Analysis.ReggeHinge4DOrbitClassification
  12
  13#print axioms hingeTypePop_is_orbitType
  14#print axioms hingeOrbitType_toPop
  15#print axioms triangle_diff_masks_ok
  16#print axioms cellTriangleCount_t11
  17#print axioms cellTriangleCount_t12
  18#print axioms cellTriangleCount_t21
  19#print axioms cellTriangleCount_t13
  20#print axioms cellTriangleCount_t31
  21#print axioms cellTriangleCount_t22
  22#print axioms cellTriangleCount_values
  23#print axioms cellTriangleCount_sum
  24#print axioms oriented_slot_total
  25#print axioms disjoint_implies_realizable
  26#print axioms decoy_overlapping_not_realizable
  27#print axioms decoy_overlapping_is_not_disjoint
  28#print axioms seed_slot_masks
  29#print axioms seed_hinge_type_t11
  30#print axioms coordPerm_preserves_pop
  31#print axioms coordPerm_preserves_type
  32#print axioms orbitRep_realizable
  33#print axioms orbitRep_type
  34#print axioms realizable_in_type_orbit
  35#print axioms realizable_matches_rep_orbit
  36#print axioms complement_preserves_kuhn
  37#print axioms complement_swaps_diff_pair
  38#print axioms complement_swaps_type
  39#print axioms orbit_count_S4
  40#print axioms orbit_count_S4_complement
  41#print axioms absolute_t11_not_S4_transitive
  42#print axioms orbitLocalSq_values
  43#print axioms slot_localSq
  44#print axioms hinge4DOrbitClassificationStatus_flags
  45

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