IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DM2NumChunk05
IndisputableMonolith/Gravity/Analysis/ReggeExactMidpointM2TTIdentity4DM2NumChunk05.lean · 279 lines · 256 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DKernelCert
3
4/-! m2Num = 8·explicitZ, chunk 5 (256 kernel decides). -/
5
6namespace IndisputableMonolith
7namespace Gravity
8namespace Analysis
9namespace ReggeExactMidpointM2TTIdentity4D
10namespace M2NumChunk05
11
12open KernelCert
13
14set_option maxRecDepth 100000
15set_option maxHeartbeats 200000000
16
17theorem e_110000 : m2Num 1 1 0 0 0 0 = 8 * explicitZ 1 1 0 0 0 0 := by decide
18theorem e_110001 : m2Num 1 1 0 0 0 1 = 8 * explicitZ 1 1 0 0 0 1 := by decide
19theorem e_110002 : m2Num 1 1 0 0 0 2 = 8 * explicitZ 1 1 0 0 0 2 := by decide
20theorem e_110003 : m2Num 1 1 0 0 0 3 = 8 * explicitZ 1 1 0 0 0 3 := by decide
21theorem e_110010 : m2Num 1 1 0 0 1 0 = 8 * explicitZ 1 1 0 0 1 0 := by decide
22theorem e_110011 : m2Num 1 1 0 0 1 1 = 8 * explicitZ 1 1 0 0 1 1 := by decide
23theorem e_110012 : m2Num 1 1 0 0 1 2 = 8 * explicitZ 1 1 0 0 1 2 := by decide
24theorem e_110013 : m2Num 1 1 0 0 1 3 = 8 * explicitZ 1 1 0 0 1 3 := by decide
25theorem e_110020 : m2Num 1 1 0 0 2 0 = 8 * explicitZ 1 1 0 0 2 0 := by decide
26theorem e_110021 : m2Num 1 1 0 0 2 1 = 8 * explicitZ 1 1 0 0 2 1 := by decide
27theorem e_110022 : m2Num 1 1 0 0 2 2 = 8 * explicitZ 1 1 0 0 2 2 := by decide
28theorem e_110023 : m2Num 1 1 0 0 2 3 = 8 * explicitZ 1 1 0 0 2 3 := by decide
29theorem e_110030 : m2Num 1 1 0 0 3 0 = 8 * explicitZ 1 1 0 0 3 0 := by decide
30theorem e_110031 : m2Num 1 1 0 0 3 1 = 8 * explicitZ 1 1 0 0 3 1 := by decide
31theorem e_110032 : m2Num 1 1 0 0 3 2 = 8 * explicitZ 1 1 0 0 3 2 := by decide
32theorem e_110033 : m2Num 1 1 0 0 3 3 = 8 * explicitZ 1 1 0 0 3 3 := by decide
33theorem e_110100 : m2Num 1 1 0 1 0 0 = 8 * explicitZ 1 1 0 1 0 0 := by decide
34theorem e_110101 : m2Num 1 1 0 1 0 1 = 8 * explicitZ 1 1 0 1 0 1 := by decide
35theorem e_110102 : m2Num 1 1 0 1 0 2 = 8 * explicitZ 1 1 0 1 0 2 := by decide
36theorem e_110103 : m2Num 1 1 0 1 0 3 = 8 * explicitZ 1 1 0 1 0 3 := by decide
37theorem e_110110 : m2Num 1 1 0 1 1 0 = 8 * explicitZ 1 1 0 1 1 0 := by decide
38theorem e_110111 : m2Num 1 1 0 1 1 1 = 8 * explicitZ 1 1 0 1 1 1 := by decide
39theorem e_110112 : m2Num 1 1 0 1 1 2 = 8 * explicitZ 1 1 0 1 1 2 := by decide
40theorem e_110113 : m2Num 1 1 0 1 1 3 = 8 * explicitZ 1 1 0 1 1 3 := by decide
41theorem e_110120 : m2Num 1 1 0 1 2 0 = 8 * explicitZ 1 1 0 1 2 0 := by decide
42theorem e_110121 : m2Num 1 1 0 1 2 1 = 8 * explicitZ 1 1 0 1 2 1 := by decide
43theorem e_110122 : m2Num 1 1 0 1 2 2 = 8 * explicitZ 1 1 0 1 2 2 := by decide
44theorem e_110123 : m2Num 1 1 0 1 2 3 = 8 * explicitZ 1 1 0 1 2 3 := by decide
45theorem e_110130 : m2Num 1 1 0 1 3 0 = 8 * explicitZ 1 1 0 1 3 0 := by decide
46theorem e_110131 : m2Num 1 1 0 1 3 1 = 8 * explicitZ 1 1 0 1 3 1 := by decide
47theorem e_110132 : m2Num 1 1 0 1 3 2 = 8 * explicitZ 1 1 0 1 3 2 := by decide
48theorem e_110133 : m2Num 1 1 0 1 3 3 = 8 * explicitZ 1 1 0 1 3 3 := by decide
49theorem e_110200 : m2Num 1 1 0 2 0 0 = 8 * explicitZ 1 1 0 2 0 0 := by decide
50theorem e_110201 : m2Num 1 1 0 2 0 1 = 8 * explicitZ 1 1 0 2 0 1 := by decide
51theorem e_110202 : m2Num 1 1 0 2 0 2 = 8 * explicitZ 1 1 0 2 0 2 := by decide
52theorem e_110203 : m2Num 1 1 0 2 0 3 = 8 * explicitZ 1 1 0 2 0 3 := by decide
53theorem e_110210 : m2Num 1 1 0 2 1 0 = 8 * explicitZ 1 1 0 2 1 0 := by decide
54theorem e_110211 : m2Num 1 1 0 2 1 1 = 8 * explicitZ 1 1 0 2 1 1 := by decide
55theorem e_110212 : m2Num 1 1 0 2 1 2 = 8 * explicitZ 1 1 0 2 1 2 := by decide
56theorem e_110213 : m2Num 1 1 0 2 1 3 = 8 * explicitZ 1 1 0 2 1 3 := by decide
57theorem e_110220 : m2Num 1 1 0 2 2 0 = 8 * explicitZ 1 1 0 2 2 0 := by decide
58theorem e_110221 : m2Num 1 1 0 2 2 1 = 8 * explicitZ 1 1 0 2 2 1 := by decide
59theorem e_110222 : m2Num 1 1 0 2 2 2 = 8 * explicitZ 1 1 0 2 2 2 := by decide
60theorem e_110223 : m2Num 1 1 0 2 2 3 = 8 * explicitZ 1 1 0 2 2 3 := by decide
61theorem e_110230 : m2Num 1 1 0 2 3 0 = 8 * explicitZ 1 1 0 2 3 0 := by decide
62theorem e_110231 : m2Num 1 1 0 2 3 1 = 8 * explicitZ 1 1 0 2 3 1 := by decide
63theorem e_110232 : m2Num 1 1 0 2 3 2 = 8 * explicitZ 1 1 0 2 3 2 := by decide
64theorem e_110233 : m2Num 1 1 0 2 3 3 = 8 * explicitZ 1 1 0 2 3 3 := by decide
65theorem e_110300 : m2Num 1 1 0 3 0 0 = 8 * explicitZ 1 1 0 3 0 0 := by decide
66theorem e_110301 : m2Num 1 1 0 3 0 1 = 8 * explicitZ 1 1 0 3 0 1 := by decide
67theorem e_110302 : m2Num 1 1 0 3 0 2 = 8 * explicitZ 1 1 0 3 0 2 := by decide
68theorem e_110303 : m2Num 1 1 0 3 0 3 = 8 * explicitZ 1 1 0 3 0 3 := by decide
69theorem e_110310 : m2Num 1 1 0 3 1 0 = 8 * explicitZ 1 1 0 3 1 0 := by decide
70theorem e_110311 : m2Num 1 1 0 3 1 1 = 8 * explicitZ 1 1 0 3 1 1 := by decide
71theorem e_110312 : m2Num 1 1 0 3 1 2 = 8 * explicitZ 1 1 0 3 1 2 := by decide
72theorem e_110313 : m2Num 1 1 0 3 1 3 = 8 * explicitZ 1 1 0 3 1 3 := by decide
73theorem e_110320 : m2Num 1 1 0 3 2 0 = 8 * explicitZ 1 1 0 3 2 0 := by decide
74theorem e_110321 : m2Num 1 1 0 3 2 1 = 8 * explicitZ 1 1 0 3 2 1 := by decide
75theorem e_110322 : m2Num 1 1 0 3 2 2 = 8 * explicitZ 1 1 0 3 2 2 := by decide
76theorem e_110323 : m2Num 1 1 0 3 2 3 = 8 * explicitZ 1 1 0 3 2 3 := by decide
77theorem e_110330 : m2Num 1 1 0 3 3 0 = 8 * explicitZ 1 1 0 3 3 0 := by decide
78theorem e_110331 : m2Num 1 1 0 3 3 1 = 8 * explicitZ 1 1 0 3 3 1 := by decide
79theorem e_110332 : m2Num 1 1 0 3 3 2 = 8 * explicitZ 1 1 0 3 3 2 := by decide
80theorem e_110333 : m2Num 1 1 0 3 3 3 = 8 * explicitZ 1 1 0 3 3 3 := by decide
81theorem e_111000 : m2Num 1 1 1 0 0 0 = 8 * explicitZ 1 1 1 0 0 0 := by decide
82theorem e_111001 : m2Num 1 1 1 0 0 1 = 8 * explicitZ 1 1 1 0 0 1 := by decide
83theorem e_111002 : m2Num 1 1 1 0 0 2 = 8 * explicitZ 1 1 1 0 0 2 := by decide
84theorem e_111003 : m2Num 1 1 1 0 0 3 = 8 * explicitZ 1 1 1 0 0 3 := by decide
85theorem e_111010 : m2Num 1 1 1 0 1 0 = 8 * explicitZ 1 1 1 0 1 0 := by decide
86theorem e_111011 : m2Num 1 1 1 0 1 1 = 8 * explicitZ 1 1 1 0 1 1 := by decide
87theorem e_111012 : m2Num 1 1 1 0 1 2 = 8 * explicitZ 1 1 1 0 1 2 := by decide
88theorem e_111013 : m2Num 1 1 1 0 1 3 = 8 * explicitZ 1 1 1 0 1 3 := by decide
89theorem e_111020 : m2Num 1 1 1 0 2 0 = 8 * explicitZ 1 1 1 0 2 0 := by decide
90theorem e_111021 : m2Num 1 1 1 0 2 1 = 8 * explicitZ 1 1 1 0 2 1 := by decide
91theorem e_111022 : m2Num 1 1 1 0 2 2 = 8 * explicitZ 1 1 1 0 2 2 := by decide
92theorem e_111023 : m2Num 1 1 1 0 2 3 = 8 * explicitZ 1 1 1 0 2 3 := by decide
93theorem e_111030 : m2Num 1 1 1 0 3 0 = 8 * explicitZ 1 1 1 0 3 0 := by decide
94theorem e_111031 : m2Num 1 1 1 0 3 1 = 8 * explicitZ 1 1 1 0 3 1 := by decide
95theorem e_111032 : m2Num 1 1 1 0 3 2 = 8 * explicitZ 1 1 1 0 3 2 := by decide
96theorem e_111033 : m2Num 1 1 1 0 3 3 = 8 * explicitZ 1 1 1 0 3 3 := by decide
97theorem e_111100 : m2Num 1 1 1 1 0 0 = 8 * explicitZ 1 1 1 1 0 0 := by decide
98theorem e_111101 : m2Num 1 1 1 1 0 1 = 8 * explicitZ 1 1 1 1 0 1 := by decide
99theorem e_111102 : m2Num 1 1 1 1 0 2 = 8 * explicitZ 1 1 1 1 0 2 := by decide
100theorem e_111103 : m2Num 1 1 1 1 0 3 = 8 * explicitZ 1 1 1 1 0 3 := by decide
101theorem e_111110 : m2Num 1 1 1 1 1 0 = 8 * explicitZ 1 1 1 1 1 0 := by decide
102theorem e_111111 : m2Num 1 1 1 1 1 1 = 8 * explicitZ 1 1 1 1 1 1 := by decide
103theorem e_111112 : m2Num 1 1 1 1 1 2 = 8 * explicitZ 1 1 1 1 1 2 := by decide
104theorem e_111113 : m2Num 1 1 1 1 1 3 = 8 * explicitZ 1 1 1 1 1 3 := by decide
105theorem e_111120 : m2Num 1 1 1 1 2 0 = 8 * explicitZ 1 1 1 1 2 0 := by decide
106theorem e_111121 : m2Num 1 1 1 1 2 1 = 8 * explicitZ 1 1 1 1 2 1 := by decide
107theorem e_111122 : m2Num 1 1 1 1 2 2 = 8 * explicitZ 1 1 1 1 2 2 := by decide
108theorem e_111123 : m2Num 1 1 1 1 2 3 = 8 * explicitZ 1 1 1 1 2 3 := by decide
109theorem e_111130 : m2Num 1 1 1 1 3 0 = 8 * explicitZ 1 1 1 1 3 0 := by decide
110theorem e_111131 : m2Num 1 1 1 1 3 1 = 8 * explicitZ 1 1 1 1 3 1 := by decide
111theorem e_111132 : m2Num 1 1 1 1 3 2 = 8 * explicitZ 1 1 1 1 3 2 := by decide
112theorem e_111133 : m2Num 1 1 1 1 3 3 = 8 * explicitZ 1 1 1 1 3 3 := by decide
113theorem e_111200 : m2Num 1 1 1 2 0 0 = 8 * explicitZ 1 1 1 2 0 0 := by decide
114theorem e_111201 : m2Num 1 1 1 2 0 1 = 8 * explicitZ 1 1 1 2 0 1 := by decide
115theorem e_111202 : m2Num 1 1 1 2 0 2 = 8 * explicitZ 1 1 1 2 0 2 := by decide
116theorem e_111203 : m2Num 1 1 1 2 0 3 = 8 * explicitZ 1 1 1 2 0 3 := by decide
117theorem e_111210 : m2Num 1 1 1 2 1 0 = 8 * explicitZ 1 1 1 2 1 0 := by decide
118theorem e_111211 : m2Num 1 1 1 2 1 1 = 8 * explicitZ 1 1 1 2 1 1 := by decide
119theorem e_111212 : m2Num 1 1 1 2 1 2 = 8 * explicitZ 1 1 1 2 1 2 := by decide
120theorem e_111213 : m2Num 1 1 1 2 1 3 = 8 * explicitZ 1 1 1 2 1 3 := by decide
121theorem e_111220 : m2Num 1 1 1 2 2 0 = 8 * explicitZ 1 1 1 2 2 0 := by decide
122theorem e_111221 : m2Num 1 1 1 2 2 1 = 8 * explicitZ 1 1 1 2 2 1 := by decide
123theorem e_111222 : m2Num 1 1 1 2 2 2 = 8 * explicitZ 1 1 1 2 2 2 := by decide
124theorem e_111223 : m2Num 1 1 1 2 2 3 = 8 * explicitZ 1 1 1 2 2 3 := by decide
125theorem e_111230 : m2Num 1 1 1 2 3 0 = 8 * explicitZ 1 1 1 2 3 0 := by decide
126theorem e_111231 : m2Num 1 1 1 2 3 1 = 8 * explicitZ 1 1 1 2 3 1 := by decide
127theorem e_111232 : m2Num 1 1 1 2 3 2 = 8 * explicitZ 1 1 1 2 3 2 := by decide
128theorem e_111233 : m2Num 1 1 1 2 3 3 = 8 * explicitZ 1 1 1 2 3 3 := by decide
129theorem e_111300 : m2Num 1 1 1 3 0 0 = 8 * explicitZ 1 1 1 3 0 0 := by decide
130theorem e_111301 : m2Num 1 1 1 3 0 1 = 8 * explicitZ 1 1 1 3 0 1 := by decide
131theorem e_111302 : m2Num 1 1 1 3 0 2 = 8 * explicitZ 1 1 1 3 0 2 := by decide
132theorem e_111303 : m2Num 1 1 1 3 0 3 = 8 * explicitZ 1 1 1 3 0 3 := by decide
133theorem e_111310 : m2Num 1 1 1 3 1 0 = 8 * explicitZ 1 1 1 3 1 0 := by decide
134theorem e_111311 : m2Num 1 1 1 3 1 1 = 8 * explicitZ 1 1 1 3 1 1 := by decide
135theorem e_111312 : m2Num 1 1 1 3 1 2 = 8 * explicitZ 1 1 1 3 1 2 := by decide
136theorem e_111313 : m2Num 1 1 1 3 1 3 = 8 * explicitZ 1 1 1 3 1 3 := by decide
137theorem e_111320 : m2Num 1 1 1 3 2 0 = 8 * explicitZ 1 1 1 3 2 0 := by decide
138theorem e_111321 : m2Num 1 1 1 3 2 1 = 8 * explicitZ 1 1 1 3 2 1 := by decide
139theorem e_111322 : m2Num 1 1 1 3 2 2 = 8 * explicitZ 1 1 1 3 2 2 := by decide
140theorem e_111323 : m2Num 1 1 1 3 2 3 = 8 * explicitZ 1 1 1 3 2 3 := by decide
141theorem e_111330 : m2Num 1 1 1 3 3 0 = 8 * explicitZ 1 1 1 3 3 0 := by decide
142theorem e_111331 : m2Num 1 1 1 3 3 1 = 8 * explicitZ 1 1 1 3 3 1 := by decide
143theorem e_111332 : m2Num 1 1 1 3 3 2 = 8 * explicitZ 1 1 1 3 3 2 := by decide
144theorem e_111333 : m2Num 1 1 1 3 3 3 = 8 * explicitZ 1 1 1 3 3 3 := by decide
145theorem e_112000 : m2Num 1 1 2 0 0 0 = 8 * explicitZ 1 1 2 0 0 0 := by decide
146theorem e_112001 : m2Num 1 1 2 0 0 1 = 8 * explicitZ 1 1 2 0 0 1 := by decide
147theorem e_112002 : m2Num 1 1 2 0 0 2 = 8 * explicitZ 1 1 2 0 0 2 := by decide
148theorem e_112003 : m2Num 1 1 2 0 0 3 = 8 * explicitZ 1 1 2 0 0 3 := by decide
149theorem e_112010 : m2Num 1 1 2 0 1 0 = 8 * explicitZ 1 1 2 0 1 0 := by decide
150theorem e_112011 : m2Num 1 1 2 0 1 1 = 8 * explicitZ 1 1 2 0 1 1 := by decide
151theorem e_112012 : m2Num 1 1 2 0 1 2 = 8 * explicitZ 1 1 2 0 1 2 := by decide
152theorem e_112013 : m2Num 1 1 2 0 1 3 = 8 * explicitZ 1 1 2 0 1 3 := by decide
153theorem e_112020 : m2Num 1 1 2 0 2 0 = 8 * explicitZ 1 1 2 0 2 0 := by decide
154theorem e_112021 : m2Num 1 1 2 0 2 1 = 8 * explicitZ 1 1 2 0 2 1 := by decide
155theorem e_112022 : m2Num 1 1 2 0 2 2 = 8 * explicitZ 1 1 2 0 2 2 := by decide
156theorem e_112023 : m2Num 1 1 2 0 2 3 = 8 * explicitZ 1 1 2 0 2 3 := by decide
157theorem e_112030 : m2Num 1 1 2 0 3 0 = 8 * explicitZ 1 1 2 0 3 0 := by decide
158theorem e_112031 : m2Num 1 1 2 0 3 1 = 8 * explicitZ 1 1 2 0 3 1 := by decide
159theorem e_112032 : m2Num 1 1 2 0 3 2 = 8 * explicitZ 1 1 2 0 3 2 := by decide
160theorem e_112033 : m2Num 1 1 2 0 3 3 = 8 * explicitZ 1 1 2 0 3 3 := by decide
161theorem e_112100 : m2Num 1 1 2 1 0 0 = 8 * explicitZ 1 1 2 1 0 0 := by decide
162theorem e_112101 : m2Num 1 1 2 1 0 1 = 8 * explicitZ 1 1 2 1 0 1 := by decide
163theorem e_112102 : m2Num 1 1 2 1 0 2 = 8 * explicitZ 1 1 2 1 0 2 := by decide
164theorem e_112103 : m2Num 1 1 2 1 0 3 = 8 * explicitZ 1 1 2 1 0 3 := by decide
165theorem e_112110 : m2Num 1 1 2 1 1 0 = 8 * explicitZ 1 1 2 1 1 0 := by decide
166theorem e_112111 : m2Num 1 1 2 1 1 1 = 8 * explicitZ 1 1 2 1 1 1 := by decide
167theorem e_112112 : m2Num 1 1 2 1 1 2 = 8 * explicitZ 1 1 2 1 1 2 := by decide
168theorem e_112113 : m2Num 1 1 2 1 1 3 = 8 * explicitZ 1 1 2 1 1 3 := by decide
169theorem e_112120 : m2Num 1 1 2 1 2 0 = 8 * explicitZ 1 1 2 1 2 0 := by decide
170theorem e_112121 : m2Num 1 1 2 1 2 1 = 8 * explicitZ 1 1 2 1 2 1 := by decide
171theorem e_112122 : m2Num 1 1 2 1 2 2 = 8 * explicitZ 1 1 2 1 2 2 := by decide
172theorem e_112123 : m2Num 1 1 2 1 2 3 = 8 * explicitZ 1 1 2 1 2 3 := by decide
173theorem e_112130 : m2Num 1 1 2 1 3 0 = 8 * explicitZ 1 1 2 1 3 0 := by decide
174theorem e_112131 : m2Num 1 1 2 1 3 1 = 8 * explicitZ 1 1 2 1 3 1 := by decide
175theorem e_112132 : m2Num 1 1 2 1 3 2 = 8 * explicitZ 1 1 2 1 3 2 := by decide
176theorem e_112133 : m2Num 1 1 2 1 3 3 = 8 * explicitZ 1 1 2 1 3 3 := by decide
177theorem e_112200 : m2Num 1 1 2 2 0 0 = 8 * explicitZ 1 1 2 2 0 0 := by decide
178theorem e_112201 : m2Num 1 1 2 2 0 1 = 8 * explicitZ 1 1 2 2 0 1 := by decide
179theorem e_112202 : m2Num 1 1 2 2 0 2 = 8 * explicitZ 1 1 2 2 0 2 := by decide
180theorem e_112203 : m2Num 1 1 2 2 0 3 = 8 * explicitZ 1 1 2 2 0 3 := by decide
181theorem e_112210 : m2Num 1 1 2 2 1 0 = 8 * explicitZ 1 1 2 2 1 0 := by decide
182theorem e_112211 : m2Num 1 1 2 2 1 1 = 8 * explicitZ 1 1 2 2 1 1 := by decide
183theorem e_112212 : m2Num 1 1 2 2 1 2 = 8 * explicitZ 1 1 2 2 1 2 := by decide
184theorem e_112213 : m2Num 1 1 2 2 1 3 = 8 * explicitZ 1 1 2 2 1 3 := by decide
185theorem e_112220 : m2Num 1 1 2 2 2 0 = 8 * explicitZ 1 1 2 2 2 0 := by decide
186theorem e_112221 : m2Num 1 1 2 2 2 1 = 8 * explicitZ 1 1 2 2 2 1 := by decide
187theorem e_112222 : m2Num 1 1 2 2 2 2 = 8 * explicitZ 1 1 2 2 2 2 := by decide
188theorem e_112223 : m2Num 1 1 2 2 2 3 = 8 * explicitZ 1 1 2 2 2 3 := by decide
189theorem e_112230 : m2Num 1 1 2 2 3 0 = 8 * explicitZ 1 1 2 2 3 0 := by decide
190theorem e_112231 : m2Num 1 1 2 2 3 1 = 8 * explicitZ 1 1 2 2 3 1 := by decide
191theorem e_112232 : m2Num 1 1 2 2 3 2 = 8 * explicitZ 1 1 2 2 3 2 := by decide
192theorem e_112233 : m2Num 1 1 2 2 3 3 = 8 * explicitZ 1 1 2 2 3 3 := by decide
193theorem e_112300 : m2Num 1 1 2 3 0 0 = 8 * explicitZ 1 1 2 3 0 0 := by decide
194theorem e_112301 : m2Num 1 1 2 3 0 1 = 8 * explicitZ 1 1 2 3 0 1 := by decide
195theorem e_112302 : m2Num 1 1 2 3 0 2 = 8 * explicitZ 1 1 2 3 0 2 := by decide
196theorem e_112303 : m2Num 1 1 2 3 0 3 = 8 * explicitZ 1 1 2 3 0 3 := by decide
197theorem e_112310 : m2Num 1 1 2 3 1 0 = 8 * explicitZ 1 1 2 3 1 0 := by decide
198theorem e_112311 : m2Num 1 1 2 3 1 1 = 8 * explicitZ 1 1 2 3 1 1 := by decide
199theorem e_112312 : m2Num 1 1 2 3 1 2 = 8 * explicitZ 1 1 2 3 1 2 := by decide
200theorem e_112313 : m2Num 1 1 2 3 1 3 = 8 * explicitZ 1 1 2 3 1 3 := by decide
201theorem e_112320 : m2Num 1 1 2 3 2 0 = 8 * explicitZ 1 1 2 3 2 0 := by decide
202theorem e_112321 : m2Num 1 1 2 3 2 1 = 8 * explicitZ 1 1 2 3 2 1 := by decide
203theorem e_112322 : m2Num 1 1 2 3 2 2 = 8 * explicitZ 1 1 2 3 2 2 := by decide
204theorem e_112323 : m2Num 1 1 2 3 2 3 = 8 * explicitZ 1 1 2 3 2 3 := by decide
205theorem e_112330 : m2Num 1 1 2 3 3 0 = 8 * explicitZ 1 1 2 3 3 0 := by decide
206theorem e_112331 : m2Num 1 1 2 3 3 1 = 8 * explicitZ 1 1 2 3 3 1 := by decide
207theorem e_112332 : m2Num 1 1 2 3 3 2 = 8 * explicitZ 1 1 2 3 3 2 := by decide
208theorem e_112333 : m2Num 1 1 2 3 3 3 = 8 * explicitZ 1 1 2 3 3 3 := by decide
209theorem e_113000 : m2Num 1 1 3 0 0 0 = 8 * explicitZ 1 1 3 0 0 0 := by decide
210theorem e_113001 : m2Num 1 1 3 0 0 1 = 8 * explicitZ 1 1 3 0 0 1 := by decide
211theorem e_113002 : m2Num 1 1 3 0 0 2 = 8 * explicitZ 1 1 3 0 0 2 := by decide
212theorem e_113003 : m2Num 1 1 3 0 0 3 = 8 * explicitZ 1 1 3 0 0 3 := by decide
213theorem e_113010 : m2Num 1 1 3 0 1 0 = 8 * explicitZ 1 1 3 0 1 0 := by decide
214theorem e_113011 : m2Num 1 1 3 0 1 1 = 8 * explicitZ 1 1 3 0 1 1 := by decide
215theorem e_113012 : m2Num 1 1 3 0 1 2 = 8 * explicitZ 1 1 3 0 1 2 := by decide
216theorem e_113013 : m2Num 1 1 3 0 1 3 = 8 * explicitZ 1 1 3 0 1 3 := by decide
217theorem e_113020 : m2Num 1 1 3 0 2 0 = 8 * explicitZ 1 1 3 0 2 0 := by decide
218theorem e_113021 : m2Num 1 1 3 0 2 1 = 8 * explicitZ 1 1 3 0 2 1 := by decide
219theorem e_113022 : m2Num 1 1 3 0 2 2 = 8 * explicitZ 1 1 3 0 2 2 := by decide
220theorem e_113023 : m2Num 1 1 3 0 2 3 = 8 * explicitZ 1 1 3 0 2 3 := by decide
221theorem e_113030 : m2Num 1 1 3 0 3 0 = 8 * explicitZ 1 1 3 0 3 0 := by decide
222theorem e_113031 : m2Num 1 1 3 0 3 1 = 8 * explicitZ 1 1 3 0 3 1 := by decide
223theorem e_113032 : m2Num 1 1 3 0 3 2 = 8 * explicitZ 1 1 3 0 3 2 := by decide
224theorem e_113033 : m2Num 1 1 3 0 3 3 = 8 * explicitZ 1 1 3 0 3 3 := by decide
225theorem e_113100 : m2Num 1 1 3 1 0 0 = 8 * explicitZ 1 1 3 1 0 0 := by decide
226theorem e_113101 : m2Num 1 1 3 1 0 1 = 8 * explicitZ 1 1 3 1 0 1 := by decide
227theorem e_113102 : m2Num 1 1 3 1 0 2 = 8 * explicitZ 1 1 3 1 0 2 := by decide
228theorem e_113103 : m2Num 1 1 3 1 0 3 = 8 * explicitZ 1 1 3 1 0 3 := by decide
229theorem e_113110 : m2Num 1 1 3 1 1 0 = 8 * explicitZ 1 1 3 1 1 0 := by decide
230theorem e_113111 : m2Num 1 1 3 1 1 1 = 8 * explicitZ 1 1 3 1 1 1 := by decide
231theorem e_113112 : m2Num 1 1 3 1 1 2 = 8 * explicitZ 1 1 3 1 1 2 := by decide
232theorem e_113113 : m2Num 1 1 3 1 1 3 = 8 * explicitZ 1 1 3 1 1 3 := by decide
233theorem e_113120 : m2Num 1 1 3 1 2 0 = 8 * explicitZ 1 1 3 1 2 0 := by decide
234theorem e_113121 : m2Num 1 1 3 1 2 1 = 8 * explicitZ 1 1 3 1 2 1 := by decide
235theorem e_113122 : m2Num 1 1 3 1 2 2 = 8 * explicitZ 1 1 3 1 2 2 := by decide
236theorem e_113123 : m2Num 1 1 3 1 2 3 = 8 * explicitZ 1 1 3 1 2 3 := by decide
237theorem e_113130 : m2Num 1 1 3 1 3 0 = 8 * explicitZ 1 1 3 1 3 0 := by decide
238theorem e_113131 : m2Num 1 1 3 1 3 1 = 8 * explicitZ 1 1 3 1 3 1 := by decide
239theorem e_113132 : m2Num 1 1 3 1 3 2 = 8 * explicitZ 1 1 3 1 3 2 := by decide
240theorem e_113133 : m2Num 1 1 3 1 3 3 = 8 * explicitZ 1 1 3 1 3 3 := by decide
241theorem e_113200 : m2Num 1 1 3 2 0 0 = 8 * explicitZ 1 1 3 2 0 0 := by decide
242theorem e_113201 : m2Num 1 1 3 2 0 1 = 8 * explicitZ 1 1 3 2 0 1 := by decide
243theorem e_113202 : m2Num 1 1 3 2 0 2 = 8 * explicitZ 1 1 3 2 0 2 := by decide
244theorem e_113203 : m2Num 1 1 3 2 0 3 = 8 * explicitZ 1 1 3 2 0 3 := by decide
245theorem e_113210 : m2Num 1 1 3 2 1 0 = 8 * explicitZ 1 1 3 2 1 0 := by decide
246theorem e_113211 : m2Num 1 1 3 2 1 1 = 8 * explicitZ 1 1 3 2 1 1 := by decide
247theorem e_113212 : m2Num 1 1 3 2 1 2 = 8 * explicitZ 1 1 3 2 1 2 := by decide
248theorem e_113213 : m2Num 1 1 3 2 1 3 = 8 * explicitZ 1 1 3 2 1 3 := by decide
249theorem e_113220 : m2Num 1 1 3 2 2 0 = 8 * explicitZ 1 1 3 2 2 0 := by decide
250theorem e_113221 : m2Num 1 1 3 2 2 1 = 8 * explicitZ 1 1 3 2 2 1 := by decide
251theorem e_113222 : m2Num 1 1 3 2 2 2 = 8 * explicitZ 1 1 3 2 2 2 := by decide
252theorem e_113223 : m2Num 1 1 3 2 2 3 = 8 * explicitZ 1 1 3 2 2 3 := by decide
253theorem e_113230 : m2Num 1 1 3 2 3 0 = 8 * explicitZ 1 1 3 2 3 0 := by decide
254theorem e_113231 : m2Num 1 1 3 2 3 1 = 8 * explicitZ 1 1 3 2 3 1 := by decide
255theorem e_113232 : m2Num 1 1 3 2 3 2 = 8 * explicitZ 1 1 3 2 3 2 := by decide
256theorem e_113233 : m2Num 1 1 3 2 3 3 = 8 * explicitZ 1 1 3 2 3 3 := by decide
257theorem e_113300 : m2Num 1 1 3 3 0 0 = 8 * explicitZ 1 1 3 3 0 0 := by decide
258theorem e_113301 : m2Num 1 1 3 3 0 1 = 8 * explicitZ 1 1 3 3 0 1 := by decide
259theorem e_113302 : m2Num 1 1 3 3 0 2 = 8 * explicitZ 1 1 3 3 0 2 := by decide
260theorem e_113303 : m2Num 1 1 3 3 0 3 = 8 * explicitZ 1 1 3 3 0 3 := by decide
261theorem e_113310 : m2Num 1 1 3 3 1 0 = 8 * explicitZ 1 1 3 3 1 0 := by decide
262theorem e_113311 : m2Num 1 1 3 3 1 1 = 8 * explicitZ 1 1 3 3 1 1 := by decide
263theorem e_113312 : m2Num 1 1 3 3 1 2 = 8 * explicitZ 1 1 3 3 1 2 := by decide
264theorem e_113313 : m2Num 1 1 3 3 1 3 = 8 * explicitZ 1 1 3 3 1 3 := by decide
265theorem e_113320 : m2Num 1 1 3 3 2 0 = 8 * explicitZ 1 1 3 3 2 0 := by decide
266theorem e_113321 : m2Num 1 1 3 3 2 1 = 8 * explicitZ 1 1 3 3 2 1 := by decide
267theorem e_113322 : m2Num 1 1 3 3 2 2 = 8 * explicitZ 1 1 3 3 2 2 := by decide
268theorem e_113323 : m2Num 1 1 3 3 2 3 = 8 * explicitZ 1 1 3 3 2 3 := by decide
269theorem e_113330 : m2Num 1 1 3 3 3 0 = 8 * explicitZ 1 1 3 3 3 0 := by decide
270theorem e_113331 : m2Num 1 1 3 3 3 1 = 8 * explicitZ 1 1 3 3 3 1 := by decide
271theorem e_113332 : m2Num 1 1 3 3 3 2 = 8 * explicitZ 1 1 3 3 3 2 := by decide
272theorem e_113333 : m2Num 1 1 3 3 3 3 = 8 * explicitZ 1 1 3 3 3 3 := by decide
273
274end M2NumChunk05
275end ReggeExactMidpointM2TTIdentity4D
276end Analysis
277end Gravity
278end IndisputableMonolith
279