IndisputableMonolith.Gravity.Analysis.ReggeHinge4DOrbitClassificationAudit
IndisputableMonolith/Gravity/Analysis/ReggeHinge4DOrbitClassificationAudit.lean · 45 lines · 0 declarations
show as:
view math explainer →
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