IndisputableMonolith.Gravity.Analysis.ReggeFlat4DHessianAssemblyAudit
IndisputableMonolith/Gravity/Analysis/ReggeFlat4DHessianAssemblyAudit.lean · 105 lines · 0 declarations
show as:
view math explainer →
1import IndisputableMonolith.Gravity.Analysis.ReggeFlat4DHessianAssembly
2
3/-!
4# Axiom audit for `ReggeFlat4DHessianAssembly`
5
6Every public theorem must print within
7`[propext, Classical.choice, Quot.sound]`.
8-/
9
10open IndisputableMonolith.Gravity.Analysis.ReggeFlat4DHessianAssembly
11
12#print axioms hasDerivAt_heronSq_a
13#print axioms hasDerivAt_heronSq_b
14#print axioms hasDerivAt_heronSq_c
15#print axioms hasDerivAt_hingeArea_a
16#print axioms hasDerivAt_hingeArea_b
17#print axioms hasDerivAt_hingeArea_c
18#print axioms heronSq_t11
19#print axioms heronSq_t12
20#print axioms heronSq_t13
21#print axioms heronSq_t22
22#print axioms hingeArea_t11
23#print axioms hingeArea_t12
24#print axioms hingeArea_t13
25#print axioms hingeArea_t22
26#print axioms areaGradA_t11
27#print axioms areaGradB_t11
28#print axioms areaGradC_t11
29#print axioms areaGradA_t12
30#print axioms areaGradB_t12
31#print axioms areaGradC_t12
32#print axioms areaGradA_t13
33#print axioms areaGradB_t13
34#print axioms areaGradC_t13
35#print axioms areaGradA_t22
36#print axioms areaGradB_t22
37#print axioms areaGradC_t22
38#print axioms hasDerivAt_area_t11_a
39#print axioms hasDerivAt_area_t11_b
40#print axioms hasDerivAt_area_t11_c
41#print axioms hasDerivAt_area_t12_a
42#print axioms hasDerivAt_area_t12_b
43#print axioms hasDerivAt_area_t12_c
44#print axioms hasDerivAt_area_t13_a
45#print axioms hasDerivAt_area_t13_b
46#print axioms hasDerivAt_area_t13_c
47#print axioms hasDerivAt_area_t22_a
48#print axioms hasDerivAt_area_t22_b
49#print axioms hasDerivAt_area_t22_c
50#print axioms complement_preserves_edge_mask
51#print axioms kernel21_eq_kernel12
52#print axioms kernel31_eq_kernel13
53#print axioms complement_swaps_type_reexport
54#print axioms areaCov11_eq_grads
55#print axioms areaCov12_eq_grads
56#print axioms areaCov22_eq_grads
57#print axioms orbitCellCount_eq_classification
58#print axioms classDot_add
59#print axioms classDot_smul
60#print axioms orbitZeroMomQuadratic_eq_bilinear
61#print axioms trueWeightZeroMomQuadratic_eq_bilinear
62#print axioms trueWeightZeroMomBilinear_symm
63#print axioms trueWeightZeroMomBilinear_add_left
64#print axioms trueWeightZeroMomBilinear_smul_left
65#print axioms trueWeightZeroMomQuadratic_add
66#print axioms classCoeff_axisTTPlus_int
67#print axioms classCoeff_decoyGauge_bit
68#print axioms kernel11_eq_sign
69#print axioms kernel12_eq_sign
70#print axioms kernel13_eq_sign
71#print axioms kernel22_eq_sign
72#print axioms signDotAxis_kernel11
73#print axioms signDotAxis_kernel12
74#print axioms signDotAxis_kernel13
75#print axioms signDotAxis_kernel22
76#print axioms signDotGauge_kernel11
77#print axioms signDotGauge_kernel12
78#print axioms signDotGauge_kernel13
79#print axioms signDotGauge_kernel22
80#print axioms deficitKernel11_dot_axisTTPlus
81#print axioms deficitKernel12_dot_axisTTPlus
82#print axioms deficitKernel13_dot_axisTTPlus
83#print axioms deficitKernel22_dot_axisTTPlus
84#print axioms deficitKernel11_dot_decoyGauge
85#print axioms deficitKernel12_dot_decoyGauge
86#print axioms deficitKernel13_dot_decoyGauge
87#print axioms deficitKernel22_dot_decoyGauge
88#print axioms deficitKernel11_dot_decoyTrace
89#print axioms deficitKernel12_dot_decoyTrace
90#print axioms deficitKernel13_dot_decoyTrace
91#print axioms deficitKernel22_dot_decoyTrace
92#print axioms deficitKernel11_dot_homothety
93#print axioms deficitKernel12_dot_homothety
94#print axioms deficitKernel13_dot_homothety
95#print axioms deficitKernel22_dot_homothety
96#print axioms orbitDeficit_dot_axisTTPlus
97#print axioms orbitDeficit_dot_decoyGauge
98#print axioms orbitDeficit_dot_decoyTrace
99#print axioms trueWeightZeroMomQuadratic_axisTTPlus
100#print axioms trueWeightZeroMomQuadratic_decoyGauge
101#print axioms trueWeightZeroMomQuadratic_decoyTrace
102#print axioms trueWeightZeroMomQuadratic_homothety
103#print axioms trueWeight_kills_gauge_at_zero_momentum
104#print axioms flat4DHessianAssemblyStatus_flags
105