IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DM2NumChunk02
IndisputableMonolith/Gravity/Analysis/ReggeExactMidpointM2TTIdentity4DM2NumChunk02.lean · 279 lines · 256 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DKernelCert
3
4/-! m2Num = 8·explicitZ, chunk 2 (256 kernel decides). -/
5
6namespace IndisputableMonolith
7namespace Gravity
8namespace Analysis
9namespace ReggeExactMidpointM2TTIdentity4D
10namespace M2NumChunk02
11
12open KernelCert
13
14set_option maxRecDepth 100000
15set_option maxHeartbeats 200000000
16
17theorem e_020000 : m2Num 0 2 0 0 0 0 = 8 * explicitZ 0 2 0 0 0 0 := by decide
18theorem e_020001 : m2Num 0 2 0 0 0 1 = 8 * explicitZ 0 2 0 0 0 1 := by decide
19theorem e_020002 : m2Num 0 2 0 0 0 2 = 8 * explicitZ 0 2 0 0 0 2 := by decide
20theorem e_020003 : m2Num 0 2 0 0 0 3 = 8 * explicitZ 0 2 0 0 0 3 := by decide
21theorem e_020010 : m2Num 0 2 0 0 1 0 = 8 * explicitZ 0 2 0 0 1 0 := by decide
22theorem e_020011 : m2Num 0 2 0 0 1 1 = 8 * explicitZ 0 2 0 0 1 1 := by decide
23theorem e_020012 : m2Num 0 2 0 0 1 2 = 8 * explicitZ 0 2 0 0 1 2 := by decide
24theorem e_020013 : m2Num 0 2 0 0 1 3 = 8 * explicitZ 0 2 0 0 1 3 := by decide
25theorem e_020020 : m2Num 0 2 0 0 2 0 = 8 * explicitZ 0 2 0 0 2 0 := by decide
26theorem e_020021 : m2Num 0 2 0 0 2 1 = 8 * explicitZ 0 2 0 0 2 1 := by decide
27theorem e_020022 : m2Num 0 2 0 0 2 2 = 8 * explicitZ 0 2 0 0 2 2 := by decide
28theorem e_020023 : m2Num 0 2 0 0 2 3 = 8 * explicitZ 0 2 0 0 2 3 := by decide
29theorem e_020030 : m2Num 0 2 0 0 3 0 = 8 * explicitZ 0 2 0 0 3 0 := by decide
30theorem e_020031 : m2Num 0 2 0 0 3 1 = 8 * explicitZ 0 2 0 0 3 1 := by decide
31theorem e_020032 : m2Num 0 2 0 0 3 2 = 8 * explicitZ 0 2 0 0 3 2 := by decide
32theorem e_020033 : m2Num 0 2 0 0 3 3 = 8 * explicitZ 0 2 0 0 3 3 := by decide
33theorem e_020100 : m2Num 0 2 0 1 0 0 = 8 * explicitZ 0 2 0 1 0 0 := by decide
34theorem e_020101 : m2Num 0 2 0 1 0 1 = 8 * explicitZ 0 2 0 1 0 1 := by decide
35theorem e_020102 : m2Num 0 2 0 1 0 2 = 8 * explicitZ 0 2 0 1 0 2 := by decide
36theorem e_020103 : m2Num 0 2 0 1 0 3 = 8 * explicitZ 0 2 0 1 0 3 := by decide
37theorem e_020110 : m2Num 0 2 0 1 1 0 = 8 * explicitZ 0 2 0 1 1 0 := by decide
38theorem e_020111 : m2Num 0 2 0 1 1 1 = 8 * explicitZ 0 2 0 1 1 1 := by decide
39theorem e_020112 : m2Num 0 2 0 1 1 2 = 8 * explicitZ 0 2 0 1 1 2 := by decide
40theorem e_020113 : m2Num 0 2 0 1 1 3 = 8 * explicitZ 0 2 0 1 1 3 := by decide
41theorem e_020120 : m2Num 0 2 0 1 2 0 = 8 * explicitZ 0 2 0 1 2 0 := by decide
42theorem e_020121 : m2Num 0 2 0 1 2 1 = 8 * explicitZ 0 2 0 1 2 1 := by decide
43theorem e_020122 : m2Num 0 2 0 1 2 2 = 8 * explicitZ 0 2 0 1 2 2 := by decide
44theorem e_020123 : m2Num 0 2 0 1 2 3 = 8 * explicitZ 0 2 0 1 2 3 := by decide
45theorem e_020130 : m2Num 0 2 0 1 3 0 = 8 * explicitZ 0 2 0 1 3 0 := by decide
46theorem e_020131 : m2Num 0 2 0 1 3 1 = 8 * explicitZ 0 2 0 1 3 1 := by decide
47theorem e_020132 : m2Num 0 2 0 1 3 2 = 8 * explicitZ 0 2 0 1 3 2 := by decide
48theorem e_020133 : m2Num 0 2 0 1 3 3 = 8 * explicitZ 0 2 0 1 3 3 := by decide
49theorem e_020200 : m2Num 0 2 0 2 0 0 = 8 * explicitZ 0 2 0 2 0 0 := by decide
50theorem e_020201 : m2Num 0 2 0 2 0 1 = 8 * explicitZ 0 2 0 2 0 1 := by decide
51theorem e_020202 : m2Num 0 2 0 2 0 2 = 8 * explicitZ 0 2 0 2 0 2 := by decide
52theorem e_020203 : m2Num 0 2 0 2 0 3 = 8 * explicitZ 0 2 0 2 0 3 := by decide
53theorem e_020210 : m2Num 0 2 0 2 1 0 = 8 * explicitZ 0 2 0 2 1 0 := by decide
54theorem e_020211 : m2Num 0 2 0 2 1 1 = 8 * explicitZ 0 2 0 2 1 1 := by decide
55theorem e_020212 : m2Num 0 2 0 2 1 2 = 8 * explicitZ 0 2 0 2 1 2 := by decide
56theorem e_020213 : m2Num 0 2 0 2 1 3 = 8 * explicitZ 0 2 0 2 1 3 := by decide
57theorem e_020220 : m2Num 0 2 0 2 2 0 = 8 * explicitZ 0 2 0 2 2 0 := by decide
58theorem e_020221 : m2Num 0 2 0 2 2 1 = 8 * explicitZ 0 2 0 2 2 1 := by decide
59theorem e_020222 : m2Num 0 2 0 2 2 2 = 8 * explicitZ 0 2 0 2 2 2 := by decide
60theorem e_020223 : m2Num 0 2 0 2 2 3 = 8 * explicitZ 0 2 0 2 2 3 := by decide
61theorem e_020230 : m2Num 0 2 0 2 3 0 = 8 * explicitZ 0 2 0 2 3 0 := by decide
62theorem e_020231 : m2Num 0 2 0 2 3 1 = 8 * explicitZ 0 2 0 2 3 1 := by decide
63theorem e_020232 : m2Num 0 2 0 2 3 2 = 8 * explicitZ 0 2 0 2 3 2 := by decide
64theorem e_020233 : m2Num 0 2 0 2 3 3 = 8 * explicitZ 0 2 0 2 3 3 := by decide
65theorem e_020300 : m2Num 0 2 0 3 0 0 = 8 * explicitZ 0 2 0 3 0 0 := by decide
66theorem e_020301 : m2Num 0 2 0 3 0 1 = 8 * explicitZ 0 2 0 3 0 1 := by decide
67theorem e_020302 : m2Num 0 2 0 3 0 2 = 8 * explicitZ 0 2 0 3 0 2 := by decide
68theorem e_020303 : m2Num 0 2 0 3 0 3 = 8 * explicitZ 0 2 0 3 0 3 := by decide
69theorem e_020310 : m2Num 0 2 0 3 1 0 = 8 * explicitZ 0 2 0 3 1 0 := by decide
70theorem e_020311 : m2Num 0 2 0 3 1 1 = 8 * explicitZ 0 2 0 3 1 1 := by decide
71theorem e_020312 : m2Num 0 2 0 3 1 2 = 8 * explicitZ 0 2 0 3 1 2 := by decide
72theorem e_020313 : m2Num 0 2 0 3 1 3 = 8 * explicitZ 0 2 0 3 1 3 := by decide
73theorem e_020320 : m2Num 0 2 0 3 2 0 = 8 * explicitZ 0 2 0 3 2 0 := by decide
74theorem e_020321 : m2Num 0 2 0 3 2 1 = 8 * explicitZ 0 2 0 3 2 1 := by decide
75theorem e_020322 : m2Num 0 2 0 3 2 2 = 8 * explicitZ 0 2 0 3 2 2 := by decide
76theorem e_020323 : m2Num 0 2 0 3 2 3 = 8 * explicitZ 0 2 0 3 2 3 := by decide
77theorem e_020330 : m2Num 0 2 0 3 3 0 = 8 * explicitZ 0 2 0 3 3 0 := by decide
78theorem e_020331 : m2Num 0 2 0 3 3 1 = 8 * explicitZ 0 2 0 3 3 1 := by decide
79theorem e_020332 : m2Num 0 2 0 3 3 2 = 8 * explicitZ 0 2 0 3 3 2 := by decide
80theorem e_020333 : m2Num 0 2 0 3 3 3 = 8 * explicitZ 0 2 0 3 3 3 := by decide
81theorem e_021000 : m2Num 0 2 1 0 0 0 = 8 * explicitZ 0 2 1 0 0 0 := by decide
82theorem e_021001 : m2Num 0 2 1 0 0 1 = 8 * explicitZ 0 2 1 0 0 1 := by decide
83theorem e_021002 : m2Num 0 2 1 0 0 2 = 8 * explicitZ 0 2 1 0 0 2 := by decide
84theorem e_021003 : m2Num 0 2 1 0 0 3 = 8 * explicitZ 0 2 1 0 0 3 := by decide
85theorem e_021010 : m2Num 0 2 1 0 1 0 = 8 * explicitZ 0 2 1 0 1 0 := by decide
86theorem e_021011 : m2Num 0 2 1 0 1 1 = 8 * explicitZ 0 2 1 0 1 1 := by decide
87theorem e_021012 : m2Num 0 2 1 0 1 2 = 8 * explicitZ 0 2 1 0 1 2 := by decide
88theorem e_021013 : m2Num 0 2 1 0 1 3 = 8 * explicitZ 0 2 1 0 1 3 := by decide
89theorem e_021020 : m2Num 0 2 1 0 2 0 = 8 * explicitZ 0 2 1 0 2 0 := by decide
90theorem e_021021 : m2Num 0 2 1 0 2 1 = 8 * explicitZ 0 2 1 0 2 1 := by decide
91theorem e_021022 : m2Num 0 2 1 0 2 2 = 8 * explicitZ 0 2 1 0 2 2 := by decide
92theorem e_021023 : m2Num 0 2 1 0 2 3 = 8 * explicitZ 0 2 1 0 2 3 := by decide
93theorem e_021030 : m2Num 0 2 1 0 3 0 = 8 * explicitZ 0 2 1 0 3 0 := by decide
94theorem e_021031 : m2Num 0 2 1 0 3 1 = 8 * explicitZ 0 2 1 0 3 1 := by decide
95theorem e_021032 : m2Num 0 2 1 0 3 2 = 8 * explicitZ 0 2 1 0 3 2 := by decide
96theorem e_021033 : m2Num 0 2 1 0 3 3 = 8 * explicitZ 0 2 1 0 3 3 := by decide
97theorem e_021100 : m2Num 0 2 1 1 0 0 = 8 * explicitZ 0 2 1 1 0 0 := by decide
98theorem e_021101 : m2Num 0 2 1 1 0 1 = 8 * explicitZ 0 2 1 1 0 1 := by decide
99theorem e_021102 : m2Num 0 2 1 1 0 2 = 8 * explicitZ 0 2 1 1 0 2 := by decide
100theorem e_021103 : m2Num 0 2 1 1 0 3 = 8 * explicitZ 0 2 1 1 0 3 := by decide
101theorem e_021110 : m2Num 0 2 1 1 1 0 = 8 * explicitZ 0 2 1 1 1 0 := by decide
102theorem e_021111 : m2Num 0 2 1 1 1 1 = 8 * explicitZ 0 2 1 1 1 1 := by decide
103theorem e_021112 : m2Num 0 2 1 1 1 2 = 8 * explicitZ 0 2 1 1 1 2 := by decide
104theorem e_021113 : m2Num 0 2 1 1 1 3 = 8 * explicitZ 0 2 1 1 1 3 := by decide
105theorem e_021120 : m2Num 0 2 1 1 2 0 = 8 * explicitZ 0 2 1 1 2 0 := by decide
106theorem e_021121 : m2Num 0 2 1 1 2 1 = 8 * explicitZ 0 2 1 1 2 1 := by decide
107theorem e_021122 : m2Num 0 2 1 1 2 2 = 8 * explicitZ 0 2 1 1 2 2 := by decide
108theorem e_021123 : m2Num 0 2 1 1 2 3 = 8 * explicitZ 0 2 1 1 2 3 := by decide
109theorem e_021130 : m2Num 0 2 1 1 3 0 = 8 * explicitZ 0 2 1 1 3 0 := by decide
110theorem e_021131 : m2Num 0 2 1 1 3 1 = 8 * explicitZ 0 2 1 1 3 1 := by decide
111theorem e_021132 : m2Num 0 2 1 1 3 2 = 8 * explicitZ 0 2 1 1 3 2 := by decide
112theorem e_021133 : m2Num 0 2 1 1 3 3 = 8 * explicitZ 0 2 1 1 3 3 := by decide
113theorem e_021200 : m2Num 0 2 1 2 0 0 = 8 * explicitZ 0 2 1 2 0 0 := by decide
114theorem e_021201 : m2Num 0 2 1 2 0 1 = 8 * explicitZ 0 2 1 2 0 1 := by decide
115theorem e_021202 : m2Num 0 2 1 2 0 2 = 8 * explicitZ 0 2 1 2 0 2 := by decide
116theorem e_021203 : m2Num 0 2 1 2 0 3 = 8 * explicitZ 0 2 1 2 0 3 := by decide
117theorem e_021210 : m2Num 0 2 1 2 1 0 = 8 * explicitZ 0 2 1 2 1 0 := by decide
118theorem e_021211 : m2Num 0 2 1 2 1 1 = 8 * explicitZ 0 2 1 2 1 1 := by decide
119theorem e_021212 : m2Num 0 2 1 2 1 2 = 8 * explicitZ 0 2 1 2 1 2 := by decide
120theorem e_021213 : m2Num 0 2 1 2 1 3 = 8 * explicitZ 0 2 1 2 1 3 := by decide
121theorem e_021220 : m2Num 0 2 1 2 2 0 = 8 * explicitZ 0 2 1 2 2 0 := by decide
122theorem e_021221 : m2Num 0 2 1 2 2 1 = 8 * explicitZ 0 2 1 2 2 1 := by decide
123theorem e_021222 : m2Num 0 2 1 2 2 2 = 8 * explicitZ 0 2 1 2 2 2 := by decide
124theorem e_021223 : m2Num 0 2 1 2 2 3 = 8 * explicitZ 0 2 1 2 2 3 := by decide
125theorem e_021230 : m2Num 0 2 1 2 3 0 = 8 * explicitZ 0 2 1 2 3 0 := by decide
126theorem e_021231 : m2Num 0 2 1 2 3 1 = 8 * explicitZ 0 2 1 2 3 1 := by decide
127theorem e_021232 : m2Num 0 2 1 2 3 2 = 8 * explicitZ 0 2 1 2 3 2 := by decide
128theorem e_021233 : m2Num 0 2 1 2 3 3 = 8 * explicitZ 0 2 1 2 3 3 := by decide
129theorem e_021300 : m2Num 0 2 1 3 0 0 = 8 * explicitZ 0 2 1 3 0 0 := by decide
130theorem e_021301 : m2Num 0 2 1 3 0 1 = 8 * explicitZ 0 2 1 3 0 1 := by decide
131theorem e_021302 : m2Num 0 2 1 3 0 2 = 8 * explicitZ 0 2 1 3 0 2 := by decide
132theorem e_021303 : m2Num 0 2 1 3 0 3 = 8 * explicitZ 0 2 1 3 0 3 := by decide
133theorem e_021310 : m2Num 0 2 1 3 1 0 = 8 * explicitZ 0 2 1 3 1 0 := by decide
134theorem e_021311 : m2Num 0 2 1 3 1 1 = 8 * explicitZ 0 2 1 3 1 1 := by decide
135theorem e_021312 : m2Num 0 2 1 3 1 2 = 8 * explicitZ 0 2 1 3 1 2 := by decide
136theorem e_021313 : m2Num 0 2 1 3 1 3 = 8 * explicitZ 0 2 1 3 1 3 := by decide
137theorem e_021320 : m2Num 0 2 1 3 2 0 = 8 * explicitZ 0 2 1 3 2 0 := by decide
138theorem e_021321 : m2Num 0 2 1 3 2 1 = 8 * explicitZ 0 2 1 3 2 1 := by decide
139theorem e_021322 : m2Num 0 2 1 3 2 2 = 8 * explicitZ 0 2 1 3 2 2 := by decide
140theorem e_021323 : m2Num 0 2 1 3 2 3 = 8 * explicitZ 0 2 1 3 2 3 := by decide
141theorem e_021330 : m2Num 0 2 1 3 3 0 = 8 * explicitZ 0 2 1 3 3 0 := by decide
142theorem e_021331 : m2Num 0 2 1 3 3 1 = 8 * explicitZ 0 2 1 3 3 1 := by decide
143theorem e_021332 : m2Num 0 2 1 3 3 2 = 8 * explicitZ 0 2 1 3 3 2 := by decide
144theorem e_021333 : m2Num 0 2 1 3 3 3 = 8 * explicitZ 0 2 1 3 3 3 := by decide
145theorem e_022000 : m2Num 0 2 2 0 0 0 = 8 * explicitZ 0 2 2 0 0 0 := by decide
146theorem e_022001 : m2Num 0 2 2 0 0 1 = 8 * explicitZ 0 2 2 0 0 1 := by decide
147theorem e_022002 : m2Num 0 2 2 0 0 2 = 8 * explicitZ 0 2 2 0 0 2 := by decide
148theorem e_022003 : m2Num 0 2 2 0 0 3 = 8 * explicitZ 0 2 2 0 0 3 := by decide
149theorem e_022010 : m2Num 0 2 2 0 1 0 = 8 * explicitZ 0 2 2 0 1 0 := by decide
150theorem e_022011 : m2Num 0 2 2 0 1 1 = 8 * explicitZ 0 2 2 0 1 1 := by decide
151theorem e_022012 : m2Num 0 2 2 0 1 2 = 8 * explicitZ 0 2 2 0 1 2 := by decide
152theorem e_022013 : m2Num 0 2 2 0 1 3 = 8 * explicitZ 0 2 2 0 1 3 := by decide
153theorem e_022020 : m2Num 0 2 2 0 2 0 = 8 * explicitZ 0 2 2 0 2 0 := by decide
154theorem e_022021 : m2Num 0 2 2 0 2 1 = 8 * explicitZ 0 2 2 0 2 1 := by decide
155theorem e_022022 : m2Num 0 2 2 0 2 2 = 8 * explicitZ 0 2 2 0 2 2 := by decide
156theorem e_022023 : m2Num 0 2 2 0 2 3 = 8 * explicitZ 0 2 2 0 2 3 := by decide
157theorem e_022030 : m2Num 0 2 2 0 3 0 = 8 * explicitZ 0 2 2 0 3 0 := by decide
158theorem e_022031 : m2Num 0 2 2 0 3 1 = 8 * explicitZ 0 2 2 0 3 1 := by decide
159theorem e_022032 : m2Num 0 2 2 0 3 2 = 8 * explicitZ 0 2 2 0 3 2 := by decide
160theorem e_022033 : m2Num 0 2 2 0 3 3 = 8 * explicitZ 0 2 2 0 3 3 := by decide
161theorem e_022100 : m2Num 0 2 2 1 0 0 = 8 * explicitZ 0 2 2 1 0 0 := by decide
162theorem e_022101 : m2Num 0 2 2 1 0 1 = 8 * explicitZ 0 2 2 1 0 1 := by decide
163theorem e_022102 : m2Num 0 2 2 1 0 2 = 8 * explicitZ 0 2 2 1 0 2 := by decide
164theorem e_022103 : m2Num 0 2 2 1 0 3 = 8 * explicitZ 0 2 2 1 0 3 := by decide
165theorem e_022110 : m2Num 0 2 2 1 1 0 = 8 * explicitZ 0 2 2 1 1 0 := by decide
166theorem e_022111 : m2Num 0 2 2 1 1 1 = 8 * explicitZ 0 2 2 1 1 1 := by decide
167theorem e_022112 : m2Num 0 2 2 1 1 2 = 8 * explicitZ 0 2 2 1 1 2 := by decide
168theorem e_022113 : m2Num 0 2 2 1 1 3 = 8 * explicitZ 0 2 2 1 1 3 := by decide
169theorem e_022120 : m2Num 0 2 2 1 2 0 = 8 * explicitZ 0 2 2 1 2 0 := by decide
170theorem e_022121 : m2Num 0 2 2 1 2 1 = 8 * explicitZ 0 2 2 1 2 1 := by decide
171theorem e_022122 : m2Num 0 2 2 1 2 2 = 8 * explicitZ 0 2 2 1 2 2 := by decide
172theorem e_022123 : m2Num 0 2 2 1 2 3 = 8 * explicitZ 0 2 2 1 2 3 := by decide
173theorem e_022130 : m2Num 0 2 2 1 3 0 = 8 * explicitZ 0 2 2 1 3 0 := by decide
174theorem e_022131 : m2Num 0 2 2 1 3 1 = 8 * explicitZ 0 2 2 1 3 1 := by decide
175theorem e_022132 : m2Num 0 2 2 1 3 2 = 8 * explicitZ 0 2 2 1 3 2 := by decide
176theorem e_022133 : m2Num 0 2 2 1 3 3 = 8 * explicitZ 0 2 2 1 3 3 := by decide
177theorem e_022200 : m2Num 0 2 2 2 0 0 = 8 * explicitZ 0 2 2 2 0 0 := by decide
178theorem e_022201 : m2Num 0 2 2 2 0 1 = 8 * explicitZ 0 2 2 2 0 1 := by decide
179theorem e_022202 : m2Num 0 2 2 2 0 2 = 8 * explicitZ 0 2 2 2 0 2 := by decide
180theorem e_022203 : m2Num 0 2 2 2 0 3 = 8 * explicitZ 0 2 2 2 0 3 := by decide
181theorem e_022210 : m2Num 0 2 2 2 1 0 = 8 * explicitZ 0 2 2 2 1 0 := by decide
182theorem e_022211 : m2Num 0 2 2 2 1 1 = 8 * explicitZ 0 2 2 2 1 1 := by decide
183theorem e_022212 : m2Num 0 2 2 2 1 2 = 8 * explicitZ 0 2 2 2 1 2 := by decide
184theorem e_022213 : m2Num 0 2 2 2 1 3 = 8 * explicitZ 0 2 2 2 1 3 := by decide
185theorem e_022220 : m2Num 0 2 2 2 2 0 = 8 * explicitZ 0 2 2 2 2 0 := by decide
186theorem e_022221 : m2Num 0 2 2 2 2 1 = 8 * explicitZ 0 2 2 2 2 1 := by decide
187theorem e_022222 : m2Num 0 2 2 2 2 2 = 8 * explicitZ 0 2 2 2 2 2 := by decide
188theorem e_022223 : m2Num 0 2 2 2 2 3 = 8 * explicitZ 0 2 2 2 2 3 := by decide
189theorem e_022230 : m2Num 0 2 2 2 3 0 = 8 * explicitZ 0 2 2 2 3 0 := by decide
190theorem e_022231 : m2Num 0 2 2 2 3 1 = 8 * explicitZ 0 2 2 2 3 1 := by decide
191theorem e_022232 : m2Num 0 2 2 2 3 2 = 8 * explicitZ 0 2 2 2 3 2 := by decide
192theorem e_022233 : m2Num 0 2 2 2 3 3 = 8 * explicitZ 0 2 2 2 3 3 := by decide
193theorem e_022300 : m2Num 0 2 2 3 0 0 = 8 * explicitZ 0 2 2 3 0 0 := by decide
194theorem e_022301 : m2Num 0 2 2 3 0 1 = 8 * explicitZ 0 2 2 3 0 1 := by decide
195theorem e_022302 : m2Num 0 2 2 3 0 2 = 8 * explicitZ 0 2 2 3 0 2 := by decide
196theorem e_022303 : m2Num 0 2 2 3 0 3 = 8 * explicitZ 0 2 2 3 0 3 := by decide
197theorem e_022310 : m2Num 0 2 2 3 1 0 = 8 * explicitZ 0 2 2 3 1 0 := by decide
198theorem e_022311 : m2Num 0 2 2 3 1 1 = 8 * explicitZ 0 2 2 3 1 1 := by decide
199theorem e_022312 : m2Num 0 2 2 3 1 2 = 8 * explicitZ 0 2 2 3 1 2 := by decide
200theorem e_022313 : m2Num 0 2 2 3 1 3 = 8 * explicitZ 0 2 2 3 1 3 := by decide
201theorem e_022320 : m2Num 0 2 2 3 2 0 = 8 * explicitZ 0 2 2 3 2 0 := by decide
202theorem e_022321 : m2Num 0 2 2 3 2 1 = 8 * explicitZ 0 2 2 3 2 1 := by decide
203theorem e_022322 : m2Num 0 2 2 3 2 2 = 8 * explicitZ 0 2 2 3 2 2 := by decide
204theorem e_022323 : m2Num 0 2 2 3 2 3 = 8 * explicitZ 0 2 2 3 2 3 := by decide
205theorem e_022330 : m2Num 0 2 2 3 3 0 = 8 * explicitZ 0 2 2 3 3 0 := by decide
206theorem e_022331 : m2Num 0 2 2 3 3 1 = 8 * explicitZ 0 2 2 3 3 1 := by decide
207theorem e_022332 : m2Num 0 2 2 3 3 2 = 8 * explicitZ 0 2 2 3 3 2 := by decide
208theorem e_022333 : m2Num 0 2 2 3 3 3 = 8 * explicitZ 0 2 2 3 3 3 := by decide
209theorem e_023000 : m2Num 0 2 3 0 0 0 = 8 * explicitZ 0 2 3 0 0 0 := by decide
210theorem e_023001 : m2Num 0 2 3 0 0 1 = 8 * explicitZ 0 2 3 0 0 1 := by decide
211theorem e_023002 : m2Num 0 2 3 0 0 2 = 8 * explicitZ 0 2 3 0 0 2 := by decide
212theorem e_023003 : m2Num 0 2 3 0 0 3 = 8 * explicitZ 0 2 3 0 0 3 := by decide
213theorem e_023010 : m2Num 0 2 3 0 1 0 = 8 * explicitZ 0 2 3 0 1 0 := by decide
214theorem e_023011 : m2Num 0 2 3 0 1 1 = 8 * explicitZ 0 2 3 0 1 1 := by decide
215theorem e_023012 : m2Num 0 2 3 0 1 2 = 8 * explicitZ 0 2 3 0 1 2 := by decide
216theorem e_023013 : m2Num 0 2 3 0 1 3 = 8 * explicitZ 0 2 3 0 1 3 := by decide
217theorem e_023020 : m2Num 0 2 3 0 2 0 = 8 * explicitZ 0 2 3 0 2 0 := by decide
218theorem e_023021 : m2Num 0 2 3 0 2 1 = 8 * explicitZ 0 2 3 0 2 1 := by decide
219theorem e_023022 : m2Num 0 2 3 0 2 2 = 8 * explicitZ 0 2 3 0 2 2 := by decide
220theorem e_023023 : m2Num 0 2 3 0 2 3 = 8 * explicitZ 0 2 3 0 2 3 := by decide
221theorem e_023030 : m2Num 0 2 3 0 3 0 = 8 * explicitZ 0 2 3 0 3 0 := by decide
222theorem e_023031 : m2Num 0 2 3 0 3 1 = 8 * explicitZ 0 2 3 0 3 1 := by decide
223theorem e_023032 : m2Num 0 2 3 0 3 2 = 8 * explicitZ 0 2 3 0 3 2 := by decide
224theorem e_023033 : m2Num 0 2 3 0 3 3 = 8 * explicitZ 0 2 3 0 3 3 := by decide
225theorem e_023100 : m2Num 0 2 3 1 0 0 = 8 * explicitZ 0 2 3 1 0 0 := by decide
226theorem e_023101 : m2Num 0 2 3 1 0 1 = 8 * explicitZ 0 2 3 1 0 1 := by decide
227theorem e_023102 : m2Num 0 2 3 1 0 2 = 8 * explicitZ 0 2 3 1 0 2 := by decide
228theorem e_023103 : m2Num 0 2 3 1 0 3 = 8 * explicitZ 0 2 3 1 0 3 := by decide
229theorem e_023110 : m2Num 0 2 3 1 1 0 = 8 * explicitZ 0 2 3 1 1 0 := by decide
230theorem e_023111 : m2Num 0 2 3 1 1 1 = 8 * explicitZ 0 2 3 1 1 1 := by decide
231theorem e_023112 : m2Num 0 2 3 1 1 2 = 8 * explicitZ 0 2 3 1 1 2 := by decide
232theorem e_023113 : m2Num 0 2 3 1 1 3 = 8 * explicitZ 0 2 3 1 1 3 := by decide
233theorem e_023120 : m2Num 0 2 3 1 2 0 = 8 * explicitZ 0 2 3 1 2 0 := by decide
234theorem e_023121 : m2Num 0 2 3 1 2 1 = 8 * explicitZ 0 2 3 1 2 1 := by decide
235theorem e_023122 : m2Num 0 2 3 1 2 2 = 8 * explicitZ 0 2 3 1 2 2 := by decide
236theorem e_023123 : m2Num 0 2 3 1 2 3 = 8 * explicitZ 0 2 3 1 2 3 := by decide
237theorem e_023130 : m2Num 0 2 3 1 3 0 = 8 * explicitZ 0 2 3 1 3 0 := by decide
238theorem e_023131 : m2Num 0 2 3 1 3 1 = 8 * explicitZ 0 2 3 1 3 1 := by decide
239theorem e_023132 : m2Num 0 2 3 1 3 2 = 8 * explicitZ 0 2 3 1 3 2 := by decide
240theorem e_023133 : m2Num 0 2 3 1 3 3 = 8 * explicitZ 0 2 3 1 3 3 := by decide
241theorem e_023200 : m2Num 0 2 3 2 0 0 = 8 * explicitZ 0 2 3 2 0 0 := by decide
242theorem e_023201 : m2Num 0 2 3 2 0 1 = 8 * explicitZ 0 2 3 2 0 1 := by decide
243theorem e_023202 : m2Num 0 2 3 2 0 2 = 8 * explicitZ 0 2 3 2 0 2 := by decide
244theorem e_023203 : m2Num 0 2 3 2 0 3 = 8 * explicitZ 0 2 3 2 0 3 := by decide
245theorem e_023210 : m2Num 0 2 3 2 1 0 = 8 * explicitZ 0 2 3 2 1 0 := by decide
246theorem e_023211 : m2Num 0 2 3 2 1 1 = 8 * explicitZ 0 2 3 2 1 1 := by decide
247theorem e_023212 : m2Num 0 2 3 2 1 2 = 8 * explicitZ 0 2 3 2 1 2 := by decide
248theorem e_023213 : m2Num 0 2 3 2 1 3 = 8 * explicitZ 0 2 3 2 1 3 := by decide
249theorem e_023220 : m2Num 0 2 3 2 2 0 = 8 * explicitZ 0 2 3 2 2 0 := by decide
250theorem e_023221 : m2Num 0 2 3 2 2 1 = 8 * explicitZ 0 2 3 2 2 1 := by decide
251theorem e_023222 : m2Num 0 2 3 2 2 2 = 8 * explicitZ 0 2 3 2 2 2 := by decide
252theorem e_023223 : m2Num 0 2 3 2 2 3 = 8 * explicitZ 0 2 3 2 2 3 := by decide
253theorem e_023230 : m2Num 0 2 3 2 3 0 = 8 * explicitZ 0 2 3 2 3 0 := by decide
254theorem e_023231 : m2Num 0 2 3 2 3 1 = 8 * explicitZ 0 2 3 2 3 1 := by decide
255theorem e_023232 : m2Num 0 2 3 2 3 2 = 8 * explicitZ 0 2 3 2 3 2 := by decide
256theorem e_023233 : m2Num 0 2 3 2 3 3 = 8 * explicitZ 0 2 3 2 3 3 := by decide
257theorem e_023300 : m2Num 0 2 3 3 0 0 = 8 * explicitZ 0 2 3 3 0 0 := by decide
258theorem e_023301 : m2Num 0 2 3 3 0 1 = 8 * explicitZ 0 2 3 3 0 1 := by decide
259theorem e_023302 : m2Num 0 2 3 3 0 2 = 8 * explicitZ 0 2 3 3 0 2 := by decide
260theorem e_023303 : m2Num 0 2 3 3 0 3 = 8 * explicitZ 0 2 3 3 0 3 := by decide
261theorem e_023310 : m2Num 0 2 3 3 1 0 = 8 * explicitZ 0 2 3 3 1 0 := by decide
262theorem e_023311 : m2Num 0 2 3 3 1 1 = 8 * explicitZ 0 2 3 3 1 1 := by decide
263theorem e_023312 : m2Num 0 2 3 3 1 2 = 8 * explicitZ 0 2 3 3 1 2 := by decide
264theorem e_023313 : m2Num 0 2 3 3 1 3 = 8 * explicitZ 0 2 3 3 1 3 := by decide
265theorem e_023320 : m2Num 0 2 3 3 2 0 = 8 * explicitZ 0 2 3 3 2 0 := by decide
266theorem e_023321 : m2Num 0 2 3 3 2 1 = 8 * explicitZ 0 2 3 3 2 1 := by decide
267theorem e_023322 : m2Num 0 2 3 3 2 2 = 8 * explicitZ 0 2 3 3 2 2 := by decide
268theorem e_023323 : m2Num 0 2 3 3 2 3 = 8 * explicitZ 0 2 3 3 2 3 := by decide
269theorem e_023330 : m2Num 0 2 3 3 3 0 = 8 * explicitZ 0 2 3 3 3 0 := by decide
270theorem e_023331 : m2Num 0 2 3 3 3 1 = 8 * explicitZ 0 2 3 3 3 1 := by decide
271theorem e_023332 : m2Num 0 2 3 3 3 2 = 8 * explicitZ 0 2 3 3 3 2 := by decide
272theorem e_023333 : m2Num 0 2 3 3 3 3 = 8 * explicitZ 0 2 3 3 3 3 := by decide
273
274end M2NumChunk02
275end ReggeExactMidpointM2TTIdentity4D
276end Analysis
277end Gravity
278end IndisputableMonolith
279