IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DM2NumChunk11
IndisputableMonolith/Gravity/Analysis/ReggeExactMidpointM2TTIdentity4DM2NumChunk11.lean · 279 lines · 256 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DKernelCert
3
4/-! m2Num = 8·explicitZ, chunk 11 (256 kernel decides). -/
5
6namespace IndisputableMonolith
7namespace Gravity
8namespace Analysis
9namespace ReggeExactMidpointM2TTIdentity4D
10namespace M2NumChunk11
11
12open KernelCert
13
14set_option maxRecDepth 100000
15set_option maxHeartbeats 200000000
16
17theorem e_230000 : m2Num 2 3 0 0 0 0 = 8 * explicitZ 2 3 0 0 0 0 := by decide
18theorem e_230001 : m2Num 2 3 0 0 0 1 = 8 * explicitZ 2 3 0 0 0 1 := by decide
19theorem e_230002 : m2Num 2 3 0 0 0 2 = 8 * explicitZ 2 3 0 0 0 2 := by decide
20theorem e_230003 : m2Num 2 3 0 0 0 3 = 8 * explicitZ 2 3 0 0 0 3 := by decide
21theorem e_230010 : m2Num 2 3 0 0 1 0 = 8 * explicitZ 2 3 0 0 1 0 := by decide
22theorem e_230011 : m2Num 2 3 0 0 1 1 = 8 * explicitZ 2 3 0 0 1 1 := by decide
23theorem e_230012 : m2Num 2 3 0 0 1 2 = 8 * explicitZ 2 3 0 0 1 2 := by decide
24theorem e_230013 : m2Num 2 3 0 0 1 3 = 8 * explicitZ 2 3 0 0 1 3 := by decide
25theorem e_230020 : m2Num 2 3 0 0 2 0 = 8 * explicitZ 2 3 0 0 2 0 := by decide
26theorem e_230021 : m2Num 2 3 0 0 2 1 = 8 * explicitZ 2 3 0 0 2 1 := by decide
27theorem e_230022 : m2Num 2 3 0 0 2 2 = 8 * explicitZ 2 3 0 0 2 2 := by decide
28theorem e_230023 : m2Num 2 3 0 0 2 3 = 8 * explicitZ 2 3 0 0 2 3 := by decide
29theorem e_230030 : m2Num 2 3 0 0 3 0 = 8 * explicitZ 2 3 0 0 3 0 := by decide
30theorem e_230031 : m2Num 2 3 0 0 3 1 = 8 * explicitZ 2 3 0 0 3 1 := by decide
31theorem e_230032 : m2Num 2 3 0 0 3 2 = 8 * explicitZ 2 3 0 0 3 2 := by decide
32theorem e_230033 : m2Num 2 3 0 0 3 3 = 8 * explicitZ 2 3 0 0 3 3 := by decide
33theorem e_230100 : m2Num 2 3 0 1 0 0 = 8 * explicitZ 2 3 0 1 0 0 := by decide
34theorem e_230101 : m2Num 2 3 0 1 0 1 = 8 * explicitZ 2 3 0 1 0 1 := by decide
35theorem e_230102 : m2Num 2 3 0 1 0 2 = 8 * explicitZ 2 3 0 1 0 2 := by decide
36theorem e_230103 : m2Num 2 3 0 1 0 3 = 8 * explicitZ 2 3 0 1 0 3 := by decide
37theorem e_230110 : m2Num 2 3 0 1 1 0 = 8 * explicitZ 2 3 0 1 1 0 := by decide
38theorem e_230111 : m2Num 2 3 0 1 1 1 = 8 * explicitZ 2 3 0 1 1 1 := by decide
39theorem e_230112 : m2Num 2 3 0 1 1 2 = 8 * explicitZ 2 3 0 1 1 2 := by decide
40theorem e_230113 : m2Num 2 3 0 1 1 3 = 8 * explicitZ 2 3 0 1 1 3 := by decide
41theorem e_230120 : m2Num 2 3 0 1 2 0 = 8 * explicitZ 2 3 0 1 2 0 := by decide
42theorem e_230121 : m2Num 2 3 0 1 2 1 = 8 * explicitZ 2 3 0 1 2 1 := by decide
43theorem e_230122 : m2Num 2 3 0 1 2 2 = 8 * explicitZ 2 3 0 1 2 2 := by decide
44theorem e_230123 : m2Num 2 3 0 1 2 3 = 8 * explicitZ 2 3 0 1 2 3 := by decide
45theorem e_230130 : m2Num 2 3 0 1 3 0 = 8 * explicitZ 2 3 0 1 3 0 := by decide
46theorem e_230131 : m2Num 2 3 0 1 3 1 = 8 * explicitZ 2 3 0 1 3 1 := by decide
47theorem e_230132 : m2Num 2 3 0 1 3 2 = 8 * explicitZ 2 3 0 1 3 2 := by decide
48theorem e_230133 : m2Num 2 3 0 1 3 3 = 8 * explicitZ 2 3 0 1 3 3 := by decide
49theorem e_230200 : m2Num 2 3 0 2 0 0 = 8 * explicitZ 2 3 0 2 0 0 := by decide
50theorem e_230201 : m2Num 2 3 0 2 0 1 = 8 * explicitZ 2 3 0 2 0 1 := by decide
51theorem e_230202 : m2Num 2 3 0 2 0 2 = 8 * explicitZ 2 3 0 2 0 2 := by decide
52theorem e_230203 : m2Num 2 3 0 2 0 3 = 8 * explicitZ 2 3 0 2 0 3 := by decide
53theorem e_230210 : m2Num 2 3 0 2 1 0 = 8 * explicitZ 2 3 0 2 1 0 := by decide
54theorem e_230211 : m2Num 2 3 0 2 1 1 = 8 * explicitZ 2 3 0 2 1 1 := by decide
55theorem e_230212 : m2Num 2 3 0 2 1 2 = 8 * explicitZ 2 3 0 2 1 2 := by decide
56theorem e_230213 : m2Num 2 3 0 2 1 3 = 8 * explicitZ 2 3 0 2 1 3 := by decide
57theorem e_230220 : m2Num 2 3 0 2 2 0 = 8 * explicitZ 2 3 0 2 2 0 := by decide
58theorem e_230221 : m2Num 2 3 0 2 2 1 = 8 * explicitZ 2 3 0 2 2 1 := by decide
59theorem e_230222 : m2Num 2 3 0 2 2 2 = 8 * explicitZ 2 3 0 2 2 2 := by decide
60theorem e_230223 : m2Num 2 3 0 2 2 3 = 8 * explicitZ 2 3 0 2 2 3 := by decide
61theorem e_230230 : m2Num 2 3 0 2 3 0 = 8 * explicitZ 2 3 0 2 3 0 := by decide
62theorem e_230231 : m2Num 2 3 0 2 3 1 = 8 * explicitZ 2 3 0 2 3 1 := by decide
63theorem e_230232 : m2Num 2 3 0 2 3 2 = 8 * explicitZ 2 3 0 2 3 2 := by decide
64theorem e_230233 : m2Num 2 3 0 2 3 3 = 8 * explicitZ 2 3 0 2 3 3 := by decide
65theorem e_230300 : m2Num 2 3 0 3 0 0 = 8 * explicitZ 2 3 0 3 0 0 := by decide
66theorem e_230301 : m2Num 2 3 0 3 0 1 = 8 * explicitZ 2 3 0 3 0 1 := by decide
67theorem e_230302 : m2Num 2 3 0 3 0 2 = 8 * explicitZ 2 3 0 3 0 2 := by decide
68theorem e_230303 : m2Num 2 3 0 3 0 3 = 8 * explicitZ 2 3 0 3 0 3 := by decide
69theorem e_230310 : m2Num 2 3 0 3 1 0 = 8 * explicitZ 2 3 0 3 1 0 := by decide
70theorem e_230311 : m2Num 2 3 0 3 1 1 = 8 * explicitZ 2 3 0 3 1 1 := by decide
71theorem e_230312 : m2Num 2 3 0 3 1 2 = 8 * explicitZ 2 3 0 3 1 2 := by decide
72theorem e_230313 : m2Num 2 3 0 3 1 3 = 8 * explicitZ 2 3 0 3 1 3 := by decide
73theorem e_230320 : m2Num 2 3 0 3 2 0 = 8 * explicitZ 2 3 0 3 2 0 := by decide
74theorem e_230321 : m2Num 2 3 0 3 2 1 = 8 * explicitZ 2 3 0 3 2 1 := by decide
75theorem e_230322 : m2Num 2 3 0 3 2 2 = 8 * explicitZ 2 3 0 3 2 2 := by decide
76theorem e_230323 : m2Num 2 3 0 3 2 3 = 8 * explicitZ 2 3 0 3 2 3 := by decide
77theorem e_230330 : m2Num 2 3 0 3 3 0 = 8 * explicitZ 2 3 0 3 3 0 := by decide
78theorem e_230331 : m2Num 2 3 0 3 3 1 = 8 * explicitZ 2 3 0 3 3 1 := by decide
79theorem e_230332 : m2Num 2 3 0 3 3 2 = 8 * explicitZ 2 3 0 3 3 2 := by decide
80theorem e_230333 : m2Num 2 3 0 3 3 3 = 8 * explicitZ 2 3 0 3 3 3 := by decide
81theorem e_231000 : m2Num 2 3 1 0 0 0 = 8 * explicitZ 2 3 1 0 0 0 := by decide
82theorem e_231001 : m2Num 2 3 1 0 0 1 = 8 * explicitZ 2 3 1 0 0 1 := by decide
83theorem e_231002 : m2Num 2 3 1 0 0 2 = 8 * explicitZ 2 3 1 0 0 2 := by decide
84theorem e_231003 : m2Num 2 3 1 0 0 3 = 8 * explicitZ 2 3 1 0 0 3 := by decide
85theorem e_231010 : m2Num 2 3 1 0 1 0 = 8 * explicitZ 2 3 1 0 1 0 := by decide
86theorem e_231011 : m2Num 2 3 1 0 1 1 = 8 * explicitZ 2 3 1 0 1 1 := by decide
87theorem e_231012 : m2Num 2 3 1 0 1 2 = 8 * explicitZ 2 3 1 0 1 2 := by decide
88theorem e_231013 : m2Num 2 3 1 0 1 3 = 8 * explicitZ 2 3 1 0 1 3 := by decide
89theorem e_231020 : m2Num 2 3 1 0 2 0 = 8 * explicitZ 2 3 1 0 2 0 := by decide
90theorem e_231021 : m2Num 2 3 1 0 2 1 = 8 * explicitZ 2 3 1 0 2 1 := by decide
91theorem e_231022 : m2Num 2 3 1 0 2 2 = 8 * explicitZ 2 3 1 0 2 2 := by decide
92theorem e_231023 : m2Num 2 3 1 0 2 3 = 8 * explicitZ 2 3 1 0 2 3 := by decide
93theorem e_231030 : m2Num 2 3 1 0 3 0 = 8 * explicitZ 2 3 1 0 3 0 := by decide
94theorem e_231031 : m2Num 2 3 1 0 3 1 = 8 * explicitZ 2 3 1 0 3 1 := by decide
95theorem e_231032 : m2Num 2 3 1 0 3 2 = 8 * explicitZ 2 3 1 0 3 2 := by decide
96theorem e_231033 : m2Num 2 3 1 0 3 3 = 8 * explicitZ 2 3 1 0 3 3 := by decide
97theorem e_231100 : m2Num 2 3 1 1 0 0 = 8 * explicitZ 2 3 1 1 0 0 := by decide
98theorem e_231101 : m2Num 2 3 1 1 0 1 = 8 * explicitZ 2 3 1 1 0 1 := by decide
99theorem e_231102 : m2Num 2 3 1 1 0 2 = 8 * explicitZ 2 3 1 1 0 2 := by decide
100theorem e_231103 : m2Num 2 3 1 1 0 3 = 8 * explicitZ 2 3 1 1 0 3 := by decide
101theorem e_231110 : m2Num 2 3 1 1 1 0 = 8 * explicitZ 2 3 1 1 1 0 := by decide
102theorem e_231111 : m2Num 2 3 1 1 1 1 = 8 * explicitZ 2 3 1 1 1 1 := by decide
103theorem e_231112 : m2Num 2 3 1 1 1 2 = 8 * explicitZ 2 3 1 1 1 2 := by decide
104theorem e_231113 : m2Num 2 3 1 1 1 3 = 8 * explicitZ 2 3 1 1 1 3 := by decide
105theorem e_231120 : m2Num 2 3 1 1 2 0 = 8 * explicitZ 2 3 1 1 2 0 := by decide
106theorem e_231121 : m2Num 2 3 1 1 2 1 = 8 * explicitZ 2 3 1 1 2 1 := by decide
107theorem e_231122 : m2Num 2 3 1 1 2 2 = 8 * explicitZ 2 3 1 1 2 2 := by decide
108theorem e_231123 : m2Num 2 3 1 1 2 3 = 8 * explicitZ 2 3 1 1 2 3 := by decide
109theorem e_231130 : m2Num 2 3 1 1 3 0 = 8 * explicitZ 2 3 1 1 3 0 := by decide
110theorem e_231131 : m2Num 2 3 1 1 3 1 = 8 * explicitZ 2 3 1 1 3 1 := by decide
111theorem e_231132 : m2Num 2 3 1 1 3 2 = 8 * explicitZ 2 3 1 1 3 2 := by decide
112theorem e_231133 : m2Num 2 3 1 1 3 3 = 8 * explicitZ 2 3 1 1 3 3 := by decide
113theorem e_231200 : m2Num 2 3 1 2 0 0 = 8 * explicitZ 2 3 1 2 0 0 := by decide
114theorem e_231201 : m2Num 2 3 1 2 0 1 = 8 * explicitZ 2 3 1 2 0 1 := by decide
115theorem e_231202 : m2Num 2 3 1 2 0 2 = 8 * explicitZ 2 3 1 2 0 2 := by decide
116theorem e_231203 : m2Num 2 3 1 2 0 3 = 8 * explicitZ 2 3 1 2 0 3 := by decide
117theorem e_231210 : m2Num 2 3 1 2 1 0 = 8 * explicitZ 2 3 1 2 1 0 := by decide
118theorem e_231211 : m2Num 2 3 1 2 1 1 = 8 * explicitZ 2 3 1 2 1 1 := by decide
119theorem e_231212 : m2Num 2 3 1 2 1 2 = 8 * explicitZ 2 3 1 2 1 2 := by decide
120theorem e_231213 : m2Num 2 3 1 2 1 3 = 8 * explicitZ 2 3 1 2 1 3 := by decide
121theorem e_231220 : m2Num 2 3 1 2 2 0 = 8 * explicitZ 2 3 1 2 2 0 := by decide
122theorem e_231221 : m2Num 2 3 1 2 2 1 = 8 * explicitZ 2 3 1 2 2 1 := by decide
123theorem e_231222 : m2Num 2 3 1 2 2 2 = 8 * explicitZ 2 3 1 2 2 2 := by decide
124theorem e_231223 : m2Num 2 3 1 2 2 3 = 8 * explicitZ 2 3 1 2 2 3 := by decide
125theorem e_231230 : m2Num 2 3 1 2 3 0 = 8 * explicitZ 2 3 1 2 3 0 := by decide
126theorem e_231231 : m2Num 2 3 1 2 3 1 = 8 * explicitZ 2 3 1 2 3 1 := by decide
127theorem e_231232 : m2Num 2 3 1 2 3 2 = 8 * explicitZ 2 3 1 2 3 2 := by decide
128theorem e_231233 : m2Num 2 3 1 2 3 3 = 8 * explicitZ 2 3 1 2 3 3 := by decide
129theorem e_231300 : m2Num 2 3 1 3 0 0 = 8 * explicitZ 2 3 1 3 0 0 := by decide
130theorem e_231301 : m2Num 2 3 1 3 0 1 = 8 * explicitZ 2 3 1 3 0 1 := by decide
131theorem e_231302 : m2Num 2 3 1 3 0 2 = 8 * explicitZ 2 3 1 3 0 2 := by decide
132theorem e_231303 : m2Num 2 3 1 3 0 3 = 8 * explicitZ 2 3 1 3 0 3 := by decide
133theorem e_231310 : m2Num 2 3 1 3 1 0 = 8 * explicitZ 2 3 1 3 1 0 := by decide
134theorem e_231311 : m2Num 2 3 1 3 1 1 = 8 * explicitZ 2 3 1 3 1 1 := by decide
135theorem e_231312 : m2Num 2 3 1 3 1 2 = 8 * explicitZ 2 3 1 3 1 2 := by decide
136theorem e_231313 : m2Num 2 3 1 3 1 3 = 8 * explicitZ 2 3 1 3 1 3 := by decide
137theorem e_231320 : m2Num 2 3 1 3 2 0 = 8 * explicitZ 2 3 1 3 2 0 := by decide
138theorem e_231321 : m2Num 2 3 1 3 2 1 = 8 * explicitZ 2 3 1 3 2 1 := by decide
139theorem e_231322 : m2Num 2 3 1 3 2 2 = 8 * explicitZ 2 3 1 3 2 2 := by decide
140theorem e_231323 : m2Num 2 3 1 3 2 3 = 8 * explicitZ 2 3 1 3 2 3 := by decide
141theorem e_231330 : m2Num 2 3 1 3 3 0 = 8 * explicitZ 2 3 1 3 3 0 := by decide
142theorem e_231331 : m2Num 2 3 1 3 3 1 = 8 * explicitZ 2 3 1 3 3 1 := by decide
143theorem e_231332 : m2Num 2 3 1 3 3 2 = 8 * explicitZ 2 3 1 3 3 2 := by decide
144theorem e_231333 : m2Num 2 3 1 3 3 3 = 8 * explicitZ 2 3 1 3 3 3 := by decide
145theorem e_232000 : m2Num 2 3 2 0 0 0 = 8 * explicitZ 2 3 2 0 0 0 := by decide
146theorem e_232001 : m2Num 2 3 2 0 0 1 = 8 * explicitZ 2 3 2 0 0 1 := by decide
147theorem e_232002 : m2Num 2 3 2 0 0 2 = 8 * explicitZ 2 3 2 0 0 2 := by decide
148theorem e_232003 : m2Num 2 3 2 0 0 3 = 8 * explicitZ 2 3 2 0 0 3 := by decide
149theorem e_232010 : m2Num 2 3 2 0 1 0 = 8 * explicitZ 2 3 2 0 1 0 := by decide
150theorem e_232011 : m2Num 2 3 2 0 1 1 = 8 * explicitZ 2 3 2 0 1 1 := by decide
151theorem e_232012 : m2Num 2 3 2 0 1 2 = 8 * explicitZ 2 3 2 0 1 2 := by decide
152theorem e_232013 : m2Num 2 3 2 0 1 3 = 8 * explicitZ 2 3 2 0 1 3 := by decide
153theorem e_232020 : m2Num 2 3 2 0 2 0 = 8 * explicitZ 2 3 2 0 2 0 := by decide
154theorem e_232021 : m2Num 2 3 2 0 2 1 = 8 * explicitZ 2 3 2 0 2 1 := by decide
155theorem e_232022 : m2Num 2 3 2 0 2 2 = 8 * explicitZ 2 3 2 0 2 2 := by decide
156theorem e_232023 : m2Num 2 3 2 0 2 3 = 8 * explicitZ 2 3 2 0 2 3 := by decide
157theorem e_232030 : m2Num 2 3 2 0 3 0 = 8 * explicitZ 2 3 2 0 3 0 := by decide
158theorem e_232031 : m2Num 2 3 2 0 3 1 = 8 * explicitZ 2 3 2 0 3 1 := by decide
159theorem e_232032 : m2Num 2 3 2 0 3 2 = 8 * explicitZ 2 3 2 0 3 2 := by decide
160theorem e_232033 : m2Num 2 3 2 0 3 3 = 8 * explicitZ 2 3 2 0 3 3 := by decide
161theorem e_232100 : m2Num 2 3 2 1 0 0 = 8 * explicitZ 2 3 2 1 0 0 := by decide
162theorem e_232101 : m2Num 2 3 2 1 0 1 = 8 * explicitZ 2 3 2 1 0 1 := by decide
163theorem e_232102 : m2Num 2 3 2 1 0 2 = 8 * explicitZ 2 3 2 1 0 2 := by decide
164theorem e_232103 : m2Num 2 3 2 1 0 3 = 8 * explicitZ 2 3 2 1 0 3 := by decide
165theorem e_232110 : m2Num 2 3 2 1 1 0 = 8 * explicitZ 2 3 2 1 1 0 := by decide
166theorem e_232111 : m2Num 2 3 2 1 1 1 = 8 * explicitZ 2 3 2 1 1 1 := by decide
167theorem e_232112 : m2Num 2 3 2 1 1 2 = 8 * explicitZ 2 3 2 1 1 2 := by decide
168theorem e_232113 : m2Num 2 3 2 1 1 3 = 8 * explicitZ 2 3 2 1 1 3 := by decide
169theorem e_232120 : m2Num 2 3 2 1 2 0 = 8 * explicitZ 2 3 2 1 2 0 := by decide
170theorem e_232121 : m2Num 2 3 2 1 2 1 = 8 * explicitZ 2 3 2 1 2 1 := by decide
171theorem e_232122 : m2Num 2 3 2 1 2 2 = 8 * explicitZ 2 3 2 1 2 2 := by decide
172theorem e_232123 : m2Num 2 3 2 1 2 3 = 8 * explicitZ 2 3 2 1 2 3 := by decide
173theorem e_232130 : m2Num 2 3 2 1 3 0 = 8 * explicitZ 2 3 2 1 3 0 := by decide
174theorem e_232131 : m2Num 2 3 2 1 3 1 = 8 * explicitZ 2 3 2 1 3 1 := by decide
175theorem e_232132 : m2Num 2 3 2 1 3 2 = 8 * explicitZ 2 3 2 1 3 2 := by decide
176theorem e_232133 : m2Num 2 3 2 1 3 3 = 8 * explicitZ 2 3 2 1 3 3 := by decide
177theorem e_232200 : m2Num 2 3 2 2 0 0 = 8 * explicitZ 2 3 2 2 0 0 := by decide
178theorem e_232201 : m2Num 2 3 2 2 0 1 = 8 * explicitZ 2 3 2 2 0 1 := by decide
179theorem e_232202 : m2Num 2 3 2 2 0 2 = 8 * explicitZ 2 3 2 2 0 2 := by decide
180theorem e_232203 : m2Num 2 3 2 2 0 3 = 8 * explicitZ 2 3 2 2 0 3 := by decide
181theorem e_232210 : m2Num 2 3 2 2 1 0 = 8 * explicitZ 2 3 2 2 1 0 := by decide
182theorem e_232211 : m2Num 2 3 2 2 1 1 = 8 * explicitZ 2 3 2 2 1 1 := by decide
183theorem e_232212 : m2Num 2 3 2 2 1 2 = 8 * explicitZ 2 3 2 2 1 2 := by decide
184theorem e_232213 : m2Num 2 3 2 2 1 3 = 8 * explicitZ 2 3 2 2 1 3 := by decide
185theorem e_232220 : m2Num 2 3 2 2 2 0 = 8 * explicitZ 2 3 2 2 2 0 := by decide
186theorem e_232221 : m2Num 2 3 2 2 2 1 = 8 * explicitZ 2 3 2 2 2 1 := by decide
187theorem e_232222 : m2Num 2 3 2 2 2 2 = 8 * explicitZ 2 3 2 2 2 2 := by decide
188theorem e_232223 : m2Num 2 3 2 2 2 3 = 8 * explicitZ 2 3 2 2 2 3 := by decide
189theorem e_232230 : m2Num 2 3 2 2 3 0 = 8 * explicitZ 2 3 2 2 3 0 := by decide
190theorem e_232231 : m2Num 2 3 2 2 3 1 = 8 * explicitZ 2 3 2 2 3 1 := by decide
191theorem e_232232 : m2Num 2 3 2 2 3 2 = 8 * explicitZ 2 3 2 2 3 2 := by decide
192theorem e_232233 : m2Num 2 3 2 2 3 3 = 8 * explicitZ 2 3 2 2 3 3 := by decide
193theorem e_232300 : m2Num 2 3 2 3 0 0 = 8 * explicitZ 2 3 2 3 0 0 := by decide
194theorem e_232301 : m2Num 2 3 2 3 0 1 = 8 * explicitZ 2 3 2 3 0 1 := by decide
195theorem e_232302 : m2Num 2 3 2 3 0 2 = 8 * explicitZ 2 3 2 3 0 2 := by decide
196theorem e_232303 : m2Num 2 3 2 3 0 3 = 8 * explicitZ 2 3 2 3 0 3 := by decide
197theorem e_232310 : m2Num 2 3 2 3 1 0 = 8 * explicitZ 2 3 2 3 1 0 := by decide
198theorem e_232311 : m2Num 2 3 2 3 1 1 = 8 * explicitZ 2 3 2 3 1 1 := by decide
199theorem e_232312 : m2Num 2 3 2 3 1 2 = 8 * explicitZ 2 3 2 3 1 2 := by decide
200theorem e_232313 : m2Num 2 3 2 3 1 3 = 8 * explicitZ 2 3 2 3 1 3 := by decide
201theorem e_232320 : m2Num 2 3 2 3 2 0 = 8 * explicitZ 2 3 2 3 2 0 := by decide
202theorem e_232321 : m2Num 2 3 2 3 2 1 = 8 * explicitZ 2 3 2 3 2 1 := by decide
203theorem e_232322 : m2Num 2 3 2 3 2 2 = 8 * explicitZ 2 3 2 3 2 2 := by decide
204theorem e_232323 : m2Num 2 3 2 3 2 3 = 8 * explicitZ 2 3 2 3 2 3 := by decide
205theorem e_232330 : m2Num 2 3 2 3 3 0 = 8 * explicitZ 2 3 2 3 3 0 := by decide
206theorem e_232331 : m2Num 2 3 2 3 3 1 = 8 * explicitZ 2 3 2 3 3 1 := by decide
207theorem e_232332 : m2Num 2 3 2 3 3 2 = 8 * explicitZ 2 3 2 3 3 2 := by decide
208theorem e_232333 : m2Num 2 3 2 3 3 3 = 8 * explicitZ 2 3 2 3 3 3 := by decide
209theorem e_233000 : m2Num 2 3 3 0 0 0 = 8 * explicitZ 2 3 3 0 0 0 := by decide
210theorem e_233001 : m2Num 2 3 3 0 0 1 = 8 * explicitZ 2 3 3 0 0 1 := by decide
211theorem e_233002 : m2Num 2 3 3 0 0 2 = 8 * explicitZ 2 3 3 0 0 2 := by decide
212theorem e_233003 : m2Num 2 3 3 0 0 3 = 8 * explicitZ 2 3 3 0 0 3 := by decide
213theorem e_233010 : m2Num 2 3 3 0 1 0 = 8 * explicitZ 2 3 3 0 1 0 := by decide
214theorem e_233011 : m2Num 2 3 3 0 1 1 = 8 * explicitZ 2 3 3 0 1 1 := by decide
215theorem e_233012 : m2Num 2 3 3 0 1 2 = 8 * explicitZ 2 3 3 0 1 2 := by decide
216theorem e_233013 : m2Num 2 3 3 0 1 3 = 8 * explicitZ 2 3 3 0 1 3 := by decide
217theorem e_233020 : m2Num 2 3 3 0 2 0 = 8 * explicitZ 2 3 3 0 2 0 := by decide
218theorem e_233021 : m2Num 2 3 3 0 2 1 = 8 * explicitZ 2 3 3 0 2 1 := by decide
219theorem e_233022 : m2Num 2 3 3 0 2 2 = 8 * explicitZ 2 3 3 0 2 2 := by decide
220theorem e_233023 : m2Num 2 3 3 0 2 3 = 8 * explicitZ 2 3 3 0 2 3 := by decide
221theorem e_233030 : m2Num 2 3 3 0 3 0 = 8 * explicitZ 2 3 3 0 3 0 := by decide
222theorem e_233031 : m2Num 2 3 3 0 3 1 = 8 * explicitZ 2 3 3 0 3 1 := by decide
223theorem e_233032 : m2Num 2 3 3 0 3 2 = 8 * explicitZ 2 3 3 0 3 2 := by decide
224theorem e_233033 : m2Num 2 3 3 0 3 3 = 8 * explicitZ 2 3 3 0 3 3 := by decide
225theorem e_233100 : m2Num 2 3 3 1 0 0 = 8 * explicitZ 2 3 3 1 0 0 := by decide
226theorem e_233101 : m2Num 2 3 3 1 0 1 = 8 * explicitZ 2 3 3 1 0 1 := by decide
227theorem e_233102 : m2Num 2 3 3 1 0 2 = 8 * explicitZ 2 3 3 1 0 2 := by decide
228theorem e_233103 : m2Num 2 3 3 1 0 3 = 8 * explicitZ 2 3 3 1 0 3 := by decide
229theorem e_233110 : m2Num 2 3 3 1 1 0 = 8 * explicitZ 2 3 3 1 1 0 := by decide
230theorem e_233111 : m2Num 2 3 3 1 1 1 = 8 * explicitZ 2 3 3 1 1 1 := by decide
231theorem e_233112 : m2Num 2 3 3 1 1 2 = 8 * explicitZ 2 3 3 1 1 2 := by decide
232theorem e_233113 : m2Num 2 3 3 1 1 3 = 8 * explicitZ 2 3 3 1 1 3 := by decide
233theorem e_233120 : m2Num 2 3 3 1 2 0 = 8 * explicitZ 2 3 3 1 2 0 := by decide
234theorem e_233121 : m2Num 2 3 3 1 2 1 = 8 * explicitZ 2 3 3 1 2 1 := by decide
235theorem e_233122 : m2Num 2 3 3 1 2 2 = 8 * explicitZ 2 3 3 1 2 2 := by decide
236theorem e_233123 : m2Num 2 3 3 1 2 3 = 8 * explicitZ 2 3 3 1 2 3 := by decide
237theorem e_233130 : m2Num 2 3 3 1 3 0 = 8 * explicitZ 2 3 3 1 3 0 := by decide
238theorem e_233131 : m2Num 2 3 3 1 3 1 = 8 * explicitZ 2 3 3 1 3 1 := by decide
239theorem e_233132 : m2Num 2 3 3 1 3 2 = 8 * explicitZ 2 3 3 1 3 2 := by decide
240theorem e_233133 : m2Num 2 3 3 1 3 3 = 8 * explicitZ 2 3 3 1 3 3 := by decide
241theorem e_233200 : m2Num 2 3 3 2 0 0 = 8 * explicitZ 2 3 3 2 0 0 := by decide
242theorem e_233201 : m2Num 2 3 3 2 0 1 = 8 * explicitZ 2 3 3 2 0 1 := by decide
243theorem e_233202 : m2Num 2 3 3 2 0 2 = 8 * explicitZ 2 3 3 2 0 2 := by decide
244theorem e_233203 : m2Num 2 3 3 2 0 3 = 8 * explicitZ 2 3 3 2 0 3 := by decide
245theorem e_233210 : m2Num 2 3 3 2 1 0 = 8 * explicitZ 2 3 3 2 1 0 := by decide
246theorem e_233211 : m2Num 2 3 3 2 1 1 = 8 * explicitZ 2 3 3 2 1 1 := by decide
247theorem e_233212 : m2Num 2 3 3 2 1 2 = 8 * explicitZ 2 3 3 2 1 2 := by decide
248theorem e_233213 : m2Num 2 3 3 2 1 3 = 8 * explicitZ 2 3 3 2 1 3 := by decide
249theorem e_233220 : m2Num 2 3 3 2 2 0 = 8 * explicitZ 2 3 3 2 2 0 := by decide
250theorem e_233221 : m2Num 2 3 3 2 2 1 = 8 * explicitZ 2 3 3 2 2 1 := by decide
251theorem e_233222 : m2Num 2 3 3 2 2 2 = 8 * explicitZ 2 3 3 2 2 2 := by decide
252theorem e_233223 : m2Num 2 3 3 2 2 3 = 8 * explicitZ 2 3 3 2 2 3 := by decide
253theorem e_233230 : m2Num 2 3 3 2 3 0 = 8 * explicitZ 2 3 3 2 3 0 := by decide
254theorem e_233231 : m2Num 2 3 3 2 3 1 = 8 * explicitZ 2 3 3 2 3 1 := by decide
255theorem e_233232 : m2Num 2 3 3 2 3 2 = 8 * explicitZ 2 3 3 2 3 2 := by decide
256theorem e_233233 : m2Num 2 3 3 2 3 3 = 8 * explicitZ 2 3 3 2 3 3 := by decide
257theorem e_233300 : m2Num 2 3 3 3 0 0 = 8 * explicitZ 2 3 3 3 0 0 := by decide
258theorem e_233301 : m2Num 2 3 3 3 0 1 = 8 * explicitZ 2 3 3 3 0 1 := by decide
259theorem e_233302 : m2Num 2 3 3 3 0 2 = 8 * explicitZ 2 3 3 3 0 2 := by decide
260theorem e_233303 : m2Num 2 3 3 3 0 3 = 8 * explicitZ 2 3 3 3 0 3 := by decide
261theorem e_233310 : m2Num 2 3 3 3 1 0 = 8 * explicitZ 2 3 3 3 1 0 := by decide
262theorem e_233311 : m2Num 2 3 3 3 1 1 = 8 * explicitZ 2 3 3 3 1 1 := by decide
263theorem e_233312 : m2Num 2 3 3 3 1 2 = 8 * explicitZ 2 3 3 3 1 2 := by decide
264theorem e_233313 : m2Num 2 3 3 3 1 3 = 8 * explicitZ 2 3 3 3 1 3 := by decide
265theorem e_233320 : m2Num 2 3 3 3 2 0 = 8 * explicitZ 2 3 3 3 2 0 := by decide
266theorem e_233321 : m2Num 2 3 3 3 2 1 = 8 * explicitZ 2 3 3 3 2 1 := by decide
267theorem e_233322 : m2Num 2 3 3 3 2 2 = 8 * explicitZ 2 3 3 3 2 2 := by decide
268theorem e_233323 : m2Num 2 3 3 3 2 3 = 8 * explicitZ 2 3 3 3 2 3 := by decide
269theorem e_233330 : m2Num 2 3 3 3 3 0 = 8 * explicitZ 2 3 3 3 3 0 := by decide
270theorem e_233331 : m2Num 2 3 3 3 3 1 = 8 * explicitZ 2 3 3 3 3 1 := by decide
271theorem e_233332 : m2Num 2 3 3 3 3 2 = 8 * explicitZ 2 3 3 3 3 2 := by decide
272theorem e_233333 : m2Num 2 3 3 3 3 3 = 8 * explicitZ 2 3 3 3 3 3 := by decide
273
274end M2NumChunk11
275end ReggeExactMidpointM2TTIdentity4D
276end Analysis
277end Gravity
278end IndisputableMonolith
279