IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DM2NumChunk15
IndisputableMonolith/Gravity/Analysis/ReggeExactMidpointM2TTIdentity4DM2NumChunk15.lean · 279 lines · 256 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DKernelCert
3
4/-! m2Num = 8·explicitZ, chunk 15 (256 kernel decides). -/
5
6namespace IndisputableMonolith
7namespace Gravity
8namespace Analysis
9namespace ReggeExactMidpointM2TTIdentity4D
10namespace M2NumChunk15
11
12open KernelCert
13
14set_option maxRecDepth 100000
15set_option maxHeartbeats 200000000
16
17theorem e_330000 : m2Num 3 3 0 0 0 0 = 8 * explicitZ 3 3 0 0 0 0 := by decide
18theorem e_330001 : m2Num 3 3 0 0 0 1 = 8 * explicitZ 3 3 0 0 0 1 := by decide
19theorem e_330002 : m2Num 3 3 0 0 0 2 = 8 * explicitZ 3 3 0 0 0 2 := by decide
20theorem e_330003 : m2Num 3 3 0 0 0 3 = 8 * explicitZ 3 3 0 0 0 3 := by decide
21theorem e_330010 : m2Num 3 3 0 0 1 0 = 8 * explicitZ 3 3 0 0 1 0 := by decide
22theorem e_330011 : m2Num 3 3 0 0 1 1 = 8 * explicitZ 3 3 0 0 1 1 := by decide
23theorem e_330012 : m2Num 3 3 0 0 1 2 = 8 * explicitZ 3 3 0 0 1 2 := by decide
24theorem e_330013 : m2Num 3 3 0 0 1 3 = 8 * explicitZ 3 3 0 0 1 3 := by decide
25theorem e_330020 : m2Num 3 3 0 0 2 0 = 8 * explicitZ 3 3 0 0 2 0 := by decide
26theorem e_330021 : m2Num 3 3 0 0 2 1 = 8 * explicitZ 3 3 0 0 2 1 := by decide
27theorem e_330022 : m2Num 3 3 0 0 2 2 = 8 * explicitZ 3 3 0 0 2 2 := by decide
28theorem e_330023 : m2Num 3 3 0 0 2 3 = 8 * explicitZ 3 3 0 0 2 3 := by decide
29theorem e_330030 : m2Num 3 3 0 0 3 0 = 8 * explicitZ 3 3 0 0 3 0 := by decide
30theorem e_330031 : m2Num 3 3 0 0 3 1 = 8 * explicitZ 3 3 0 0 3 1 := by decide
31theorem e_330032 : m2Num 3 3 0 0 3 2 = 8 * explicitZ 3 3 0 0 3 2 := by decide
32theorem e_330033 : m2Num 3 3 0 0 3 3 = 8 * explicitZ 3 3 0 0 3 3 := by decide
33theorem e_330100 : m2Num 3 3 0 1 0 0 = 8 * explicitZ 3 3 0 1 0 0 := by decide
34theorem e_330101 : m2Num 3 3 0 1 0 1 = 8 * explicitZ 3 3 0 1 0 1 := by decide
35theorem e_330102 : m2Num 3 3 0 1 0 2 = 8 * explicitZ 3 3 0 1 0 2 := by decide
36theorem e_330103 : m2Num 3 3 0 1 0 3 = 8 * explicitZ 3 3 0 1 0 3 := by decide
37theorem e_330110 : m2Num 3 3 0 1 1 0 = 8 * explicitZ 3 3 0 1 1 0 := by decide
38theorem e_330111 : m2Num 3 3 0 1 1 1 = 8 * explicitZ 3 3 0 1 1 1 := by decide
39theorem e_330112 : m2Num 3 3 0 1 1 2 = 8 * explicitZ 3 3 0 1 1 2 := by decide
40theorem e_330113 : m2Num 3 3 0 1 1 3 = 8 * explicitZ 3 3 0 1 1 3 := by decide
41theorem e_330120 : m2Num 3 3 0 1 2 0 = 8 * explicitZ 3 3 0 1 2 0 := by decide
42theorem e_330121 : m2Num 3 3 0 1 2 1 = 8 * explicitZ 3 3 0 1 2 1 := by decide
43theorem e_330122 : m2Num 3 3 0 1 2 2 = 8 * explicitZ 3 3 0 1 2 2 := by decide
44theorem e_330123 : m2Num 3 3 0 1 2 3 = 8 * explicitZ 3 3 0 1 2 3 := by decide
45theorem e_330130 : m2Num 3 3 0 1 3 0 = 8 * explicitZ 3 3 0 1 3 0 := by decide
46theorem e_330131 : m2Num 3 3 0 1 3 1 = 8 * explicitZ 3 3 0 1 3 1 := by decide
47theorem e_330132 : m2Num 3 3 0 1 3 2 = 8 * explicitZ 3 3 0 1 3 2 := by decide
48theorem e_330133 : m2Num 3 3 0 1 3 3 = 8 * explicitZ 3 3 0 1 3 3 := by decide
49theorem e_330200 : m2Num 3 3 0 2 0 0 = 8 * explicitZ 3 3 0 2 0 0 := by decide
50theorem e_330201 : m2Num 3 3 0 2 0 1 = 8 * explicitZ 3 3 0 2 0 1 := by decide
51theorem e_330202 : m2Num 3 3 0 2 0 2 = 8 * explicitZ 3 3 0 2 0 2 := by decide
52theorem e_330203 : m2Num 3 3 0 2 0 3 = 8 * explicitZ 3 3 0 2 0 3 := by decide
53theorem e_330210 : m2Num 3 3 0 2 1 0 = 8 * explicitZ 3 3 0 2 1 0 := by decide
54theorem e_330211 : m2Num 3 3 0 2 1 1 = 8 * explicitZ 3 3 0 2 1 1 := by decide
55theorem e_330212 : m2Num 3 3 0 2 1 2 = 8 * explicitZ 3 3 0 2 1 2 := by decide
56theorem e_330213 : m2Num 3 3 0 2 1 3 = 8 * explicitZ 3 3 0 2 1 3 := by decide
57theorem e_330220 : m2Num 3 3 0 2 2 0 = 8 * explicitZ 3 3 0 2 2 0 := by decide
58theorem e_330221 : m2Num 3 3 0 2 2 1 = 8 * explicitZ 3 3 0 2 2 1 := by decide
59theorem e_330222 : m2Num 3 3 0 2 2 2 = 8 * explicitZ 3 3 0 2 2 2 := by decide
60theorem e_330223 : m2Num 3 3 0 2 2 3 = 8 * explicitZ 3 3 0 2 2 3 := by decide
61theorem e_330230 : m2Num 3 3 0 2 3 0 = 8 * explicitZ 3 3 0 2 3 0 := by decide
62theorem e_330231 : m2Num 3 3 0 2 3 1 = 8 * explicitZ 3 3 0 2 3 1 := by decide
63theorem e_330232 : m2Num 3 3 0 2 3 2 = 8 * explicitZ 3 3 0 2 3 2 := by decide
64theorem e_330233 : m2Num 3 3 0 2 3 3 = 8 * explicitZ 3 3 0 2 3 3 := by decide
65theorem e_330300 : m2Num 3 3 0 3 0 0 = 8 * explicitZ 3 3 0 3 0 0 := by decide
66theorem e_330301 : m2Num 3 3 0 3 0 1 = 8 * explicitZ 3 3 0 3 0 1 := by decide
67theorem e_330302 : m2Num 3 3 0 3 0 2 = 8 * explicitZ 3 3 0 3 0 2 := by decide
68theorem e_330303 : m2Num 3 3 0 3 0 3 = 8 * explicitZ 3 3 0 3 0 3 := by decide
69theorem e_330310 : m2Num 3 3 0 3 1 0 = 8 * explicitZ 3 3 0 3 1 0 := by decide
70theorem e_330311 : m2Num 3 3 0 3 1 1 = 8 * explicitZ 3 3 0 3 1 1 := by decide
71theorem e_330312 : m2Num 3 3 0 3 1 2 = 8 * explicitZ 3 3 0 3 1 2 := by decide
72theorem e_330313 : m2Num 3 3 0 3 1 3 = 8 * explicitZ 3 3 0 3 1 3 := by decide
73theorem e_330320 : m2Num 3 3 0 3 2 0 = 8 * explicitZ 3 3 0 3 2 0 := by decide
74theorem e_330321 : m2Num 3 3 0 3 2 1 = 8 * explicitZ 3 3 0 3 2 1 := by decide
75theorem e_330322 : m2Num 3 3 0 3 2 2 = 8 * explicitZ 3 3 0 3 2 2 := by decide
76theorem e_330323 : m2Num 3 3 0 3 2 3 = 8 * explicitZ 3 3 0 3 2 3 := by decide
77theorem e_330330 : m2Num 3 3 0 3 3 0 = 8 * explicitZ 3 3 0 3 3 0 := by decide
78theorem e_330331 : m2Num 3 3 0 3 3 1 = 8 * explicitZ 3 3 0 3 3 1 := by decide
79theorem e_330332 : m2Num 3 3 0 3 3 2 = 8 * explicitZ 3 3 0 3 3 2 := by decide
80theorem e_330333 : m2Num 3 3 0 3 3 3 = 8 * explicitZ 3 3 0 3 3 3 := by decide
81theorem e_331000 : m2Num 3 3 1 0 0 0 = 8 * explicitZ 3 3 1 0 0 0 := by decide
82theorem e_331001 : m2Num 3 3 1 0 0 1 = 8 * explicitZ 3 3 1 0 0 1 := by decide
83theorem e_331002 : m2Num 3 3 1 0 0 2 = 8 * explicitZ 3 3 1 0 0 2 := by decide
84theorem e_331003 : m2Num 3 3 1 0 0 3 = 8 * explicitZ 3 3 1 0 0 3 := by decide
85theorem e_331010 : m2Num 3 3 1 0 1 0 = 8 * explicitZ 3 3 1 0 1 0 := by decide
86theorem e_331011 : m2Num 3 3 1 0 1 1 = 8 * explicitZ 3 3 1 0 1 1 := by decide
87theorem e_331012 : m2Num 3 3 1 0 1 2 = 8 * explicitZ 3 3 1 0 1 2 := by decide
88theorem e_331013 : m2Num 3 3 1 0 1 3 = 8 * explicitZ 3 3 1 0 1 3 := by decide
89theorem e_331020 : m2Num 3 3 1 0 2 0 = 8 * explicitZ 3 3 1 0 2 0 := by decide
90theorem e_331021 : m2Num 3 3 1 0 2 1 = 8 * explicitZ 3 3 1 0 2 1 := by decide
91theorem e_331022 : m2Num 3 3 1 0 2 2 = 8 * explicitZ 3 3 1 0 2 2 := by decide
92theorem e_331023 : m2Num 3 3 1 0 2 3 = 8 * explicitZ 3 3 1 0 2 3 := by decide
93theorem e_331030 : m2Num 3 3 1 0 3 0 = 8 * explicitZ 3 3 1 0 3 0 := by decide
94theorem e_331031 : m2Num 3 3 1 0 3 1 = 8 * explicitZ 3 3 1 0 3 1 := by decide
95theorem e_331032 : m2Num 3 3 1 0 3 2 = 8 * explicitZ 3 3 1 0 3 2 := by decide
96theorem e_331033 : m2Num 3 3 1 0 3 3 = 8 * explicitZ 3 3 1 0 3 3 := by decide
97theorem e_331100 : m2Num 3 3 1 1 0 0 = 8 * explicitZ 3 3 1 1 0 0 := by decide
98theorem e_331101 : m2Num 3 3 1 1 0 1 = 8 * explicitZ 3 3 1 1 0 1 := by decide
99theorem e_331102 : m2Num 3 3 1 1 0 2 = 8 * explicitZ 3 3 1 1 0 2 := by decide
100theorem e_331103 : m2Num 3 3 1 1 0 3 = 8 * explicitZ 3 3 1 1 0 3 := by decide
101theorem e_331110 : m2Num 3 3 1 1 1 0 = 8 * explicitZ 3 3 1 1 1 0 := by decide
102theorem e_331111 : m2Num 3 3 1 1 1 1 = 8 * explicitZ 3 3 1 1 1 1 := by decide
103theorem e_331112 : m2Num 3 3 1 1 1 2 = 8 * explicitZ 3 3 1 1 1 2 := by decide
104theorem e_331113 : m2Num 3 3 1 1 1 3 = 8 * explicitZ 3 3 1 1 1 3 := by decide
105theorem e_331120 : m2Num 3 3 1 1 2 0 = 8 * explicitZ 3 3 1 1 2 0 := by decide
106theorem e_331121 : m2Num 3 3 1 1 2 1 = 8 * explicitZ 3 3 1 1 2 1 := by decide
107theorem e_331122 : m2Num 3 3 1 1 2 2 = 8 * explicitZ 3 3 1 1 2 2 := by decide
108theorem e_331123 : m2Num 3 3 1 1 2 3 = 8 * explicitZ 3 3 1 1 2 3 := by decide
109theorem e_331130 : m2Num 3 3 1 1 3 0 = 8 * explicitZ 3 3 1 1 3 0 := by decide
110theorem e_331131 : m2Num 3 3 1 1 3 1 = 8 * explicitZ 3 3 1 1 3 1 := by decide
111theorem e_331132 : m2Num 3 3 1 1 3 2 = 8 * explicitZ 3 3 1 1 3 2 := by decide
112theorem e_331133 : m2Num 3 3 1 1 3 3 = 8 * explicitZ 3 3 1 1 3 3 := by decide
113theorem e_331200 : m2Num 3 3 1 2 0 0 = 8 * explicitZ 3 3 1 2 0 0 := by decide
114theorem e_331201 : m2Num 3 3 1 2 0 1 = 8 * explicitZ 3 3 1 2 0 1 := by decide
115theorem e_331202 : m2Num 3 3 1 2 0 2 = 8 * explicitZ 3 3 1 2 0 2 := by decide
116theorem e_331203 : m2Num 3 3 1 2 0 3 = 8 * explicitZ 3 3 1 2 0 3 := by decide
117theorem e_331210 : m2Num 3 3 1 2 1 0 = 8 * explicitZ 3 3 1 2 1 0 := by decide
118theorem e_331211 : m2Num 3 3 1 2 1 1 = 8 * explicitZ 3 3 1 2 1 1 := by decide
119theorem e_331212 : m2Num 3 3 1 2 1 2 = 8 * explicitZ 3 3 1 2 1 2 := by decide
120theorem e_331213 : m2Num 3 3 1 2 1 3 = 8 * explicitZ 3 3 1 2 1 3 := by decide
121theorem e_331220 : m2Num 3 3 1 2 2 0 = 8 * explicitZ 3 3 1 2 2 0 := by decide
122theorem e_331221 : m2Num 3 3 1 2 2 1 = 8 * explicitZ 3 3 1 2 2 1 := by decide
123theorem e_331222 : m2Num 3 3 1 2 2 2 = 8 * explicitZ 3 3 1 2 2 2 := by decide
124theorem e_331223 : m2Num 3 3 1 2 2 3 = 8 * explicitZ 3 3 1 2 2 3 := by decide
125theorem e_331230 : m2Num 3 3 1 2 3 0 = 8 * explicitZ 3 3 1 2 3 0 := by decide
126theorem e_331231 : m2Num 3 3 1 2 3 1 = 8 * explicitZ 3 3 1 2 3 1 := by decide
127theorem e_331232 : m2Num 3 3 1 2 3 2 = 8 * explicitZ 3 3 1 2 3 2 := by decide
128theorem e_331233 : m2Num 3 3 1 2 3 3 = 8 * explicitZ 3 3 1 2 3 3 := by decide
129theorem e_331300 : m2Num 3 3 1 3 0 0 = 8 * explicitZ 3 3 1 3 0 0 := by decide
130theorem e_331301 : m2Num 3 3 1 3 0 1 = 8 * explicitZ 3 3 1 3 0 1 := by decide
131theorem e_331302 : m2Num 3 3 1 3 0 2 = 8 * explicitZ 3 3 1 3 0 2 := by decide
132theorem e_331303 : m2Num 3 3 1 3 0 3 = 8 * explicitZ 3 3 1 3 0 3 := by decide
133theorem e_331310 : m2Num 3 3 1 3 1 0 = 8 * explicitZ 3 3 1 3 1 0 := by decide
134theorem e_331311 : m2Num 3 3 1 3 1 1 = 8 * explicitZ 3 3 1 3 1 1 := by decide
135theorem e_331312 : m2Num 3 3 1 3 1 2 = 8 * explicitZ 3 3 1 3 1 2 := by decide
136theorem e_331313 : m2Num 3 3 1 3 1 3 = 8 * explicitZ 3 3 1 3 1 3 := by decide
137theorem e_331320 : m2Num 3 3 1 3 2 0 = 8 * explicitZ 3 3 1 3 2 0 := by decide
138theorem e_331321 : m2Num 3 3 1 3 2 1 = 8 * explicitZ 3 3 1 3 2 1 := by decide
139theorem e_331322 : m2Num 3 3 1 3 2 2 = 8 * explicitZ 3 3 1 3 2 2 := by decide
140theorem e_331323 : m2Num 3 3 1 3 2 3 = 8 * explicitZ 3 3 1 3 2 3 := by decide
141theorem e_331330 : m2Num 3 3 1 3 3 0 = 8 * explicitZ 3 3 1 3 3 0 := by decide
142theorem e_331331 : m2Num 3 3 1 3 3 1 = 8 * explicitZ 3 3 1 3 3 1 := by decide
143theorem e_331332 : m2Num 3 3 1 3 3 2 = 8 * explicitZ 3 3 1 3 3 2 := by decide
144theorem e_331333 : m2Num 3 3 1 3 3 3 = 8 * explicitZ 3 3 1 3 3 3 := by decide
145theorem e_332000 : m2Num 3 3 2 0 0 0 = 8 * explicitZ 3 3 2 0 0 0 := by decide
146theorem e_332001 : m2Num 3 3 2 0 0 1 = 8 * explicitZ 3 3 2 0 0 1 := by decide
147theorem e_332002 : m2Num 3 3 2 0 0 2 = 8 * explicitZ 3 3 2 0 0 2 := by decide
148theorem e_332003 : m2Num 3 3 2 0 0 3 = 8 * explicitZ 3 3 2 0 0 3 := by decide
149theorem e_332010 : m2Num 3 3 2 0 1 0 = 8 * explicitZ 3 3 2 0 1 0 := by decide
150theorem e_332011 : m2Num 3 3 2 0 1 1 = 8 * explicitZ 3 3 2 0 1 1 := by decide
151theorem e_332012 : m2Num 3 3 2 0 1 2 = 8 * explicitZ 3 3 2 0 1 2 := by decide
152theorem e_332013 : m2Num 3 3 2 0 1 3 = 8 * explicitZ 3 3 2 0 1 3 := by decide
153theorem e_332020 : m2Num 3 3 2 0 2 0 = 8 * explicitZ 3 3 2 0 2 0 := by decide
154theorem e_332021 : m2Num 3 3 2 0 2 1 = 8 * explicitZ 3 3 2 0 2 1 := by decide
155theorem e_332022 : m2Num 3 3 2 0 2 2 = 8 * explicitZ 3 3 2 0 2 2 := by decide
156theorem e_332023 : m2Num 3 3 2 0 2 3 = 8 * explicitZ 3 3 2 0 2 3 := by decide
157theorem e_332030 : m2Num 3 3 2 0 3 0 = 8 * explicitZ 3 3 2 0 3 0 := by decide
158theorem e_332031 : m2Num 3 3 2 0 3 1 = 8 * explicitZ 3 3 2 0 3 1 := by decide
159theorem e_332032 : m2Num 3 3 2 0 3 2 = 8 * explicitZ 3 3 2 0 3 2 := by decide
160theorem e_332033 : m2Num 3 3 2 0 3 3 = 8 * explicitZ 3 3 2 0 3 3 := by decide
161theorem e_332100 : m2Num 3 3 2 1 0 0 = 8 * explicitZ 3 3 2 1 0 0 := by decide
162theorem e_332101 : m2Num 3 3 2 1 0 1 = 8 * explicitZ 3 3 2 1 0 1 := by decide
163theorem e_332102 : m2Num 3 3 2 1 0 2 = 8 * explicitZ 3 3 2 1 0 2 := by decide
164theorem e_332103 : m2Num 3 3 2 1 0 3 = 8 * explicitZ 3 3 2 1 0 3 := by decide
165theorem e_332110 : m2Num 3 3 2 1 1 0 = 8 * explicitZ 3 3 2 1 1 0 := by decide
166theorem e_332111 : m2Num 3 3 2 1 1 1 = 8 * explicitZ 3 3 2 1 1 1 := by decide
167theorem e_332112 : m2Num 3 3 2 1 1 2 = 8 * explicitZ 3 3 2 1 1 2 := by decide
168theorem e_332113 : m2Num 3 3 2 1 1 3 = 8 * explicitZ 3 3 2 1 1 3 := by decide
169theorem e_332120 : m2Num 3 3 2 1 2 0 = 8 * explicitZ 3 3 2 1 2 0 := by decide
170theorem e_332121 : m2Num 3 3 2 1 2 1 = 8 * explicitZ 3 3 2 1 2 1 := by decide
171theorem e_332122 : m2Num 3 3 2 1 2 2 = 8 * explicitZ 3 3 2 1 2 2 := by decide
172theorem e_332123 : m2Num 3 3 2 1 2 3 = 8 * explicitZ 3 3 2 1 2 3 := by decide
173theorem e_332130 : m2Num 3 3 2 1 3 0 = 8 * explicitZ 3 3 2 1 3 0 := by decide
174theorem e_332131 : m2Num 3 3 2 1 3 1 = 8 * explicitZ 3 3 2 1 3 1 := by decide
175theorem e_332132 : m2Num 3 3 2 1 3 2 = 8 * explicitZ 3 3 2 1 3 2 := by decide
176theorem e_332133 : m2Num 3 3 2 1 3 3 = 8 * explicitZ 3 3 2 1 3 3 := by decide
177theorem e_332200 : m2Num 3 3 2 2 0 0 = 8 * explicitZ 3 3 2 2 0 0 := by decide
178theorem e_332201 : m2Num 3 3 2 2 0 1 = 8 * explicitZ 3 3 2 2 0 1 := by decide
179theorem e_332202 : m2Num 3 3 2 2 0 2 = 8 * explicitZ 3 3 2 2 0 2 := by decide
180theorem e_332203 : m2Num 3 3 2 2 0 3 = 8 * explicitZ 3 3 2 2 0 3 := by decide
181theorem e_332210 : m2Num 3 3 2 2 1 0 = 8 * explicitZ 3 3 2 2 1 0 := by decide
182theorem e_332211 : m2Num 3 3 2 2 1 1 = 8 * explicitZ 3 3 2 2 1 1 := by decide
183theorem e_332212 : m2Num 3 3 2 2 1 2 = 8 * explicitZ 3 3 2 2 1 2 := by decide
184theorem e_332213 : m2Num 3 3 2 2 1 3 = 8 * explicitZ 3 3 2 2 1 3 := by decide
185theorem e_332220 : m2Num 3 3 2 2 2 0 = 8 * explicitZ 3 3 2 2 2 0 := by decide
186theorem e_332221 : m2Num 3 3 2 2 2 1 = 8 * explicitZ 3 3 2 2 2 1 := by decide
187theorem e_332222 : m2Num 3 3 2 2 2 2 = 8 * explicitZ 3 3 2 2 2 2 := by decide
188theorem e_332223 : m2Num 3 3 2 2 2 3 = 8 * explicitZ 3 3 2 2 2 3 := by decide
189theorem e_332230 : m2Num 3 3 2 2 3 0 = 8 * explicitZ 3 3 2 2 3 0 := by decide
190theorem e_332231 : m2Num 3 3 2 2 3 1 = 8 * explicitZ 3 3 2 2 3 1 := by decide
191theorem e_332232 : m2Num 3 3 2 2 3 2 = 8 * explicitZ 3 3 2 2 3 2 := by decide
192theorem e_332233 : m2Num 3 3 2 2 3 3 = 8 * explicitZ 3 3 2 2 3 3 := by decide
193theorem e_332300 : m2Num 3 3 2 3 0 0 = 8 * explicitZ 3 3 2 3 0 0 := by decide
194theorem e_332301 : m2Num 3 3 2 3 0 1 = 8 * explicitZ 3 3 2 3 0 1 := by decide
195theorem e_332302 : m2Num 3 3 2 3 0 2 = 8 * explicitZ 3 3 2 3 0 2 := by decide
196theorem e_332303 : m2Num 3 3 2 3 0 3 = 8 * explicitZ 3 3 2 3 0 3 := by decide
197theorem e_332310 : m2Num 3 3 2 3 1 0 = 8 * explicitZ 3 3 2 3 1 0 := by decide
198theorem e_332311 : m2Num 3 3 2 3 1 1 = 8 * explicitZ 3 3 2 3 1 1 := by decide
199theorem e_332312 : m2Num 3 3 2 3 1 2 = 8 * explicitZ 3 3 2 3 1 2 := by decide
200theorem e_332313 : m2Num 3 3 2 3 1 3 = 8 * explicitZ 3 3 2 3 1 3 := by decide
201theorem e_332320 : m2Num 3 3 2 3 2 0 = 8 * explicitZ 3 3 2 3 2 0 := by decide
202theorem e_332321 : m2Num 3 3 2 3 2 1 = 8 * explicitZ 3 3 2 3 2 1 := by decide
203theorem e_332322 : m2Num 3 3 2 3 2 2 = 8 * explicitZ 3 3 2 3 2 2 := by decide
204theorem e_332323 : m2Num 3 3 2 3 2 3 = 8 * explicitZ 3 3 2 3 2 3 := by decide
205theorem e_332330 : m2Num 3 3 2 3 3 0 = 8 * explicitZ 3 3 2 3 3 0 := by decide
206theorem e_332331 : m2Num 3 3 2 3 3 1 = 8 * explicitZ 3 3 2 3 3 1 := by decide
207theorem e_332332 : m2Num 3 3 2 3 3 2 = 8 * explicitZ 3 3 2 3 3 2 := by decide
208theorem e_332333 : m2Num 3 3 2 3 3 3 = 8 * explicitZ 3 3 2 3 3 3 := by decide
209theorem e_333000 : m2Num 3 3 3 0 0 0 = 8 * explicitZ 3 3 3 0 0 0 := by decide
210theorem e_333001 : m2Num 3 3 3 0 0 1 = 8 * explicitZ 3 3 3 0 0 1 := by decide
211theorem e_333002 : m2Num 3 3 3 0 0 2 = 8 * explicitZ 3 3 3 0 0 2 := by decide
212theorem e_333003 : m2Num 3 3 3 0 0 3 = 8 * explicitZ 3 3 3 0 0 3 := by decide
213theorem e_333010 : m2Num 3 3 3 0 1 0 = 8 * explicitZ 3 3 3 0 1 0 := by decide
214theorem e_333011 : m2Num 3 3 3 0 1 1 = 8 * explicitZ 3 3 3 0 1 1 := by decide
215theorem e_333012 : m2Num 3 3 3 0 1 2 = 8 * explicitZ 3 3 3 0 1 2 := by decide
216theorem e_333013 : m2Num 3 3 3 0 1 3 = 8 * explicitZ 3 3 3 0 1 3 := by decide
217theorem e_333020 : m2Num 3 3 3 0 2 0 = 8 * explicitZ 3 3 3 0 2 0 := by decide
218theorem e_333021 : m2Num 3 3 3 0 2 1 = 8 * explicitZ 3 3 3 0 2 1 := by decide
219theorem e_333022 : m2Num 3 3 3 0 2 2 = 8 * explicitZ 3 3 3 0 2 2 := by decide
220theorem e_333023 : m2Num 3 3 3 0 2 3 = 8 * explicitZ 3 3 3 0 2 3 := by decide
221theorem e_333030 : m2Num 3 3 3 0 3 0 = 8 * explicitZ 3 3 3 0 3 0 := by decide
222theorem e_333031 : m2Num 3 3 3 0 3 1 = 8 * explicitZ 3 3 3 0 3 1 := by decide
223theorem e_333032 : m2Num 3 3 3 0 3 2 = 8 * explicitZ 3 3 3 0 3 2 := by decide
224theorem e_333033 : m2Num 3 3 3 0 3 3 = 8 * explicitZ 3 3 3 0 3 3 := by decide
225theorem e_333100 : m2Num 3 3 3 1 0 0 = 8 * explicitZ 3 3 3 1 0 0 := by decide
226theorem e_333101 : m2Num 3 3 3 1 0 1 = 8 * explicitZ 3 3 3 1 0 1 := by decide
227theorem e_333102 : m2Num 3 3 3 1 0 2 = 8 * explicitZ 3 3 3 1 0 2 := by decide
228theorem e_333103 : m2Num 3 3 3 1 0 3 = 8 * explicitZ 3 3 3 1 0 3 := by decide
229theorem e_333110 : m2Num 3 3 3 1 1 0 = 8 * explicitZ 3 3 3 1 1 0 := by decide
230theorem e_333111 : m2Num 3 3 3 1 1 1 = 8 * explicitZ 3 3 3 1 1 1 := by decide
231theorem e_333112 : m2Num 3 3 3 1 1 2 = 8 * explicitZ 3 3 3 1 1 2 := by decide
232theorem e_333113 : m2Num 3 3 3 1 1 3 = 8 * explicitZ 3 3 3 1 1 3 := by decide
233theorem e_333120 : m2Num 3 3 3 1 2 0 = 8 * explicitZ 3 3 3 1 2 0 := by decide
234theorem e_333121 : m2Num 3 3 3 1 2 1 = 8 * explicitZ 3 3 3 1 2 1 := by decide
235theorem e_333122 : m2Num 3 3 3 1 2 2 = 8 * explicitZ 3 3 3 1 2 2 := by decide
236theorem e_333123 : m2Num 3 3 3 1 2 3 = 8 * explicitZ 3 3 3 1 2 3 := by decide
237theorem e_333130 : m2Num 3 3 3 1 3 0 = 8 * explicitZ 3 3 3 1 3 0 := by decide
238theorem e_333131 : m2Num 3 3 3 1 3 1 = 8 * explicitZ 3 3 3 1 3 1 := by decide
239theorem e_333132 : m2Num 3 3 3 1 3 2 = 8 * explicitZ 3 3 3 1 3 2 := by decide
240theorem e_333133 : m2Num 3 3 3 1 3 3 = 8 * explicitZ 3 3 3 1 3 3 := by decide
241theorem e_333200 : m2Num 3 3 3 2 0 0 = 8 * explicitZ 3 3 3 2 0 0 := by decide
242theorem e_333201 : m2Num 3 3 3 2 0 1 = 8 * explicitZ 3 3 3 2 0 1 := by decide
243theorem e_333202 : m2Num 3 3 3 2 0 2 = 8 * explicitZ 3 3 3 2 0 2 := by decide
244theorem e_333203 : m2Num 3 3 3 2 0 3 = 8 * explicitZ 3 3 3 2 0 3 := by decide
245theorem e_333210 : m2Num 3 3 3 2 1 0 = 8 * explicitZ 3 3 3 2 1 0 := by decide
246theorem e_333211 : m2Num 3 3 3 2 1 1 = 8 * explicitZ 3 3 3 2 1 1 := by decide
247theorem e_333212 : m2Num 3 3 3 2 1 2 = 8 * explicitZ 3 3 3 2 1 2 := by decide
248theorem e_333213 : m2Num 3 3 3 2 1 3 = 8 * explicitZ 3 3 3 2 1 3 := by decide
249theorem e_333220 : m2Num 3 3 3 2 2 0 = 8 * explicitZ 3 3 3 2 2 0 := by decide
250theorem e_333221 : m2Num 3 3 3 2 2 1 = 8 * explicitZ 3 3 3 2 2 1 := by decide
251theorem e_333222 : m2Num 3 3 3 2 2 2 = 8 * explicitZ 3 3 3 2 2 2 := by decide
252theorem e_333223 : m2Num 3 3 3 2 2 3 = 8 * explicitZ 3 3 3 2 2 3 := by decide
253theorem e_333230 : m2Num 3 3 3 2 3 0 = 8 * explicitZ 3 3 3 2 3 0 := by decide
254theorem e_333231 : m2Num 3 3 3 2 3 1 = 8 * explicitZ 3 3 3 2 3 1 := by decide
255theorem e_333232 : m2Num 3 3 3 2 3 2 = 8 * explicitZ 3 3 3 2 3 2 := by decide
256theorem e_333233 : m2Num 3 3 3 2 3 3 = 8 * explicitZ 3 3 3 2 3 3 := by decide
257theorem e_333300 : m2Num 3 3 3 3 0 0 = 8 * explicitZ 3 3 3 3 0 0 := by decide
258theorem e_333301 : m2Num 3 3 3 3 0 1 = 8 * explicitZ 3 3 3 3 0 1 := by decide
259theorem e_333302 : m2Num 3 3 3 3 0 2 = 8 * explicitZ 3 3 3 3 0 2 := by decide
260theorem e_333303 : m2Num 3 3 3 3 0 3 = 8 * explicitZ 3 3 3 3 0 3 := by decide
261theorem e_333310 : m2Num 3 3 3 3 1 0 = 8 * explicitZ 3 3 3 3 1 0 := by decide
262theorem e_333311 : m2Num 3 3 3 3 1 1 = 8 * explicitZ 3 3 3 3 1 1 := by decide
263theorem e_333312 : m2Num 3 3 3 3 1 2 = 8 * explicitZ 3 3 3 3 1 2 := by decide
264theorem e_333313 : m2Num 3 3 3 3 1 3 = 8 * explicitZ 3 3 3 3 1 3 := by decide
265theorem e_333320 : m2Num 3 3 3 3 2 0 = 8 * explicitZ 3 3 3 3 2 0 := by decide
266theorem e_333321 : m2Num 3 3 3 3 2 1 = 8 * explicitZ 3 3 3 3 2 1 := by decide
267theorem e_333322 : m2Num 3 3 3 3 2 2 = 8 * explicitZ 3 3 3 3 2 2 := by decide
268theorem e_333323 : m2Num 3 3 3 3 2 3 = 8 * explicitZ 3 3 3 3 2 3 := by decide
269theorem e_333330 : m2Num 3 3 3 3 3 0 = 8 * explicitZ 3 3 3 3 3 0 := by decide
270theorem e_333331 : m2Num 3 3 3 3 3 1 = 8 * explicitZ 3 3 3 3 3 1 := by decide
271theorem e_333332 : m2Num 3 3 3 3 3 2 = 8 * explicitZ 3 3 3 3 3 2 := by decide
272theorem e_333333 : m2Num 3 3 3 3 3 3 = 8 * explicitZ 3 3 3 3 3 3 := by decide
273
274end M2NumChunk15
275end ReggeExactMidpointM2TTIdentity4D
276end Analysis
277end Gravity
278end IndisputableMonolith
279