IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DM2NumChunk08
IndisputableMonolith/Gravity/Analysis/ReggeExactMidpointM2TTIdentity4DM2NumChunk08.lean · 279 lines · 256 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DKernelCert
3
4/-! m2Num = 8·explicitZ, chunk 8 (256 kernel decides). -/
5
6namespace IndisputableMonolith
7namespace Gravity
8namespace Analysis
9namespace ReggeExactMidpointM2TTIdentity4D
10namespace M2NumChunk08
11
12open KernelCert
13
14set_option maxRecDepth 100000
15set_option maxHeartbeats 200000000
16
17theorem e_200000 : m2Num 2 0 0 0 0 0 = 8 * explicitZ 2 0 0 0 0 0 := by decide
18theorem e_200001 : m2Num 2 0 0 0 0 1 = 8 * explicitZ 2 0 0 0 0 1 := by decide
19theorem e_200002 : m2Num 2 0 0 0 0 2 = 8 * explicitZ 2 0 0 0 0 2 := by decide
20theorem e_200003 : m2Num 2 0 0 0 0 3 = 8 * explicitZ 2 0 0 0 0 3 := by decide
21theorem e_200010 : m2Num 2 0 0 0 1 0 = 8 * explicitZ 2 0 0 0 1 0 := by decide
22theorem e_200011 : m2Num 2 0 0 0 1 1 = 8 * explicitZ 2 0 0 0 1 1 := by decide
23theorem e_200012 : m2Num 2 0 0 0 1 2 = 8 * explicitZ 2 0 0 0 1 2 := by decide
24theorem e_200013 : m2Num 2 0 0 0 1 3 = 8 * explicitZ 2 0 0 0 1 3 := by decide
25theorem e_200020 : m2Num 2 0 0 0 2 0 = 8 * explicitZ 2 0 0 0 2 0 := by decide
26theorem e_200021 : m2Num 2 0 0 0 2 1 = 8 * explicitZ 2 0 0 0 2 1 := by decide
27theorem e_200022 : m2Num 2 0 0 0 2 2 = 8 * explicitZ 2 0 0 0 2 2 := by decide
28theorem e_200023 : m2Num 2 0 0 0 2 3 = 8 * explicitZ 2 0 0 0 2 3 := by decide
29theorem e_200030 : m2Num 2 0 0 0 3 0 = 8 * explicitZ 2 0 0 0 3 0 := by decide
30theorem e_200031 : m2Num 2 0 0 0 3 1 = 8 * explicitZ 2 0 0 0 3 1 := by decide
31theorem e_200032 : m2Num 2 0 0 0 3 2 = 8 * explicitZ 2 0 0 0 3 2 := by decide
32theorem e_200033 : m2Num 2 0 0 0 3 3 = 8 * explicitZ 2 0 0 0 3 3 := by decide
33theorem e_200100 : m2Num 2 0 0 1 0 0 = 8 * explicitZ 2 0 0 1 0 0 := by decide
34theorem e_200101 : m2Num 2 0 0 1 0 1 = 8 * explicitZ 2 0 0 1 0 1 := by decide
35theorem e_200102 : m2Num 2 0 0 1 0 2 = 8 * explicitZ 2 0 0 1 0 2 := by decide
36theorem e_200103 : m2Num 2 0 0 1 0 3 = 8 * explicitZ 2 0 0 1 0 3 := by decide
37theorem e_200110 : m2Num 2 0 0 1 1 0 = 8 * explicitZ 2 0 0 1 1 0 := by decide
38theorem e_200111 : m2Num 2 0 0 1 1 1 = 8 * explicitZ 2 0 0 1 1 1 := by decide
39theorem e_200112 : m2Num 2 0 0 1 1 2 = 8 * explicitZ 2 0 0 1 1 2 := by decide
40theorem e_200113 : m2Num 2 0 0 1 1 3 = 8 * explicitZ 2 0 0 1 1 3 := by decide
41theorem e_200120 : m2Num 2 0 0 1 2 0 = 8 * explicitZ 2 0 0 1 2 0 := by decide
42theorem e_200121 : m2Num 2 0 0 1 2 1 = 8 * explicitZ 2 0 0 1 2 1 := by decide
43theorem e_200122 : m2Num 2 0 0 1 2 2 = 8 * explicitZ 2 0 0 1 2 2 := by decide
44theorem e_200123 : m2Num 2 0 0 1 2 3 = 8 * explicitZ 2 0 0 1 2 3 := by decide
45theorem e_200130 : m2Num 2 0 0 1 3 0 = 8 * explicitZ 2 0 0 1 3 0 := by decide
46theorem e_200131 : m2Num 2 0 0 1 3 1 = 8 * explicitZ 2 0 0 1 3 1 := by decide
47theorem e_200132 : m2Num 2 0 0 1 3 2 = 8 * explicitZ 2 0 0 1 3 2 := by decide
48theorem e_200133 : m2Num 2 0 0 1 3 3 = 8 * explicitZ 2 0 0 1 3 3 := by decide
49theorem e_200200 : m2Num 2 0 0 2 0 0 = 8 * explicitZ 2 0 0 2 0 0 := by decide
50theorem e_200201 : m2Num 2 0 0 2 0 1 = 8 * explicitZ 2 0 0 2 0 1 := by decide
51theorem e_200202 : m2Num 2 0 0 2 0 2 = 8 * explicitZ 2 0 0 2 0 2 := by decide
52theorem e_200203 : m2Num 2 0 0 2 0 3 = 8 * explicitZ 2 0 0 2 0 3 := by decide
53theorem e_200210 : m2Num 2 0 0 2 1 0 = 8 * explicitZ 2 0 0 2 1 0 := by decide
54theorem e_200211 : m2Num 2 0 0 2 1 1 = 8 * explicitZ 2 0 0 2 1 1 := by decide
55theorem e_200212 : m2Num 2 0 0 2 1 2 = 8 * explicitZ 2 0 0 2 1 2 := by decide
56theorem e_200213 : m2Num 2 0 0 2 1 3 = 8 * explicitZ 2 0 0 2 1 3 := by decide
57theorem e_200220 : m2Num 2 0 0 2 2 0 = 8 * explicitZ 2 0 0 2 2 0 := by decide
58theorem e_200221 : m2Num 2 0 0 2 2 1 = 8 * explicitZ 2 0 0 2 2 1 := by decide
59theorem e_200222 : m2Num 2 0 0 2 2 2 = 8 * explicitZ 2 0 0 2 2 2 := by decide
60theorem e_200223 : m2Num 2 0 0 2 2 3 = 8 * explicitZ 2 0 0 2 2 3 := by decide
61theorem e_200230 : m2Num 2 0 0 2 3 0 = 8 * explicitZ 2 0 0 2 3 0 := by decide
62theorem e_200231 : m2Num 2 0 0 2 3 1 = 8 * explicitZ 2 0 0 2 3 1 := by decide
63theorem e_200232 : m2Num 2 0 0 2 3 2 = 8 * explicitZ 2 0 0 2 3 2 := by decide
64theorem e_200233 : m2Num 2 0 0 2 3 3 = 8 * explicitZ 2 0 0 2 3 3 := by decide
65theorem e_200300 : m2Num 2 0 0 3 0 0 = 8 * explicitZ 2 0 0 3 0 0 := by decide
66theorem e_200301 : m2Num 2 0 0 3 0 1 = 8 * explicitZ 2 0 0 3 0 1 := by decide
67theorem e_200302 : m2Num 2 0 0 3 0 2 = 8 * explicitZ 2 0 0 3 0 2 := by decide
68theorem e_200303 : m2Num 2 0 0 3 0 3 = 8 * explicitZ 2 0 0 3 0 3 := by decide
69theorem e_200310 : m2Num 2 0 0 3 1 0 = 8 * explicitZ 2 0 0 3 1 0 := by decide
70theorem e_200311 : m2Num 2 0 0 3 1 1 = 8 * explicitZ 2 0 0 3 1 1 := by decide
71theorem e_200312 : m2Num 2 0 0 3 1 2 = 8 * explicitZ 2 0 0 3 1 2 := by decide
72theorem e_200313 : m2Num 2 0 0 3 1 3 = 8 * explicitZ 2 0 0 3 1 3 := by decide
73theorem e_200320 : m2Num 2 0 0 3 2 0 = 8 * explicitZ 2 0 0 3 2 0 := by decide
74theorem e_200321 : m2Num 2 0 0 3 2 1 = 8 * explicitZ 2 0 0 3 2 1 := by decide
75theorem e_200322 : m2Num 2 0 0 3 2 2 = 8 * explicitZ 2 0 0 3 2 2 := by decide
76theorem e_200323 : m2Num 2 0 0 3 2 3 = 8 * explicitZ 2 0 0 3 2 3 := by decide
77theorem e_200330 : m2Num 2 0 0 3 3 0 = 8 * explicitZ 2 0 0 3 3 0 := by decide
78theorem e_200331 : m2Num 2 0 0 3 3 1 = 8 * explicitZ 2 0 0 3 3 1 := by decide
79theorem e_200332 : m2Num 2 0 0 3 3 2 = 8 * explicitZ 2 0 0 3 3 2 := by decide
80theorem e_200333 : m2Num 2 0 0 3 3 3 = 8 * explicitZ 2 0 0 3 3 3 := by decide
81theorem e_201000 : m2Num 2 0 1 0 0 0 = 8 * explicitZ 2 0 1 0 0 0 := by decide
82theorem e_201001 : m2Num 2 0 1 0 0 1 = 8 * explicitZ 2 0 1 0 0 1 := by decide
83theorem e_201002 : m2Num 2 0 1 0 0 2 = 8 * explicitZ 2 0 1 0 0 2 := by decide
84theorem e_201003 : m2Num 2 0 1 0 0 3 = 8 * explicitZ 2 0 1 0 0 3 := by decide
85theorem e_201010 : m2Num 2 0 1 0 1 0 = 8 * explicitZ 2 0 1 0 1 0 := by decide
86theorem e_201011 : m2Num 2 0 1 0 1 1 = 8 * explicitZ 2 0 1 0 1 1 := by decide
87theorem e_201012 : m2Num 2 0 1 0 1 2 = 8 * explicitZ 2 0 1 0 1 2 := by decide
88theorem e_201013 : m2Num 2 0 1 0 1 3 = 8 * explicitZ 2 0 1 0 1 3 := by decide
89theorem e_201020 : m2Num 2 0 1 0 2 0 = 8 * explicitZ 2 0 1 0 2 0 := by decide
90theorem e_201021 : m2Num 2 0 1 0 2 1 = 8 * explicitZ 2 0 1 0 2 1 := by decide
91theorem e_201022 : m2Num 2 0 1 0 2 2 = 8 * explicitZ 2 0 1 0 2 2 := by decide
92theorem e_201023 : m2Num 2 0 1 0 2 3 = 8 * explicitZ 2 0 1 0 2 3 := by decide
93theorem e_201030 : m2Num 2 0 1 0 3 0 = 8 * explicitZ 2 0 1 0 3 0 := by decide
94theorem e_201031 : m2Num 2 0 1 0 3 1 = 8 * explicitZ 2 0 1 0 3 1 := by decide
95theorem e_201032 : m2Num 2 0 1 0 3 2 = 8 * explicitZ 2 0 1 0 3 2 := by decide
96theorem e_201033 : m2Num 2 0 1 0 3 3 = 8 * explicitZ 2 0 1 0 3 3 := by decide
97theorem e_201100 : m2Num 2 0 1 1 0 0 = 8 * explicitZ 2 0 1 1 0 0 := by decide
98theorem e_201101 : m2Num 2 0 1 1 0 1 = 8 * explicitZ 2 0 1 1 0 1 := by decide
99theorem e_201102 : m2Num 2 0 1 1 0 2 = 8 * explicitZ 2 0 1 1 0 2 := by decide
100theorem e_201103 : m2Num 2 0 1 1 0 3 = 8 * explicitZ 2 0 1 1 0 3 := by decide
101theorem e_201110 : m2Num 2 0 1 1 1 0 = 8 * explicitZ 2 0 1 1 1 0 := by decide
102theorem e_201111 : m2Num 2 0 1 1 1 1 = 8 * explicitZ 2 0 1 1 1 1 := by decide
103theorem e_201112 : m2Num 2 0 1 1 1 2 = 8 * explicitZ 2 0 1 1 1 2 := by decide
104theorem e_201113 : m2Num 2 0 1 1 1 3 = 8 * explicitZ 2 0 1 1 1 3 := by decide
105theorem e_201120 : m2Num 2 0 1 1 2 0 = 8 * explicitZ 2 0 1 1 2 0 := by decide
106theorem e_201121 : m2Num 2 0 1 1 2 1 = 8 * explicitZ 2 0 1 1 2 1 := by decide
107theorem e_201122 : m2Num 2 0 1 1 2 2 = 8 * explicitZ 2 0 1 1 2 2 := by decide
108theorem e_201123 : m2Num 2 0 1 1 2 3 = 8 * explicitZ 2 0 1 1 2 3 := by decide
109theorem e_201130 : m2Num 2 0 1 1 3 0 = 8 * explicitZ 2 0 1 1 3 0 := by decide
110theorem e_201131 : m2Num 2 0 1 1 3 1 = 8 * explicitZ 2 0 1 1 3 1 := by decide
111theorem e_201132 : m2Num 2 0 1 1 3 2 = 8 * explicitZ 2 0 1 1 3 2 := by decide
112theorem e_201133 : m2Num 2 0 1 1 3 3 = 8 * explicitZ 2 0 1 1 3 3 := by decide
113theorem e_201200 : m2Num 2 0 1 2 0 0 = 8 * explicitZ 2 0 1 2 0 0 := by decide
114theorem e_201201 : m2Num 2 0 1 2 0 1 = 8 * explicitZ 2 0 1 2 0 1 := by decide
115theorem e_201202 : m2Num 2 0 1 2 0 2 = 8 * explicitZ 2 0 1 2 0 2 := by decide
116theorem e_201203 : m2Num 2 0 1 2 0 3 = 8 * explicitZ 2 0 1 2 0 3 := by decide
117theorem e_201210 : m2Num 2 0 1 2 1 0 = 8 * explicitZ 2 0 1 2 1 0 := by decide
118theorem e_201211 : m2Num 2 0 1 2 1 1 = 8 * explicitZ 2 0 1 2 1 1 := by decide
119theorem e_201212 : m2Num 2 0 1 2 1 2 = 8 * explicitZ 2 0 1 2 1 2 := by decide
120theorem e_201213 : m2Num 2 0 1 2 1 3 = 8 * explicitZ 2 0 1 2 1 3 := by decide
121theorem e_201220 : m2Num 2 0 1 2 2 0 = 8 * explicitZ 2 0 1 2 2 0 := by decide
122theorem e_201221 : m2Num 2 0 1 2 2 1 = 8 * explicitZ 2 0 1 2 2 1 := by decide
123theorem e_201222 : m2Num 2 0 1 2 2 2 = 8 * explicitZ 2 0 1 2 2 2 := by decide
124theorem e_201223 : m2Num 2 0 1 2 2 3 = 8 * explicitZ 2 0 1 2 2 3 := by decide
125theorem e_201230 : m2Num 2 0 1 2 3 0 = 8 * explicitZ 2 0 1 2 3 0 := by decide
126theorem e_201231 : m2Num 2 0 1 2 3 1 = 8 * explicitZ 2 0 1 2 3 1 := by decide
127theorem e_201232 : m2Num 2 0 1 2 3 2 = 8 * explicitZ 2 0 1 2 3 2 := by decide
128theorem e_201233 : m2Num 2 0 1 2 3 3 = 8 * explicitZ 2 0 1 2 3 3 := by decide
129theorem e_201300 : m2Num 2 0 1 3 0 0 = 8 * explicitZ 2 0 1 3 0 0 := by decide
130theorem e_201301 : m2Num 2 0 1 3 0 1 = 8 * explicitZ 2 0 1 3 0 1 := by decide
131theorem e_201302 : m2Num 2 0 1 3 0 2 = 8 * explicitZ 2 0 1 3 0 2 := by decide
132theorem e_201303 : m2Num 2 0 1 3 0 3 = 8 * explicitZ 2 0 1 3 0 3 := by decide
133theorem e_201310 : m2Num 2 0 1 3 1 0 = 8 * explicitZ 2 0 1 3 1 0 := by decide
134theorem e_201311 : m2Num 2 0 1 3 1 1 = 8 * explicitZ 2 0 1 3 1 1 := by decide
135theorem e_201312 : m2Num 2 0 1 3 1 2 = 8 * explicitZ 2 0 1 3 1 2 := by decide
136theorem e_201313 : m2Num 2 0 1 3 1 3 = 8 * explicitZ 2 0 1 3 1 3 := by decide
137theorem e_201320 : m2Num 2 0 1 3 2 0 = 8 * explicitZ 2 0 1 3 2 0 := by decide
138theorem e_201321 : m2Num 2 0 1 3 2 1 = 8 * explicitZ 2 0 1 3 2 1 := by decide
139theorem e_201322 : m2Num 2 0 1 3 2 2 = 8 * explicitZ 2 0 1 3 2 2 := by decide
140theorem e_201323 : m2Num 2 0 1 3 2 3 = 8 * explicitZ 2 0 1 3 2 3 := by decide
141theorem e_201330 : m2Num 2 0 1 3 3 0 = 8 * explicitZ 2 0 1 3 3 0 := by decide
142theorem e_201331 : m2Num 2 0 1 3 3 1 = 8 * explicitZ 2 0 1 3 3 1 := by decide
143theorem e_201332 : m2Num 2 0 1 3 3 2 = 8 * explicitZ 2 0 1 3 3 2 := by decide
144theorem e_201333 : m2Num 2 0 1 3 3 3 = 8 * explicitZ 2 0 1 3 3 3 := by decide
145theorem e_202000 : m2Num 2 0 2 0 0 0 = 8 * explicitZ 2 0 2 0 0 0 := by decide
146theorem e_202001 : m2Num 2 0 2 0 0 1 = 8 * explicitZ 2 0 2 0 0 1 := by decide
147theorem e_202002 : m2Num 2 0 2 0 0 2 = 8 * explicitZ 2 0 2 0 0 2 := by decide
148theorem e_202003 : m2Num 2 0 2 0 0 3 = 8 * explicitZ 2 0 2 0 0 3 := by decide
149theorem e_202010 : m2Num 2 0 2 0 1 0 = 8 * explicitZ 2 0 2 0 1 0 := by decide
150theorem e_202011 : m2Num 2 0 2 0 1 1 = 8 * explicitZ 2 0 2 0 1 1 := by decide
151theorem e_202012 : m2Num 2 0 2 0 1 2 = 8 * explicitZ 2 0 2 0 1 2 := by decide
152theorem e_202013 : m2Num 2 0 2 0 1 3 = 8 * explicitZ 2 0 2 0 1 3 := by decide
153theorem e_202020 : m2Num 2 0 2 0 2 0 = 8 * explicitZ 2 0 2 0 2 0 := by decide
154theorem e_202021 : m2Num 2 0 2 0 2 1 = 8 * explicitZ 2 0 2 0 2 1 := by decide
155theorem e_202022 : m2Num 2 0 2 0 2 2 = 8 * explicitZ 2 0 2 0 2 2 := by decide
156theorem e_202023 : m2Num 2 0 2 0 2 3 = 8 * explicitZ 2 0 2 0 2 3 := by decide
157theorem e_202030 : m2Num 2 0 2 0 3 0 = 8 * explicitZ 2 0 2 0 3 0 := by decide
158theorem e_202031 : m2Num 2 0 2 0 3 1 = 8 * explicitZ 2 0 2 0 3 1 := by decide
159theorem e_202032 : m2Num 2 0 2 0 3 2 = 8 * explicitZ 2 0 2 0 3 2 := by decide
160theorem e_202033 : m2Num 2 0 2 0 3 3 = 8 * explicitZ 2 0 2 0 3 3 := by decide
161theorem e_202100 : m2Num 2 0 2 1 0 0 = 8 * explicitZ 2 0 2 1 0 0 := by decide
162theorem e_202101 : m2Num 2 0 2 1 0 1 = 8 * explicitZ 2 0 2 1 0 1 := by decide
163theorem e_202102 : m2Num 2 0 2 1 0 2 = 8 * explicitZ 2 0 2 1 0 2 := by decide
164theorem e_202103 : m2Num 2 0 2 1 0 3 = 8 * explicitZ 2 0 2 1 0 3 := by decide
165theorem e_202110 : m2Num 2 0 2 1 1 0 = 8 * explicitZ 2 0 2 1 1 0 := by decide
166theorem e_202111 : m2Num 2 0 2 1 1 1 = 8 * explicitZ 2 0 2 1 1 1 := by decide
167theorem e_202112 : m2Num 2 0 2 1 1 2 = 8 * explicitZ 2 0 2 1 1 2 := by decide
168theorem e_202113 : m2Num 2 0 2 1 1 3 = 8 * explicitZ 2 0 2 1 1 3 := by decide
169theorem e_202120 : m2Num 2 0 2 1 2 0 = 8 * explicitZ 2 0 2 1 2 0 := by decide
170theorem e_202121 : m2Num 2 0 2 1 2 1 = 8 * explicitZ 2 0 2 1 2 1 := by decide
171theorem e_202122 : m2Num 2 0 2 1 2 2 = 8 * explicitZ 2 0 2 1 2 2 := by decide
172theorem e_202123 : m2Num 2 0 2 1 2 3 = 8 * explicitZ 2 0 2 1 2 3 := by decide
173theorem e_202130 : m2Num 2 0 2 1 3 0 = 8 * explicitZ 2 0 2 1 3 0 := by decide
174theorem e_202131 : m2Num 2 0 2 1 3 1 = 8 * explicitZ 2 0 2 1 3 1 := by decide
175theorem e_202132 : m2Num 2 0 2 1 3 2 = 8 * explicitZ 2 0 2 1 3 2 := by decide
176theorem e_202133 : m2Num 2 0 2 1 3 3 = 8 * explicitZ 2 0 2 1 3 3 := by decide
177theorem e_202200 : m2Num 2 0 2 2 0 0 = 8 * explicitZ 2 0 2 2 0 0 := by decide
178theorem e_202201 : m2Num 2 0 2 2 0 1 = 8 * explicitZ 2 0 2 2 0 1 := by decide
179theorem e_202202 : m2Num 2 0 2 2 0 2 = 8 * explicitZ 2 0 2 2 0 2 := by decide
180theorem e_202203 : m2Num 2 0 2 2 0 3 = 8 * explicitZ 2 0 2 2 0 3 := by decide
181theorem e_202210 : m2Num 2 0 2 2 1 0 = 8 * explicitZ 2 0 2 2 1 0 := by decide
182theorem e_202211 : m2Num 2 0 2 2 1 1 = 8 * explicitZ 2 0 2 2 1 1 := by decide
183theorem e_202212 : m2Num 2 0 2 2 1 2 = 8 * explicitZ 2 0 2 2 1 2 := by decide
184theorem e_202213 : m2Num 2 0 2 2 1 3 = 8 * explicitZ 2 0 2 2 1 3 := by decide
185theorem e_202220 : m2Num 2 0 2 2 2 0 = 8 * explicitZ 2 0 2 2 2 0 := by decide
186theorem e_202221 : m2Num 2 0 2 2 2 1 = 8 * explicitZ 2 0 2 2 2 1 := by decide
187theorem e_202222 : m2Num 2 0 2 2 2 2 = 8 * explicitZ 2 0 2 2 2 2 := by decide
188theorem e_202223 : m2Num 2 0 2 2 2 3 = 8 * explicitZ 2 0 2 2 2 3 := by decide
189theorem e_202230 : m2Num 2 0 2 2 3 0 = 8 * explicitZ 2 0 2 2 3 0 := by decide
190theorem e_202231 : m2Num 2 0 2 2 3 1 = 8 * explicitZ 2 0 2 2 3 1 := by decide
191theorem e_202232 : m2Num 2 0 2 2 3 2 = 8 * explicitZ 2 0 2 2 3 2 := by decide
192theorem e_202233 : m2Num 2 0 2 2 3 3 = 8 * explicitZ 2 0 2 2 3 3 := by decide
193theorem e_202300 : m2Num 2 0 2 3 0 0 = 8 * explicitZ 2 0 2 3 0 0 := by decide
194theorem e_202301 : m2Num 2 0 2 3 0 1 = 8 * explicitZ 2 0 2 3 0 1 := by decide
195theorem e_202302 : m2Num 2 0 2 3 0 2 = 8 * explicitZ 2 0 2 3 0 2 := by decide
196theorem e_202303 : m2Num 2 0 2 3 0 3 = 8 * explicitZ 2 0 2 3 0 3 := by decide
197theorem e_202310 : m2Num 2 0 2 3 1 0 = 8 * explicitZ 2 0 2 3 1 0 := by decide
198theorem e_202311 : m2Num 2 0 2 3 1 1 = 8 * explicitZ 2 0 2 3 1 1 := by decide
199theorem e_202312 : m2Num 2 0 2 3 1 2 = 8 * explicitZ 2 0 2 3 1 2 := by decide
200theorem e_202313 : m2Num 2 0 2 3 1 3 = 8 * explicitZ 2 0 2 3 1 3 := by decide
201theorem e_202320 : m2Num 2 0 2 3 2 0 = 8 * explicitZ 2 0 2 3 2 0 := by decide
202theorem e_202321 : m2Num 2 0 2 3 2 1 = 8 * explicitZ 2 0 2 3 2 1 := by decide
203theorem e_202322 : m2Num 2 0 2 3 2 2 = 8 * explicitZ 2 0 2 3 2 2 := by decide
204theorem e_202323 : m2Num 2 0 2 3 2 3 = 8 * explicitZ 2 0 2 3 2 3 := by decide
205theorem e_202330 : m2Num 2 0 2 3 3 0 = 8 * explicitZ 2 0 2 3 3 0 := by decide
206theorem e_202331 : m2Num 2 0 2 3 3 1 = 8 * explicitZ 2 0 2 3 3 1 := by decide
207theorem e_202332 : m2Num 2 0 2 3 3 2 = 8 * explicitZ 2 0 2 3 3 2 := by decide
208theorem e_202333 : m2Num 2 0 2 3 3 3 = 8 * explicitZ 2 0 2 3 3 3 := by decide
209theorem e_203000 : m2Num 2 0 3 0 0 0 = 8 * explicitZ 2 0 3 0 0 0 := by decide
210theorem e_203001 : m2Num 2 0 3 0 0 1 = 8 * explicitZ 2 0 3 0 0 1 := by decide
211theorem e_203002 : m2Num 2 0 3 0 0 2 = 8 * explicitZ 2 0 3 0 0 2 := by decide
212theorem e_203003 : m2Num 2 0 3 0 0 3 = 8 * explicitZ 2 0 3 0 0 3 := by decide
213theorem e_203010 : m2Num 2 0 3 0 1 0 = 8 * explicitZ 2 0 3 0 1 0 := by decide
214theorem e_203011 : m2Num 2 0 3 0 1 1 = 8 * explicitZ 2 0 3 0 1 1 := by decide
215theorem e_203012 : m2Num 2 0 3 0 1 2 = 8 * explicitZ 2 0 3 0 1 2 := by decide
216theorem e_203013 : m2Num 2 0 3 0 1 3 = 8 * explicitZ 2 0 3 0 1 3 := by decide
217theorem e_203020 : m2Num 2 0 3 0 2 0 = 8 * explicitZ 2 0 3 0 2 0 := by decide
218theorem e_203021 : m2Num 2 0 3 0 2 1 = 8 * explicitZ 2 0 3 0 2 1 := by decide
219theorem e_203022 : m2Num 2 0 3 0 2 2 = 8 * explicitZ 2 0 3 0 2 2 := by decide
220theorem e_203023 : m2Num 2 0 3 0 2 3 = 8 * explicitZ 2 0 3 0 2 3 := by decide
221theorem e_203030 : m2Num 2 0 3 0 3 0 = 8 * explicitZ 2 0 3 0 3 0 := by decide
222theorem e_203031 : m2Num 2 0 3 0 3 1 = 8 * explicitZ 2 0 3 0 3 1 := by decide
223theorem e_203032 : m2Num 2 0 3 0 3 2 = 8 * explicitZ 2 0 3 0 3 2 := by decide
224theorem e_203033 : m2Num 2 0 3 0 3 3 = 8 * explicitZ 2 0 3 0 3 3 := by decide
225theorem e_203100 : m2Num 2 0 3 1 0 0 = 8 * explicitZ 2 0 3 1 0 0 := by decide
226theorem e_203101 : m2Num 2 0 3 1 0 1 = 8 * explicitZ 2 0 3 1 0 1 := by decide
227theorem e_203102 : m2Num 2 0 3 1 0 2 = 8 * explicitZ 2 0 3 1 0 2 := by decide
228theorem e_203103 : m2Num 2 0 3 1 0 3 = 8 * explicitZ 2 0 3 1 0 3 := by decide
229theorem e_203110 : m2Num 2 0 3 1 1 0 = 8 * explicitZ 2 0 3 1 1 0 := by decide
230theorem e_203111 : m2Num 2 0 3 1 1 1 = 8 * explicitZ 2 0 3 1 1 1 := by decide
231theorem e_203112 : m2Num 2 0 3 1 1 2 = 8 * explicitZ 2 0 3 1 1 2 := by decide
232theorem e_203113 : m2Num 2 0 3 1 1 3 = 8 * explicitZ 2 0 3 1 1 3 := by decide
233theorem e_203120 : m2Num 2 0 3 1 2 0 = 8 * explicitZ 2 0 3 1 2 0 := by decide
234theorem e_203121 : m2Num 2 0 3 1 2 1 = 8 * explicitZ 2 0 3 1 2 1 := by decide
235theorem e_203122 : m2Num 2 0 3 1 2 2 = 8 * explicitZ 2 0 3 1 2 2 := by decide
236theorem e_203123 : m2Num 2 0 3 1 2 3 = 8 * explicitZ 2 0 3 1 2 3 := by decide
237theorem e_203130 : m2Num 2 0 3 1 3 0 = 8 * explicitZ 2 0 3 1 3 0 := by decide
238theorem e_203131 : m2Num 2 0 3 1 3 1 = 8 * explicitZ 2 0 3 1 3 1 := by decide
239theorem e_203132 : m2Num 2 0 3 1 3 2 = 8 * explicitZ 2 0 3 1 3 2 := by decide
240theorem e_203133 : m2Num 2 0 3 1 3 3 = 8 * explicitZ 2 0 3 1 3 3 := by decide
241theorem e_203200 : m2Num 2 0 3 2 0 0 = 8 * explicitZ 2 0 3 2 0 0 := by decide
242theorem e_203201 : m2Num 2 0 3 2 0 1 = 8 * explicitZ 2 0 3 2 0 1 := by decide
243theorem e_203202 : m2Num 2 0 3 2 0 2 = 8 * explicitZ 2 0 3 2 0 2 := by decide
244theorem e_203203 : m2Num 2 0 3 2 0 3 = 8 * explicitZ 2 0 3 2 0 3 := by decide
245theorem e_203210 : m2Num 2 0 3 2 1 0 = 8 * explicitZ 2 0 3 2 1 0 := by decide
246theorem e_203211 : m2Num 2 0 3 2 1 1 = 8 * explicitZ 2 0 3 2 1 1 := by decide
247theorem e_203212 : m2Num 2 0 3 2 1 2 = 8 * explicitZ 2 0 3 2 1 2 := by decide
248theorem e_203213 : m2Num 2 0 3 2 1 3 = 8 * explicitZ 2 0 3 2 1 3 := by decide
249theorem e_203220 : m2Num 2 0 3 2 2 0 = 8 * explicitZ 2 0 3 2 2 0 := by decide
250theorem e_203221 : m2Num 2 0 3 2 2 1 = 8 * explicitZ 2 0 3 2 2 1 := by decide
251theorem e_203222 : m2Num 2 0 3 2 2 2 = 8 * explicitZ 2 0 3 2 2 2 := by decide
252theorem e_203223 : m2Num 2 0 3 2 2 3 = 8 * explicitZ 2 0 3 2 2 3 := by decide
253theorem e_203230 : m2Num 2 0 3 2 3 0 = 8 * explicitZ 2 0 3 2 3 0 := by decide
254theorem e_203231 : m2Num 2 0 3 2 3 1 = 8 * explicitZ 2 0 3 2 3 1 := by decide
255theorem e_203232 : m2Num 2 0 3 2 3 2 = 8 * explicitZ 2 0 3 2 3 2 := by decide
256theorem e_203233 : m2Num 2 0 3 2 3 3 = 8 * explicitZ 2 0 3 2 3 3 := by decide
257theorem e_203300 : m2Num 2 0 3 3 0 0 = 8 * explicitZ 2 0 3 3 0 0 := by decide
258theorem e_203301 : m2Num 2 0 3 3 0 1 = 8 * explicitZ 2 0 3 3 0 1 := by decide
259theorem e_203302 : m2Num 2 0 3 3 0 2 = 8 * explicitZ 2 0 3 3 0 2 := by decide
260theorem e_203303 : m2Num 2 0 3 3 0 3 = 8 * explicitZ 2 0 3 3 0 3 := by decide
261theorem e_203310 : m2Num 2 0 3 3 1 0 = 8 * explicitZ 2 0 3 3 1 0 := by decide
262theorem e_203311 : m2Num 2 0 3 3 1 1 = 8 * explicitZ 2 0 3 3 1 1 := by decide
263theorem e_203312 : m2Num 2 0 3 3 1 2 = 8 * explicitZ 2 0 3 3 1 2 := by decide
264theorem e_203313 : m2Num 2 0 3 3 1 3 = 8 * explicitZ 2 0 3 3 1 3 := by decide
265theorem e_203320 : m2Num 2 0 3 3 2 0 = 8 * explicitZ 2 0 3 3 2 0 := by decide
266theorem e_203321 : m2Num 2 0 3 3 2 1 = 8 * explicitZ 2 0 3 3 2 1 := by decide
267theorem e_203322 : m2Num 2 0 3 3 2 2 = 8 * explicitZ 2 0 3 3 2 2 := by decide
268theorem e_203323 : m2Num 2 0 3 3 2 3 = 8 * explicitZ 2 0 3 3 2 3 := by decide
269theorem e_203330 : m2Num 2 0 3 3 3 0 = 8 * explicitZ 2 0 3 3 3 0 := by decide
270theorem e_203331 : m2Num 2 0 3 3 3 1 = 8 * explicitZ 2 0 3 3 3 1 := by decide
271theorem e_203332 : m2Num 2 0 3 3 3 2 = 8 * explicitZ 2 0 3 3 3 2 := by decide
272theorem e_203333 : m2Num 2 0 3 3 3 3 = 8 * explicitZ 2 0 3 3 3 3 := by decide
273
274end M2NumChunk08
275end ReggeExactMidpointM2TTIdentity4D
276end Analysis
277end Gravity
278end IndisputableMonolith
279