IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DM2NumChunk04
IndisputableMonolith/Gravity/Analysis/ReggeExactMidpointM2TTIdentity4DM2NumChunk04.lean · 279 lines · 256 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DKernelCert
3
4/-! m2Num = 8·explicitZ, chunk 4 (256 kernel decides). -/
5
6namespace IndisputableMonolith
7namespace Gravity
8namespace Analysis
9namespace ReggeExactMidpointM2TTIdentity4D
10namespace M2NumChunk04
11
12open KernelCert
13
14set_option maxRecDepth 100000
15set_option maxHeartbeats 200000000
16
17theorem e_100000 : m2Num 1 0 0 0 0 0 = 8 * explicitZ 1 0 0 0 0 0 := by decide
18theorem e_100001 : m2Num 1 0 0 0 0 1 = 8 * explicitZ 1 0 0 0 0 1 := by decide
19theorem e_100002 : m2Num 1 0 0 0 0 2 = 8 * explicitZ 1 0 0 0 0 2 := by decide
20theorem e_100003 : m2Num 1 0 0 0 0 3 = 8 * explicitZ 1 0 0 0 0 3 := by decide
21theorem e_100010 : m2Num 1 0 0 0 1 0 = 8 * explicitZ 1 0 0 0 1 0 := by decide
22theorem e_100011 : m2Num 1 0 0 0 1 1 = 8 * explicitZ 1 0 0 0 1 1 := by decide
23theorem e_100012 : m2Num 1 0 0 0 1 2 = 8 * explicitZ 1 0 0 0 1 2 := by decide
24theorem e_100013 : m2Num 1 0 0 0 1 3 = 8 * explicitZ 1 0 0 0 1 3 := by decide
25theorem e_100020 : m2Num 1 0 0 0 2 0 = 8 * explicitZ 1 0 0 0 2 0 := by decide
26theorem e_100021 : m2Num 1 0 0 0 2 1 = 8 * explicitZ 1 0 0 0 2 1 := by decide
27theorem e_100022 : m2Num 1 0 0 0 2 2 = 8 * explicitZ 1 0 0 0 2 2 := by decide
28theorem e_100023 : m2Num 1 0 0 0 2 3 = 8 * explicitZ 1 0 0 0 2 3 := by decide
29theorem e_100030 : m2Num 1 0 0 0 3 0 = 8 * explicitZ 1 0 0 0 3 0 := by decide
30theorem e_100031 : m2Num 1 0 0 0 3 1 = 8 * explicitZ 1 0 0 0 3 1 := by decide
31theorem e_100032 : m2Num 1 0 0 0 3 2 = 8 * explicitZ 1 0 0 0 3 2 := by decide
32theorem e_100033 : m2Num 1 0 0 0 3 3 = 8 * explicitZ 1 0 0 0 3 3 := by decide
33theorem e_100100 : m2Num 1 0 0 1 0 0 = 8 * explicitZ 1 0 0 1 0 0 := by decide
34theorem e_100101 : m2Num 1 0 0 1 0 1 = 8 * explicitZ 1 0 0 1 0 1 := by decide
35theorem e_100102 : m2Num 1 0 0 1 0 2 = 8 * explicitZ 1 0 0 1 0 2 := by decide
36theorem e_100103 : m2Num 1 0 0 1 0 3 = 8 * explicitZ 1 0 0 1 0 3 := by decide
37theorem e_100110 : m2Num 1 0 0 1 1 0 = 8 * explicitZ 1 0 0 1 1 0 := by decide
38theorem e_100111 : m2Num 1 0 0 1 1 1 = 8 * explicitZ 1 0 0 1 1 1 := by decide
39theorem e_100112 : m2Num 1 0 0 1 1 2 = 8 * explicitZ 1 0 0 1 1 2 := by decide
40theorem e_100113 : m2Num 1 0 0 1 1 3 = 8 * explicitZ 1 0 0 1 1 3 := by decide
41theorem e_100120 : m2Num 1 0 0 1 2 0 = 8 * explicitZ 1 0 0 1 2 0 := by decide
42theorem e_100121 : m2Num 1 0 0 1 2 1 = 8 * explicitZ 1 0 0 1 2 1 := by decide
43theorem e_100122 : m2Num 1 0 0 1 2 2 = 8 * explicitZ 1 0 0 1 2 2 := by decide
44theorem e_100123 : m2Num 1 0 0 1 2 3 = 8 * explicitZ 1 0 0 1 2 3 := by decide
45theorem e_100130 : m2Num 1 0 0 1 3 0 = 8 * explicitZ 1 0 0 1 3 0 := by decide
46theorem e_100131 : m2Num 1 0 0 1 3 1 = 8 * explicitZ 1 0 0 1 3 1 := by decide
47theorem e_100132 : m2Num 1 0 0 1 3 2 = 8 * explicitZ 1 0 0 1 3 2 := by decide
48theorem e_100133 : m2Num 1 0 0 1 3 3 = 8 * explicitZ 1 0 0 1 3 3 := by decide
49theorem e_100200 : m2Num 1 0 0 2 0 0 = 8 * explicitZ 1 0 0 2 0 0 := by decide
50theorem e_100201 : m2Num 1 0 0 2 0 1 = 8 * explicitZ 1 0 0 2 0 1 := by decide
51theorem e_100202 : m2Num 1 0 0 2 0 2 = 8 * explicitZ 1 0 0 2 0 2 := by decide
52theorem e_100203 : m2Num 1 0 0 2 0 3 = 8 * explicitZ 1 0 0 2 0 3 := by decide
53theorem e_100210 : m2Num 1 0 0 2 1 0 = 8 * explicitZ 1 0 0 2 1 0 := by decide
54theorem e_100211 : m2Num 1 0 0 2 1 1 = 8 * explicitZ 1 0 0 2 1 1 := by decide
55theorem e_100212 : m2Num 1 0 0 2 1 2 = 8 * explicitZ 1 0 0 2 1 2 := by decide
56theorem e_100213 : m2Num 1 0 0 2 1 3 = 8 * explicitZ 1 0 0 2 1 3 := by decide
57theorem e_100220 : m2Num 1 0 0 2 2 0 = 8 * explicitZ 1 0 0 2 2 0 := by decide
58theorem e_100221 : m2Num 1 0 0 2 2 1 = 8 * explicitZ 1 0 0 2 2 1 := by decide
59theorem e_100222 : m2Num 1 0 0 2 2 2 = 8 * explicitZ 1 0 0 2 2 2 := by decide
60theorem e_100223 : m2Num 1 0 0 2 2 3 = 8 * explicitZ 1 0 0 2 2 3 := by decide
61theorem e_100230 : m2Num 1 0 0 2 3 0 = 8 * explicitZ 1 0 0 2 3 0 := by decide
62theorem e_100231 : m2Num 1 0 0 2 3 1 = 8 * explicitZ 1 0 0 2 3 1 := by decide
63theorem e_100232 : m2Num 1 0 0 2 3 2 = 8 * explicitZ 1 0 0 2 3 2 := by decide
64theorem e_100233 : m2Num 1 0 0 2 3 3 = 8 * explicitZ 1 0 0 2 3 3 := by decide
65theorem e_100300 : m2Num 1 0 0 3 0 0 = 8 * explicitZ 1 0 0 3 0 0 := by decide
66theorem e_100301 : m2Num 1 0 0 3 0 1 = 8 * explicitZ 1 0 0 3 0 1 := by decide
67theorem e_100302 : m2Num 1 0 0 3 0 2 = 8 * explicitZ 1 0 0 3 0 2 := by decide
68theorem e_100303 : m2Num 1 0 0 3 0 3 = 8 * explicitZ 1 0 0 3 0 3 := by decide
69theorem e_100310 : m2Num 1 0 0 3 1 0 = 8 * explicitZ 1 0 0 3 1 0 := by decide
70theorem e_100311 : m2Num 1 0 0 3 1 1 = 8 * explicitZ 1 0 0 3 1 1 := by decide
71theorem e_100312 : m2Num 1 0 0 3 1 2 = 8 * explicitZ 1 0 0 3 1 2 := by decide
72theorem e_100313 : m2Num 1 0 0 3 1 3 = 8 * explicitZ 1 0 0 3 1 3 := by decide
73theorem e_100320 : m2Num 1 0 0 3 2 0 = 8 * explicitZ 1 0 0 3 2 0 := by decide
74theorem e_100321 : m2Num 1 0 0 3 2 1 = 8 * explicitZ 1 0 0 3 2 1 := by decide
75theorem e_100322 : m2Num 1 0 0 3 2 2 = 8 * explicitZ 1 0 0 3 2 2 := by decide
76theorem e_100323 : m2Num 1 0 0 3 2 3 = 8 * explicitZ 1 0 0 3 2 3 := by decide
77theorem e_100330 : m2Num 1 0 0 3 3 0 = 8 * explicitZ 1 0 0 3 3 0 := by decide
78theorem e_100331 : m2Num 1 0 0 3 3 1 = 8 * explicitZ 1 0 0 3 3 1 := by decide
79theorem e_100332 : m2Num 1 0 0 3 3 2 = 8 * explicitZ 1 0 0 3 3 2 := by decide
80theorem e_100333 : m2Num 1 0 0 3 3 3 = 8 * explicitZ 1 0 0 3 3 3 := by decide
81theorem e_101000 : m2Num 1 0 1 0 0 0 = 8 * explicitZ 1 0 1 0 0 0 := by decide
82theorem e_101001 : m2Num 1 0 1 0 0 1 = 8 * explicitZ 1 0 1 0 0 1 := by decide
83theorem e_101002 : m2Num 1 0 1 0 0 2 = 8 * explicitZ 1 0 1 0 0 2 := by decide
84theorem e_101003 : m2Num 1 0 1 0 0 3 = 8 * explicitZ 1 0 1 0 0 3 := by decide
85theorem e_101010 : m2Num 1 0 1 0 1 0 = 8 * explicitZ 1 0 1 0 1 0 := by decide
86theorem e_101011 : m2Num 1 0 1 0 1 1 = 8 * explicitZ 1 0 1 0 1 1 := by decide
87theorem e_101012 : m2Num 1 0 1 0 1 2 = 8 * explicitZ 1 0 1 0 1 2 := by decide
88theorem e_101013 : m2Num 1 0 1 0 1 3 = 8 * explicitZ 1 0 1 0 1 3 := by decide
89theorem e_101020 : m2Num 1 0 1 0 2 0 = 8 * explicitZ 1 0 1 0 2 0 := by decide
90theorem e_101021 : m2Num 1 0 1 0 2 1 = 8 * explicitZ 1 0 1 0 2 1 := by decide
91theorem e_101022 : m2Num 1 0 1 0 2 2 = 8 * explicitZ 1 0 1 0 2 2 := by decide
92theorem e_101023 : m2Num 1 0 1 0 2 3 = 8 * explicitZ 1 0 1 0 2 3 := by decide
93theorem e_101030 : m2Num 1 0 1 0 3 0 = 8 * explicitZ 1 0 1 0 3 0 := by decide
94theorem e_101031 : m2Num 1 0 1 0 3 1 = 8 * explicitZ 1 0 1 0 3 1 := by decide
95theorem e_101032 : m2Num 1 0 1 0 3 2 = 8 * explicitZ 1 0 1 0 3 2 := by decide
96theorem e_101033 : m2Num 1 0 1 0 3 3 = 8 * explicitZ 1 0 1 0 3 3 := by decide
97theorem e_101100 : m2Num 1 0 1 1 0 0 = 8 * explicitZ 1 0 1 1 0 0 := by decide
98theorem e_101101 : m2Num 1 0 1 1 0 1 = 8 * explicitZ 1 0 1 1 0 1 := by decide
99theorem e_101102 : m2Num 1 0 1 1 0 2 = 8 * explicitZ 1 0 1 1 0 2 := by decide
100theorem e_101103 : m2Num 1 0 1 1 0 3 = 8 * explicitZ 1 0 1 1 0 3 := by decide
101theorem e_101110 : m2Num 1 0 1 1 1 0 = 8 * explicitZ 1 0 1 1 1 0 := by decide
102theorem e_101111 : m2Num 1 0 1 1 1 1 = 8 * explicitZ 1 0 1 1 1 1 := by decide
103theorem e_101112 : m2Num 1 0 1 1 1 2 = 8 * explicitZ 1 0 1 1 1 2 := by decide
104theorem e_101113 : m2Num 1 0 1 1 1 3 = 8 * explicitZ 1 0 1 1 1 3 := by decide
105theorem e_101120 : m2Num 1 0 1 1 2 0 = 8 * explicitZ 1 0 1 1 2 0 := by decide
106theorem e_101121 : m2Num 1 0 1 1 2 1 = 8 * explicitZ 1 0 1 1 2 1 := by decide
107theorem e_101122 : m2Num 1 0 1 1 2 2 = 8 * explicitZ 1 0 1 1 2 2 := by decide
108theorem e_101123 : m2Num 1 0 1 1 2 3 = 8 * explicitZ 1 0 1 1 2 3 := by decide
109theorem e_101130 : m2Num 1 0 1 1 3 0 = 8 * explicitZ 1 0 1 1 3 0 := by decide
110theorem e_101131 : m2Num 1 0 1 1 3 1 = 8 * explicitZ 1 0 1 1 3 1 := by decide
111theorem e_101132 : m2Num 1 0 1 1 3 2 = 8 * explicitZ 1 0 1 1 3 2 := by decide
112theorem e_101133 : m2Num 1 0 1 1 3 3 = 8 * explicitZ 1 0 1 1 3 3 := by decide
113theorem e_101200 : m2Num 1 0 1 2 0 0 = 8 * explicitZ 1 0 1 2 0 0 := by decide
114theorem e_101201 : m2Num 1 0 1 2 0 1 = 8 * explicitZ 1 0 1 2 0 1 := by decide
115theorem e_101202 : m2Num 1 0 1 2 0 2 = 8 * explicitZ 1 0 1 2 0 2 := by decide
116theorem e_101203 : m2Num 1 0 1 2 0 3 = 8 * explicitZ 1 0 1 2 0 3 := by decide
117theorem e_101210 : m2Num 1 0 1 2 1 0 = 8 * explicitZ 1 0 1 2 1 0 := by decide
118theorem e_101211 : m2Num 1 0 1 2 1 1 = 8 * explicitZ 1 0 1 2 1 1 := by decide
119theorem e_101212 : m2Num 1 0 1 2 1 2 = 8 * explicitZ 1 0 1 2 1 2 := by decide
120theorem e_101213 : m2Num 1 0 1 2 1 3 = 8 * explicitZ 1 0 1 2 1 3 := by decide
121theorem e_101220 : m2Num 1 0 1 2 2 0 = 8 * explicitZ 1 0 1 2 2 0 := by decide
122theorem e_101221 : m2Num 1 0 1 2 2 1 = 8 * explicitZ 1 0 1 2 2 1 := by decide
123theorem e_101222 : m2Num 1 0 1 2 2 2 = 8 * explicitZ 1 0 1 2 2 2 := by decide
124theorem e_101223 : m2Num 1 0 1 2 2 3 = 8 * explicitZ 1 0 1 2 2 3 := by decide
125theorem e_101230 : m2Num 1 0 1 2 3 0 = 8 * explicitZ 1 0 1 2 3 0 := by decide
126theorem e_101231 : m2Num 1 0 1 2 3 1 = 8 * explicitZ 1 0 1 2 3 1 := by decide
127theorem e_101232 : m2Num 1 0 1 2 3 2 = 8 * explicitZ 1 0 1 2 3 2 := by decide
128theorem e_101233 : m2Num 1 0 1 2 3 3 = 8 * explicitZ 1 0 1 2 3 3 := by decide
129theorem e_101300 : m2Num 1 0 1 3 0 0 = 8 * explicitZ 1 0 1 3 0 0 := by decide
130theorem e_101301 : m2Num 1 0 1 3 0 1 = 8 * explicitZ 1 0 1 3 0 1 := by decide
131theorem e_101302 : m2Num 1 0 1 3 0 2 = 8 * explicitZ 1 0 1 3 0 2 := by decide
132theorem e_101303 : m2Num 1 0 1 3 0 3 = 8 * explicitZ 1 0 1 3 0 3 := by decide
133theorem e_101310 : m2Num 1 0 1 3 1 0 = 8 * explicitZ 1 0 1 3 1 0 := by decide
134theorem e_101311 : m2Num 1 0 1 3 1 1 = 8 * explicitZ 1 0 1 3 1 1 := by decide
135theorem e_101312 : m2Num 1 0 1 3 1 2 = 8 * explicitZ 1 0 1 3 1 2 := by decide
136theorem e_101313 : m2Num 1 0 1 3 1 3 = 8 * explicitZ 1 0 1 3 1 3 := by decide
137theorem e_101320 : m2Num 1 0 1 3 2 0 = 8 * explicitZ 1 0 1 3 2 0 := by decide
138theorem e_101321 : m2Num 1 0 1 3 2 1 = 8 * explicitZ 1 0 1 3 2 1 := by decide
139theorem e_101322 : m2Num 1 0 1 3 2 2 = 8 * explicitZ 1 0 1 3 2 2 := by decide
140theorem e_101323 : m2Num 1 0 1 3 2 3 = 8 * explicitZ 1 0 1 3 2 3 := by decide
141theorem e_101330 : m2Num 1 0 1 3 3 0 = 8 * explicitZ 1 0 1 3 3 0 := by decide
142theorem e_101331 : m2Num 1 0 1 3 3 1 = 8 * explicitZ 1 0 1 3 3 1 := by decide
143theorem e_101332 : m2Num 1 0 1 3 3 2 = 8 * explicitZ 1 0 1 3 3 2 := by decide
144theorem e_101333 : m2Num 1 0 1 3 3 3 = 8 * explicitZ 1 0 1 3 3 3 := by decide
145theorem e_102000 : m2Num 1 0 2 0 0 0 = 8 * explicitZ 1 0 2 0 0 0 := by decide
146theorem e_102001 : m2Num 1 0 2 0 0 1 = 8 * explicitZ 1 0 2 0 0 1 := by decide
147theorem e_102002 : m2Num 1 0 2 0 0 2 = 8 * explicitZ 1 0 2 0 0 2 := by decide
148theorem e_102003 : m2Num 1 0 2 0 0 3 = 8 * explicitZ 1 0 2 0 0 3 := by decide
149theorem e_102010 : m2Num 1 0 2 0 1 0 = 8 * explicitZ 1 0 2 0 1 0 := by decide
150theorem e_102011 : m2Num 1 0 2 0 1 1 = 8 * explicitZ 1 0 2 0 1 1 := by decide
151theorem e_102012 : m2Num 1 0 2 0 1 2 = 8 * explicitZ 1 0 2 0 1 2 := by decide
152theorem e_102013 : m2Num 1 0 2 0 1 3 = 8 * explicitZ 1 0 2 0 1 3 := by decide
153theorem e_102020 : m2Num 1 0 2 0 2 0 = 8 * explicitZ 1 0 2 0 2 0 := by decide
154theorem e_102021 : m2Num 1 0 2 0 2 1 = 8 * explicitZ 1 0 2 0 2 1 := by decide
155theorem e_102022 : m2Num 1 0 2 0 2 2 = 8 * explicitZ 1 0 2 0 2 2 := by decide
156theorem e_102023 : m2Num 1 0 2 0 2 3 = 8 * explicitZ 1 0 2 0 2 3 := by decide
157theorem e_102030 : m2Num 1 0 2 0 3 0 = 8 * explicitZ 1 0 2 0 3 0 := by decide
158theorem e_102031 : m2Num 1 0 2 0 3 1 = 8 * explicitZ 1 0 2 0 3 1 := by decide
159theorem e_102032 : m2Num 1 0 2 0 3 2 = 8 * explicitZ 1 0 2 0 3 2 := by decide
160theorem e_102033 : m2Num 1 0 2 0 3 3 = 8 * explicitZ 1 0 2 0 3 3 := by decide
161theorem e_102100 : m2Num 1 0 2 1 0 0 = 8 * explicitZ 1 0 2 1 0 0 := by decide
162theorem e_102101 : m2Num 1 0 2 1 0 1 = 8 * explicitZ 1 0 2 1 0 1 := by decide
163theorem e_102102 : m2Num 1 0 2 1 0 2 = 8 * explicitZ 1 0 2 1 0 2 := by decide
164theorem e_102103 : m2Num 1 0 2 1 0 3 = 8 * explicitZ 1 0 2 1 0 3 := by decide
165theorem e_102110 : m2Num 1 0 2 1 1 0 = 8 * explicitZ 1 0 2 1 1 0 := by decide
166theorem e_102111 : m2Num 1 0 2 1 1 1 = 8 * explicitZ 1 0 2 1 1 1 := by decide
167theorem e_102112 : m2Num 1 0 2 1 1 2 = 8 * explicitZ 1 0 2 1 1 2 := by decide
168theorem e_102113 : m2Num 1 0 2 1 1 3 = 8 * explicitZ 1 0 2 1 1 3 := by decide
169theorem e_102120 : m2Num 1 0 2 1 2 0 = 8 * explicitZ 1 0 2 1 2 0 := by decide
170theorem e_102121 : m2Num 1 0 2 1 2 1 = 8 * explicitZ 1 0 2 1 2 1 := by decide
171theorem e_102122 : m2Num 1 0 2 1 2 2 = 8 * explicitZ 1 0 2 1 2 2 := by decide
172theorem e_102123 : m2Num 1 0 2 1 2 3 = 8 * explicitZ 1 0 2 1 2 3 := by decide
173theorem e_102130 : m2Num 1 0 2 1 3 0 = 8 * explicitZ 1 0 2 1 3 0 := by decide
174theorem e_102131 : m2Num 1 0 2 1 3 1 = 8 * explicitZ 1 0 2 1 3 1 := by decide
175theorem e_102132 : m2Num 1 0 2 1 3 2 = 8 * explicitZ 1 0 2 1 3 2 := by decide
176theorem e_102133 : m2Num 1 0 2 1 3 3 = 8 * explicitZ 1 0 2 1 3 3 := by decide
177theorem e_102200 : m2Num 1 0 2 2 0 0 = 8 * explicitZ 1 0 2 2 0 0 := by decide
178theorem e_102201 : m2Num 1 0 2 2 0 1 = 8 * explicitZ 1 0 2 2 0 1 := by decide
179theorem e_102202 : m2Num 1 0 2 2 0 2 = 8 * explicitZ 1 0 2 2 0 2 := by decide
180theorem e_102203 : m2Num 1 0 2 2 0 3 = 8 * explicitZ 1 0 2 2 0 3 := by decide
181theorem e_102210 : m2Num 1 0 2 2 1 0 = 8 * explicitZ 1 0 2 2 1 0 := by decide
182theorem e_102211 : m2Num 1 0 2 2 1 1 = 8 * explicitZ 1 0 2 2 1 1 := by decide
183theorem e_102212 : m2Num 1 0 2 2 1 2 = 8 * explicitZ 1 0 2 2 1 2 := by decide
184theorem e_102213 : m2Num 1 0 2 2 1 3 = 8 * explicitZ 1 0 2 2 1 3 := by decide
185theorem e_102220 : m2Num 1 0 2 2 2 0 = 8 * explicitZ 1 0 2 2 2 0 := by decide
186theorem e_102221 : m2Num 1 0 2 2 2 1 = 8 * explicitZ 1 0 2 2 2 1 := by decide
187theorem e_102222 : m2Num 1 0 2 2 2 2 = 8 * explicitZ 1 0 2 2 2 2 := by decide
188theorem e_102223 : m2Num 1 0 2 2 2 3 = 8 * explicitZ 1 0 2 2 2 3 := by decide
189theorem e_102230 : m2Num 1 0 2 2 3 0 = 8 * explicitZ 1 0 2 2 3 0 := by decide
190theorem e_102231 : m2Num 1 0 2 2 3 1 = 8 * explicitZ 1 0 2 2 3 1 := by decide
191theorem e_102232 : m2Num 1 0 2 2 3 2 = 8 * explicitZ 1 0 2 2 3 2 := by decide
192theorem e_102233 : m2Num 1 0 2 2 3 3 = 8 * explicitZ 1 0 2 2 3 3 := by decide
193theorem e_102300 : m2Num 1 0 2 3 0 0 = 8 * explicitZ 1 0 2 3 0 0 := by decide
194theorem e_102301 : m2Num 1 0 2 3 0 1 = 8 * explicitZ 1 0 2 3 0 1 := by decide
195theorem e_102302 : m2Num 1 0 2 3 0 2 = 8 * explicitZ 1 0 2 3 0 2 := by decide
196theorem e_102303 : m2Num 1 0 2 3 0 3 = 8 * explicitZ 1 0 2 3 0 3 := by decide
197theorem e_102310 : m2Num 1 0 2 3 1 0 = 8 * explicitZ 1 0 2 3 1 0 := by decide
198theorem e_102311 : m2Num 1 0 2 3 1 1 = 8 * explicitZ 1 0 2 3 1 1 := by decide
199theorem e_102312 : m2Num 1 0 2 3 1 2 = 8 * explicitZ 1 0 2 3 1 2 := by decide
200theorem e_102313 : m2Num 1 0 2 3 1 3 = 8 * explicitZ 1 0 2 3 1 3 := by decide
201theorem e_102320 : m2Num 1 0 2 3 2 0 = 8 * explicitZ 1 0 2 3 2 0 := by decide
202theorem e_102321 : m2Num 1 0 2 3 2 1 = 8 * explicitZ 1 0 2 3 2 1 := by decide
203theorem e_102322 : m2Num 1 0 2 3 2 2 = 8 * explicitZ 1 0 2 3 2 2 := by decide
204theorem e_102323 : m2Num 1 0 2 3 2 3 = 8 * explicitZ 1 0 2 3 2 3 := by decide
205theorem e_102330 : m2Num 1 0 2 3 3 0 = 8 * explicitZ 1 0 2 3 3 0 := by decide
206theorem e_102331 : m2Num 1 0 2 3 3 1 = 8 * explicitZ 1 0 2 3 3 1 := by decide
207theorem e_102332 : m2Num 1 0 2 3 3 2 = 8 * explicitZ 1 0 2 3 3 2 := by decide
208theorem e_102333 : m2Num 1 0 2 3 3 3 = 8 * explicitZ 1 0 2 3 3 3 := by decide
209theorem e_103000 : m2Num 1 0 3 0 0 0 = 8 * explicitZ 1 0 3 0 0 0 := by decide
210theorem e_103001 : m2Num 1 0 3 0 0 1 = 8 * explicitZ 1 0 3 0 0 1 := by decide
211theorem e_103002 : m2Num 1 0 3 0 0 2 = 8 * explicitZ 1 0 3 0 0 2 := by decide
212theorem e_103003 : m2Num 1 0 3 0 0 3 = 8 * explicitZ 1 0 3 0 0 3 := by decide
213theorem e_103010 : m2Num 1 0 3 0 1 0 = 8 * explicitZ 1 0 3 0 1 0 := by decide
214theorem e_103011 : m2Num 1 0 3 0 1 1 = 8 * explicitZ 1 0 3 0 1 1 := by decide
215theorem e_103012 : m2Num 1 0 3 0 1 2 = 8 * explicitZ 1 0 3 0 1 2 := by decide
216theorem e_103013 : m2Num 1 0 3 0 1 3 = 8 * explicitZ 1 0 3 0 1 3 := by decide
217theorem e_103020 : m2Num 1 0 3 0 2 0 = 8 * explicitZ 1 0 3 0 2 0 := by decide
218theorem e_103021 : m2Num 1 0 3 0 2 1 = 8 * explicitZ 1 0 3 0 2 1 := by decide
219theorem e_103022 : m2Num 1 0 3 0 2 2 = 8 * explicitZ 1 0 3 0 2 2 := by decide
220theorem e_103023 : m2Num 1 0 3 0 2 3 = 8 * explicitZ 1 0 3 0 2 3 := by decide
221theorem e_103030 : m2Num 1 0 3 0 3 0 = 8 * explicitZ 1 0 3 0 3 0 := by decide
222theorem e_103031 : m2Num 1 0 3 0 3 1 = 8 * explicitZ 1 0 3 0 3 1 := by decide
223theorem e_103032 : m2Num 1 0 3 0 3 2 = 8 * explicitZ 1 0 3 0 3 2 := by decide
224theorem e_103033 : m2Num 1 0 3 0 3 3 = 8 * explicitZ 1 0 3 0 3 3 := by decide
225theorem e_103100 : m2Num 1 0 3 1 0 0 = 8 * explicitZ 1 0 3 1 0 0 := by decide
226theorem e_103101 : m2Num 1 0 3 1 0 1 = 8 * explicitZ 1 0 3 1 0 1 := by decide
227theorem e_103102 : m2Num 1 0 3 1 0 2 = 8 * explicitZ 1 0 3 1 0 2 := by decide
228theorem e_103103 : m2Num 1 0 3 1 0 3 = 8 * explicitZ 1 0 3 1 0 3 := by decide
229theorem e_103110 : m2Num 1 0 3 1 1 0 = 8 * explicitZ 1 0 3 1 1 0 := by decide
230theorem e_103111 : m2Num 1 0 3 1 1 1 = 8 * explicitZ 1 0 3 1 1 1 := by decide
231theorem e_103112 : m2Num 1 0 3 1 1 2 = 8 * explicitZ 1 0 3 1 1 2 := by decide
232theorem e_103113 : m2Num 1 0 3 1 1 3 = 8 * explicitZ 1 0 3 1 1 3 := by decide
233theorem e_103120 : m2Num 1 0 3 1 2 0 = 8 * explicitZ 1 0 3 1 2 0 := by decide
234theorem e_103121 : m2Num 1 0 3 1 2 1 = 8 * explicitZ 1 0 3 1 2 1 := by decide
235theorem e_103122 : m2Num 1 0 3 1 2 2 = 8 * explicitZ 1 0 3 1 2 2 := by decide
236theorem e_103123 : m2Num 1 0 3 1 2 3 = 8 * explicitZ 1 0 3 1 2 3 := by decide
237theorem e_103130 : m2Num 1 0 3 1 3 0 = 8 * explicitZ 1 0 3 1 3 0 := by decide
238theorem e_103131 : m2Num 1 0 3 1 3 1 = 8 * explicitZ 1 0 3 1 3 1 := by decide
239theorem e_103132 : m2Num 1 0 3 1 3 2 = 8 * explicitZ 1 0 3 1 3 2 := by decide
240theorem e_103133 : m2Num 1 0 3 1 3 3 = 8 * explicitZ 1 0 3 1 3 3 := by decide
241theorem e_103200 : m2Num 1 0 3 2 0 0 = 8 * explicitZ 1 0 3 2 0 0 := by decide
242theorem e_103201 : m2Num 1 0 3 2 0 1 = 8 * explicitZ 1 0 3 2 0 1 := by decide
243theorem e_103202 : m2Num 1 0 3 2 0 2 = 8 * explicitZ 1 0 3 2 0 2 := by decide
244theorem e_103203 : m2Num 1 0 3 2 0 3 = 8 * explicitZ 1 0 3 2 0 3 := by decide
245theorem e_103210 : m2Num 1 0 3 2 1 0 = 8 * explicitZ 1 0 3 2 1 0 := by decide
246theorem e_103211 : m2Num 1 0 3 2 1 1 = 8 * explicitZ 1 0 3 2 1 1 := by decide
247theorem e_103212 : m2Num 1 0 3 2 1 2 = 8 * explicitZ 1 0 3 2 1 2 := by decide
248theorem e_103213 : m2Num 1 0 3 2 1 3 = 8 * explicitZ 1 0 3 2 1 3 := by decide
249theorem e_103220 : m2Num 1 0 3 2 2 0 = 8 * explicitZ 1 0 3 2 2 0 := by decide
250theorem e_103221 : m2Num 1 0 3 2 2 1 = 8 * explicitZ 1 0 3 2 2 1 := by decide
251theorem e_103222 : m2Num 1 0 3 2 2 2 = 8 * explicitZ 1 0 3 2 2 2 := by decide
252theorem e_103223 : m2Num 1 0 3 2 2 3 = 8 * explicitZ 1 0 3 2 2 3 := by decide
253theorem e_103230 : m2Num 1 0 3 2 3 0 = 8 * explicitZ 1 0 3 2 3 0 := by decide
254theorem e_103231 : m2Num 1 0 3 2 3 1 = 8 * explicitZ 1 0 3 2 3 1 := by decide
255theorem e_103232 : m2Num 1 0 3 2 3 2 = 8 * explicitZ 1 0 3 2 3 2 := by decide
256theorem e_103233 : m2Num 1 0 3 2 3 3 = 8 * explicitZ 1 0 3 2 3 3 := by decide
257theorem e_103300 : m2Num 1 0 3 3 0 0 = 8 * explicitZ 1 0 3 3 0 0 := by decide
258theorem e_103301 : m2Num 1 0 3 3 0 1 = 8 * explicitZ 1 0 3 3 0 1 := by decide
259theorem e_103302 : m2Num 1 0 3 3 0 2 = 8 * explicitZ 1 0 3 3 0 2 := by decide
260theorem e_103303 : m2Num 1 0 3 3 0 3 = 8 * explicitZ 1 0 3 3 0 3 := by decide
261theorem e_103310 : m2Num 1 0 3 3 1 0 = 8 * explicitZ 1 0 3 3 1 0 := by decide
262theorem e_103311 : m2Num 1 0 3 3 1 1 = 8 * explicitZ 1 0 3 3 1 1 := by decide
263theorem e_103312 : m2Num 1 0 3 3 1 2 = 8 * explicitZ 1 0 3 3 1 2 := by decide
264theorem e_103313 : m2Num 1 0 3 3 1 3 = 8 * explicitZ 1 0 3 3 1 3 := by decide
265theorem e_103320 : m2Num 1 0 3 3 2 0 = 8 * explicitZ 1 0 3 3 2 0 := by decide
266theorem e_103321 : m2Num 1 0 3 3 2 1 = 8 * explicitZ 1 0 3 3 2 1 := by decide
267theorem e_103322 : m2Num 1 0 3 3 2 2 = 8 * explicitZ 1 0 3 3 2 2 := by decide
268theorem e_103323 : m2Num 1 0 3 3 2 3 = 8 * explicitZ 1 0 3 3 2 3 := by decide
269theorem e_103330 : m2Num 1 0 3 3 3 0 = 8 * explicitZ 1 0 3 3 3 0 := by decide
270theorem e_103331 : m2Num 1 0 3 3 3 1 = 8 * explicitZ 1 0 3 3 3 1 := by decide
271theorem e_103332 : m2Num 1 0 3 3 3 2 = 8 * explicitZ 1 0 3 3 3 2 := by decide
272theorem e_103333 : m2Num 1 0 3 3 3 3 = 8 * explicitZ 1 0 3 3 3 3 := by decide
273
274end M2NumChunk04
275end ReggeExactMidpointM2TTIdentity4D
276end Analysis
277end Gravity
278end IndisputableMonolith
279