IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DM2NumChunk00
IndisputableMonolith/Gravity/Analysis/ReggeExactMidpointM2TTIdentity4DM2NumChunk00.lean · 279 lines · 256 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DKernelCert
3
4/-! m2Num = 8·explicitZ, chunk 0 (256 kernel decides). -/
5
6namespace IndisputableMonolith
7namespace Gravity
8namespace Analysis
9namespace ReggeExactMidpointM2TTIdentity4D
10namespace M2NumChunk00
11
12open KernelCert
13
14set_option maxRecDepth 100000
15set_option maxHeartbeats 200000000
16
17theorem e_000000 : m2Num 0 0 0 0 0 0 = 8 * explicitZ 0 0 0 0 0 0 := by decide
18theorem e_000001 : m2Num 0 0 0 0 0 1 = 8 * explicitZ 0 0 0 0 0 1 := by decide
19theorem e_000002 : m2Num 0 0 0 0 0 2 = 8 * explicitZ 0 0 0 0 0 2 := by decide
20theorem e_000003 : m2Num 0 0 0 0 0 3 = 8 * explicitZ 0 0 0 0 0 3 := by decide
21theorem e_000010 : m2Num 0 0 0 0 1 0 = 8 * explicitZ 0 0 0 0 1 0 := by decide
22theorem e_000011 : m2Num 0 0 0 0 1 1 = 8 * explicitZ 0 0 0 0 1 1 := by decide
23theorem e_000012 : m2Num 0 0 0 0 1 2 = 8 * explicitZ 0 0 0 0 1 2 := by decide
24theorem e_000013 : m2Num 0 0 0 0 1 3 = 8 * explicitZ 0 0 0 0 1 3 := by decide
25theorem e_000020 : m2Num 0 0 0 0 2 0 = 8 * explicitZ 0 0 0 0 2 0 := by decide
26theorem e_000021 : m2Num 0 0 0 0 2 1 = 8 * explicitZ 0 0 0 0 2 1 := by decide
27theorem e_000022 : m2Num 0 0 0 0 2 2 = 8 * explicitZ 0 0 0 0 2 2 := by decide
28theorem e_000023 : m2Num 0 0 0 0 2 3 = 8 * explicitZ 0 0 0 0 2 3 := by decide
29theorem e_000030 : m2Num 0 0 0 0 3 0 = 8 * explicitZ 0 0 0 0 3 0 := by decide
30theorem e_000031 : m2Num 0 0 0 0 3 1 = 8 * explicitZ 0 0 0 0 3 1 := by decide
31theorem e_000032 : m2Num 0 0 0 0 3 2 = 8 * explicitZ 0 0 0 0 3 2 := by decide
32theorem e_000033 : m2Num 0 0 0 0 3 3 = 8 * explicitZ 0 0 0 0 3 3 := by decide
33theorem e_000100 : m2Num 0 0 0 1 0 0 = 8 * explicitZ 0 0 0 1 0 0 := by decide
34theorem e_000101 : m2Num 0 0 0 1 0 1 = 8 * explicitZ 0 0 0 1 0 1 := by decide
35theorem e_000102 : m2Num 0 0 0 1 0 2 = 8 * explicitZ 0 0 0 1 0 2 := by decide
36theorem e_000103 : m2Num 0 0 0 1 0 3 = 8 * explicitZ 0 0 0 1 0 3 := by decide
37theorem e_000110 : m2Num 0 0 0 1 1 0 = 8 * explicitZ 0 0 0 1 1 0 := by decide
38theorem e_000111 : m2Num 0 0 0 1 1 1 = 8 * explicitZ 0 0 0 1 1 1 := by decide
39theorem e_000112 : m2Num 0 0 0 1 1 2 = 8 * explicitZ 0 0 0 1 1 2 := by decide
40theorem e_000113 : m2Num 0 0 0 1 1 3 = 8 * explicitZ 0 0 0 1 1 3 := by decide
41theorem e_000120 : m2Num 0 0 0 1 2 0 = 8 * explicitZ 0 0 0 1 2 0 := by decide
42theorem e_000121 : m2Num 0 0 0 1 2 1 = 8 * explicitZ 0 0 0 1 2 1 := by decide
43theorem e_000122 : m2Num 0 0 0 1 2 2 = 8 * explicitZ 0 0 0 1 2 2 := by decide
44theorem e_000123 : m2Num 0 0 0 1 2 3 = 8 * explicitZ 0 0 0 1 2 3 := by decide
45theorem e_000130 : m2Num 0 0 0 1 3 0 = 8 * explicitZ 0 0 0 1 3 0 := by decide
46theorem e_000131 : m2Num 0 0 0 1 3 1 = 8 * explicitZ 0 0 0 1 3 1 := by decide
47theorem e_000132 : m2Num 0 0 0 1 3 2 = 8 * explicitZ 0 0 0 1 3 2 := by decide
48theorem e_000133 : m2Num 0 0 0 1 3 3 = 8 * explicitZ 0 0 0 1 3 3 := by decide
49theorem e_000200 : m2Num 0 0 0 2 0 0 = 8 * explicitZ 0 0 0 2 0 0 := by decide
50theorem e_000201 : m2Num 0 0 0 2 0 1 = 8 * explicitZ 0 0 0 2 0 1 := by decide
51theorem e_000202 : m2Num 0 0 0 2 0 2 = 8 * explicitZ 0 0 0 2 0 2 := by decide
52theorem e_000203 : m2Num 0 0 0 2 0 3 = 8 * explicitZ 0 0 0 2 0 3 := by decide
53theorem e_000210 : m2Num 0 0 0 2 1 0 = 8 * explicitZ 0 0 0 2 1 0 := by decide
54theorem e_000211 : m2Num 0 0 0 2 1 1 = 8 * explicitZ 0 0 0 2 1 1 := by decide
55theorem e_000212 : m2Num 0 0 0 2 1 2 = 8 * explicitZ 0 0 0 2 1 2 := by decide
56theorem e_000213 : m2Num 0 0 0 2 1 3 = 8 * explicitZ 0 0 0 2 1 3 := by decide
57theorem e_000220 : m2Num 0 0 0 2 2 0 = 8 * explicitZ 0 0 0 2 2 0 := by decide
58theorem e_000221 : m2Num 0 0 0 2 2 1 = 8 * explicitZ 0 0 0 2 2 1 := by decide
59theorem e_000222 : m2Num 0 0 0 2 2 2 = 8 * explicitZ 0 0 0 2 2 2 := by decide
60theorem e_000223 : m2Num 0 0 0 2 2 3 = 8 * explicitZ 0 0 0 2 2 3 := by decide
61theorem e_000230 : m2Num 0 0 0 2 3 0 = 8 * explicitZ 0 0 0 2 3 0 := by decide
62theorem e_000231 : m2Num 0 0 0 2 3 1 = 8 * explicitZ 0 0 0 2 3 1 := by decide
63theorem e_000232 : m2Num 0 0 0 2 3 2 = 8 * explicitZ 0 0 0 2 3 2 := by decide
64theorem e_000233 : m2Num 0 0 0 2 3 3 = 8 * explicitZ 0 0 0 2 3 3 := by decide
65theorem e_000300 : m2Num 0 0 0 3 0 0 = 8 * explicitZ 0 0 0 3 0 0 := by decide
66theorem e_000301 : m2Num 0 0 0 3 0 1 = 8 * explicitZ 0 0 0 3 0 1 := by decide
67theorem e_000302 : m2Num 0 0 0 3 0 2 = 8 * explicitZ 0 0 0 3 0 2 := by decide
68theorem e_000303 : m2Num 0 0 0 3 0 3 = 8 * explicitZ 0 0 0 3 0 3 := by decide
69theorem e_000310 : m2Num 0 0 0 3 1 0 = 8 * explicitZ 0 0 0 3 1 0 := by decide
70theorem e_000311 : m2Num 0 0 0 3 1 1 = 8 * explicitZ 0 0 0 3 1 1 := by decide
71theorem e_000312 : m2Num 0 0 0 3 1 2 = 8 * explicitZ 0 0 0 3 1 2 := by decide
72theorem e_000313 : m2Num 0 0 0 3 1 3 = 8 * explicitZ 0 0 0 3 1 3 := by decide
73theorem e_000320 : m2Num 0 0 0 3 2 0 = 8 * explicitZ 0 0 0 3 2 0 := by decide
74theorem e_000321 : m2Num 0 0 0 3 2 1 = 8 * explicitZ 0 0 0 3 2 1 := by decide
75theorem e_000322 : m2Num 0 0 0 3 2 2 = 8 * explicitZ 0 0 0 3 2 2 := by decide
76theorem e_000323 : m2Num 0 0 0 3 2 3 = 8 * explicitZ 0 0 0 3 2 3 := by decide
77theorem e_000330 : m2Num 0 0 0 3 3 0 = 8 * explicitZ 0 0 0 3 3 0 := by decide
78theorem e_000331 : m2Num 0 0 0 3 3 1 = 8 * explicitZ 0 0 0 3 3 1 := by decide
79theorem e_000332 : m2Num 0 0 0 3 3 2 = 8 * explicitZ 0 0 0 3 3 2 := by decide
80theorem e_000333 : m2Num 0 0 0 3 3 3 = 8 * explicitZ 0 0 0 3 3 3 := by decide
81theorem e_001000 : m2Num 0 0 1 0 0 0 = 8 * explicitZ 0 0 1 0 0 0 := by decide
82theorem e_001001 : m2Num 0 0 1 0 0 1 = 8 * explicitZ 0 0 1 0 0 1 := by decide
83theorem e_001002 : m2Num 0 0 1 0 0 2 = 8 * explicitZ 0 0 1 0 0 2 := by decide
84theorem e_001003 : m2Num 0 0 1 0 0 3 = 8 * explicitZ 0 0 1 0 0 3 := by decide
85theorem e_001010 : m2Num 0 0 1 0 1 0 = 8 * explicitZ 0 0 1 0 1 0 := by decide
86theorem e_001011 : m2Num 0 0 1 0 1 1 = 8 * explicitZ 0 0 1 0 1 1 := by decide
87theorem e_001012 : m2Num 0 0 1 0 1 2 = 8 * explicitZ 0 0 1 0 1 2 := by decide
88theorem e_001013 : m2Num 0 0 1 0 1 3 = 8 * explicitZ 0 0 1 0 1 3 := by decide
89theorem e_001020 : m2Num 0 0 1 0 2 0 = 8 * explicitZ 0 0 1 0 2 0 := by decide
90theorem e_001021 : m2Num 0 0 1 0 2 1 = 8 * explicitZ 0 0 1 0 2 1 := by decide
91theorem e_001022 : m2Num 0 0 1 0 2 2 = 8 * explicitZ 0 0 1 0 2 2 := by decide
92theorem e_001023 : m2Num 0 0 1 0 2 3 = 8 * explicitZ 0 0 1 0 2 3 := by decide
93theorem e_001030 : m2Num 0 0 1 0 3 0 = 8 * explicitZ 0 0 1 0 3 0 := by decide
94theorem e_001031 : m2Num 0 0 1 0 3 1 = 8 * explicitZ 0 0 1 0 3 1 := by decide
95theorem e_001032 : m2Num 0 0 1 0 3 2 = 8 * explicitZ 0 0 1 0 3 2 := by decide
96theorem e_001033 : m2Num 0 0 1 0 3 3 = 8 * explicitZ 0 0 1 0 3 3 := by decide
97theorem e_001100 : m2Num 0 0 1 1 0 0 = 8 * explicitZ 0 0 1 1 0 0 := by decide
98theorem e_001101 : m2Num 0 0 1 1 0 1 = 8 * explicitZ 0 0 1 1 0 1 := by decide
99theorem e_001102 : m2Num 0 0 1 1 0 2 = 8 * explicitZ 0 0 1 1 0 2 := by decide
100theorem e_001103 : m2Num 0 0 1 1 0 3 = 8 * explicitZ 0 0 1 1 0 3 := by decide
101theorem e_001110 : m2Num 0 0 1 1 1 0 = 8 * explicitZ 0 0 1 1 1 0 := by decide
102theorem e_001111 : m2Num 0 0 1 1 1 1 = 8 * explicitZ 0 0 1 1 1 1 := by decide
103theorem e_001112 : m2Num 0 0 1 1 1 2 = 8 * explicitZ 0 0 1 1 1 2 := by decide
104theorem e_001113 : m2Num 0 0 1 1 1 3 = 8 * explicitZ 0 0 1 1 1 3 := by decide
105theorem e_001120 : m2Num 0 0 1 1 2 0 = 8 * explicitZ 0 0 1 1 2 0 := by decide
106theorem e_001121 : m2Num 0 0 1 1 2 1 = 8 * explicitZ 0 0 1 1 2 1 := by decide
107theorem e_001122 : m2Num 0 0 1 1 2 2 = 8 * explicitZ 0 0 1 1 2 2 := by decide
108theorem e_001123 : m2Num 0 0 1 1 2 3 = 8 * explicitZ 0 0 1 1 2 3 := by decide
109theorem e_001130 : m2Num 0 0 1 1 3 0 = 8 * explicitZ 0 0 1 1 3 0 := by decide
110theorem e_001131 : m2Num 0 0 1 1 3 1 = 8 * explicitZ 0 0 1 1 3 1 := by decide
111theorem e_001132 : m2Num 0 0 1 1 3 2 = 8 * explicitZ 0 0 1 1 3 2 := by decide
112theorem e_001133 : m2Num 0 0 1 1 3 3 = 8 * explicitZ 0 0 1 1 3 3 := by decide
113theorem e_001200 : m2Num 0 0 1 2 0 0 = 8 * explicitZ 0 0 1 2 0 0 := by decide
114theorem e_001201 : m2Num 0 0 1 2 0 1 = 8 * explicitZ 0 0 1 2 0 1 := by decide
115theorem e_001202 : m2Num 0 0 1 2 0 2 = 8 * explicitZ 0 0 1 2 0 2 := by decide
116theorem e_001203 : m2Num 0 0 1 2 0 3 = 8 * explicitZ 0 0 1 2 0 3 := by decide
117theorem e_001210 : m2Num 0 0 1 2 1 0 = 8 * explicitZ 0 0 1 2 1 0 := by decide
118theorem e_001211 : m2Num 0 0 1 2 1 1 = 8 * explicitZ 0 0 1 2 1 1 := by decide
119theorem e_001212 : m2Num 0 0 1 2 1 2 = 8 * explicitZ 0 0 1 2 1 2 := by decide
120theorem e_001213 : m2Num 0 0 1 2 1 3 = 8 * explicitZ 0 0 1 2 1 3 := by decide
121theorem e_001220 : m2Num 0 0 1 2 2 0 = 8 * explicitZ 0 0 1 2 2 0 := by decide
122theorem e_001221 : m2Num 0 0 1 2 2 1 = 8 * explicitZ 0 0 1 2 2 1 := by decide
123theorem e_001222 : m2Num 0 0 1 2 2 2 = 8 * explicitZ 0 0 1 2 2 2 := by decide
124theorem e_001223 : m2Num 0 0 1 2 2 3 = 8 * explicitZ 0 0 1 2 2 3 := by decide
125theorem e_001230 : m2Num 0 0 1 2 3 0 = 8 * explicitZ 0 0 1 2 3 0 := by decide
126theorem e_001231 : m2Num 0 0 1 2 3 1 = 8 * explicitZ 0 0 1 2 3 1 := by decide
127theorem e_001232 : m2Num 0 0 1 2 3 2 = 8 * explicitZ 0 0 1 2 3 2 := by decide
128theorem e_001233 : m2Num 0 0 1 2 3 3 = 8 * explicitZ 0 0 1 2 3 3 := by decide
129theorem e_001300 : m2Num 0 0 1 3 0 0 = 8 * explicitZ 0 0 1 3 0 0 := by decide
130theorem e_001301 : m2Num 0 0 1 3 0 1 = 8 * explicitZ 0 0 1 3 0 1 := by decide
131theorem e_001302 : m2Num 0 0 1 3 0 2 = 8 * explicitZ 0 0 1 3 0 2 := by decide
132theorem e_001303 : m2Num 0 0 1 3 0 3 = 8 * explicitZ 0 0 1 3 0 3 := by decide
133theorem e_001310 : m2Num 0 0 1 3 1 0 = 8 * explicitZ 0 0 1 3 1 0 := by decide
134theorem e_001311 : m2Num 0 0 1 3 1 1 = 8 * explicitZ 0 0 1 3 1 1 := by decide
135theorem e_001312 : m2Num 0 0 1 3 1 2 = 8 * explicitZ 0 0 1 3 1 2 := by decide
136theorem e_001313 : m2Num 0 0 1 3 1 3 = 8 * explicitZ 0 0 1 3 1 3 := by decide
137theorem e_001320 : m2Num 0 0 1 3 2 0 = 8 * explicitZ 0 0 1 3 2 0 := by decide
138theorem e_001321 : m2Num 0 0 1 3 2 1 = 8 * explicitZ 0 0 1 3 2 1 := by decide
139theorem e_001322 : m2Num 0 0 1 3 2 2 = 8 * explicitZ 0 0 1 3 2 2 := by decide
140theorem e_001323 : m2Num 0 0 1 3 2 3 = 8 * explicitZ 0 0 1 3 2 3 := by decide
141theorem e_001330 : m2Num 0 0 1 3 3 0 = 8 * explicitZ 0 0 1 3 3 0 := by decide
142theorem e_001331 : m2Num 0 0 1 3 3 1 = 8 * explicitZ 0 0 1 3 3 1 := by decide
143theorem e_001332 : m2Num 0 0 1 3 3 2 = 8 * explicitZ 0 0 1 3 3 2 := by decide
144theorem e_001333 : m2Num 0 0 1 3 3 3 = 8 * explicitZ 0 0 1 3 3 3 := by decide
145theorem e_002000 : m2Num 0 0 2 0 0 0 = 8 * explicitZ 0 0 2 0 0 0 := by decide
146theorem e_002001 : m2Num 0 0 2 0 0 1 = 8 * explicitZ 0 0 2 0 0 1 := by decide
147theorem e_002002 : m2Num 0 0 2 0 0 2 = 8 * explicitZ 0 0 2 0 0 2 := by decide
148theorem e_002003 : m2Num 0 0 2 0 0 3 = 8 * explicitZ 0 0 2 0 0 3 := by decide
149theorem e_002010 : m2Num 0 0 2 0 1 0 = 8 * explicitZ 0 0 2 0 1 0 := by decide
150theorem e_002011 : m2Num 0 0 2 0 1 1 = 8 * explicitZ 0 0 2 0 1 1 := by decide
151theorem e_002012 : m2Num 0 0 2 0 1 2 = 8 * explicitZ 0 0 2 0 1 2 := by decide
152theorem e_002013 : m2Num 0 0 2 0 1 3 = 8 * explicitZ 0 0 2 0 1 3 := by decide
153theorem e_002020 : m2Num 0 0 2 0 2 0 = 8 * explicitZ 0 0 2 0 2 0 := by decide
154theorem e_002021 : m2Num 0 0 2 0 2 1 = 8 * explicitZ 0 0 2 0 2 1 := by decide
155theorem e_002022 : m2Num 0 0 2 0 2 2 = 8 * explicitZ 0 0 2 0 2 2 := by decide
156theorem e_002023 : m2Num 0 0 2 0 2 3 = 8 * explicitZ 0 0 2 0 2 3 := by decide
157theorem e_002030 : m2Num 0 0 2 0 3 0 = 8 * explicitZ 0 0 2 0 3 0 := by decide
158theorem e_002031 : m2Num 0 0 2 0 3 1 = 8 * explicitZ 0 0 2 0 3 1 := by decide
159theorem e_002032 : m2Num 0 0 2 0 3 2 = 8 * explicitZ 0 0 2 0 3 2 := by decide
160theorem e_002033 : m2Num 0 0 2 0 3 3 = 8 * explicitZ 0 0 2 0 3 3 := by decide
161theorem e_002100 : m2Num 0 0 2 1 0 0 = 8 * explicitZ 0 0 2 1 0 0 := by decide
162theorem e_002101 : m2Num 0 0 2 1 0 1 = 8 * explicitZ 0 0 2 1 0 1 := by decide
163theorem e_002102 : m2Num 0 0 2 1 0 2 = 8 * explicitZ 0 0 2 1 0 2 := by decide
164theorem e_002103 : m2Num 0 0 2 1 0 3 = 8 * explicitZ 0 0 2 1 0 3 := by decide
165theorem e_002110 : m2Num 0 0 2 1 1 0 = 8 * explicitZ 0 0 2 1 1 0 := by decide
166theorem e_002111 : m2Num 0 0 2 1 1 1 = 8 * explicitZ 0 0 2 1 1 1 := by decide
167theorem e_002112 : m2Num 0 0 2 1 1 2 = 8 * explicitZ 0 0 2 1 1 2 := by decide
168theorem e_002113 : m2Num 0 0 2 1 1 3 = 8 * explicitZ 0 0 2 1 1 3 := by decide
169theorem e_002120 : m2Num 0 0 2 1 2 0 = 8 * explicitZ 0 0 2 1 2 0 := by decide
170theorem e_002121 : m2Num 0 0 2 1 2 1 = 8 * explicitZ 0 0 2 1 2 1 := by decide
171theorem e_002122 : m2Num 0 0 2 1 2 2 = 8 * explicitZ 0 0 2 1 2 2 := by decide
172theorem e_002123 : m2Num 0 0 2 1 2 3 = 8 * explicitZ 0 0 2 1 2 3 := by decide
173theorem e_002130 : m2Num 0 0 2 1 3 0 = 8 * explicitZ 0 0 2 1 3 0 := by decide
174theorem e_002131 : m2Num 0 0 2 1 3 1 = 8 * explicitZ 0 0 2 1 3 1 := by decide
175theorem e_002132 : m2Num 0 0 2 1 3 2 = 8 * explicitZ 0 0 2 1 3 2 := by decide
176theorem e_002133 : m2Num 0 0 2 1 3 3 = 8 * explicitZ 0 0 2 1 3 3 := by decide
177theorem e_002200 : m2Num 0 0 2 2 0 0 = 8 * explicitZ 0 0 2 2 0 0 := by decide
178theorem e_002201 : m2Num 0 0 2 2 0 1 = 8 * explicitZ 0 0 2 2 0 1 := by decide
179theorem e_002202 : m2Num 0 0 2 2 0 2 = 8 * explicitZ 0 0 2 2 0 2 := by decide
180theorem e_002203 : m2Num 0 0 2 2 0 3 = 8 * explicitZ 0 0 2 2 0 3 := by decide
181theorem e_002210 : m2Num 0 0 2 2 1 0 = 8 * explicitZ 0 0 2 2 1 0 := by decide
182theorem e_002211 : m2Num 0 0 2 2 1 1 = 8 * explicitZ 0 0 2 2 1 1 := by decide
183theorem e_002212 : m2Num 0 0 2 2 1 2 = 8 * explicitZ 0 0 2 2 1 2 := by decide
184theorem e_002213 : m2Num 0 0 2 2 1 3 = 8 * explicitZ 0 0 2 2 1 3 := by decide
185theorem e_002220 : m2Num 0 0 2 2 2 0 = 8 * explicitZ 0 0 2 2 2 0 := by decide
186theorem e_002221 : m2Num 0 0 2 2 2 1 = 8 * explicitZ 0 0 2 2 2 1 := by decide
187theorem e_002222 : m2Num 0 0 2 2 2 2 = 8 * explicitZ 0 0 2 2 2 2 := by decide
188theorem e_002223 : m2Num 0 0 2 2 2 3 = 8 * explicitZ 0 0 2 2 2 3 := by decide
189theorem e_002230 : m2Num 0 0 2 2 3 0 = 8 * explicitZ 0 0 2 2 3 0 := by decide
190theorem e_002231 : m2Num 0 0 2 2 3 1 = 8 * explicitZ 0 0 2 2 3 1 := by decide
191theorem e_002232 : m2Num 0 0 2 2 3 2 = 8 * explicitZ 0 0 2 2 3 2 := by decide
192theorem e_002233 : m2Num 0 0 2 2 3 3 = 8 * explicitZ 0 0 2 2 3 3 := by decide
193theorem e_002300 : m2Num 0 0 2 3 0 0 = 8 * explicitZ 0 0 2 3 0 0 := by decide
194theorem e_002301 : m2Num 0 0 2 3 0 1 = 8 * explicitZ 0 0 2 3 0 1 := by decide
195theorem e_002302 : m2Num 0 0 2 3 0 2 = 8 * explicitZ 0 0 2 3 0 2 := by decide
196theorem e_002303 : m2Num 0 0 2 3 0 3 = 8 * explicitZ 0 0 2 3 0 3 := by decide
197theorem e_002310 : m2Num 0 0 2 3 1 0 = 8 * explicitZ 0 0 2 3 1 0 := by decide
198theorem e_002311 : m2Num 0 0 2 3 1 1 = 8 * explicitZ 0 0 2 3 1 1 := by decide
199theorem e_002312 : m2Num 0 0 2 3 1 2 = 8 * explicitZ 0 0 2 3 1 2 := by decide
200theorem e_002313 : m2Num 0 0 2 3 1 3 = 8 * explicitZ 0 0 2 3 1 3 := by decide
201theorem e_002320 : m2Num 0 0 2 3 2 0 = 8 * explicitZ 0 0 2 3 2 0 := by decide
202theorem e_002321 : m2Num 0 0 2 3 2 1 = 8 * explicitZ 0 0 2 3 2 1 := by decide
203theorem e_002322 : m2Num 0 0 2 3 2 2 = 8 * explicitZ 0 0 2 3 2 2 := by decide
204theorem e_002323 : m2Num 0 0 2 3 2 3 = 8 * explicitZ 0 0 2 3 2 3 := by decide
205theorem e_002330 : m2Num 0 0 2 3 3 0 = 8 * explicitZ 0 0 2 3 3 0 := by decide
206theorem e_002331 : m2Num 0 0 2 3 3 1 = 8 * explicitZ 0 0 2 3 3 1 := by decide
207theorem e_002332 : m2Num 0 0 2 3 3 2 = 8 * explicitZ 0 0 2 3 3 2 := by decide
208theorem e_002333 : m2Num 0 0 2 3 3 3 = 8 * explicitZ 0 0 2 3 3 3 := by decide
209theorem e_003000 : m2Num 0 0 3 0 0 0 = 8 * explicitZ 0 0 3 0 0 0 := by decide
210theorem e_003001 : m2Num 0 0 3 0 0 1 = 8 * explicitZ 0 0 3 0 0 1 := by decide
211theorem e_003002 : m2Num 0 0 3 0 0 2 = 8 * explicitZ 0 0 3 0 0 2 := by decide
212theorem e_003003 : m2Num 0 0 3 0 0 3 = 8 * explicitZ 0 0 3 0 0 3 := by decide
213theorem e_003010 : m2Num 0 0 3 0 1 0 = 8 * explicitZ 0 0 3 0 1 0 := by decide
214theorem e_003011 : m2Num 0 0 3 0 1 1 = 8 * explicitZ 0 0 3 0 1 1 := by decide
215theorem e_003012 : m2Num 0 0 3 0 1 2 = 8 * explicitZ 0 0 3 0 1 2 := by decide
216theorem e_003013 : m2Num 0 0 3 0 1 3 = 8 * explicitZ 0 0 3 0 1 3 := by decide
217theorem e_003020 : m2Num 0 0 3 0 2 0 = 8 * explicitZ 0 0 3 0 2 0 := by decide
218theorem e_003021 : m2Num 0 0 3 0 2 1 = 8 * explicitZ 0 0 3 0 2 1 := by decide
219theorem e_003022 : m2Num 0 0 3 0 2 2 = 8 * explicitZ 0 0 3 0 2 2 := by decide
220theorem e_003023 : m2Num 0 0 3 0 2 3 = 8 * explicitZ 0 0 3 0 2 3 := by decide
221theorem e_003030 : m2Num 0 0 3 0 3 0 = 8 * explicitZ 0 0 3 0 3 0 := by decide
222theorem e_003031 : m2Num 0 0 3 0 3 1 = 8 * explicitZ 0 0 3 0 3 1 := by decide
223theorem e_003032 : m2Num 0 0 3 0 3 2 = 8 * explicitZ 0 0 3 0 3 2 := by decide
224theorem e_003033 : m2Num 0 0 3 0 3 3 = 8 * explicitZ 0 0 3 0 3 3 := by decide
225theorem e_003100 : m2Num 0 0 3 1 0 0 = 8 * explicitZ 0 0 3 1 0 0 := by decide
226theorem e_003101 : m2Num 0 0 3 1 0 1 = 8 * explicitZ 0 0 3 1 0 1 := by decide
227theorem e_003102 : m2Num 0 0 3 1 0 2 = 8 * explicitZ 0 0 3 1 0 2 := by decide
228theorem e_003103 : m2Num 0 0 3 1 0 3 = 8 * explicitZ 0 0 3 1 0 3 := by decide
229theorem e_003110 : m2Num 0 0 3 1 1 0 = 8 * explicitZ 0 0 3 1 1 0 := by decide
230theorem e_003111 : m2Num 0 0 3 1 1 1 = 8 * explicitZ 0 0 3 1 1 1 := by decide
231theorem e_003112 : m2Num 0 0 3 1 1 2 = 8 * explicitZ 0 0 3 1 1 2 := by decide
232theorem e_003113 : m2Num 0 0 3 1 1 3 = 8 * explicitZ 0 0 3 1 1 3 := by decide
233theorem e_003120 : m2Num 0 0 3 1 2 0 = 8 * explicitZ 0 0 3 1 2 0 := by decide
234theorem e_003121 : m2Num 0 0 3 1 2 1 = 8 * explicitZ 0 0 3 1 2 1 := by decide
235theorem e_003122 : m2Num 0 0 3 1 2 2 = 8 * explicitZ 0 0 3 1 2 2 := by decide
236theorem e_003123 : m2Num 0 0 3 1 2 3 = 8 * explicitZ 0 0 3 1 2 3 := by decide
237theorem e_003130 : m2Num 0 0 3 1 3 0 = 8 * explicitZ 0 0 3 1 3 0 := by decide
238theorem e_003131 : m2Num 0 0 3 1 3 1 = 8 * explicitZ 0 0 3 1 3 1 := by decide
239theorem e_003132 : m2Num 0 0 3 1 3 2 = 8 * explicitZ 0 0 3 1 3 2 := by decide
240theorem e_003133 : m2Num 0 0 3 1 3 3 = 8 * explicitZ 0 0 3 1 3 3 := by decide
241theorem e_003200 : m2Num 0 0 3 2 0 0 = 8 * explicitZ 0 0 3 2 0 0 := by decide
242theorem e_003201 : m2Num 0 0 3 2 0 1 = 8 * explicitZ 0 0 3 2 0 1 := by decide
243theorem e_003202 : m2Num 0 0 3 2 0 2 = 8 * explicitZ 0 0 3 2 0 2 := by decide
244theorem e_003203 : m2Num 0 0 3 2 0 3 = 8 * explicitZ 0 0 3 2 0 3 := by decide
245theorem e_003210 : m2Num 0 0 3 2 1 0 = 8 * explicitZ 0 0 3 2 1 0 := by decide
246theorem e_003211 : m2Num 0 0 3 2 1 1 = 8 * explicitZ 0 0 3 2 1 1 := by decide
247theorem e_003212 : m2Num 0 0 3 2 1 2 = 8 * explicitZ 0 0 3 2 1 2 := by decide
248theorem e_003213 : m2Num 0 0 3 2 1 3 = 8 * explicitZ 0 0 3 2 1 3 := by decide
249theorem e_003220 : m2Num 0 0 3 2 2 0 = 8 * explicitZ 0 0 3 2 2 0 := by decide
250theorem e_003221 : m2Num 0 0 3 2 2 1 = 8 * explicitZ 0 0 3 2 2 1 := by decide
251theorem e_003222 : m2Num 0 0 3 2 2 2 = 8 * explicitZ 0 0 3 2 2 2 := by decide
252theorem e_003223 : m2Num 0 0 3 2 2 3 = 8 * explicitZ 0 0 3 2 2 3 := by decide
253theorem e_003230 : m2Num 0 0 3 2 3 0 = 8 * explicitZ 0 0 3 2 3 0 := by decide
254theorem e_003231 : m2Num 0 0 3 2 3 1 = 8 * explicitZ 0 0 3 2 3 1 := by decide
255theorem e_003232 : m2Num 0 0 3 2 3 2 = 8 * explicitZ 0 0 3 2 3 2 := by decide
256theorem e_003233 : m2Num 0 0 3 2 3 3 = 8 * explicitZ 0 0 3 2 3 3 := by decide
257theorem e_003300 : m2Num 0 0 3 3 0 0 = 8 * explicitZ 0 0 3 3 0 0 := by decide
258theorem e_003301 : m2Num 0 0 3 3 0 1 = 8 * explicitZ 0 0 3 3 0 1 := by decide
259theorem e_003302 : m2Num 0 0 3 3 0 2 = 8 * explicitZ 0 0 3 3 0 2 := by decide
260theorem e_003303 : m2Num 0 0 3 3 0 3 = 8 * explicitZ 0 0 3 3 0 3 := by decide
261theorem e_003310 : m2Num 0 0 3 3 1 0 = 8 * explicitZ 0 0 3 3 1 0 := by decide
262theorem e_003311 : m2Num 0 0 3 3 1 1 = 8 * explicitZ 0 0 3 3 1 1 := by decide
263theorem e_003312 : m2Num 0 0 3 3 1 2 = 8 * explicitZ 0 0 3 3 1 2 := by decide
264theorem e_003313 : m2Num 0 0 3 3 1 3 = 8 * explicitZ 0 0 3 3 1 3 := by decide
265theorem e_003320 : m2Num 0 0 3 3 2 0 = 8 * explicitZ 0 0 3 3 2 0 := by decide
266theorem e_003321 : m2Num 0 0 3 3 2 1 = 8 * explicitZ 0 0 3 3 2 1 := by decide
267theorem e_003322 : m2Num 0 0 3 3 2 2 = 8 * explicitZ 0 0 3 3 2 2 := by decide
268theorem e_003323 : m2Num 0 0 3 3 2 3 = 8 * explicitZ 0 0 3 3 2 3 := by decide
269theorem e_003330 : m2Num 0 0 3 3 3 0 = 8 * explicitZ 0 0 3 3 3 0 := by decide
270theorem e_003331 : m2Num 0 0 3 3 3 1 = 8 * explicitZ 0 0 3 3 3 1 := by decide
271theorem e_003332 : m2Num 0 0 3 3 3 2 = 8 * explicitZ 0 0 3 3 3 2 := by decide
272theorem e_003333 : m2Num 0 0 3 3 3 3 = 8 * explicitZ 0 0 3 3 3 3 := by decide
273
274end M2NumChunk00
275end ReggeExactMidpointM2TTIdentity4D
276end Analysis
277end Gravity
278end IndisputableMonolith
279