IndisputableMonolith.Gravity.Analysis.ReggeHinge4DDihedralKernelAudit
IndisputableMonolith/Gravity/Analysis/ReggeHinge4DDihedralKernelAudit.lean · 50 lines · 0 declarations
show as:
view math explainer →
1import IndisputableMonolith.Gravity.Analysis.ReggeHinge4DDihedralKernel
2
3/-!
4# Axiom audit for `ReggeHinge4DDihedralKernel`
5
6Every public theorem must print within
7`[propext, Classical.choice, Quot.sound]`.
8-/
9
10open IndisputableMonolith.Gravity.Analysis.ReggeHinge4DDihedralKernel
11
12#print axioms seedFlatSqEdges_simplex0
13#print axioms seedFlatSqEdges_simplex1
14#print axioms cos_numForm
15#print axioms hingeGramDet_flat
16#print axioms apexDotNum_flat
17#print axioms apex3NormSqNum_flat
18#print axioms apex4NormSqNum_flat
19#print axioms cosDihedral_flat
20#print axioms cosDihedral_flat_sq
21#print axioms cosDihedral_flat_pos
22#print axioms sinDihedral_flat
23#print axioms hasDerivAt_cosDihedral_slot0
24#print axioms hasDerivAt_cosDihedral_slot1
25#print axioms hasDerivAt_cosDihedral_slot2
26#print axioms hasDerivAt_cosDihedral_slot3
27#print axioms hasDerivAt_cosDihedral_slot4
28#print axioms hasDerivAt_cosDihedral_slot5
29#print axioms hasDerivAt_cosDihedral_slot6
30#print axioms hasDerivAt_cosDihedral_slot7
31#print axioms hasDerivAt_cosDihedral_slot8
32#print axioms hasDerivAt_cosDihedral_slot9
33#print axioms hasDerivAt_cosDihedral_coord
34#print axioms angleKernel_eight
35#print axioms angleKernel_nine
36#print axioms singleSimplexDeficitKernel_eight
37#print axioms singleSimplexDeficitKernel_nine
38#print axioms singleSimplexDeficitKernel_le_seven
39#print axioms assembleClassKernel_eval
40#print axioms partialDeficitClassKernel_three
41#print axioms partialDeficitClassKernel_seven
42#print axioms partialDeficitClassKernel_eleven
43#print axioms partialDeficitClassKernel_zero_off
44#print axioms partialDeficitClassKernel_values
45#print axioms cosDihedralKernel_nonvacuous
46#print axioms cosDihedral_uniformScale_decoy
47#print axioms cosDihedral_homothety_stationary
48#print axioms partialDeficitClassKernel_swap23
49#print axioms hinge4DDihedralKernelStatus_flags
50