IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DM2NumChunk13
IndisputableMonolith/Gravity/Analysis/ReggeExactMidpointM2TTIdentity4DM2NumChunk13.lean · 279 lines · 256 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DKernelCert
3
4/-! m2Num = 8·explicitZ, chunk 13 (256 kernel decides). -/
5
6namespace IndisputableMonolith
7namespace Gravity
8namespace Analysis
9namespace ReggeExactMidpointM2TTIdentity4D
10namespace M2NumChunk13
11
12open KernelCert
13
14set_option maxRecDepth 100000
15set_option maxHeartbeats 200000000
16
17theorem e_310000 : m2Num 3 1 0 0 0 0 = 8 * explicitZ 3 1 0 0 0 0 := by decide
18theorem e_310001 : m2Num 3 1 0 0 0 1 = 8 * explicitZ 3 1 0 0 0 1 := by decide
19theorem e_310002 : m2Num 3 1 0 0 0 2 = 8 * explicitZ 3 1 0 0 0 2 := by decide
20theorem e_310003 : m2Num 3 1 0 0 0 3 = 8 * explicitZ 3 1 0 0 0 3 := by decide
21theorem e_310010 : m2Num 3 1 0 0 1 0 = 8 * explicitZ 3 1 0 0 1 0 := by decide
22theorem e_310011 : m2Num 3 1 0 0 1 1 = 8 * explicitZ 3 1 0 0 1 1 := by decide
23theorem e_310012 : m2Num 3 1 0 0 1 2 = 8 * explicitZ 3 1 0 0 1 2 := by decide
24theorem e_310013 : m2Num 3 1 0 0 1 3 = 8 * explicitZ 3 1 0 0 1 3 := by decide
25theorem e_310020 : m2Num 3 1 0 0 2 0 = 8 * explicitZ 3 1 0 0 2 0 := by decide
26theorem e_310021 : m2Num 3 1 0 0 2 1 = 8 * explicitZ 3 1 0 0 2 1 := by decide
27theorem e_310022 : m2Num 3 1 0 0 2 2 = 8 * explicitZ 3 1 0 0 2 2 := by decide
28theorem e_310023 : m2Num 3 1 0 0 2 3 = 8 * explicitZ 3 1 0 0 2 3 := by decide
29theorem e_310030 : m2Num 3 1 0 0 3 0 = 8 * explicitZ 3 1 0 0 3 0 := by decide
30theorem e_310031 : m2Num 3 1 0 0 3 1 = 8 * explicitZ 3 1 0 0 3 1 := by decide
31theorem e_310032 : m2Num 3 1 0 0 3 2 = 8 * explicitZ 3 1 0 0 3 2 := by decide
32theorem e_310033 : m2Num 3 1 0 0 3 3 = 8 * explicitZ 3 1 0 0 3 3 := by decide
33theorem e_310100 : m2Num 3 1 0 1 0 0 = 8 * explicitZ 3 1 0 1 0 0 := by decide
34theorem e_310101 : m2Num 3 1 0 1 0 1 = 8 * explicitZ 3 1 0 1 0 1 := by decide
35theorem e_310102 : m2Num 3 1 0 1 0 2 = 8 * explicitZ 3 1 0 1 0 2 := by decide
36theorem e_310103 : m2Num 3 1 0 1 0 3 = 8 * explicitZ 3 1 0 1 0 3 := by decide
37theorem e_310110 : m2Num 3 1 0 1 1 0 = 8 * explicitZ 3 1 0 1 1 0 := by decide
38theorem e_310111 : m2Num 3 1 0 1 1 1 = 8 * explicitZ 3 1 0 1 1 1 := by decide
39theorem e_310112 : m2Num 3 1 0 1 1 2 = 8 * explicitZ 3 1 0 1 1 2 := by decide
40theorem e_310113 : m2Num 3 1 0 1 1 3 = 8 * explicitZ 3 1 0 1 1 3 := by decide
41theorem e_310120 : m2Num 3 1 0 1 2 0 = 8 * explicitZ 3 1 0 1 2 0 := by decide
42theorem e_310121 : m2Num 3 1 0 1 2 1 = 8 * explicitZ 3 1 0 1 2 1 := by decide
43theorem e_310122 : m2Num 3 1 0 1 2 2 = 8 * explicitZ 3 1 0 1 2 2 := by decide
44theorem e_310123 : m2Num 3 1 0 1 2 3 = 8 * explicitZ 3 1 0 1 2 3 := by decide
45theorem e_310130 : m2Num 3 1 0 1 3 0 = 8 * explicitZ 3 1 0 1 3 0 := by decide
46theorem e_310131 : m2Num 3 1 0 1 3 1 = 8 * explicitZ 3 1 0 1 3 1 := by decide
47theorem e_310132 : m2Num 3 1 0 1 3 2 = 8 * explicitZ 3 1 0 1 3 2 := by decide
48theorem e_310133 : m2Num 3 1 0 1 3 3 = 8 * explicitZ 3 1 0 1 3 3 := by decide
49theorem e_310200 : m2Num 3 1 0 2 0 0 = 8 * explicitZ 3 1 0 2 0 0 := by decide
50theorem e_310201 : m2Num 3 1 0 2 0 1 = 8 * explicitZ 3 1 0 2 0 1 := by decide
51theorem e_310202 : m2Num 3 1 0 2 0 2 = 8 * explicitZ 3 1 0 2 0 2 := by decide
52theorem e_310203 : m2Num 3 1 0 2 0 3 = 8 * explicitZ 3 1 0 2 0 3 := by decide
53theorem e_310210 : m2Num 3 1 0 2 1 0 = 8 * explicitZ 3 1 0 2 1 0 := by decide
54theorem e_310211 : m2Num 3 1 0 2 1 1 = 8 * explicitZ 3 1 0 2 1 1 := by decide
55theorem e_310212 : m2Num 3 1 0 2 1 2 = 8 * explicitZ 3 1 0 2 1 2 := by decide
56theorem e_310213 : m2Num 3 1 0 2 1 3 = 8 * explicitZ 3 1 0 2 1 3 := by decide
57theorem e_310220 : m2Num 3 1 0 2 2 0 = 8 * explicitZ 3 1 0 2 2 0 := by decide
58theorem e_310221 : m2Num 3 1 0 2 2 1 = 8 * explicitZ 3 1 0 2 2 1 := by decide
59theorem e_310222 : m2Num 3 1 0 2 2 2 = 8 * explicitZ 3 1 0 2 2 2 := by decide
60theorem e_310223 : m2Num 3 1 0 2 2 3 = 8 * explicitZ 3 1 0 2 2 3 := by decide
61theorem e_310230 : m2Num 3 1 0 2 3 0 = 8 * explicitZ 3 1 0 2 3 0 := by decide
62theorem e_310231 : m2Num 3 1 0 2 3 1 = 8 * explicitZ 3 1 0 2 3 1 := by decide
63theorem e_310232 : m2Num 3 1 0 2 3 2 = 8 * explicitZ 3 1 0 2 3 2 := by decide
64theorem e_310233 : m2Num 3 1 0 2 3 3 = 8 * explicitZ 3 1 0 2 3 3 := by decide
65theorem e_310300 : m2Num 3 1 0 3 0 0 = 8 * explicitZ 3 1 0 3 0 0 := by decide
66theorem e_310301 : m2Num 3 1 0 3 0 1 = 8 * explicitZ 3 1 0 3 0 1 := by decide
67theorem e_310302 : m2Num 3 1 0 3 0 2 = 8 * explicitZ 3 1 0 3 0 2 := by decide
68theorem e_310303 : m2Num 3 1 0 3 0 3 = 8 * explicitZ 3 1 0 3 0 3 := by decide
69theorem e_310310 : m2Num 3 1 0 3 1 0 = 8 * explicitZ 3 1 0 3 1 0 := by decide
70theorem e_310311 : m2Num 3 1 0 3 1 1 = 8 * explicitZ 3 1 0 3 1 1 := by decide
71theorem e_310312 : m2Num 3 1 0 3 1 2 = 8 * explicitZ 3 1 0 3 1 2 := by decide
72theorem e_310313 : m2Num 3 1 0 3 1 3 = 8 * explicitZ 3 1 0 3 1 3 := by decide
73theorem e_310320 : m2Num 3 1 0 3 2 0 = 8 * explicitZ 3 1 0 3 2 0 := by decide
74theorem e_310321 : m2Num 3 1 0 3 2 1 = 8 * explicitZ 3 1 0 3 2 1 := by decide
75theorem e_310322 : m2Num 3 1 0 3 2 2 = 8 * explicitZ 3 1 0 3 2 2 := by decide
76theorem e_310323 : m2Num 3 1 0 3 2 3 = 8 * explicitZ 3 1 0 3 2 3 := by decide
77theorem e_310330 : m2Num 3 1 0 3 3 0 = 8 * explicitZ 3 1 0 3 3 0 := by decide
78theorem e_310331 : m2Num 3 1 0 3 3 1 = 8 * explicitZ 3 1 0 3 3 1 := by decide
79theorem e_310332 : m2Num 3 1 0 3 3 2 = 8 * explicitZ 3 1 0 3 3 2 := by decide
80theorem e_310333 : m2Num 3 1 0 3 3 3 = 8 * explicitZ 3 1 0 3 3 3 := by decide
81theorem e_311000 : m2Num 3 1 1 0 0 0 = 8 * explicitZ 3 1 1 0 0 0 := by decide
82theorem e_311001 : m2Num 3 1 1 0 0 1 = 8 * explicitZ 3 1 1 0 0 1 := by decide
83theorem e_311002 : m2Num 3 1 1 0 0 2 = 8 * explicitZ 3 1 1 0 0 2 := by decide
84theorem e_311003 : m2Num 3 1 1 0 0 3 = 8 * explicitZ 3 1 1 0 0 3 := by decide
85theorem e_311010 : m2Num 3 1 1 0 1 0 = 8 * explicitZ 3 1 1 0 1 0 := by decide
86theorem e_311011 : m2Num 3 1 1 0 1 1 = 8 * explicitZ 3 1 1 0 1 1 := by decide
87theorem e_311012 : m2Num 3 1 1 0 1 2 = 8 * explicitZ 3 1 1 0 1 2 := by decide
88theorem e_311013 : m2Num 3 1 1 0 1 3 = 8 * explicitZ 3 1 1 0 1 3 := by decide
89theorem e_311020 : m2Num 3 1 1 0 2 0 = 8 * explicitZ 3 1 1 0 2 0 := by decide
90theorem e_311021 : m2Num 3 1 1 0 2 1 = 8 * explicitZ 3 1 1 0 2 1 := by decide
91theorem e_311022 : m2Num 3 1 1 0 2 2 = 8 * explicitZ 3 1 1 0 2 2 := by decide
92theorem e_311023 : m2Num 3 1 1 0 2 3 = 8 * explicitZ 3 1 1 0 2 3 := by decide
93theorem e_311030 : m2Num 3 1 1 0 3 0 = 8 * explicitZ 3 1 1 0 3 0 := by decide
94theorem e_311031 : m2Num 3 1 1 0 3 1 = 8 * explicitZ 3 1 1 0 3 1 := by decide
95theorem e_311032 : m2Num 3 1 1 0 3 2 = 8 * explicitZ 3 1 1 0 3 2 := by decide
96theorem e_311033 : m2Num 3 1 1 0 3 3 = 8 * explicitZ 3 1 1 0 3 3 := by decide
97theorem e_311100 : m2Num 3 1 1 1 0 0 = 8 * explicitZ 3 1 1 1 0 0 := by decide
98theorem e_311101 : m2Num 3 1 1 1 0 1 = 8 * explicitZ 3 1 1 1 0 1 := by decide
99theorem e_311102 : m2Num 3 1 1 1 0 2 = 8 * explicitZ 3 1 1 1 0 2 := by decide
100theorem e_311103 : m2Num 3 1 1 1 0 3 = 8 * explicitZ 3 1 1 1 0 3 := by decide
101theorem e_311110 : m2Num 3 1 1 1 1 0 = 8 * explicitZ 3 1 1 1 1 0 := by decide
102theorem e_311111 : m2Num 3 1 1 1 1 1 = 8 * explicitZ 3 1 1 1 1 1 := by decide
103theorem e_311112 : m2Num 3 1 1 1 1 2 = 8 * explicitZ 3 1 1 1 1 2 := by decide
104theorem e_311113 : m2Num 3 1 1 1 1 3 = 8 * explicitZ 3 1 1 1 1 3 := by decide
105theorem e_311120 : m2Num 3 1 1 1 2 0 = 8 * explicitZ 3 1 1 1 2 0 := by decide
106theorem e_311121 : m2Num 3 1 1 1 2 1 = 8 * explicitZ 3 1 1 1 2 1 := by decide
107theorem e_311122 : m2Num 3 1 1 1 2 2 = 8 * explicitZ 3 1 1 1 2 2 := by decide
108theorem e_311123 : m2Num 3 1 1 1 2 3 = 8 * explicitZ 3 1 1 1 2 3 := by decide
109theorem e_311130 : m2Num 3 1 1 1 3 0 = 8 * explicitZ 3 1 1 1 3 0 := by decide
110theorem e_311131 : m2Num 3 1 1 1 3 1 = 8 * explicitZ 3 1 1 1 3 1 := by decide
111theorem e_311132 : m2Num 3 1 1 1 3 2 = 8 * explicitZ 3 1 1 1 3 2 := by decide
112theorem e_311133 : m2Num 3 1 1 1 3 3 = 8 * explicitZ 3 1 1 1 3 3 := by decide
113theorem e_311200 : m2Num 3 1 1 2 0 0 = 8 * explicitZ 3 1 1 2 0 0 := by decide
114theorem e_311201 : m2Num 3 1 1 2 0 1 = 8 * explicitZ 3 1 1 2 0 1 := by decide
115theorem e_311202 : m2Num 3 1 1 2 0 2 = 8 * explicitZ 3 1 1 2 0 2 := by decide
116theorem e_311203 : m2Num 3 1 1 2 0 3 = 8 * explicitZ 3 1 1 2 0 3 := by decide
117theorem e_311210 : m2Num 3 1 1 2 1 0 = 8 * explicitZ 3 1 1 2 1 0 := by decide
118theorem e_311211 : m2Num 3 1 1 2 1 1 = 8 * explicitZ 3 1 1 2 1 1 := by decide
119theorem e_311212 : m2Num 3 1 1 2 1 2 = 8 * explicitZ 3 1 1 2 1 2 := by decide
120theorem e_311213 : m2Num 3 1 1 2 1 3 = 8 * explicitZ 3 1 1 2 1 3 := by decide
121theorem e_311220 : m2Num 3 1 1 2 2 0 = 8 * explicitZ 3 1 1 2 2 0 := by decide
122theorem e_311221 : m2Num 3 1 1 2 2 1 = 8 * explicitZ 3 1 1 2 2 1 := by decide
123theorem e_311222 : m2Num 3 1 1 2 2 2 = 8 * explicitZ 3 1 1 2 2 2 := by decide
124theorem e_311223 : m2Num 3 1 1 2 2 3 = 8 * explicitZ 3 1 1 2 2 3 := by decide
125theorem e_311230 : m2Num 3 1 1 2 3 0 = 8 * explicitZ 3 1 1 2 3 0 := by decide
126theorem e_311231 : m2Num 3 1 1 2 3 1 = 8 * explicitZ 3 1 1 2 3 1 := by decide
127theorem e_311232 : m2Num 3 1 1 2 3 2 = 8 * explicitZ 3 1 1 2 3 2 := by decide
128theorem e_311233 : m2Num 3 1 1 2 3 3 = 8 * explicitZ 3 1 1 2 3 3 := by decide
129theorem e_311300 : m2Num 3 1 1 3 0 0 = 8 * explicitZ 3 1 1 3 0 0 := by decide
130theorem e_311301 : m2Num 3 1 1 3 0 1 = 8 * explicitZ 3 1 1 3 0 1 := by decide
131theorem e_311302 : m2Num 3 1 1 3 0 2 = 8 * explicitZ 3 1 1 3 0 2 := by decide
132theorem e_311303 : m2Num 3 1 1 3 0 3 = 8 * explicitZ 3 1 1 3 0 3 := by decide
133theorem e_311310 : m2Num 3 1 1 3 1 0 = 8 * explicitZ 3 1 1 3 1 0 := by decide
134theorem e_311311 : m2Num 3 1 1 3 1 1 = 8 * explicitZ 3 1 1 3 1 1 := by decide
135theorem e_311312 : m2Num 3 1 1 3 1 2 = 8 * explicitZ 3 1 1 3 1 2 := by decide
136theorem e_311313 : m2Num 3 1 1 3 1 3 = 8 * explicitZ 3 1 1 3 1 3 := by decide
137theorem e_311320 : m2Num 3 1 1 3 2 0 = 8 * explicitZ 3 1 1 3 2 0 := by decide
138theorem e_311321 : m2Num 3 1 1 3 2 1 = 8 * explicitZ 3 1 1 3 2 1 := by decide
139theorem e_311322 : m2Num 3 1 1 3 2 2 = 8 * explicitZ 3 1 1 3 2 2 := by decide
140theorem e_311323 : m2Num 3 1 1 3 2 3 = 8 * explicitZ 3 1 1 3 2 3 := by decide
141theorem e_311330 : m2Num 3 1 1 3 3 0 = 8 * explicitZ 3 1 1 3 3 0 := by decide
142theorem e_311331 : m2Num 3 1 1 3 3 1 = 8 * explicitZ 3 1 1 3 3 1 := by decide
143theorem e_311332 : m2Num 3 1 1 3 3 2 = 8 * explicitZ 3 1 1 3 3 2 := by decide
144theorem e_311333 : m2Num 3 1 1 3 3 3 = 8 * explicitZ 3 1 1 3 3 3 := by decide
145theorem e_312000 : m2Num 3 1 2 0 0 0 = 8 * explicitZ 3 1 2 0 0 0 := by decide
146theorem e_312001 : m2Num 3 1 2 0 0 1 = 8 * explicitZ 3 1 2 0 0 1 := by decide
147theorem e_312002 : m2Num 3 1 2 0 0 2 = 8 * explicitZ 3 1 2 0 0 2 := by decide
148theorem e_312003 : m2Num 3 1 2 0 0 3 = 8 * explicitZ 3 1 2 0 0 3 := by decide
149theorem e_312010 : m2Num 3 1 2 0 1 0 = 8 * explicitZ 3 1 2 0 1 0 := by decide
150theorem e_312011 : m2Num 3 1 2 0 1 1 = 8 * explicitZ 3 1 2 0 1 1 := by decide
151theorem e_312012 : m2Num 3 1 2 0 1 2 = 8 * explicitZ 3 1 2 0 1 2 := by decide
152theorem e_312013 : m2Num 3 1 2 0 1 3 = 8 * explicitZ 3 1 2 0 1 3 := by decide
153theorem e_312020 : m2Num 3 1 2 0 2 0 = 8 * explicitZ 3 1 2 0 2 0 := by decide
154theorem e_312021 : m2Num 3 1 2 0 2 1 = 8 * explicitZ 3 1 2 0 2 1 := by decide
155theorem e_312022 : m2Num 3 1 2 0 2 2 = 8 * explicitZ 3 1 2 0 2 2 := by decide
156theorem e_312023 : m2Num 3 1 2 0 2 3 = 8 * explicitZ 3 1 2 0 2 3 := by decide
157theorem e_312030 : m2Num 3 1 2 0 3 0 = 8 * explicitZ 3 1 2 0 3 0 := by decide
158theorem e_312031 : m2Num 3 1 2 0 3 1 = 8 * explicitZ 3 1 2 0 3 1 := by decide
159theorem e_312032 : m2Num 3 1 2 0 3 2 = 8 * explicitZ 3 1 2 0 3 2 := by decide
160theorem e_312033 : m2Num 3 1 2 0 3 3 = 8 * explicitZ 3 1 2 0 3 3 := by decide
161theorem e_312100 : m2Num 3 1 2 1 0 0 = 8 * explicitZ 3 1 2 1 0 0 := by decide
162theorem e_312101 : m2Num 3 1 2 1 0 1 = 8 * explicitZ 3 1 2 1 0 1 := by decide
163theorem e_312102 : m2Num 3 1 2 1 0 2 = 8 * explicitZ 3 1 2 1 0 2 := by decide
164theorem e_312103 : m2Num 3 1 2 1 0 3 = 8 * explicitZ 3 1 2 1 0 3 := by decide
165theorem e_312110 : m2Num 3 1 2 1 1 0 = 8 * explicitZ 3 1 2 1 1 0 := by decide
166theorem e_312111 : m2Num 3 1 2 1 1 1 = 8 * explicitZ 3 1 2 1 1 1 := by decide
167theorem e_312112 : m2Num 3 1 2 1 1 2 = 8 * explicitZ 3 1 2 1 1 2 := by decide
168theorem e_312113 : m2Num 3 1 2 1 1 3 = 8 * explicitZ 3 1 2 1 1 3 := by decide
169theorem e_312120 : m2Num 3 1 2 1 2 0 = 8 * explicitZ 3 1 2 1 2 0 := by decide
170theorem e_312121 : m2Num 3 1 2 1 2 1 = 8 * explicitZ 3 1 2 1 2 1 := by decide
171theorem e_312122 : m2Num 3 1 2 1 2 2 = 8 * explicitZ 3 1 2 1 2 2 := by decide
172theorem e_312123 : m2Num 3 1 2 1 2 3 = 8 * explicitZ 3 1 2 1 2 3 := by decide
173theorem e_312130 : m2Num 3 1 2 1 3 0 = 8 * explicitZ 3 1 2 1 3 0 := by decide
174theorem e_312131 : m2Num 3 1 2 1 3 1 = 8 * explicitZ 3 1 2 1 3 1 := by decide
175theorem e_312132 : m2Num 3 1 2 1 3 2 = 8 * explicitZ 3 1 2 1 3 2 := by decide
176theorem e_312133 : m2Num 3 1 2 1 3 3 = 8 * explicitZ 3 1 2 1 3 3 := by decide
177theorem e_312200 : m2Num 3 1 2 2 0 0 = 8 * explicitZ 3 1 2 2 0 0 := by decide
178theorem e_312201 : m2Num 3 1 2 2 0 1 = 8 * explicitZ 3 1 2 2 0 1 := by decide
179theorem e_312202 : m2Num 3 1 2 2 0 2 = 8 * explicitZ 3 1 2 2 0 2 := by decide
180theorem e_312203 : m2Num 3 1 2 2 0 3 = 8 * explicitZ 3 1 2 2 0 3 := by decide
181theorem e_312210 : m2Num 3 1 2 2 1 0 = 8 * explicitZ 3 1 2 2 1 0 := by decide
182theorem e_312211 : m2Num 3 1 2 2 1 1 = 8 * explicitZ 3 1 2 2 1 1 := by decide
183theorem e_312212 : m2Num 3 1 2 2 1 2 = 8 * explicitZ 3 1 2 2 1 2 := by decide
184theorem e_312213 : m2Num 3 1 2 2 1 3 = 8 * explicitZ 3 1 2 2 1 3 := by decide
185theorem e_312220 : m2Num 3 1 2 2 2 0 = 8 * explicitZ 3 1 2 2 2 0 := by decide
186theorem e_312221 : m2Num 3 1 2 2 2 1 = 8 * explicitZ 3 1 2 2 2 1 := by decide
187theorem e_312222 : m2Num 3 1 2 2 2 2 = 8 * explicitZ 3 1 2 2 2 2 := by decide
188theorem e_312223 : m2Num 3 1 2 2 2 3 = 8 * explicitZ 3 1 2 2 2 3 := by decide
189theorem e_312230 : m2Num 3 1 2 2 3 0 = 8 * explicitZ 3 1 2 2 3 0 := by decide
190theorem e_312231 : m2Num 3 1 2 2 3 1 = 8 * explicitZ 3 1 2 2 3 1 := by decide
191theorem e_312232 : m2Num 3 1 2 2 3 2 = 8 * explicitZ 3 1 2 2 3 2 := by decide
192theorem e_312233 : m2Num 3 1 2 2 3 3 = 8 * explicitZ 3 1 2 2 3 3 := by decide
193theorem e_312300 : m2Num 3 1 2 3 0 0 = 8 * explicitZ 3 1 2 3 0 0 := by decide
194theorem e_312301 : m2Num 3 1 2 3 0 1 = 8 * explicitZ 3 1 2 3 0 1 := by decide
195theorem e_312302 : m2Num 3 1 2 3 0 2 = 8 * explicitZ 3 1 2 3 0 2 := by decide
196theorem e_312303 : m2Num 3 1 2 3 0 3 = 8 * explicitZ 3 1 2 3 0 3 := by decide
197theorem e_312310 : m2Num 3 1 2 3 1 0 = 8 * explicitZ 3 1 2 3 1 0 := by decide
198theorem e_312311 : m2Num 3 1 2 3 1 1 = 8 * explicitZ 3 1 2 3 1 1 := by decide
199theorem e_312312 : m2Num 3 1 2 3 1 2 = 8 * explicitZ 3 1 2 3 1 2 := by decide
200theorem e_312313 : m2Num 3 1 2 3 1 3 = 8 * explicitZ 3 1 2 3 1 3 := by decide
201theorem e_312320 : m2Num 3 1 2 3 2 0 = 8 * explicitZ 3 1 2 3 2 0 := by decide
202theorem e_312321 : m2Num 3 1 2 3 2 1 = 8 * explicitZ 3 1 2 3 2 1 := by decide
203theorem e_312322 : m2Num 3 1 2 3 2 2 = 8 * explicitZ 3 1 2 3 2 2 := by decide
204theorem e_312323 : m2Num 3 1 2 3 2 3 = 8 * explicitZ 3 1 2 3 2 3 := by decide
205theorem e_312330 : m2Num 3 1 2 3 3 0 = 8 * explicitZ 3 1 2 3 3 0 := by decide
206theorem e_312331 : m2Num 3 1 2 3 3 1 = 8 * explicitZ 3 1 2 3 3 1 := by decide
207theorem e_312332 : m2Num 3 1 2 3 3 2 = 8 * explicitZ 3 1 2 3 3 2 := by decide
208theorem e_312333 : m2Num 3 1 2 3 3 3 = 8 * explicitZ 3 1 2 3 3 3 := by decide
209theorem e_313000 : m2Num 3 1 3 0 0 0 = 8 * explicitZ 3 1 3 0 0 0 := by decide
210theorem e_313001 : m2Num 3 1 3 0 0 1 = 8 * explicitZ 3 1 3 0 0 1 := by decide
211theorem e_313002 : m2Num 3 1 3 0 0 2 = 8 * explicitZ 3 1 3 0 0 2 := by decide
212theorem e_313003 : m2Num 3 1 3 0 0 3 = 8 * explicitZ 3 1 3 0 0 3 := by decide
213theorem e_313010 : m2Num 3 1 3 0 1 0 = 8 * explicitZ 3 1 3 0 1 0 := by decide
214theorem e_313011 : m2Num 3 1 3 0 1 1 = 8 * explicitZ 3 1 3 0 1 1 := by decide
215theorem e_313012 : m2Num 3 1 3 0 1 2 = 8 * explicitZ 3 1 3 0 1 2 := by decide
216theorem e_313013 : m2Num 3 1 3 0 1 3 = 8 * explicitZ 3 1 3 0 1 3 := by decide
217theorem e_313020 : m2Num 3 1 3 0 2 0 = 8 * explicitZ 3 1 3 0 2 0 := by decide
218theorem e_313021 : m2Num 3 1 3 0 2 1 = 8 * explicitZ 3 1 3 0 2 1 := by decide
219theorem e_313022 : m2Num 3 1 3 0 2 2 = 8 * explicitZ 3 1 3 0 2 2 := by decide
220theorem e_313023 : m2Num 3 1 3 0 2 3 = 8 * explicitZ 3 1 3 0 2 3 := by decide
221theorem e_313030 : m2Num 3 1 3 0 3 0 = 8 * explicitZ 3 1 3 0 3 0 := by decide
222theorem e_313031 : m2Num 3 1 3 0 3 1 = 8 * explicitZ 3 1 3 0 3 1 := by decide
223theorem e_313032 : m2Num 3 1 3 0 3 2 = 8 * explicitZ 3 1 3 0 3 2 := by decide
224theorem e_313033 : m2Num 3 1 3 0 3 3 = 8 * explicitZ 3 1 3 0 3 3 := by decide
225theorem e_313100 : m2Num 3 1 3 1 0 0 = 8 * explicitZ 3 1 3 1 0 0 := by decide
226theorem e_313101 : m2Num 3 1 3 1 0 1 = 8 * explicitZ 3 1 3 1 0 1 := by decide
227theorem e_313102 : m2Num 3 1 3 1 0 2 = 8 * explicitZ 3 1 3 1 0 2 := by decide
228theorem e_313103 : m2Num 3 1 3 1 0 3 = 8 * explicitZ 3 1 3 1 0 3 := by decide
229theorem e_313110 : m2Num 3 1 3 1 1 0 = 8 * explicitZ 3 1 3 1 1 0 := by decide
230theorem e_313111 : m2Num 3 1 3 1 1 1 = 8 * explicitZ 3 1 3 1 1 1 := by decide
231theorem e_313112 : m2Num 3 1 3 1 1 2 = 8 * explicitZ 3 1 3 1 1 2 := by decide
232theorem e_313113 : m2Num 3 1 3 1 1 3 = 8 * explicitZ 3 1 3 1 1 3 := by decide
233theorem e_313120 : m2Num 3 1 3 1 2 0 = 8 * explicitZ 3 1 3 1 2 0 := by decide
234theorem e_313121 : m2Num 3 1 3 1 2 1 = 8 * explicitZ 3 1 3 1 2 1 := by decide
235theorem e_313122 : m2Num 3 1 3 1 2 2 = 8 * explicitZ 3 1 3 1 2 2 := by decide
236theorem e_313123 : m2Num 3 1 3 1 2 3 = 8 * explicitZ 3 1 3 1 2 3 := by decide
237theorem e_313130 : m2Num 3 1 3 1 3 0 = 8 * explicitZ 3 1 3 1 3 0 := by decide
238theorem e_313131 : m2Num 3 1 3 1 3 1 = 8 * explicitZ 3 1 3 1 3 1 := by decide
239theorem e_313132 : m2Num 3 1 3 1 3 2 = 8 * explicitZ 3 1 3 1 3 2 := by decide
240theorem e_313133 : m2Num 3 1 3 1 3 3 = 8 * explicitZ 3 1 3 1 3 3 := by decide
241theorem e_313200 : m2Num 3 1 3 2 0 0 = 8 * explicitZ 3 1 3 2 0 0 := by decide
242theorem e_313201 : m2Num 3 1 3 2 0 1 = 8 * explicitZ 3 1 3 2 0 1 := by decide
243theorem e_313202 : m2Num 3 1 3 2 0 2 = 8 * explicitZ 3 1 3 2 0 2 := by decide
244theorem e_313203 : m2Num 3 1 3 2 0 3 = 8 * explicitZ 3 1 3 2 0 3 := by decide
245theorem e_313210 : m2Num 3 1 3 2 1 0 = 8 * explicitZ 3 1 3 2 1 0 := by decide
246theorem e_313211 : m2Num 3 1 3 2 1 1 = 8 * explicitZ 3 1 3 2 1 1 := by decide
247theorem e_313212 : m2Num 3 1 3 2 1 2 = 8 * explicitZ 3 1 3 2 1 2 := by decide
248theorem e_313213 : m2Num 3 1 3 2 1 3 = 8 * explicitZ 3 1 3 2 1 3 := by decide
249theorem e_313220 : m2Num 3 1 3 2 2 0 = 8 * explicitZ 3 1 3 2 2 0 := by decide
250theorem e_313221 : m2Num 3 1 3 2 2 1 = 8 * explicitZ 3 1 3 2 2 1 := by decide
251theorem e_313222 : m2Num 3 1 3 2 2 2 = 8 * explicitZ 3 1 3 2 2 2 := by decide
252theorem e_313223 : m2Num 3 1 3 2 2 3 = 8 * explicitZ 3 1 3 2 2 3 := by decide
253theorem e_313230 : m2Num 3 1 3 2 3 0 = 8 * explicitZ 3 1 3 2 3 0 := by decide
254theorem e_313231 : m2Num 3 1 3 2 3 1 = 8 * explicitZ 3 1 3 2 3 1 := by decide
255theorem e_313232 : m2Num 3 1 3 2 3 2 = 8 * explicitZ 3 1 3 2 3 2 := by decide
256theorem e_313233 : m2Num 3 1 3 2 3 3 = 8 * explicitZ 3 1 3 2 3 3 := by decide
257theorem e_313300 : m2Num 3 1 3 3 0 0 = 8 * explicitZ 3 1 3 3 0 0 := by decide
258theorem e_313301 : m2Num 3 1 3 3 0 1 = 8 * explicitZ 3 1 3 3 0 1 := by decide
259theorem e_313302 : m2Num 3 1 3 3 0 2 = 8 * explicitZ 3 1 3 3 0 2 := by decide
260theorem e_313303 : m2Num 3 1 3 3 0 3 = 8 * explicitZ 3 1 3 3 0 3 := by decide
261theorem e_313310 : m2Num 3 1 3 3 1 0 = 8 * explicitZ 3 1 3 3 1 0 := by decide
262theorem e_313311 : m2Num 3 1 3 3 1 1 = 8 * explicitZ 3 1 3 3 1 1 := by decide
263theorem e_313312 : m2Num 3 1 3 3 1 2 = 8 * explicitZ 3 1 3 3 1 2 := by decide
264theorem e_313313 : m2Num 3 1 3 3 1 3 = 8 * explicitZ 3 1 3 3 1 3 := by decide
265theorem e_313320 : m2Num 3 1 3 3 2 0 = 8 * explicitZ 3 1 3 3 2 0 := by decide
266theorem e_313321 : m2Num 3 1 3 3 2 1 = 8 * explicitZ 3 1 3 3 2 1 := by decide
267theorem e_313322 : m2Num 3 1 3 3 2 2 = 8 * explicitZ 3 1 3 3 2 2 := by decide
268theorem e_313323 : m2Num 3 1 3 3 2 3 = 8 * explicitZ 3 1 3 3 2 3 := by decide
269theorem e_313330 : m2Num 3 1 3 3 3 0 = 8 * explicitZ 3 1 3 3 3 0 := by decide
270theorem e_313331 : m2Num 3 1 3 3 3 1 = 8 * explicitZ 3 1 3 3 3 1 := by decide
271theorem e_313332 : m2Num 3 1 3 3 3 2 = 8 * explicitZ 3 1 3 3 3 2 := by decide
272theorem e_313333 : m2Num 3 1 3 3 3 3 = 8 * explicitZ 3 1 3 3 3 3 := by decide
273
274end M2NumChunk13
275end ReggeExactMidpointM2TTIdentity4D
276end Analysis
277end Gravity
278end IndisputableMonolith
279