IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DM2NumChunk06
IndisputableMonolith/Gravity/Analysis/ReggeExactMidpointM2TTIdentity4DM2NumChunk06.lean · 279 lines · 256 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DKernelCert
3
4/-! m2Num = 8·explicitZ, chunk 6 (256 kernel decides). -/
5
6namespace IndisputableMonolith
7namespace Gravity
8namespace Analysis
9namespace ReggeExactMidpointM2TTIdentity4D
10namespace M2NumChunk06
11
12open KernelCert
13
14set_option maxRecDepth 100000
15set_option maxHeartbeats 200000000
16
17theorem e_120000 : m2Num 1 2 0 0 0 0 = 8 * explicitZ 1 2 0 0 0 0 := by decide
18theorem e_120001 : m2Num 1 2 0 0 0 1 = 8 * explicitZ 1 2 0 0 0 1 := by decide
19theorem e_120002 : m2Num 1 2 0 0 0 2 = 8 * explicitZ 1 2 0 0 0 2 := by decide
20theorem e_120003 : m2Num 1 2 0 0 0 3 = 8 * explicitZ 1 2 0 0 0 3 := by decide
21theorem e_120010 : m2Num 1 2 0 0 1 0 = 8 * explicitZ 1 2 0 0 1 0 := by decide
22theorem e_120011 : m2Num 1 2 0 0 1 1 = 8 * explicitZ 1 2 0 0 1 1 := by decide
23theorem e_120012 : m2Num 1 2 0 0 1 2 = 8 * explicitZ 1 2 0 0 1 2 := by decide
24theorem e_120013 : m2Num 1 2 0 0 1 3 = 8 * explicitZ 1 2 0 0 1 3 := by decide
25theorem e_120020 : m2Num 1 2 0 0 2 0 = 8 * explicitZ 1 2 0 0 2 0 := by decide
26theorem e_120021 : m2Num 1 2 0 0 2 1 = 8 * explicitZ 1 2 0 0 2 1 := by decide
27theorem e_120022 : m2Num 1 2 0 0 2 2 = 8 * explicitZ 1 2 0 0 2 2 := by decide
28theorem e_120023 : m2Num 1 2 0 0 2 3 = 8 * explicitZ 1 2 0 0 2 3 := by decide
29theorem e_120030 : m2Num 1 2 0 0 3 0 = 8 * explicitZ 1 2 0 0 3 0 := by decide
30theorem e_120031 : m2Num 1 2 0 0 3 1 = 8 * explicitZ 1 2 0 0 3 1 := by decide
31theorem e_120032 : m2Num 1 2 0 0 3 2 = 8 * explicitZ 1 2 0 0 3 2 := by decide
32theorem e_120033 : m2Num 1 2 0 0 3 3 = 8 * explicitZ 1 2 0 0 3 3 := by decide
33theorem e_120100 : m2Num 1 2 0 1 0 0 = 8 * explicitZ 1 2 0 1 0 0 := by decide
34theorem e_120101 : m2Num 1 2 0 1 0 1 = 8 * explicitZ 1 2 0 1 0 1 := by decide
35theorem e_120102 : m2Num 1 2 0 1 0 2 = 8 * explicitZ 1 2 0 1 0 2 := by decide
36theorem e_120103 : m2Num 1 2 0 1 0 3 = 8 * explicitZ 1 2 0 1 0 3 := by decide
37theorem e_120110 : m2Num 1 2 0 1 1 0 = 8 * explicitZ 1 2 0 1 1 0 := by decide
38theorem e_120111 : m2Num 1 2 0 1 1 1 = 8 * explicitZ 1 2 0 1 1 1 := by decide
39theorem e_120112 : m2Num 1 2 0 1 1 2 = 8 * explicitZ 1 2 0 1 1 2 := by decide
40theorem e_120113 : m2Num 1 2 0 1 1 3 = 8 * explicitZ 1 2 0 1 1 3 := by decide
41theorem e_120120 : m2Num 1 2 0 1 2 0 = 8 * explicitZ 1 2 0 1 2 0 := by decide
42theorem e_120121 : m2Num 1 2 0 1 2 1 = 8 * explicitZ 1 2 0 1 2 1 := by decide
43theorem e_120122 : m2Num 1 2 0 1 2 2 = 8 * explicitZ 1 2 0 1 2 2 := by decide
44theorem e_120123 : m2Num 1 2 0 1 2 3 = 8 * explicitZ 1 2 0 1 2 3 := by decide
45theorem e_120130 : m2Num 1 2 0 1 3 0 = 8 * explicitZ 1 2 0 1 3 0 := by decide
46theorem e_120131 : m2Num 1 2 0 1 3 1 = 8 * explicitZ 1 2 0 1 3 1 := by decide
47theorem e_120132 : m2Num 1 2 0 1 3 2 = 8 * explicitZ 1 2 0 1 3 2 := by decide
48theorem e_120133 : m2Num 1 2 0 1 3 3 = 8 * explicitZ 1 2 0 1 3 3 := by decide
49theorem e_120200 : m2Num 1 2 0 2 0 0 = 8 * explicitZ 1 2 0 2 0 0 := by decide
50theorem e_120201 : m2Num 1 2 0 2 0 1 = 8 * explicitZ 1 2 0 2 0 1 := by decide
51theorem e_120202 : m2Num 1 2 0 2 0 2 = 8 * explicitZ 1 2 0 2 0 2 := by decide
52theorem e_120203 : m2Num 1 2 0 2 0 3 = 8 * explicitZ 1 2 0 2 0 3 := by decide
53theorem e_120210 : m2Num 1 2 0 2 1 0 = 8 * explicitZ 1 2 0 2 1 0 := by decide
54theorem e_120211 : m2Num 1 2 0 2 1 1 = 8 * explicitZ 1 2 0 2 1 1 := by decide
55theorem e_120212 : m2Num 1 2 0 2 1 2 = 8 * explicitZ 1 2 0 2 1 2 := by decide
56theorem e_120213 : m2Num 1 2 0 2 1 3 = 8 * explicitZ 1 2 0 2 1 3 := by decide
57theorem e_120220 : m2Num 1 2 0 2 2 0 = 8 * explicitZ 1 2 0 2 2 0 := by decide
58theorem e_120221 : m2Num 1 2 0 2 2 1 = 8 * explicitZ 1 2 0 2 2 1 := by decide
59theorem e_120222 : m2Num 1 2 0 2 2 2 = 8 * explicitZ 1 2 0 2 2 2 := by decide
60theorem e_120223 : m2Num 1 2 0 2 2 3 = 8 * explicitZ 1 2 0 2 2 3 := by decide
61theorem e_120230 : m2Num 1 2 0 2 3 0 = 8 * explicitZ 1 2 0 2 3 0 := by decide
62theorem e_120231 : m2Num 1 2 0 2 3 1 = 8 * explicitZ 1 2 0 2 3 1 := by decide
63theorem e_120232 : m2Num 1 2 0 2 3 2 = 8 * explicitZ 1 2 0 2 3 2 := by decide
64theorem e_120233 : m2Num 1 2 0 2 3 3 = 8 * explicitZ 1 2 0 2 3 3 := by decide
65theorem e_120300 : m2Num 1 2 0 3 0 0 = 8 * explicitZ 1 2 0 3 0 0 := by decide
66theorem e_120301 : m2Num 1 2 0 3 0 1 = 8 * explicitZ 1 2 0 3 0 1 := by decide
67theorem e_120302 : m2Num 1 2 0 3 0 2 = 8 * explicitZ 1 2 0 3 0 2 := by decide
68theorem e_120303 : m2Num 1 2 0 3 0 3 = 8 * explicitZ 1 2 0 3 0 3 := by decide
69theorem e_120310 : m2Num 1 2 0 3 1 0 = 8 * explicitZ 1 2 0 3 1 0 := by decide
70theorem e_120311 : m2Num 1 2 0 3 1 1 = 8 * explicitZ 1 2 0 3 1 1 := by decide
71theorem e_120312 : m2Num 1 2 0 3 1 2 = 8 * explicitZ 1 2 0 3 1 2 := by decide
72theorem e_120313 : m2Num 1 2 0 3 1 3 = 8 * explicitZ 1 2 0 3 1 3 := by decide
73theorem e_120320 : m2Num 1 2 0 3 2 0 = 8 * explicitZ 1 2 0 3 2 0 := by decide
74theorem e_120321 : m2Num 1 2 0 3 2 1 = 8 * explicitZ 1 2 0 3 2 1 := by decide
75theorem e_120322 : m2Num 1 2 0 3 2 2 = 8 * explicitZ 1 2 0 3 2 2 := by decide
76theorem e_120323 : m2Num 1 2 0 3 2 3 = 8 * explicitZ 1 2 0 3 2 3 := by decide
77theorem e_120330 : m2Num 1 2 0 3 3 0 = 8 * explicitZ 1 2 0 3 3 0 := by decide
78theorem e_120331 : m2Num 1 2 0 3 3 1 = 8 * explicitZ 1 2 0 3 3 1 := by decide
79theorem e_120332 : m2Num 1 2 0 3 3 2 = 8 * explicitZ 1 2 0 3 3 2 := by decide
80theorem e_120333 : m2Num 1 2 0 3 3 3 = 8 * explicitZ 1 2 0 3 3 3 := by decide
81theorem e_121000 : m2Num 1 2 1 0 0 0 = 8 * explicitZ 1 2 1 0 0 0 := by decide
82theorem e_121001 : m2Num 1 2 1 0 0 1 = 8 * explicitZ 1 2 1 0 0 1 := by decide
83theorem e_121002 : m2Num 1 2 1 0 0 2 = 8 * explicitZ 1 2 1 0 0 2 := by decide
84theorem e_121003 : m2Num 1 2 1 0 0 3 = 8 * explicitZ 1 2 1 0 0 3 := by decide
85theorem e_121010 : m2Num 1 2 1 0 1 0 = 8 * explicitZ 1 2 1 0 1 0 := by decide
86theorem e_121011 : m2Num 1 2 1 0 1 1 = 8 * explicitZ 1 2 1 0 1 1 := by decide
87theorem e_121012 : m2Num 1 2 1 0 1 2 = 8 * explicitZ 1 2 1 0 1 2 := by decide
88theorem e_121013 : m2Num 1 2 1 0 1 3 = 8 * explicitZ 1 2 1 0 1 3 := by decide
89theorem e_121020 : m2Num 1 2 1 0 2 0 = 8 * explicitZ 1 2 1 0 2 0 := by decide
90theorem e_121021 : m2Num 1 2 1 0 2 1 = 8 * explicitZ 1 2 1 0 2 1 := by decide
91theorem e_121022 : m2Num 1 2 1 0 2 2 = 8 * explicitZ 1 2 1 0 2 2 := by decide
92theorem e_121023 : m2Num 1 2 1 0 2 3 = 8 * explicitZ 1 2 1 0 2 3 := by decide
93theorem e_121030 : m2Num 1 2 1 0 3 0 = 8 * explicitZ 1 2 1 0 3 0 := by decide
94theorem e_121031 : m2Num 1 2 1 0 3 1 = 8 * explicitZ 1 2 1 0 3 1 := by decide
95theorem e_121032 : m2Num 1 2 1 0 3 2 = 8 * explicitZ 1 2 1 0 3 2 := by decide
96theorem e_121033 : m2Num 1 2 1 0 3 3 = 8 * explicitZ 1 2 1 0 3 3 := by decide
97theorem e_121100 : m2Num 1 2 1 1 0 0 = 8 * explicitZ 1 2 1 1 0 0 := by decide
98theorem e_121101 : m2Num 1 2 1 1 0 1 = 8 * explicitZ 1 2 1 1 0 1 := by decide
99theorem e_121102 : m2Num 1 2 1 1 0 2 = 8 * explicitZ 1 2 1 1 0 2 := by decide
100theorem e_121103 : m2Num 1 2 1 1 0 3 = 8 * explicitZ 1 2 1 1 0 3 := by decide
101theorem e_121110 : m2Num 1 2 1 1 1 0 = 8 * explicitZ 1 2 1 1 1 0 := by decide
102theorem e_121111 : m2Num 1 2 1 1 1 1 = 8 * explicitZ 1 2 1 1 1 1 := by decide
103theorem e_121112 : m2Num 1 2 1 1 1 2 = 8 * explicitZ 1 2 1 1 1 2 := by decide
104theorem e_121113 : m2Num 1 2 1 1 1 3 = 8 * explicitZ 1 2 1 1 1 3 := by decide
105theorem e_121120 : m2Num 1 2 1 1 2 0 = 8 * explicitZ 1 2 1 1 2 0 := by decide
106theorem e_121121 : m2Num 1 2 1 1 2 1 = 8 * explicitZ 1 2 1 1 2 1 := by decide
107theorem e_121122 : m2Num 1 2 1 1 2 2 = 8 * explicitZ 1 2 1 1 2 2 := by decide
108theorem e_121123 : m2Num 1 2 1 1 2 3 = 8 * explicitZ 1 2 1 1 2 3 := by decide
109theorem e_121130 : m2Num 1 2 1 1 3 0 = 8 * explicitZ 1 2 1 1 3 0 := by decide
110theorem e_121131 : m2Num 1 2 1 1 3 1 = 8 * explicitZ 1 2 1 1 3 1 := by decide
111theorem e_121132 : m2Num 1 2 1 1 3 2 = 8 * explicitZ 1 2 1 1 3 2 := by decide
112theorem e_121133 : m2Num 1 2 1 1 3 3 = 8 * explicitZ 1 2 1 1 3 3 := by decide
113theorem e_121200 : m2Num 1 2 1 2 0 0 = 8 * explicitZ 1 2 1 2 0 0 := by decide
114theorem e_121201 : m2Num 1 2 1 2 0 1 = 8 * explicitZ 1 2 1 2 0 1 := by decide
115theorem e_121202 : m2Num 1 2 1 2 0 2 = 8 * explicitZ 1 2 1 2 0 2 := by decide
116theorem e_121203 : m2Num 1 2 1 2 0 3 = 8 * explicitZ 1 2 1 2 0 3 := by decide
117theorem e_121210 : m2Num 1 2 1 2 1 0 = 8 * explicitZ 1 2 1 2 1 0 := by decide
118theorem e_121211 : m2Num 1 2 1 2 1 1 = 8 * explicitZ 1 2 1 2 1 1 := by decide
119theorem e_121212 : m2Num 1 2 1 2 1 2 = 8 * explicitZ 1 2 1 2 1 2 := by decide
120theorem e_121213 : m2Num 1 2 1 2 1 3 = 8 * explicitZ 1 2 1 2 1 3 := by decide
121theorem e_121220 : m2Num 1 2 1 2 2 0 = 8 * explicitZ 1 2 1 2 2 0 := by decide
122theorem e_121221 : m2Num 1 2 1 2 2 1 = 8 * explicitZ 1 2 1 2 2 1 := by decide
123theorem e_121222 : m2Num 1 2 1 2 2 2 = 8 * explicitZ 1 2 1 2 2 2 := by decide
124theorem e_121223 : m2Num 1 2 1 2 2 3 = 8 * explicitZ 1 2 1 2 2 3 := by decide
125theorem e_121230 : m2Num 1 2 1 2 3 0 = 8 * explicitZ 1 2 1 2 3 0 := by decide
126theorem e_121231 : m2Num 1 2 1 2 3 1 = 8 * explicitZ 1 2 1 2 3 1 := by decide
127theorem e_121232 : m2Num 1 2 1 2 3 2 = 8 * explicitZ 1 2 1 2 3 2 := by decide
128theorem e_121233 : m2Num 1 2 1 2 3 3 = 8 * explicitZ 1 2 1 2 3 3 := by decide
129theorem e_121300 : m2Num 1 2 1 3 0 0 = 8 * explicitZ 1 2 1 3 0 0 := by decide
130theorem e_121301 : m2Num 1 2 1 3 0 1 = 8 * explicitZ 1 2 1 3 0 1 := by decide
131theorem e_121302 : m2Num 1 2 1 3 0 2 = 8 * explicitZ 1 2 1 3 0 2 := by decide
132theorem e_121303 : m2Num 1 2 1 3 0 3 = 8 * explicitZ 1 2 1 3 0 3 := by decide
133theorem e_121310 : m2Num 1 2 1 3 1 0 = 8 * explicitZ 1 2 1 3 1 0 := by decide
134theorem e_121311 : m2Num 1 2 1 3 1 1 = 8 * explicitZ 1 2 1 3 1 1 := by decide
135theorem e_121312 : m2Num 1 2 1 3 1 2 = 8 * explicitZ 1 2 1 3 1 2 := by decide
136theorem e_121313 : m2Num 1 2 1 3 1 3 = 8 * explicitZ 1 2 1 3 1 3 := by decide
137theorem e_121320 : m2Num 1 2 1 3 2 0 = 8 * explicitZ 1 2 1 3 2 0 := by decide
138theorem e_121321 : m2Num 1 2 1 3 2 1 = 8 * explicitZ 1 2 1 3 2 1 := by decide
139theorem e_121322 : m2Num 1 2 1 3 2 2 = 8 * explicitZ 1 2 1 3 2 2 := by decide
140theorem e_121323 : m2Num 1 2 1 3 2 3 = 8 * explicitZ 1 2 1 3 2 3 := by decide
141theorem e_121330 : m2Num 1 2 1 3 3 0 = 8 * explicitZ 1 2 1 3 3 0 := by decide
142theorem e_121331 : m2Num 1 2 1 3 3 1 = 8 * explicitZ 1 2 1 3 3 1 := by decide
143theorem e_121332 : m2Num 1 2 1 3 3 2 = 8 * explicitZ 1 2 1 3 3 2 := by decide
144theorem e_121333 : m2Num 1 2 1 3 3 3 = 8 * explicitZ 1 2 1 3 3 3 := by decide
145theorem e_122000 : m2Num 1 2 2 0 0 0 = 8 * explicitZ 1 2 2 0 0 0 := by decide
146theorem e_122001 : m2Num 1 2 2 0 0 1 = 8 * explicitZ 1 2 2 0 0 1 := by decide
147theorem e_122002 : m2Num 1 2 2 0 0 2 = 8 * explicitZ 1 2 2 0 0 2 := by decide
148theorem e_122003 : m2Num 1 2 2 0 0 3 = 8 * explicitZ 1 2 2 0 0 3 := by decide
149theorem e_122010 : m2Num 1 2 2 0 1 0 = 8 * explicitZ 1 2 2 0 1 0 := by decide
150theorem e_122011 : m2Num 1 2 2 0 1 1 = 8 * explicitZ 1 2 2 0 1 1 := by decide
151theorem e_122012 : m2Num 1 2 2 0 1 2 = 8 * explicitZ 1 2 2 0 1 2 := by decide
152theorem e_122013 : m2Num 1 2 2 0 1 3 = 8 * explicitZ 1 2 2 0 1 3 := by decide
153theorem e_122020 : m2Num 1 2 2 0 2 0 = 8 * explicitZ 1 2 2 0 2 0 := by decide
154theorem e_122021 : m2Num 1 2 2 0 2 1 = 8 * explicitZ 1 2 2 0 2 1 := by decide
155theorem e_122022 : m2Num 1 2 2 0 2 2 = 8 * explicitZ 1 2 2 0 2 2 := by decide
156theorem e_122023 : m2Num 1 2 2 0 2 3 = 8 * explicitZ 1 2 2 0 2 3 := by decide
157theorem e_122030 : m2Num 1 2 2 0 3 0 = 8 * explicitZ 1 2 2 0 3 0 := by decide
158theorem e_122031 : m2Num 1 2 2 0 3 1 = 8 * explicitZ 1 2 2 0 3 1 := by decide
159theorem e_122032 : m2Num 1 2 2 0 3 2 = 8 * explicitZ 1 2 2 0 3 2 := by decide
160theorem e_122033 : m2Num 1 2 2 0 3 3 = 8 * explicitZ 1 2 2 0 3 3 := by decide
161theorem e_122100 : m2Num 1 2 2 1 0 0 = 8 * explicitZ 1 2 2 1 0 0 := by decide
162theorem e_122101 : m2Num 1 2 2 1 0 1 = 8 * explicitZ 1 2 2 1 0 1 := by decide
163theorem e_122102 : m2Num 1 2 2 1 0 2 = 8 * explicitZ 1 2 2 1 0 2 := by decide
164theorem e_122103 : m2Num 1 2 2 1 0 3 = 8 * explicitZ 1 2 2 1 0 3 := by decide
165theorem e_122110 : m2Num 1 2 2 1 1 0 = 8 * explicitZ 1 2 2 1 1 0 := by decide
166theorem e_122111 : m2Num 1 2 2 1 1 1 = 8 * explicitZ 1 2 2 1 1 1 := by decide
167theorem e_122112 : m2Num 1 2 2 1 1 2 = 8 * explicitZ 1 2 2 1 1 2 := by decide
168theorem e_122113 : m2Num 1 2 2 1 1 3 = 8 * explicitZ 1 2 2 1 1 3 := by decide
169theorem e_122120 : m2Num 1 2 2 1 2 0 = 8 * explicitZ 1 2 2 1 2 0 := by decide
170theorem e_122121 : m2Num 1 2 2 1 2 1 = 8 * explicitZ 1 2 2 1 2 1 := by decide
171theorem e_122122 : m2Num 1 2 2 1 2 2 = 8 * explicitZ 1 2 2 1 2 2 := by decide
172theorem e_122123 : m2Num 1 2 2 1 2 3 = 8 * explicitZ 1 2 2 1 2 3 := by decide
173theorem e_122130 : m2Num 1 2 2 1 3 0 = 8 * explicitZ 1 2 2 1 3 0 := by decide
174theorem e_122131 : m2Num 1 2 2 1 3 1 = 8 * explicitZ 1 2 2 1 3 1 := by decide
175theorem e_122132 : m2Num 1 2 2 1 3 2 = 8 * explicitZ 1 2 2 1 3 2 := by decide
176theorem e_122133 : m2Num 1 2 2 1 3 3 = 8 * explicitZ 1 2 2 1 3 3 := by decide
177theorem e_122200 : m2Num 1 2 2 2 0 0 = 8 * explicitZ 1 2 2 2 0 0 := by decide
178theorem e_122201 : m2Num 1 2 2 2 0 1 = 8 * explicitZ 1 2 2 2 0 1 := by decide
179theorem e_122202 : m2Num 1 2 2 2 0 2 = 8 * explicitZ 1 2 2 2 0 2 := by decide
180theorem e_122203 : m2Num 1 2 2 2 0 3 = 8 * explicitZ 1 2 2 2 0 3 := by decide
181theorem e_122210 : m2Num 1 2 2 2 1 0 = 8 * explicitZ 1 2 2 2 1 0 := by decide
182theorem e_122211 : m2Num 1 2 2 2 1 1 = 8 * explicitZ 1 2 2 2 1 1 := by decide
183theorem e_122212 : m2Num 1 2 2 2 1 2 = 8 * explicitZ 1 2 2 2 1 2 := by decide
184theorem e_122213 : m2Num 1 2 2 2 1 3 = 8 * explicitZ 1 2 2 2 1 3 := by decide
185theorem e_122220 : m2Num 1 2 2 2 2 0 = 8 * explicitZ 1 2 2 2 2 0 := by decide
186theorem e_122221 : m2Num 1 2 2 2 2 1 = 8 * explicitZ 1 2 2 2 2 1 := by decide
187theorem e_122222 : m2Num 1 2 2 2 2 2 = 8 * explicitZ 1 2 2 2 2 2 := by decide
188theorem e_122223 : m2Num 1 2 2 2 2 3 = 8 * explicitZ 1 2 2 2 2 3 := by decide
189theorem e_122230 : m2Num 1 2 2 2 3 0 = 8 * explicitZ 1 2 2 2 3 0 := by decide
190theorem e_122231 : m2Num 1 2 2 2 3 1 = 8 * explicitZ 1 2 2 2 3 1 := by decide
191theorem e_122232 : m2Num 1 2 2 2 3 2 = 8 * explicitZ 1 2 2 2 3 2 := by decide
192theorem e_122233 : m2Num 1 2 2 2 3 3 = 8 * explicitZ 1 2 2 2 3 3 := by decide
193theorem e_122300 : m2Num 1 2 2 3 0 0 = 8 * explicitZ 1 2 2 3 0 0 := by decide
194theorem e_122301 : m2Num 1 2 2 3 0 1 = 8 * explicitZ 1 2 2 3 0 1 := by decide
195theorem e_122302 : m2Num 1 2 2 3 0 2 = 8 * explicitZ 1 2 2 3 0 2 := by decide
196theorem e_122303 : m2Num 1 2 2 3 0 3 = 8 * explicitZ 1 2 2 3 0 3 := by decide
197theorem e_122310 : m2Num 1 2 2 3 1 0 = 8 * explicitZ 1 2 2 3 1 0 := by decide
198theorem e_122311 : m2Num 1 2 2 3 1 1 = 8 * explicitZ 1 2 2 3 1 1 := by decide
199theorem e_122312 : m2Num 1 2 2 3 1 2 = 8 * explicitZ 1 2 2 3 1 2 := by decide
200theorem e_122313 : m2Num 1 2 2 3 1 3 = 8 * explicitZ 1 2 2 3 1 3 := by decide
201theorem e_122320 : m2Num 1 2 2 3 2 0 = 8 * explicitZ 1 2 2 3 2 0 := by decide
202theorem e_122321 : m2Num 1 2 2 3 2 1 = 8 * explicitZ 1 2 2 3 2 1 := by decide
203theorem e_122322 : m2Num 1 2 2 3 2 2 = 8 * explicitZ 1 2 2 3 2 2 := by decide
204theorem e_122323 : m2Num 1 2 2 3 2 3 = 8 * explicitZ 1 2 2 3 2 3 := by decide
205theorem e_122330 : m2Num 1 2 2 3 3 0 = 8 * explicitZ 1 2 2 3 3 0 := by decide
206theorem e_122331 : m2Num 1 2 2 3 3 1 = 8 * explicitZ 1 2 2 3 3 1 := by decide
207theorem e_122332 : m2Num 1 2 2 3 3 2 = 8 * explicitZ 1 2 2 3 3 2 := by decide
208theorem e_122333 : m2Num 1 2 2 3 3 3 = 8 * explicitZ 1 2 2 3 3 3 := by decide
209theorem e_123000 : m2Num 1 2 3 0 0 0 = 8 * explicitZ 1 2 3 0 0 0 := by decide
210theorem e_123001 : m2Num 1 2 3 0 0 1 = 8 * explicitZ 1 2 3 0 0 1 := by decide
211theorem e_123002 : m2Num 1 2 3 0 0 2 = 8 * explicitZ 1 2 3 0 0 2 := by decide
212theorem e_123003 : m2Num 1 2 3 0 0 3 = 8 * explicitZ 1 2 3 0 0 3 := by decide
213theorem e_123010 : m2Num 1 2 3 0 1 0 = 8 * explicitZ 1 2 3 0 1 0 := by decide
214theorem e_123011 : m2Num 1 2 3 0 1 1 = 8 * explicitZ 1 2 3 0 1 1 := by decide
215theorem e_123012 : m2Num 1 2 3 0 1 2 = 8 * explicitZ 1 2 3 0 1 2 := by decide
216theorem e_123013 : m2Num 1 2 3 0 1 3 = 8 * explicitZ 1 2 3 0 1 3 := by decide
217theorem e_123020 : m2Num 1 2 3 0 2 0 = 8 * explicitZ 1 2 3 0 2 0 := by decide
218theorem e_123021 : m2Num 1 2 3 0 2 1 = 8 * explicitZ 1 2 3 0 2 1 := by decide
219theorem e_123022 : m2Num 1 2 3 0 2 2 = 8 * explicitZ 1 2 3 0 2 2 := by decide
220theorem e_123023 : m2Num 1 2 3 0 2 3 = 8 * explicitZ 1 2 3 0 2 3 := by decide
221theorem e_123030 : m2Num 1 2 3 0 3 0 = 8 * explicitZ 1 2 3 0 3 0 := by decide
222theorem e_123031 : m2Num 1 2 3 0 3 1 = 8 * explicitZ 1 2 3 0 3 1 := by decide
223theorem e_123032 : m2Num 1 2 3 0 3 2 = 8 * explicitZ 1 2 3 0 3 2 := by decide
224theorem e_123033 : m2Num 1 2 3 0 3 3 = 8 * explicitZ 1 2 3 0 3 3 := by decide
225theorem e_123100 : m2Num 1 2 3 1 0 0 = 8 * explicitZ 1 2 3 1 0 0 := by decide
226theorem e_123101 : m2Num 1 2 3 1 0 1 = 8 * explicitZ 1 2 3 1 0 1 := by decide
227theorem e_123102 : m2Num 1 2 3 1 0 2 = 8 * explicitZ 1 2 3 1 0 2 := by decide
228theorem e_123103 : m2Num 1 2 3 1 0 3 = 8 * explicitZ 1 2 3 1 0 3 := by decide
229theorem e_123110 : m2Num 1 2 3 1 1 0 = 8 * explicitZ 1 2 3 1 1 0 := by decide
230theorem e_123111 : m2Num 1 2 3 1 1 1 = 8 * explicitZ 1 2 3 1 1 1 := by decide
231theorem e_123112 : m2Num 1 2 3 1 1 2 = 8 * explicitZ 1 2 3 1 1 2 := by decide
232theorem e_123113 : m2Num 1 2 3 1 1 3 = 8 * explicitZ 1 2 3 1 1 3 := by decide
233theorem e_123120 : m2Num 1 2 3 1 2 0 = 8 * explicitZ 1 2 3 1 2 0 := by decide
234theorem e_123121 : m2Num 1 2 3 1 2 1 = 8 * explicitZ 1 2 3 1 2 1 := by decide
235theorem e_123122 : m2Num 1 2 3 1 2 2 = 8 * explicitZ 1 2 3 1 2 2 := by decide
236theorem e_123123 : m2Num 1 2 3 1 2 3 = 8 * explicitZ 1 2 3 1 2 3 := by decide
237theorem e_123130 : m2Num 1 2 3 1 3 0 = 8 * explicitZ 1 2 3 1 3 0 := by decide
238theorem e_123131 : m2Num 1 2 3 1 3 1 = 8 * explicitZ 1 2 3 1 3 1 := by decide
239theorem e_123132 : m2Num 1 2 3 1 3 2 = 8 * explicitZ 1 2 3 1 3 2 := by decide
240theorem e_123133 : m2Num 1 2 3 1 3 3 = 8 * explicitZ 1 2 3 1 3 3 := by decide
241theorem e_123200 : m2Num 1 2 3 2 0 0 = 8 * explicitZ 1 2 3 2 0 0 := by decide
242theorem e_123201 : m2Num 1 2 3 2 0 1 = 8 * explicitZ 1 2 3 2 0 1 := by decide
243theorem e_123202 : m2Num 1 2 3 2 0 2 = 8 * explicitZ 1 2 3 2 0 2 := by decide
244theorem e_123203 : m2Num 1 2 3 2 0 3 = 8 * explicitZ 1 2 3 2 0 3 := by decide
245theorem e_123210 : m2Num 1 2 3 2 1 0 = 8 * explicitZ 1 2 3 2 1 0 := by decide
246theorem e_123211 : m2Num 1 2 3 2 1 1 = 8 * explicitZ 1 2 3 2 1 1 := by decide
247theorem e_123212 : m2Num 1 2 3 2 1 2 = 8 * explicitZ 1 2 3 2 1 2 := by decide
248theorem e_123213 : m2Num 1 2 3 2 1 3 = 8 * explicitZ 1 2 3 2 1 3 := by decide
249theorem e_123220 : m2Num 1 2 3 2 2 0 = 8 * explicitZ 1 2 3 2 2 0 := by decide
250theorem e_123221 : m2Num 1 2 3 2 2 1 = 8 * explicitZ 1 2 3 2 2 1 := by decide
251theorem e_123222 : m2Num 1 2 3 2 2 2 = 8 * explicitZ 1 2 3 2 2 2 := by decide
252theorem e_123223 : m2Num 1 2 3 2 2 3 = 8 * explicitZ 1 2 3 2 2 3 := by decide
253theorem e_123230 : m2Num 1 2 3 2 3 0 = 8 * explicitZ 1 2 3 2 3 0 := by decide
254theorem e_123231 : m2Num 1 2 3 2 3 1 = 8 * explicitZ 1 2 3 2 3 1 := by decide
255theorem e_123232 : m2Num 1 2 3 2 3 2 = 8 * explicitZ 1 2 3 2 3 2 := by decide
256theorem e_123233 : m2Num 1 2 3 2 3 3 = 8 * explicitZ 1 2 3 2 3 3 := by decide
257theorem e_123300 : m2Num 1 2 3 3 0 0 = 8 * explicitZ 1 2 3 3 0 0 := by decide
258theorem e_123301 : m2Num 1 2 3 3 0 1 = 8 * explicitZ 1 2 3 3 0 1 := by decide
259theorem e_123302 : m2Num 1 2 3 3 0 2 = 8 * explicitZ 1 2 3 3 0 2 := by decide
260theorem e_123303 : m2Num 1 2 3 3 0 3 = 8 * explicitZ 1 2 3 3 0 3 := by decide
261theorem e_123310 : m2Num 1 2 3 3 1 0 = 8 * explicitZ 1 2 3 3 1 0 := by decide
262theorem e_123311 : m2Num 1 2 3 3 1 1 = 8 * explicitZ 1 2 3 3 1 1 := by decide
263theorem e_123312 : m2Num 1 2 3 3 1 2 = 8 * explicitZ 1 2 3 3 1 2 := by decide
264theorem e_123313 : m2Num 1 2 3 3 1 3 = 8 * explicitZ 1 2 3 3 1 3 := by decide
265theorem e_123320 : m2Num 1 2 3 3 2 0 = 8 * explicitZ 1 2 3 3 2 0 := by decide
266theorem e_123321 : m2Num 1 2 3 3 2 1 = 8 * explicitZ 1 2 3 3 2 1 := by decide
267theorem e_123322 : m2Num 1 2 3 3 2 2 = 8 * explicitZ 1 2 3 3 2 2 := by decide
268theorem e_123323 : m2Num 1 2 3 3 2 3 = 8 * explicitZ 1 2 3 3 2 3 := by decide
269theorem e_123330 : m2Num 1 2 3 3 3 0 = 8 * explicitZ 1 2 3 3 3 0 := by decide
270theorem e_123331 : m2Num 1 2 3 3 3 1 = 8 * explicitZ 1 2 3 3 3 1 := by decide
271theorem e_123332 : m2Num 1 2 3 3 3 2 = 8 * explicitZ 1 2 3 3 3 2 := by decide
272theorem e_123333 : m2Num 1 2 3 3 3 3 = 8 * explicitZ 1 2 3 3 3 3 := by decide
273
274end M2NumChunk06
275end ReggeExactMidpointM2TTIdentity4D
276end Analysis
277end Gravity
278end IndisputableMonolith
279