IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DM2NumChunk12
IndisputableMonolith/Gravity/Analysis/ReggeExactMidpointM2TTIdentity4DM2NumChunk12.lean · 279 lines · 256 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DKernelCert
3
4/-! m2Num = 8·explicitZ, chunk 12 (256 kernel decides). -/
5
6namespace IndisputableMonolith
7namespace Gravity
8namespace Analysis
9namespace ReggeExactMidpointM2TTIdentity4D
10namespace M2NumChunk12
11
12open KernelCert
13
14set_option maxRecDepth 100000
15set_option maxHeartbeats 200000000
16
17theorem e_300000 : m2Num 3 0 0 0 0 0 = 8 * explicitZ 3 0 0 0 0 0 := by decide
18theorem e_300001 : m2Num 3 0 0 0 0 1 = 8 * explicitZ 3 0 0 0 0 1 := by decide
19theorem e_300002 : m2Num 3 0 0 0 0 2 = 8 * explicitZ 3 0 0 0 0 2 := by decide
20theorem e_300003 : m2Num 3 0 0 0 0 3 = 8 * explicitZ 3 0 0 0 0 3 := by decide
21theorem e_300010 : m2Num 3 0 0 0 1 0 = 8 * explicitZ 3 0 0 0 1 0 := by decide
22theorem e_300011 : m2Num 3 0 0 0 1 1 = 8 * explicitZ 3 0 0 0 1 1 := by decide
23theorem e_300012 : m2Num 3 0 0 0 1 2 = 8 * explicitZ 3 0 0 0 1 2 := by decide
24theorem e_300013 : m2Num 3 0 0 0 1 3 = 8 * explicitZ 3 0 0 0 1 3 := by decide
25theorem e_300020 : m2Num 3 0 0 0 2 0 = 8 * explicitZ 3 0 0 0 2 0 := by decide
26theorem e_300021 : m2Num 3 0 0 0 2 1 = 8 * explicitZ 3 0 0 0 2 1 := by decide
27theorem e_300022 : m2Num 3 0 0 0 2 2 = 8 * explicitZ 3 0 0 0 2 2 := by decide
28theorem e_300023 : m2Num 3 0 0 0 2 3 = 8 * explicitZ 3 0 0 0 2 3 := by decide
29theorem e_300030 : m2Num 3 0 0 0 3 0 = 8 * explicitZ 3 0 0 0 3 0 := by decide
30theorem e_300031 : m2Num 3 0 0 0 3 1 = 8 * explicitZ 3 0 0 0 3 1 := by decide
31theorem e_300032 : m2Num 3 0 0 0 3 2 = 8 * explicitZ 3 0 0 0 3 2 := by decide
32theorem e_300033 : m2Num 3 0 0 0 3 3 = 8 * explicitZ 3 0 0 0 3 3 := by decide
33theorem e_300100 : m2Num 3 0 0 1 0 0 = 8 * explicitZ 3 0 0 1 0 0 := by decide
34theorem e_300101 : m2Num 3 0 0 1 0 1 = 8 * explicitZ 3 0 0 1 0 1 := by decide
35theorem e_300102 : m2Num 3 0 0 1 0 2 = 8 * explicitZ 3 0 0 1 0 2 := by decide
36theorem e_300103 : m2Num 3 0 0 1 0 3 = 8 * explicitZ 3 0 0 1 0 3 := by decide
37theorem e_300110 : m2Num 3 0 0 1 1 0 = 8 * explicitZ 3 0 0 1 1 0 := by decide
38theorem e_300111 : m2Num 3 0 0 1 1 1 = 8 * explicitZ 3 0 0 1 1 1 := by decide
39theorem e_300112 : m2Num 3 0 0 1 1 2 = 8 * explicitZ 3 0 0 1 1 2 := by decide
40theorem e_300113 : m2Num 3 0 0 1 1 3 = 8 * explicitZ 3 0 0 1 1 3 := by decide
41theorem e_300120 : m2Num 3 0 0 1 2 0 = 8 * explicitZ 3 0 0 1 2 0 := by decide
42theorem e_300121 : m2Num 3 0 0 1 2 1 = 8 * explicitZ 3 0 0 1 2 1 := by decide
43theorem e_300122 : m2Num 3 0 0 1 2 2 = 8 * explicitZ 3 0 0 1 2 2 := by decide
44theorem e_300123 : m2Num 3 0 0 1 2 3 = 8 * explicitZ 3 0 0 1 2 3 := by decide
45theorem e_300130 : m2Num 3 0 0 1 3 0 = 8 * explicitZ 3 0 0 1 3 0 := by decide
46theorem e_300131 : m2Num 3 0 0 1 3 1 = 8 * explicitZ 3 0 0 1 3 1 := by decide
47theorem e_300132 : m2Num 3 0 0 1 3 2 = 8 * explicitZ 3 0 0 1 3 2 := by decide
48theorem e_300133 : m2Num 3 0 0 1 3 3 = 8 * explicitZ 3 0 0 1 3 3 := by decide
49theorem e_300200 : m2Num 3 0 0 2 0 0 = 8 * explicitZ 3 0 0 2 0 0 := by decide
50theorem e_300201 : m2Num 3 0 0 2 0 1 = 8 * explicitZ 3 0 0 2 0 1 := by decide
51theorem e_300202 : m2Num 3 0 0 2 0 2 = 8 * explicitZ 3 0 0 2 0 2 := by decide
52theorem e_300203 : m2Num 3 0 0 2 0 3 = 8 * explicitZ 3 0 0 2 0 3 := by decide
53theorem e_300210 : m2Num 3 0 0 2 1 0 = 8 * explicitZ 3 0 0 2 1 0 := by decide
54theorem e_300211 : m2Num 3 0 0 2 1 1 = 8 * explicitZ 3 0 0 2 1 1 := by decide
55theorem e_300212 : m2Num 3 0 0 2 1 2 = 8 * explicitZ 3 0 0 2 1 2 := by decide
56theorem e_300213 : m2Num 3 0 0 2 1 3 = 8 * explicitZ 3 0 0 2 1 3 := by decide
57theorem e_300220 : m2Num 3 0 0 2 2 0 = 8 * explicitZ 3 0 0 2 2 0 := by decide
58theorem e_300221 : m2Num 3 0 0 2 2 1 = 8 * explicitZ 3 0 0 2 2 1 := by decide
59theorem e_300222 : m2Num 3 0 0 2 2 2 = 8 * explicitZ 3 0 0 2 2 2 := by decide
60theorem e_300223 : m2Num 3 0 0 2 2 3 = 8 * explicitZ 3 0 0 2 2 3 := by decide
61theorem e_300230 : m2Num 3 0 0 2 3 0 = 8 * explicitZ 3 0 0 2 3 0 := by decide
62theorem e_300231 : m2Num 3 0 0 2 3 1 = 8 * explicitZ 3 0 0 2 3 1 := by decide
63theorem e_300232 : m2Num 3 0 0 2 3 2 = 8 * explicitZ 3 0 0 2 3 2 := by decide
64theorem e_300233 : m2Num 3 0 0 2 3 3 = 8 * explicitZ 3 0 0 2 3 3 := by decide
65theorem e_300300 : m2Num 3 0 0 3 0 0 = 8 * explicitZ 3 0 0 3 0 0 := by decide
66theorem e_300301 : m2Num 3 0 0 3 0 1 = 8 * explicitZ 3 0 0 3 0 1 := by decide
67theorem e_300302 : m2Num 3 0 0 3 0 2 = 8 * explicitZ 3 0 0 3 0 2 := by decide
68theorem e_300303 : m2Num 3 0 0 3 0 3 = 8 * explicitZ 3 0 0 3 0 3 := by decide
69theorem e_300310 : m2Num 3 0 0 3 1 0 = 8 * explicitZ 3 0 0 3 1 0 := by decide
70theorem e_300311 : m2Num 3 0 0 3 1 1 = 8 * explicitZ 3 0 0 3 1 1 := by decide
71theorem e_300312 : m2Num 3 0 0 3 1 2 = 8 * explicitZ 3 0 0 3 1 2 := by decide
72theorem e_300313 : m2Num 3 0 0 3 1 3 = 8 * explicitZ 3 0 0 3 1 3 := by decide
73theorem e_300320 : m2Num 3 0 0 3 2 0 = 8 * explicitZ 3 0 0 3 2 0 := by decide
74theorem e_300321 : m2Num 3 0 0 3 2 1 = 8 * explicitZ 3 0 0 3 2 1 := by decide
75theorem e_300322 : m2Num 3 0 0 3 2 2 = 8 * explicitZ 3 0 0 3 2 2 := by decide
76theorem e_300323 : m2Num 3 0 0 3 2 3 = 8 * explicitZ 3 0 0 3 2 3 := by decide
77theorem e_300330 : m2Num 3 0 0 3 3 0 = 8 * explicitZ 3 0 0 3 3 0 := by decide
78theorem e_300331 : m2Num 3 0 0 3 3 1 = 8 * explicitZ 3 0 0 3 3 1 := by decide
79theorem e_300332 : m2Num 3 0 0 3 3 2 = 8 * explicitZ 3 0 0 3 3 2 := by decide
80theorem e_300333 : m2Num 3 0 0 3 3 3 = 8 * explicitZ 3 0 0 3 3 3 := by decide
81theorem e_301000 : m2Num 3 0 1 0 0 0 = 8 * explicitZ 3 0 1 0 0 0 := by decide
82theorem e_301001 : m2Num 3 0 1 0 0 1 = 8 * explicitZ 3 0 1 0 0 1 := by decide
83theorem e_301002 : m2Num 3 0 1 0 0 2 = 8 * explicitZ 3 0 1 0 0 2 := by decide
84theorem e_301003 : m2Num 3 0 1 0 0 3 = 8 * explicitZ 3 0 1 0 0 3 := by decide
85theorem e_301010 : m2Num 3 0 1 0 1 0 = 8 * explicitZ 3 0 1 0 1 0 := by decide
86theorem e_301011 : m2Num 3 0 1 0 1 1 = 8 * explicitZ 3 0 1 0 1 1 := by decide
87theorem e_301012 : m2Num 3 0 1 0 1 2 = 8 * explicitZ 3 0 1 0 1 2 := by decide
88theorem e_301013 : m2Num 3 0 1 0 1 3 = 8 * explicitZ 3 0 1 0 1 3 := by decide
89theorem e_301020 : m2Num 3 0 1 0 2 0 = 8 * explicitZ 3 0 1 0 2 0 := by decide
90theorem e_301021 : m2Num 3 0 1 0 2 1 = 8 * explicitZ 3 0 1 0 2 1 := by decide
91theorem e_301022 : m2Num 3 0 1 0 2 2 = 8 * explicitZ 3 0 1 0 2 2 := by decide
92theorem e_301023 : m2Num 3 0 1 0 2 3 = 8 * explicitZ 3 0 1 0 2 3 := by decide
93theorem e_301030 : m2Num 3 0 1 0 3 0 = 8 * explicitZ 3 0 1 0 3 0 := by decide
94theorem e_301031 : m2Num 3 0 1 0 3 1 = 8 * explicitZ 3 0 1 0 3 1 := by decide
95theorem e_301032 : m2Num 3 0 1 0 3 2 = 8 * explicitZ 3 0 1 0 3 2 := by decide
96theorem e_301033 : m2Num 3 0 1 0 3 3 = 8 * explicitZ 3 0 1 0 3 3 := by decide
97theorem e_301100 : m2Num 3 0 1 1 0 0 = 8 * explicitZ 3 0 1 1 0 0 := by decide
98theorem e_301101 : m2Num 3 0 1 1 0 1 = 8 * explicitZ 3 0 1 1 0 1 := by decide
99theorem e_301102 : m2Num 3 0 1 1 0 2 = 8 * explicitZ 3 0 1 1 0 2 := by decide
100theorem e_301103 : m2Num 3 0 1 1 0 3 = 8 * explicitZ 3 0 1 1 0 3 := by decide
101theorem e_301110 : m2Num 3 0 1 1 1 0 = 8 * explicitZ 3 0 1 1 1 0 := by decide
102theorem e_301111 : m2Num 3 0 1 1 1 1 = 8 * explicitZ 3 0 1 1 1 1 := by decide
103theorem e_301112 : m2Num 3 0 1 1 1 2 = 8 * explicitZ 3 0 1 1 1 2 := by decide
104theorem e_301113 : m2Num 3 0 1 1 1 3 = 8 * explicitZ 3 0 1 1 1 3 := by decide
105theorem e_301120 : m2Num 3 0 1 1 2 0 = 8 * explicitZ 3 0 1 1 2 0 := by decide
106theorem e_301121 : m2Num 3 0 1 1 2 1 = 8 * explicitZ 3 0 1 1 2 1 := by decide
107theorem e_301122 : m2Num 3 0 1 1 2 2 = 8 * explicitZ 3 0 1 1 2 2 := by decide
108theorem e_301123 : m2Num 3 0 1 1 2 3 = 8 * explicitZ 3 0 1 1 2 3 := by decide
109theorem e_301130 : m2Num 3 0 1 1 3 0 = 8 * explicitZ 3 0 1 1 3 0 := by decide
110theorem e_301131 : m2Num 3 0 1 1 3 1 = 8 * explicitZ 3 0 1 1 3 1 := by decide
111theorem e_301132 : m2Num 3 0 1 1 3 2 = 8 * explicitZ 3 0 1 1 3 2 := by decide
112theorem e_301133 : m2Num 3 0 1 1 3 3 = 8 * explicitZ 3 0 1 1 3 3 := by decide
113theorem e_301200 : m2Num 3 0 1 2 0 0 = 8 * explicitZ 3 0 1 2 0 0 := by decide
114theorem e_301201 : m2Num 3 0 1 2 0 1 = 8 * explicitZ 3 0 1 2 0 1 := by decide
115theorem e_301202 : m2Num 3 0 1 2 0 2 = 8 * explicitZ 3 0 1 2 0 2 := by decide
116theorem e_301203 : m2Num 3 0 1 2 0 3 = 8 * explicitZ 3 0 1 2 0 3 := by decide
117theorem e_301210 : m2Num 3 0 1 2 1 0 = 8 * explicitZ 3 0 1 2 1 0 := by decide
118theorem e_301211 : m2Num 3 0 1 2 1 1 = 8 * explicitZ 3 0 1 2 1 1 := by decide
119theorem e_301212 : m2Num 3 0 1 2 1 2 = 8 * explicitZ 3 0 1 2 1 2 := by decide
120theorem e_301213 : m2Num 3 0 1 2 1 3 = 8 * explicitZ 3 0 1 2 1 3 := by decide
121theorem e_301220 : m2Num 3 0 1 2 2 0 = 8 * explicitZ 3 0 1 2 2 0 := by decide
122theorem e_301221 : m2Num 3 0 1 2 2 1 = 8 * explicitZ 3 0 1 2 2 1 := by decide
123theorem e_301222 : m2Num 3 0 1 2 2 2 = 8 * explicitZ 3 0 1 2 2 2 := by decide
124theorem e_301223 : m2Num 3 0 1 2 2 3 = 8 * explicitZ 3 0 1 2 2 3 := by decide
125theorem e_301230 : m2Num 3 0 1 2 3 0 = 8 * explicitZ 3 0 1 2 3 0 := by decide
126theorem e_301231 : m2Num 3 0 1 2 3 1 = 8 * explicitZ 3 0 1 2 3 1 := by decide
127theorem e_301232 : m2Num 3 0 1 2 3 2 = 8 * explicitZ 3 0 1 2 3 2 := by decide
128theorem e_301233 : m2Num 3 0 1 2 3 3 = 8 * explicitZ 3 0 1 2 3 3 := by decide
129theorem e_301300 : m2Num 3 0 1 3 0 0 = 8 * explicitZ 3 0 1 3 0 0 := by decide
130theorem e_301301 : m2Num 3 0 1 3 0 1 = 8 * explicitZ 3 0 1 3 0 1 := by decide
131theorem e_301302 : m2Num 3 0 1 3 0 2 = 8 * explicitZ 3 0 1 3 0 2 := by decide
132theorem e_301303 : m2Num 3 0 1 3 0 3 = 8 * explicitZ 3 0 1 3 0 3 := by decide
133theorem e_301310 : m2Num 3 0 1 3 1 0 = 8 * explicitZ 3 0 1 3 1 0 := by decide
134theorem e_301311 : m2Num 3 0 1 3 1 1 = 8 * explicitZ 3 0 1 3 1 1 := by decide
135theorem e_301312 : m2Num 3 0 1 3 1 2 = 8 * explicitZ 3 0 1 3 1 2 := by decide
136theorem e_301313 : m2Num 3 0 1 3 1 3 = 8 * explicitZ 3 0 1 3 1 3 := by decide
137theorem e_301320 : m2Num 3 0 1 3 2 0 = 8 * explicitZ 3 0 1 3 2 0 := by decide
138theorem e_301321 : m2Num 3 0 1 3 2 1 = 8 * explicitZ 3 0 1 3 2 1 := by decide
139theorem e_301322 : m2Num 3 0 1 3 2 2 = 8 * explicitZ 3 0 1 3 2 2 := by decide
140theorem e_301323 : m2Num 3 0 1 3 2 3 = 8 * explicitZ 3 0 1 3 2 3 := by decide
141theorem e_301330 : m2Num 3 0 1 3 3 0 = 8 * explicitZ 3 0 1 3 3 0 := by decide
142theorem e_301331 : m2Num 3 0 1 3 3 1 = 8 * explicitZ 3 0 1 3 3 1 := by decide
143theorem e_301332 : m2Num 3 0 1 3 3 2 = 8 * explicitZ 3 0 1 3 3 2 := by decide
144theorem e_301333 : m2Num 3 0 1 3 3 3 = 8 * explicitZ 3 0 1 3 3 3 := by decide
145theorem e_302000 : m2Num 3 0 2 0 0 0 = 8 * explicitZ 3 0 2 0 0 0 := by decide
146theorem e_302001 : m2Num 3 0 2 0 0 1 = 8 * explicitZ 3 0 2 0 0 1 := by decide
147theorem e_302002 : m2Num 3 0 2 0 0 2 = 8 * explicitZ 3 0 2 0 0 2 := by decide
148theorem e_302003 : m2Num 3 0 2 0 0 3 = 8 * explicitZ 3 0 2 0 0 3 := by decide
149theorem e_302010 : m2Num 3 0 2 0 1 0 = 8 * explicitZ 3 0 2 0 1 0 := by decide
150theorem e_302011 : m2Num 3 0 2 0 1 1 = 8 * explicitZ 3 0 2 0 1 1 := by decide
151theorem e_302012 : m2Num 3 0 2 0 1 2 = 8 * explicitZ 3 0 2 0 1 2 := by decide
152theorem e_302013 : m2Num 3 0 2 0 1 3 = 8 * explicitZ 3 0 2 0 1 3 := by decide
153theorem e_302020 : m2Num 3 0 2 0 2 0 = 8 * explicitZ 3 0 2 0 2 0 := by decide
154theorem e_302021 : m2Num 3 0 2 0 2 1 = 8 * explicitZ 3 0 2 0 2 1 := by decide
155theorem e_302022 : m2Num 3 0 2 0 2 2 = 8 * explicitZ 3 0 2 0 2 2 := by decide
156theorem e_302023 : m2Num 3 0 2 0 2 3 = 8 * explicitZ 3 0 2 0 2 3 := by decide
157theorem e_302030 : m2Num 3 0 2 0 3 0 = 8 * explicitZ 3 0 2 0 3 0 := by decide
158theorem e_302031 : m2Num 3 0 2 0 3 1 = 8 * explicitZ 3 0 2 0 3 1 := by decide
159theorem e_302032 : m2Num 3 0 2 0 3 2 = 8 * explicitZ 3 0 2 0 3 2 := by decide
160theorem e_302033 : m2Num 3 0 2 0 3 3 = 8 * explicitZ 3 0 2 0 3 3 := by decide
161theorem e_302100 : m2Num 3 0 2 1 0 0 = 8 * explicitZ 3 0 2 1 0 0 := by decide
162theorem e_302101 : m2Num 3 0 2 1 0 1 = 8 * explicitZ 3 0 2 1 0 1 := by decide
163theorem e_302102 : m2Num 3 0 2 1 0 2 = 8 * explicitZ 3 0 2 1 0 2 := by decide
164theorem e_302103 : m2Num 3 0 2 1 0 3 = 8 * explicitZ 3 0 2 1 0 3 := by decide
165theorem e_302110 : m2Num 3 0 2 1 1 0 = 8 * explicitZ 3 0 2 1 1 0 := by decide
166theorem e_302111 : m2Num 3 0 2 1 1 1 = 8 * explicitZ 3 0 2 1 1 1 := by decide
167theorem e_302112 : m2Num 3 0 2 1 1 2 = 8 * explicitZ 3 0 2 1 1 2 := by decide
168theorem e_302113 : m2Num 3 0 2 1 1 3 = 8 * explicitZ 3 0 2 1 1 3 := by decide
169theorem e_302120 : m2Num 3 0 2 1 2 0 = 8 * explicitZ 3 0 2 1 2 0 := by decide
170theorem e_302121 : m2Num 3 0 2 1 2 1 = 8 * explicitZ 3 0 2 1 2 1 := by decide
171theorem e_302122 : m2Num 3 0 2 1 2 2 = 8 * explicitZ 3 0 2 1 2 2 := by decide
172theorem e_302123 : m2Num 3 0 2 1 2 3 = 8 * explicitZ 3 0 2 1 2 3 := by decide
173theorem e_302130 : m2Num 3 0 2 1 3 0 = 8 * explicitZ 3 0 2 1 3 0 := by decide
174theorem e_302131 : m2Num 3 0 2 1 3 1 = 8 * explicitZ 3 0 2 1 3 1 := by decide
175theorem e_302132 : m2Num 3 0 2 1 3 2 = 8 * explicitZ 3 0 2 1 3 2 := by decide
176theorem e_302133 : m2Num 3 0 2 1 3 3 = 8 * explicitZ 3 0 2 1 3 3 := by decide
177theorem e_302200 : m2Num 3 0 2 2 0 0 = 8 * explicitZ 3 0 2 2 0 0 := by decide
178theorem e_302201 : m2Num 3 0 2 2 0 1 = 8 * explicitZ 3 0 2 2 0 1 := by decide
179theorem e_302202 : m2Num 3 0 2 2 0 2 = 8 * explicitZ 3 0 2 2 0 2 := by decide
180theorem e_302203 : m2Num 3 0 2 2 0 3 = 8 * explicitZ 3 0 2 2 0 3 := by decide
181theorem e_302210 : m2Num 3 0 2 2 1 0 = 8 * explicitZ 3 0 2 2 1 0 := by decide
182theorem e_302211 : m2Num 3 0 2 2 1 1 = 8 * explicitZ 3 0 2 2 1 1 := by decide
183theorem e_302212 : m2Num 3 0 2 2 1 2 = 8 * explicitZ 3 0 2 2 1 2 := by decide
184theorem e_302213 : m2Num 3 0 2 2 1 3 = 8 * explicitZ 3 0 2 2 1 3 := by decide
185theorem e_302220 : m2Num 3 0 2 2 2 0 = 8 * explicitZ 3 0 2 2 2 0 := by decide
186theorem e_302221 : m2Num 3 0 2 2 2 1 = 8 * explicitZ 3 0 2 2 2 1 := by decide
187theorem e_302222 : m2Num 3 0 2 2 2 2 = 8 * explicitZ 3 0 2 2 2 2 := by decide
188theorem e_302223 : m2Num 3 0 2 2 2 3 = 8 * explicitZ 3 0 2 2 2 3 := by decide
189theorem e_302230 : m2Num 3 0 2 2 3 0 = 8 * explicitZ 3 0 2 2 3 0 := by decide
190theorem e_302231 : m2Num 3 0 2 2 3 1 = 8 * explicitZ 3 0 2 2 3 1 := by decide
191theorem e_302232 : m2Num 3 0 2 2 3 2 = 8 * explicitZ 3 0 2 2 3 2 := by decide
192theorem e_302233 : m2Num 3 0 2 2 3 3 = 8 * explicitZ 3 0 2 2 3 3 := by decide
193theorem e_302300 : m2Num 3 0 2 3 0 0 = 8 * explicitZ 3 0 2 3 0 0 := by decide
194theorem e_302301 : m2Num 3 0 2 3 0 1 = 8 * explicitZ 3 0 2 3 0 1 := by decide
195theorem e_302302 : m2Num 3 0 2 3 0 2 = 8 * explicitZ 3 0 2 3 0 2 := by decide
196theorem e_302303 : m2Num 3 0 2 3 0 3 = 8 * explicitZ 3 0 2 3 0 3 := by decide
197theorem e_302310 : m2Num 3 0 2 3 1 0 = 8 * explicitZ 3 0 2 3 1 0 := by decide
198theorem e_302311 : m2Num 3 0 2 3 1 1 = 8 * explicitZ 3 0 2 3 1 1 := by decide
199theorem e_302312 : m2Num 3 0 2 3 1 2 = 8 * explicitZ 3 0 2 3 1 2 := by decide
200theorem e_302313 : m2Num 3 0 2 3 1 3 = 8 * explicitZ 3 0 2 3 1 3 := by decide
201theorem e_302320 : m2Num 3 0 2 3 2 0 = 8 * explicitZ 3 0 2 3 2 0 := by decide
202theorem e_302321 : m2Num 3 0 2 3 2 1 = 8 * explicitZ 3 0 2 3 2 1 := by decide
203theorem e_302322 : m2Num 3 0 2 3 2 2 = 8 * explicitZ 3 0 2 3 2 2 := by decide
204theorem e_302323 : m2Num 3 0 2 3 2 3 = 8 * explicitZ 3 0 2 3 2 3 := by decide
205theorem e_302330 : m2Num 3 0 2 3 3 0 = 8 * explicitZ 3 0 2 3 3 0 := by decide
206theorem e_302331 : m2Num 3 0 2 3 3 1 = 8 * explicitZ 3 0 2 3 3 1 := by decide
207theorem e_302332 : m2Num 3 0 2 3 3 2 = 8 * explicitZ 3 0 2 3 3 2 := by decide
208theorem e_302333 : m2Num 3 0 2 3 3 3 = 8 * explicitZ 3 0 2 3 3 3 := by decide
209theorem e_303000 : m2Num 3 0 3 0 0 0 = 8 * explicitZ 3 0 3 0 0 0 := by decide
210theorem e_303001 : m2Num 3 0 3 0 0 1 = 8 * explicitZ 3 0 3 0 0 1 := by decide
211theorem e_303002 : m2Num 3 0 3 0 0 2 = 8 * explicitZ 3 0 3 0 0 2 := by decide
212theorem e_303003 : m2Num 3 0 3 0 0 3 = 8 * explicitZ 3 0 3 0 0 3 := by decide
213theorem e_303010 : m2Num 3 0 3 0 1 0 = 8 * explicitZ 3 0 3 0 1 0 := by decide
214theorem e_303011 : m2Num 3 0 3 0 1 1 = 8 * explicitZ 3 0 3 0 1 1 := by decide
215theorem e_303012 : m2Num 3 0 3 0 1 2 = 8 * explicitZ 3 0 3 0 1 2 := by decide
216theorem e_303013 : m2Num 3 0 3 0 1 3 = 8 * explicitZ 3 0 3 0 1 3 := by decide
217theorem e_303020 : m2Num 3 0 3 0 2 0 = 8 * explicitZ 3 0 3 0 2 0 := by decide
218theorem e_303021 : m2Num 3 0 3 0 2 1 = 8 * explicitZ 3 0 3 0 2 1 := by decide
219theorem e_303022 : m2Num 3 0 3 0 2 2 = 8 * explicitZ 3 0 3 0 2 2 := by decide
220theorem e_303023 : m2Num 3 0 3 0 2 3 = 8 * explicitZ 3 0 3 0 2 3 := by decide
221theorem e_303030 : m2Num 3 0 3 0 3 0 = 8 * explicitZ 3 0 3 0 3 0 := by decide
222theorem e_303031 : m2Num 3 0 3 0 3 1 = 8 * explicitZ 3 0 3 0 3 1 := by decide
223theorem e_303032 : m2Num 3 0 3 0 3 2 = 8 * explicitZ 3 0 3 0 3 2 := by decide
224theorem e_303033 : m2Num 3 0 3 0 3 3 = 8 * explicitZ 3 0 3 0 3 3 := by decide
225theorem e_303100 : m2Num 3 0 3 1 0 0 = 8 * explicitZ 3 0 3 1 0 0 := by decide
226theorem e_303101 : m2Num 3 0 3 1 0 1 = 8 * explicitZ 3 0 3 1 0 1 := by decide
227theorem e_303102 : m2Num 3 0 3 1 0 2 = 8 * explicitZ 3 0 3 1 0 2 := by decide
228theorem e_303103 : m2Num 3 0 3 1 0 3 = 8 * explicitZ 3 0 3 1 0 3 := by decide
229theorem e_303110 : m2Num 3 0 3 1 1 0 = 8 * explicitZ 3 0 3 1 1 0 := by decide
230theorem e_303111 : m2Num 3 0 3 1 1 1 = 8 * explicitZ 3 0 3 1 1 1 := by decide
231theorem e_303112 : m2Num 3 0 3 1 1 2 = 8 * explicitZ 3 0 3 1 1 2 := by decide
232theorem e_303113 : m2Num 3 0 3 1 1 3 = 8 * explicitZ 3 0 3 1 1 3 := by decide
233theorem e_303120 : m2Num 3 0 3 1 2 0 = 8 * explicitZ 3 0 3 1 2 0 := by decide
234theorem e_303121 : m2Num 3 0 3 1 2 1 = 8 * explicitZ 3 0 3 1 2 1 := by decide
235theorem e_303122 : m2Num 3 0 3 1 2 2 = 8 * explicitZ 3 0 3 1 2 2 := by decide
236theorem e_303123 : m2Num 3 0 3 1 2 3 = 8 * explicitZ 3 0 3 1 2 3 := by decide
237theorem e_303130 : m2Num 3 0 3 1 3 0 = 8 * explicitZ 3 0 3 1 3 0 := by decide
238theorem e_303131 : m2Num 3 0 3 1 3 1 = 8 * explicitZ 3 0 3 1 3 1 := by decide
239theorem e_303132 : m2Num 3 0 3 1 3 2 = 8 * explicitZ 3 0 3 1 3 2 := by decide
240theorem e_303133 : m2Num 3 0 3 1 3 3 = 8 * explicitZ 3 0 3 1 3 3 := by decide
241theorem e_303200 : m2Num 3 0 3 2 0 0 = 8 * explicitZ 3 0 3 2 0 0 := by decide
242theorem e_303201 : m2Num 3 0 3 2 0 1 = 8 * explicitZ 3 0 3 2 0 1 := by decide
243theorem e_303202 : m2Num 3 0 3 2 0 2 = 8 * explicitZ 3 0 3 2 0 2 := by decide
244theorem e_303203 : m2Num 3 0 3 2 0 3 = 8 * explicitZ 3 0 3 2 0 3 := by decide
245theorem e_303210 : m2Num 3 0 3 2 1 0 = 8 * explicitZ 3 0 3 2 1 0 := by decide
246theorem e_303211 : m2Num 3 0 3 2 1 1 = 8 * explicitZ 3 0 3 2 1 1 := by decide
247theorem e_303212 : m2Num 3 0 3 2 1 2 = 8 * explicitZ 3 0 3 2 1 2 := by decide
248theorem e_303213 : m2Num 3 0 3 2 1 3 = 8 * explicitZ 3 0 3 2 1 3 := by decide
249theorem e_303220 : m2Num 3 0 3 2 2 0 = 8 * explicitZ 3 0 3 2 2 0 := by decide
250theorem e_303221 : m2Num 3 0 3 2 2 1 = 8 * explicitZ 3 0 3 2 2 1 := by decide
251theorem e_303222 : m2Num 3 0 3 2 2 2 = 8 * explicitZ 3 0 3 2 2 2 := by decide
252theorem e_303223 : m2Num 3 0 3 2 2 3 = 8 * explicitZ 3 0 3 2 2 3 := by decide
253theorem e_303230 : m2Num 3 0 3 2 3 0 = 8 * explicitZ 3 0 3 2 3 0 := by decide
254theorem e_303231 : m2Num 3 0 3 2 3 1 = 8 * explicitZ 3 0 3 2 3 1 := by decide
255theorem e_303232 : m2Num 3 0 3 2 3 2 = 8 * explicitZ 3 0 3 2 3 2 := by decide
256theorem e_303233 : m2Num 3 0 3 2 3 3 = 8 * explicitZ 3 0 3 2 3 3 := by decide
257theorem e_303300 : m2Num 3 0 3 3 0 0 = 8 * explicitZ 3 0 3 3 0 0 := by decide
258theorem e_303301 : m2Num 3 0 3 3 0 1 = 8 * explicitZ 3 0 3 3 0 1 := by decide
259theorem e_303302 : m2Num 3 0 3 3 0 2 = 8 * explicitZ 3 0 3 3 0 2 := by decide
260theorem e_303303 : m2Num 3 0 3 3 0 3 = 8 * explicitZ 3 0 3 3 0 3 := by decide
261theorem e_303310 : m2Num 3 0 3 3 1 0 = 8 * explicitZ 3 0 3 3 1 0 := by decide
262theorem e_303311 : m2Num 3 0 3 3 1 1 = 8 * explicitZ 3 0 3 3 1 1 := by decide
263theorem e_303312 : m2Num 3 0 3 3 1 2 = 8 * explicitZ 3 0 3 3 1 2 := by decide
264theorem e_303313 : m2Num 3 0 3 3 1 3 = 8 * explicitZ 3 0 3 3 1 3 := by decide
265theorem e_303320 : m2Num 3 0 3 3 2 0 = 8 * explicitZ 3 0 3 3 2 0 := by decide
266theorem e_303321 : m2Num 3 0 3 3 2 1 = 8 * explicitZ 3 0 3 3 2 1 := by decide
267theorem e_303322 : m2Num 3 0 3 3 2 2 = 8 * explicitZ 3 0 3 3 2 2 := by decide
268theorem e_303323 : m2Num 3 0 3 3 2 3 = 8 * explicitZ 3 0 3 3 2 3 := by decide
269theorem e_303330 : m2Num 3 0 3 3 3 0 = 8 * explicitZ 3 0 3 3 3 0 := by decide
270theorem e_303331 : m2Num 3 0 3 3 3 1 = 8 * explicitZ 3 0 3 3 3 1 := by decide
271theorem e_303332 : m2Num 3 0 3 3 3 2 = 8 * explicitZ 3 0 3 3 3 2 := by decide
272theorem e_303333 : m2Num 3 0 3 3 3 3 = 8 * explicitZ 3 0 3 3 3 3 := by decide
273
274end M2NumChunk12
275end ReggeExactMidpointM2TTIdentity4D
276end Analysis
277end Gravity
278end IndisputableMonolith
279