IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DM2NumChunk10
IndisputableMonolith/Gravity/Analysis/ReggeExactMidpointM2TTIdentity4DM2NumChunk10.lean · 279 lines · 256 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DKernelCert
3
4/-! m2Num = 8·explicitZ, chunk 10 (256 kernel decides). -/
5
6namespace IndisputableMonolith
7namespace Gravity
8namespace Analysis
9namespace ReggeExactMidpointM2TTIdentity4D
10namespace M2NumChunk10
11
12open KernelCert
13
14set_option maxRecDepth 100000
15set_option maxHeartbeats 200000000
16
17theorem e_220000 : m2Num 2 2 0 0 0 0 = 8 * explicitZ 2 2 0 0 0 0 := by decide
18theorem e_220001 : m2Num 2 2 0 0 0 1 = 8 * explicitZ 2 2 0 0 0 1 := by decide
19theorem e_220002 : m2Num 2 2 0 0 0 2 = 8 * explicitZ 2 2 0 0 0 2 := by decide
20theorem e_220003 : m2Num 2 2 0 0 0 3 = 8 * explicitZ 2 2 0 0 0 3 := by decide
21theorem e_220010 : m2Num 2 2 0 0 1 0 = 8 * explicitZ 2 2 0 0 1 0 := by decide
22theorem e_220011 : m2Num 2 2 0 0 1 1 = 8 * explicitZ 2 2 0 0 1 1 := by decide
23theorem e_220012 : m2Num 2 2 0 0 1 2 = 8 * explicitZ 2 2 0 0 1 2 := by decide
24theorem e_220013 : m2Num 2 2 0 0 1 3 = 8 * explicitZ 2 2 0 0 1 3 := by decide
25theorem e_220020 : m2Num 2 2 0 0 2 0 = 8 * explicitZ 2 2 0 0 2 0 := by decide
26theorem e_220021 : m2Num 2 2 0 0 2 1 = 8 * explicitZ 2 2 0 0 2 1 := by decide
27theorem e_220022 : m2Num 2 2 0 0 2 2 = 8 * explicitZ 2 2 0 0 2 2 := by decide
28theorem e_220023 : m2Num 2 2 0 0 2 3 = 8 * explicitZ 2 2 0 0 2 3 := by decide
29theorem e_220030 : m2Num 2 2 0 0 3 0 = 8 * explicitZ 2 2 0 0 3 0 := by decide
30theorem e_220031 : m2Num 2 2 0 0 3 1 = 8 * explicitZ 2 2 0 0 3 1 := by decide
31theorem e_220032 : m2Num 2 2 0 0 3 2 = 8 * explicitZ 2 2 0 0 3 2 := by decide
32theorem e_220033 : m2Num 2 2 0 0 3 3 = 8 * explicitZ 2 2 0 0 3 3 := by decide
33theorem e_220100 : m2Num 2 2 0 1 0 0 = 8 * explicitZ 2 2 0 1 0 0 := by decide
34theorem e_220101 : m2Num 2 2 0 1 0 1 = 8 * explicitZ 2 2 0 1 0 1 := by decide
35theorem e_220102 : m2Num 2 2 0 1 0 2 = 8 * explicitZ 2 2 0 1 0 2 := by decide
36theorem e_220103 : m2Num 2 2 0 1 0 3 = 8 * explicitZ 2 2 0 1 0 3 := by decide
37theorem e_220110 : m2Num 2 2 0 1 1 0 = 8 * explicitZ 2 2 0 1 1 0 := by decide
38theorem e_220111 : m2Num 2 2 0 1 1 1 = 8 * explicitZ 2 2 0 1 1 1 := by decide
39theorem e_220112 : m2Num 2 2 0 1 1 2 = 8 * explicitZ 2 2 0 1 1 2 := by decide
40theorem e_220113 : m2Num 2 2 0 1 1 3 = 8 * explicitZ 2 2 0 1 1 3 := by decide
41theorem e_220120 : m2Num 2 2 0 1 2 0 = 8 * explicitZ 2 2 0 1 2 0 := by decide
42theorem e_220121 : m2Num 2 2 0 1 2 1 = 8 * explicitZ 2 2 0 1 2 1 := by decide
43theorem e_220122 : m2Num 2 2 0 1 2 2 = 8 * explicitZ 2 2 0 1 2 2 := by decide
44theorem e_220123 : m2Num 2 2 0 1 2 3 = 8 * explicitZ 2 2 0 1 2 3 := by decide
45theorem e_220130 : m2Num 2 2 0 1 3 0 = 8 * explicitZ 2 2 0 1 3 0 := by decide
46theorem e_220131 : m2Num 2 2 0 1 3 1 = 8 * explicitZ 2 2 0 1 3 1 := by decide
47theorem e_220132 : m2Num 2 2 0 1 3 2 = 8 * explicitZ 2 2 0 1 3 2 := by decide
48theorem e_220133 : m2Num 2 2 0 1 3 3 = 8 * explicitZ 2 2 0 1 3 3 := by decide
49theorem e_220200 : m2Num 2 2 0 2 0 0 = 8 * explicitZ 2 2 0 2 0 0 := by decide
50theorem e_220201 : m2Num 2 2 0 2 0 1 = 8 * explicitZ 2 2 0 2 0 1 := by decide
51theorem e_220202 : m2Num 2 2 0 2 0 2 = 8 * explicitZ 2 2 0 2 0 2 := by decide
52theorem e_220203 : m2Num 2 2 0 2 0 3 = 8 * explicitZ 2 2 0 2 0 3 := by decide
53theorem e_220210 : m2Num 2 2 0 2 1 0 = 8 * explicitZ 2 2 0 2 1 0 := by decide
54theorem e_220211 : m2Num 2 2 0 2 1 1 = 8 * explicitZ 2 2 0 2 1 1 := by decide
55theorem e_220212 : m2Num 2 2 0 2 1 2 = 8 * explicitZ 2 2 0 2 1 2 := by decide
56theorem e_220213 : m2Num 2 2 0 2 1 3 = 8 * explicitZ 2 2 0 2 1 3 := by decide
57theorem e_220220 : m2Num 2 2 0 2 2 0 = 8 * explicitZ 2 2 0 2 2 0 := by decide
58theorem e_220221 : m2Num 2 2 0 2 2 1 = 8 * explicitZ 2 2 0 2 2 1 := by decide
59theorem e_220222 : m2Num 2 2 0 2 2 2 = 8 * explicitZ 2 2 0 2 2 2 := by decide
60theorem e_220223 : m2Num 2 2 0 2 2 3 = 8 * explicitZ 2 2 0 2 2 3 := by decide
61theorem e_220230 : m2Num 2 2 0 2 3 0 = 8 * explicitZ 2 2 0 2 3 0 := by decide
62theorem e_220231 : m2Num 2 2 0 2 3 1 = 8 * explicitZ 2 2 0 2 3 1 := by decide
63theorem e_220232 : m2Num 2 2 0 2 3 2 = 8 * explicitZ 2 2 0 2 3 2 := by decide
64theorem e_220233 : m2Num 2 2 0 2 3 3 = 8 * explicitZ 2 2 0 2 3 3 := by decide
65theorem e_220300 : m2Num 2 2 0 3 0 0 = 8 * explicitZ 2 2 0 3 0 0 := by decide
66theorem e_220301 : m2Num 2 2 0 3 0 1 = 8 * explicitZ 2 2 0 3 0 1 := by decide
67theorem e_220302 : m2Num 2 2 0 3 0 2 = 8 * explicitZ 2 2 0 3 0 2 := by decide
68theorem e_220303 : m2Num 2 2 0 3 0 3 = 8 * explicitZ 2 2 0 3 0 3 := by decide
69theorem e_220310 : m2Num 2 2 0 3 1 0 = 8 * explicitZ 2 2 0 3 1 0 := by decide
70theorem e_220311 : m2Num 2 2 0 3 1 1 = 8 * explicitZ 2 2 0 3 1 1 := by decide
71theorem e_220312 : m2Num 2 2 0 3 1 2 = 8 * explicitZ 2 2 0 3 1 2 := by decide
72theorem e_220313 : m2Num 2 2 0 3 1 3 = 8 * explicitZ 2 2 0 3 1 3 := by decide
73theorem e_220320 : m2Num 2 2 0 3 2 0 = 8 * explicitZ 2 2 0 3 2 0 := by decide
74theorem e_220321 : m2Num 2 2 0 3 2 1 = 8 * explicitZ 2 2 0 3 2 1 := by decide
75theorem e_220322 : m2Num 2 2 0 3 2 2 = 8 * explicitZ 2 2 0 3 2 2 := by decide
76theorem e_220323 : m2Num 2 2 0 3 2 3 = 8 * explicitZ 2 2 0 3 2 3 := by decide
77theorem e_220330 : m2Num 2 2 0 3 3 0 = 8 * explicitZ 2 2 0 3 3 0 := by decide
78theorem e_220331 : m2Num 2 2 0 3 3 1 = 8 * explicitZ 2 2 0 3 3 1 := by decide
79theorem e_220332 : m2Num 2 2 0 3 3 2 = 8 * explicitZ 2 2 0 3 3 2 := by decide
80theorem e_220333 : m2Num 2 2 0 3 3 3 = 8 * explicitZ 2 2 0 3 3 3 := by decide
81theorem e_221000 : m2Num 2 2 1 0 0 0 = 8 * explicitZ 2 2 1 0 0 0 := by decide
82theorem e_221001 : m2Num 2 2 1 0 0 1 = 8 * explicitZ 2 2 1 0 0 1 := by decide
83theorem e_221002 : m2Num 2 2 1 0 0 2 = 8 * explicitZ 2 2 1 0 0 2 := by decide
84theorem e_221003 : m2Num 2 2 1 0 0 3 = 8 * explicitZ 2 2 1 0 0 3 := by decide
85theorem e_221010 : m2Num 2 2 1 0 1 0 = 8 * explicitZ 2 2 1 0 1 0 := by decide
86theorem e_221011 : m2Num 2 2 1 0 1 1 = 8 * explicitZ 2 2 1 0 1 1 := by decide
87theorem e_221012 : m2Num 2 2 1 0 1 2 = 8 * explicitZ 2 2 1 0 1 2 := by decide
88theorem e_221013 : m2Num 2 2 1 0 1 3 = 8 * explicitZ 2 2 1 0 1 3 := by decide
89theorem e_221020 : m2Num 2 2 1 0 2 0 = 8 * explicitZ 2 2 1 0 2 0 := by decide
90theorem e_221021 : m2Num 2 2 1 0 2 1 = 8 * explicitZ 2 2 1 0 2 1 := by decide
91theorem e_221022 : m2Num 2 2 1 0 2 2 = 8 * explicitZ 2 2 1 0 2 2 := by decide
92theorem e_221023 : m2Num 2 2 1 0 2 3 = 8 * explicitZ 2 2 1 0 2 3 := by decide
93theorem e_221030 : m2Num 2 2 1 0 3 0 = 8 * explicitZ 2 2 1 0 3 0 := by decide
94theorem e_221031 : m2Num 2 2 1 0 3 1 = 8 * explicitZ 2 2 1 0 3 1 := by decide
95theorem e_221032 : m2Num 2 2 1 0 3 2 = 8 * explicitZ 2 2 1 0 3 2 := by decide
96theorem e_221033 : m2Num 2 2 1 0 3 3 = 8 * explicitZ 2 2 1 0 3 3 := by decide
97theorem e_221100 : m2Num 2 2 1 1 0 0 = 8 * explicitZ 2 2 1 1 0 0 := by decide
98theorem e_221101 : m2Num 2 2 1 1 0 1 = 8 * explicitZ 2 2 1 1 0 1 := by decide
99theorem e_221102 : m2Num 2 2 1 1 0 2 = 8 * explicitZ 2 2 1 1 0 2 := by decide
100theorem e_221103 : m2Num 2 2 1 1 0 3 = 8 * explicitZ 2 2 1 1 0 3 := by decide
101theorem e_221110 : m2Num 2 2 1 1 1 0 = 8 * explicitZ 2 2 1 1 1 0 := by decide
102theorem e_221111 : m2Num 2 2 1 1 1 1 = 8 * explicitZ 2 2 1 1 1 1 := by decide
103theorem e_221112 : m2Num 2 2 1 1 1 2 = 8 * explicitZ 2 2 1 1 1 2 := by decide
104theorem e_221113 : m2Num 2 2 1 1 1 3 = 8 * explicitZ 2 2 1 1 1 3 := by decide
105theorem e_221120 : m2Num 2 2 1 1 2 0 = 8 * explicitZ 2 2 1 1 2 0 := by decide
106theorem e_221121 : m2Num 2 2 1 1 2 1 = 8 * explicitZ 2 2 1 1 2 1 := by decide
107theorem e_221122 : m2Num 2 2 1 1 2 2 = 8 * explicitZ 2 2 1 1 2 2 := by decide
108theorem e_221123 : m2Num 2 2 1 1 2 3 = 8 * explicitZ 2 2 1 1 2 3 := by decide
109theorem e_221130 : m2Num 2 2 1 1 3 0 = 8 * explicitZ 2 2 1 1 3 0 := by decide
110theorem e_221131 : m2Num 2 2 1 1 3 1 = 8 * explicitZ 2 2 1 1 3 1 := by decide
111theorem e_221132 : m2Num 2 2 1 1 3 2 = 8 * explicitZ 2 2 1 1 3 2 := by decide
112theorem e_221133 : m2Num 2 2 1 1 3 3 = 8 * explicitZ 2 2 1 1 3 3 := by decide
113theorem e_221200 : m2Num 2 2 1 2 0 0 = 8 * explicitZ 2 2 1 2 0 0 := by decide
114theorem e_221201 : m2Num 2 2 1 2 0 1 = 8 * explicitZ 2 2 1 2 0 1 := by decide
115theorem e_221202 : m2Num 2 2 1 2 0 2 = 8 * explicitZ 2 2 1 2 0 2 := by decide
116theorem e_221203 : m2Num 2 2 1 2 0 3 = 8 * explicitZ 2 2 1 2 0 3 := by decide
117theorem e_221210 : m2Num 2 2 1 2 1 0 = 8 * explicitZ 2 2 1 2 1 0 := by decide
118theorem e_221211 : m2Num 2 2 1 2 1 1 = 8 * explicitZ 2 2 1 2 1 1 := by decide
119theorem e_221212 : m2Num 2 2 1 2 1 2 = 8 * explicitZ 2 2 1 2 1 2 := by decide
120theorem e_221213 : m2Num 2 2 1 2 1 3 = 8 * explicitZ 2 2 1 2 1 3 := by decide
121theorem e_221220 : m2Num 2 2 1 2 2 0 = 8 * explicitZ 2 2 1 2 2 0 := by decide
122theorem e_221221 : m2Num 2 2 1 2 2 1 = 8 * explicitZ 2 2 1 2 2 1 := by decide
123theorem e_221222 : m2Num 2 2 1 2 2 2 = 8 * explicitZ 2 2 1 2 2 2 := by decide
124theorem e_221223 : m2Num 2 2 1 2 2 3 = 8 * explicitZ 2 2 1 2 2 3 := by decide
125theorem e_221230 : m2Num 2 2 1 2 3 0 = 8 * explicitZ 2 2 1 2 3 0 := by decide
126theorem e_221231 : m2Num 2 2 1 2 3 1 = 8 * explicitZ 2 2 1 2 3 1 := by decide
127theorem e_221232 : m2Num 2 2 1 2 3 2 = 8 * explicitZ 2 2 1 2 3 2 := by decide
128theorem e_221233 : m2Num 2 2 1 2 3 3 = 8 * explicitZ 2 2 1 2 3 3 := by decide
129theorem e_221300 : m2Num 2 2 1 3 0 0 = 8 * explicitZ 2 2 1 3 0 0 := by decide
130theorem e_221301 : m2Num 2 2 1 3 0 1 = 8 * explicitZ 2 2 1 3 0 1 := by decide
131theorem e_221302 : m2Num 2 2 1 3 0 2 = 8 * explicitZ 2 2 1 3 0 2 := by decide
132theorem e_221303 : m2Num 2 2 1 3 0 3 = 8 * explicitZ 2 2 1 3 0 3 := by decide
133theorem e_221310 : m2Num 2 2 1 3 1 0 = 8 * explicitZ 2 2 1 3 1 0 := by decide
134theorem e_221311 : m2Num 2 2 1 3 1 1 = 8 * explicitZ 2 2 1 3 1 1 := by decide
135theorem e_221312 : m2Num 2 2 1 3 1 2 = 8 * explicitZ 2 2 1 3 1 2 := by decide
136theorem e_221313 : m2Num 2 2 1 3 1 3 = 8 * explicitZ 2 2 1 3 1 3 := by decide
137theorem e_221320 : m2Num 2 2 1 3 2 0 = 8 * explicitZ 2 2 1 3 2 0 := by decide
138theorem e_221321 : m2Num 2 2 1 3 2 1 = 8 * explicitZ 2 2 1 3 2 1 := by decide
139theorem e_221322 : m2Num 2 2 1 3 2 2 = 8 * explicitZ 2 2 1 3 2 2 := by decide
140theorem e_221323 : m2Num 2 2 1 3 2 3 = 8 * explicitZ 2 2 1 3 2 3 := by decide
141theorem e_221330 : m2Num 2 2 1 3 3 0 = 8 * explicitZ 2 2 1 3 3 0 := by decide
142theorem e_221331 : m2Num 2 2 1 3 3 1 = 8 * explicitZ 2 2 1 3 3 1 := by decide
143theorem e_221332 : m2Num 2 2 1 3 3 2 = 8 * explicitZ 2 2 1 3 3 2 := by decide
144theorem e_221333 : m2Num 2 2 1 3 3 3 = 8 * explicitZ 2 2 1 3 3 3 := by decide
145theorem e_222000 : m2Num 2 2 2 0 0 0 = 8 * explicitZ 2 2 2 0 0 0 := by decide
146theorem e_222001 : m2Num 2 2 2 0 0 1 = 8 * explicitZ 2 2 2 0 0 1 := by decide
147theorem e_222002 : m2Num 2 2 2 0 0 2 = 8 * explicitZ 2 2 2 0 0 2 := by decide
148theorem e_222003 : m2Num 2 2 2 0 0 3 = 8 * explicitZ 2 2 2 0 0 3 := by decide
149theorem e_222010 : m2Num 2 2 2 0 1 0 = 8 * explicitZ 2 2 2 0 1 0 := by decide
150theorem e_222011 : m2Num 2 2 2 0 1 1 = 8 * explicitZ 2 2 2 0 1 1 := by decide
151theorem e_222012 : m2Num 2 2 2 0 1 2 = 8 * explicitZ 2 2 2 0 1 2 := by decide
152theorem e_222013 : m2Num 2 2 2 0 1 3 = 8 * explicitZ 2 2 2 0 1 3 := by decide
153theorem e_222020 : m2Num 2 2 2 0 2 0 = 8 * explicitZ 2 2 2 0 2 0 := by decide
154theorem e_222021 : m2Num 2 2 2 0 2 1 = 8 * explicitZ 2 2 2 0 2 1 := by decide
155theorem e_222022 : m2Num 2 2 2 0 2 2 = 8 * explicitZ 2 2 2 0 2 2 := by decide
156theorem e_222023 : m2Num 2 2 2 0 2 3 = 8 * explicitZ 2 2 2 0 2 3 := by decide
157theorem e_222030 : m2Num 2 2 2 0 3 0 = 8 * explicitZ 2 2 2 0 3 0 := by decide
158theorem e_222031 : m2Num 2 2 2 0 3 1 = 8 * explicitZ 2 2 2 0 3 1 := by decide
159theorem e_222032 : m2Num 2 2 2 0 3 2 = 8 * explicitZ 2 2 2 0 3 2 := by decide
160theorem e_222033 : m2Num 2 2 2 0 3 3 = 8 * explicitZ 2 2 2 0 3 3 := by decide
161theorem e_222100 : m2Num 2 2 2 1 0 0 = 8 * explicitZ 2 2 2 1 0 0 := by decide
162theorem e_222101 : m2Num 2 2 2 1 0 1 = 8 * explicitZ 2 2 2 1 0 1 := by decide
163theorem e_222102 : m2Num 2 2 2 1 0 2 = 8 * explicitZ 2 2 2 1 0 2 := by decide
164theorem e_222103 : m2Num 2 2 2 1 0 3 = 8 * explicitZ 2 2 2 1 0 3 := by decide
165theorem e_222110 : m2Num 2 2 2 1 1 0 = 8 * explicitZ 2 2 2 1 1 0 := by decide
166theorem e_222111 : m2Num 2 2 2 1 1 1 = 8 * explicitZ 2 2 2 1 1 1 := by decide
167theorem e_222112 : m2Num 2 2 2 1 1 2 = 8 * explicitZ 2 2 2 1 1 2 := by decide
168theorem e_222113 : m2Num 2 2 2 1 1 3 = 8 * explicitZ 2 2 2 1 1 3 := by decide
169theorem e_222120 : m2Num 2 2 2 1 2 0 = 8 * explicitZ 2 2 2 1 2 0 := by decide
170theorem e_222121 : m2Num 2 2 2 1 2 1 = 8 * explicitZ 2 2 2 1 2 1 := by decide
171theorem e_222122 : m2Num 2 2 2 1 2 2 = 8 * explicitZ 2 2 2 1 2 2 := by decide
172theorem e_222123 : m2Num 2 2 2 1 2 3 = 8 * explicitZ 2 2 2 1 2 3 := by decide
173theorem e_222130 : m2Num 2 2 2 1 3 0 = 8 * explicitZ 2 2 2 1 3 0 := by decide
174theorem e_222131 : m2Num 2 2 2 1 3 1 = 8 * explicitZ 2 2 2 1 3 1 := by decide
175theorem e_222132 : m2Num 2 2 2 1 3 2 = 8 * explicitZ 2 2 2 1 3 2 := by decide
176theorem e_222133 : m2Num 2 2 2 1 3 3 = 8 * explicitZ 2 2 2 1 3 3 := by decide
177theorem e_222200 : m2Num 2 2 2 2 0 0 = 8 * explicitZ 2 2 2 2 0 0 := by decide
178theorem e_222201 : m2Num 2 2 2 2 0 1 = 8 * explicitZ 2 2 2 2 0 1 := by decide
179theorem e_222202 : m2Num 2 2 2 2 0 2 = 8 * explicitZ 2 2 2 2 0 2 := by decide
180theorem e_222203 : m2Num 2 2 2 2 0 3 = 8 * explicitZ 2 2 2 2 0 3 := by decide
181theorem e_222210 : m2Num 2 2 2 2 1 0 = 8 * explicitZ 2 2 2 2 1 0 := by decide
182theorem e_222211 : m2Num 2 2 2 2 1 1 = 8 * explicitZ 2 2 2 2 1 1 := by decide
183theorem e_222212 : m2Num 2 2 2 2 1 2 = 8 * explicitZ 2 2 2 2 1 2 := by decide
184theorem e_222213 : m2Num 2 2 2 2 1 3 = 8 * explicitZ 2 2 2 2 1 3 := by decide
185theorem e_222220 : m2Num 2 2 2 2 2 0 = 8 * explicitZ 2 2 2 2 2 0 := by decide
186theorem e_222221 : m2Num 2 2 2 2 2 1 = 8 * explicitZ 2 2 2 2 2 1 := by decide
187theorem e_222222 : m2Num 2 2 2 2 2 2 = 8 * explicitZ 2 2 2 2 2 2 := by decide
188theorem e_222223 : m2Num 2 2 2 2 2 3 = 8 * explicitZ 2 2 2 2 2 3 := by decide
189theorem e_222230 : m2Num 2 2 2 2 3 0 = 8 * explicitZ 2 2 2 2 3 0 := by decide
190theorem e_222231 : m2Num 2 2 2 2 3 1 = 8 * explicitZ 2 2 2 2 3 1 := by decide
191theorem e_222232 : m2Num 2 2 2 2 3 2 = 8 * explicitZ 2 2 2 2 3 2 := by decide
192theorem e_222233 : m2Num 2 2 2 2 3 3 = 8 * explicitZ 2 2 2 2 3 3 := by decide
193theorem e_222300 : m2Num 2 2 2 3 0 0 = 8 * explicitZ 2 2 2 3 0 0 := by decide
194theorem e_222301 : m2Num 2 2 2 3 0 1 = 8 * explicitZ 2 2 2 3 0 1 := by decide
195theorem e_222302 : m2Num 2 2 2 3 0 2 = 8 * explicitZ 2 2 2 3 0 2 := by decide
196theorem e_222303 : m2Num 2 2 2 3 0 3 = 8 * explicitZ 2 2 2 3 0 3 := by decide
197theorem e_222310 : m2Num 2 2 2 3 1 0 = 8 * explicitZ 2 2 2 3 1 0 := by decide
198theorem e_222311 : m2Num 2 2 2 3 1 1 = 8 * explicitZ 2 2 2 3 1 1 := by decide
199theorem e_222312 : m2Num 2 2 2 3 1 2 = 8 * explicitZ 2 2 2 3 1 2 := by decide
200theorem e_222313 : m2Num 2 2 2 3 1 3 = 8 * explicitZ 2 2 2 3 1 3 := by decide
201theorem e_222320 : m2Num 2 2 2 3 2 0 = 8 * explicitZ 2 2 2 3 2 0 := by decide
202theorem e_222321 : m2Num 2 2 2 3 2 1 = 8 * explicitZ 2 2 2 3 2 1 := by decide
203theorem e_222322 : m2Num 2 2 2 3 2 2 = 8 * explicitZ 2 2 2 3 2 2 := by decide
204theorem e_222323 : m2Num 2 2 2 3 2 3 = 8 * explicitZ 2 2 2 3 2 3 := by decide
205theorem e_222330 : m2Num 2 2 2 3 3 0 = 8 * explicitZ 2 2 2 3 3 0 := by decide
206theorem e_222331 : m2Num 2 2 2 3 3 1 = 8 * explicitZ 2 2 2 3 3 1 := by decide
207theorem e_222332 : m2Num 2 2 2 3 3 2 = 8 * explicitZ 2 2 2 3 3 2 := by decide
208theorem e_222333 : m2Num 2 2 2 3 3 3 = 8 * explicitZ 2 2 2 3 3 3 := by decide
209theorem e_223000 : m2Num 2 2 3 0 0 0 = 8 * explicitZ 2 2 3 0 0 0 := by decide
210theorem e_223001 : m2Num 2 2 3 0 0 1 = 8 * explicitZ 2 2 3 0 0 1 := by decide
211theorem e_223002 : m2Num 2 2 3 0 0 2 = 8 * explicitZ 2 2 3 0 0 2 := by decide
212theorem e_223003 : m2Num 2 2 3 0 0 3 = 8 * explicitZ 2 2 3 0 0 3 := by decide
213theorem e_223010 : m2Num 2 2 3 0 1 0 = 8 * explicitZ 2 2 3 0 1 0 := by decide
214theorem e_223011 : m2Num 2 2 3 0 1 1 = 8 * explicitZ 2 2 3 0 1 1 := by decide
215theorem e_223012 : m2Num 2 2 3 0 1 2 = 8 * explicitZ 2 2 3 0 1 2 := by decide
216theorem e_223013 : m2Num 2 2 3 0 1 3 = 8 * explicitZ 2 2 3 0 1 3 := by decide
217theorem e_223020 : m2Num 2 2 3 0 2 0 = 8 * explicitZ 2 2 3 0 2 0 := by decide
218theorem e_223021 : m2Num 2 2 3 0 2 1 = 8 * explicitZ 2 2 3 0 2 1 := by decide
219theorem e_223022 : m2Num 2 2 3 0 2 2 = 8 * explicitZ 2 2 3 0 2 2 := by decide
220theorem e_223023 : m2Num 2 2 3 0 2 3 = 8 * explicitZ 2 2 3 0 2 3 := by decide
221theorem e_223030 : m2Num 2 2 3 0 3 0 = 8 * explicitZ 2 2 3 0 3 0 := by decide
222theorem e_223031 : m2Num 2 2 3 0 3 1 = 8 * explicitZ 2 2 3 0 3 1 := by decide
223theorem e_223032 : m2Num 2 2 3 0 3 2 = 8 * explicitZ 2 2 3 0 3 2 := by decide
224theorem e_223033 : m2Num 2 2 3 0 3 3 = 8 * explicitZ 2 2 3 0 3 3 := by decide
225theorem e_223100 : m2Num 2 2 3 1 0 0 = 8 * explicitZ 2 2 3 1 0 0 := by decide
226theorem e_223101 : m2Num 2 2 3 1 0 1 = 8 * explicitZ 2 2 3 1 0 1 := by decide
227theorem e_223102 : m2Num 2 2 3 1 0 2 = 8 * explicitZ 2 2 3 1 0 2 := by decide
228theorem e_223103 : m2Num 2 2 3 1 0 3 = 8 * explicitZ 2 2 3 1 0 3 := by decide
229theorem e_223110 : m2Num 2 2 3 1 1 0 = 8 * explicitZ 2 2 3 1 1 0 := by decide
230theorem e_223111 : m2Num 2 2 3 1 1 1 = 8 * explicitZ 2 2 3 1 1 1 := by decide
231theorem e_223112 : m2Num 2 2 3 1 1 2 = 8 * explicitZ 2 2 3 1 1 2 := by decide
232theorem e_223113 : m2Num 2 2 3 1 1 3 = 8 * explicitZ 2 2 3 1 1 3 := by decide
233theorem e_223120 : m2Num 2 2 3 1 2 0 = 8 * explicitZ 2 2 3 1 2 0 := by decide
234theorem e_223121 : m2Num 2 2 3 1 2 1 = 8 * explicitZ 2 2 3 1 2 1 := by decide
235theorem e_223122 : m2Num 2 2 3 1 2 2 = 8 * explicitZ 2 2 3 1 2 2 := by decide
236theorem e_223123 : m2Num 2 2 3 1 2 3 = 8 * explicitZ 2 2 3 1 2 3 := by decide
237theorem e_223130 : m2Num 2 2 3 1 3 0 = 8 * explicitZ 2 2 3 1 3 0 := by decide
238theorem e_223131 : m2Num 2 2 3 1 3 1 = 8 * explicitZ 2 2 3 1 3 1 := by decide
239theorem e_223132 : m2Num 2 2 3 1 3 2 = 8 * explicitZ 2 2 3 1 3 2 := by decide
240theorem e_223133 : m2Num 2 2 3 1 3 3 = 8 * explicitZ 2 2 3 1 3 3 := by decide
241theorem e_223200 : m2Num 2 2 3 2 0 0 = 8 * explicitZ 2 2 3 2 0 0 := by decide
242theorem e_223201 : m2Num 2 2 3 2 0 1 = 8 * explicitZ 2 2 3 2 0 1 := by decide
243theorem e_223202 : m2Num 2 2 3 2 0 2 = 8 * explicitZ 2 2 3 2 0 2 := by decide
244theorem e_223203 : m2Num 2 2 3 2 0 3 = 8 * explicitZ 2 2 3 2 0 3 := by decide
245theorem e_223210 : m2Num 2 2 3 2 1 0 = 8 * explicitZ 2 2 3 2 1 0 := by decide
246theorem e_223211 : m2Num 2 2 3 2 1 1 = 8 * explicitZ 2 2 3 2 1 1 := by decide
247theorem e_223212 : m2Num 2 2 3 2 1 2 = 8 * explicitZ 2 2 3 2 1 2 := by decide
248theorem e_223213 : m2Num 2 2 3 2 1 3 = 8 * explicitZ 2 2 3 2 1 3 := by decide
249theorem e_223220 : m2Num 2 2 3 2 2 0 = 8 * explicitZ 2 2 3 2 2 0 := by decide
250theorem e_223221 : m2Num 2 2 3 2 2 1 = 8 * explicitZ 2 2 3 2 2 1 := by decide
251theorem e_223222 : m2Num 2 2 3 2 2 2 = 8 * explicitZ 2 2 3 2 2 2 := by decide
252theorem e_223223 : m2Num 2 2 3 2 2 3 = 8 * explicitZ 2 2 3 2 2 3 := by decide
253theorem e_223230 : m2Num 2 2 3 2 3 0 = 8 * explicitZ 2 2 3 2 3 0 := by decide
254theorem e_223231 : m2Num 2 2 3 2 3 1 = 8 * explicitZ 2 2 3 2 3 1 := by decide
255theorem e_223232 : m2Num 2 2 3 2 3 2 = 8 * explicitZ 2 2 3 2 3 2 := by decide
256theorem e_223233 : m2Num 2 2 3 2 3 3 = 8 * explicitZ 2 2 3 2 3 3 := by decide
257theorem e_223300 : m2Num 2 2 3 3 0 0 = 8 * explicitZ 2 2 3 3 0 0 := by decide
258theorem e_223301 : m2Num 2 2 3 3 0 1 = 8 * explicitZ 2 2 3 3 0 1 := by decide
259theorem e_223302 : m2Num 2 2 3 3 0 2 = 8 * explicitZ 2 2 3 3 0 2 := by decide
260theorem e_223303 : m2Num 2 2 3 3 0 3 = 8 * explicitZ 2 2 3 3 0 3 := by decide
261theorem e_223310 : m2Num 2 2 3 3 1 0 = 8 * explicitZ 2 2 3 3 1 0 := by decide
262theorem e_223311 : m2Num 2 2 3 3 1 1 = 8 * explicitZ 2 2 3 3 1 1 := by decide
263theorem e_223312 : m2Num 2 2 3 3 1 2 = 8 * explicitZ 2 2 3 3 1 2 := by decide
264theorem e_223313 : m2Num 2 2 3 3 1 3 = 8 * explicitZ 2 2 3 3 1 3 := by decide
265theorem e_223320 : m2Num 2 2 3 3 2 0 = 8 * explicitZ 2 2 3 3 2 0 := by decide
266theorem e_223321 : m2Num 2 2 3 3 2 1 = 8 * explicitZ 2 2 3 3 2 1 := by decide
267theorem e_223322 : m2Num 2 2 3 3 2 2 = 8 * explicitZ 2 2 3 3 2 2 := by decide
268theorem e_223323 : m2Num 2 2 3 3 2 3 = 8 * explicitZ 2 2 3 3 2 3 := by decide
269theorem e_223330 : m2Num 2 2 3 3 3 0 = 8 * explicitZ 2 2 3 3 3 0 := by decide
270theorem e_223331 : m2Num 2 2 3 3 3 1 = 8 * explicitZ 2 2 3 3 3 1 := by decide
271theorem e_223332 : m2Num 2 2 3 3 3 2 = 8 * explicitZ 2 2 3 3 3 2 := by decide
272theorem e_223333 : m2Num 2 2 3 3 3 3 = 8 * explicitZ 2 2 3 3 3 3 := by decide
273
274end M2NumChunk10
275end ReggeExactMidpointM2TTIdentity4D
276end Analysis
277end Gravity
278end IndisputableMonolith
279