IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DM2NumChunk09
IndisputableMonolith/Gravity/Analysis/ReggeExactMidpointM2TTIdentity4DM2NumChunk09.lean · 279 lines · 256 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DKernelCert
3
4/-! m2Num = 8·explicitZ, chunk 9 (256 kernel decides). -/
5
6namespace IndisputableMonolith
7namespace Gravity
8namespace Analysis
9namespace ReggeExactMidpointM2TTIdentity4D
10namespace M2NumChunk09
11
12open KernelCert
13
14set_option maxRecDepth 100000
15set_option maxHeartbeats 200000000
16
17theorem e_210000 : m2Num 2 1 0 0 0 0 = 8 * explicitZ 2 1 0 0 0 0 := by decide
18theorem e_210001 : m2Num 2 1 0 0 0 1 = 8 * explicitZ 2 1 0 0 0 1 := by decide
19theorem e_210002 : m2Num 2 1 0 0 0 2 = 8 * explicitZ 2 1 0 0 0 2 := by decide
20theorem e_210003 : m2Num 2 1 0 0 0 3 = 8 * explicitZ 2 1 0 0 0 3 := by decide
21theorem e_210010 : m2Num 2 1 0 0 1 0 = 8 * explicitZ 2 1 0 0 1 0 := by decide
22theorem e_210011 : m2Num 2 1 0 0 1 1 = 8 * explicitZ 2 1 0 0 1 1 := by decide
23theorem e_210012 : m2Num 2 1 0 0 1 2 = 8 * explicitZ 2 1 0 0 1 2 := by decide
24theorem e_210013 : m2Num 2 1 0 0 1 3 = 8 * explicitZ 2 1 0 0 1 3 := by decide
25theorem e_210020 : m2Num 2 1 0 0 2 0 = 8 * explicitZ 2 1 0 0 2 0 := by decide
26theorem e_210021 : m2Num 2 1 0 0 2 1 = 8 * explicitZ 2 1 0 0 2 1 := by decide
27theorem e_210022 : m2Num 2 1 0 0 2 2 = 8 * explicitZ 2 1 0 0 2 2 := by decide
28theorem e_210023 : m2Num 2 1 0 0 2 3 = 8 * explicitZ 2 1 0 0 2 3 := by decide
29theorem e_210030 : m2Num 2 1 0 0 3 0 = 8 * explicitZ 2 1 0 0 3 0 := by decide
30theorem e_210031 : m2Num 2 1 0 0 3 1 = 8 * explicitZ 2 1 0 0 3 1 := by decide
31theorem e_210032 : m2Num 2 1 0 0 3 2 = 8 * explicitZ 2 1 0 0 3 2 := by decide
32theorem e_210033 : m2Num 2 1 0 0 3 3 = 8 * explicitZ 2 1 0 0 3 3 := by decide
33theorem e_210100 : m2Num 2 1 0 1 0 0 = 8 * explicitZ 2 1 0 1 0 0 := by decide
34theorem e_210101 : m2Num 2 1 0 1 0 1 = 8 * explicitZ 2 1 0 1 0 1 := by decide
35theorem e_210102 : m2Num 2 1 0 1 0 2 = 8 * explicitZ 2 1 0 1 0 2 := by decide
36theorem e_210103 : m2Num 2 1 0 1 0 3 = 8 * explicitZ 2 1 0 1 0 3 := by decide
37theorem e_210110 : m2Num 2 1 0 1 1 0 = 8 * explicitZ 2 1 0 1 1 0 := by decide
38theorem e_210111 : m2Num 2 1 0 1 1 1 = 8 * explicitZ 2 1 0 1 1 1 := by decide
39theorem e_210112 : m2Num 2 1 0 1 1 2 = 8 * explicitZ 2 1 0 1 1 2 := by decide
40theorem e_210113 : m2Num 2 1 0 1 1 3 = 8 * explicitZ 2 1 0 1 1 3 := by decide
41theorem e_210120 : m2Num 2 1 0 1 2 0 = 8 * explicitZ 2 1 0 1 2 0 := by decide
42theorem e_210121 : m2Num 2 1 0 1 2 1 = 8 * explicitZ 2 1 0 1 2 1 := by decide
43theorem e_210122 : m2Num 2 1 0 1 2 2 = 8 * explicitZ 2 1 0 1 2 2 := by decide
44theorem e_210123 : m2Num 2 1 0 1 2 3 = 8 * explicitZ 2 1 0 1 2 3 := by decide
45theorem e_210130 : m2Num 2 1 0 1 3 0 = 8 * explicitZ 2 1 0 1 3 0 := by decide
46theorem e_210131 : m2Num 2 1 0 1 3 1 = 8 * explicitZ 2 1 0 1 3 1 := by decide
47theorem e_210132 : m2Num 2 1 0 1 3 2 = 8 * explicitZ 2 1 0 1 3 2 := by decide
48theorem e_210133 : m2Num 2 1 0 1 3 3 = 8 * explicitZ 2 1 0 1 3 3 := by decide
49theorem e_210200 : m2Num 2 1 0 2 0 0 = 8 * explicitZ 2 1 0 2 0 0 := by decide
50theorem e_210201 : m2Num 2 1 0 2 0 1 = 8 * explicitZ 2 1 0 2 0 1 := by decide
51theorem e_210202 : m2Num 2 1 0 2 0 2 = 8 * explicitZ 2 1 0 2 0 2 := by decide
52theorem e_210203 : m2Num 2 1 0 2 0 3 = 8 * explicitZ 2 1 0 2 0 3 := by decide
53theorem e_210210 : m2Num 2 1 0 2 1 0 = 8 * explicitZ 2 1 0 2 1 0 := by decide
54theorem e_210211 : m2Num 2 1 0 2 1 1 = 8 * explicitZ 2 1 0 2 1 1 := by decide
55theorem e_210212 : m2Num 2 1 0 2 1 2 = 8 * explicitZ 2 1 0 2 1 2 := by decide
56theorem e_210213 : m2Num 2 1 0 2 1 3 = 8 * explicitZ 2 1 0 2 1 3 := by decide
57theorem e_210220 : m2Num 2 1 0 2 2 0 = 8 * explicitZ 2 1 0 2 2 0 := by decide
58theorem e_210221 : m2Num 2 1 0 2 2 1 = 8 * explicitZ 2 1 0 2 2 1 := by decide
59theorem e_210222 : m2Num 2 1 0 2 2 2 = 8 * explicitZ 2 1 0 2 2 2 := by decide
60theorem e_210223 : m2Num 2 1 0 2 2 3 = 8 * explicitZ 2 1 0 2 2 3 := by decide
61theorem e_210230 : m2Num 2 1 0 2 3 0 = 8 * explicitZ 2 1 0 2 3 0 := by decide
62theorem e_210231 : m2Num 2 1 0 2 3 1 = 8 * explicitZ 2 1 0 2 3 1 := by decide
63theorem e_210232 : m2Num 2 1 0 2 3 2 = 8 * explicitZ 2 1 0 2 3 2 := by decide
64theorem e_210233 : m2Num 2 1 0 2 3 3 = 8 * explicitZ 2 1 0 2 3 3 := by decide
65theorem e_210300 : m2Num 2 1 0 3 0 0 = 8 * explicitZ 2 1 0 3 0 0 := by decide
66theorem e_210301 : m2Num 2 1 0 3 0 1 = 8 * explicitZ 2 1 0 3 0 1 := by decide
67theorem e_210302 : m2Num 2 1 0 3 0 2 = 8 * explicitZ 2 1 0 3 0 2 := by decide
68theorem e_210303 : m2Num 2 1 0 3 0 3 = 8 * explicitZ 2 1 0 3 0 3 := by decide
69theorem e_210310 : m2Num 2 1 0 3 1 0 = 8 * explicitZ 2 1 0 3 1 0 := by decide
70theorem e_210311 : m2Num 2 1 0 3 1 1 = 8 * explicitZ 2 1 0 3 1 1 := by decide
71theorem e_210312 : m2Num 2 1 0 3 1 2 = 8 * explicitZ 2 1 0 3 1 2 := by decide
72theorem e_210313 : m2Num 2 1 0 3 1 3 = 8 * explicitZ 2 1 0 3 1 3 := by decide
73theorem e_210320 : m2Num 2 1 0 3 2 0 = 8 * explicitZ 2 1 0 3 2 0 := by decide
74theorem e_210321 : m2Num 2 1 0 3 2 1 = 8 * explicitZ 2 1 0 3 2 1 := by decide
75theorem e_210322 : m2Num 2 1 0 3 2 2 = 8 * explicitZ 2 1 0 3 2 2 := by decide
76theorem e_210323 : m2Num 2 1 0 3 2 3 = 8 * explicitZ 2 1 0 3 2 3 := by decide
77theorem e_210330 : m2Num 2 1 0 3 3 0 = 8 * explicitZ 2 1 0 3 3 0 := by decide
78theorem e_210331 : m2Num 2 1 0 3 3 1 = 8 * explicitZ 2 1 0 3 3 1 := by decide
79theorem e_210332 : m2Num 2 1 0 3 3 2 = 8 * explicitZ 2 1 0 3 3 2 := by decide
80theorem e_210333 : m2Num 2 1 0 3 3 3 = 8 * explicitZ 2 1 0 3 3 3 := by decide
81theorem e_211000 : m2Num 2 1 1 0 0 0 = 8 * explicitZ 2 1 1 0 0 0 := by decide
82theorem e_211001 : m2Num 2 1 1 0 0 1 = 8 * explicitZ 2 1 1 0 0 1 := by decide
83theorem e_211002 : m2Num 2 1 1 0 0 2 = 8 * explicitZ 2 1 1 0 0 2 := by decide
84theorem e_211003 : m2Num 2 1 1 0 0 3 = 8 * explicitZ 2 1 1 0 0 3 := by decide
85theorem e_211010 : m2Num 2 1 1 0 1 0 = 8 * explicitZ 2 1 1 0 1 0 := by decide
86theorem e_211011 : m2Num 2 1 1 0 1 1 = 8 * explicitZ 2 1 1 0 1 1 := by decide
87theorem e_211012 : m2Num 2 1 1 0 1 2 = 8 * explicitZ 2 1 1 0 1 2 := by decide
88theorem e_211013 : m2Num 2 1 1 0 1 3 = 8 * explicitZ 2 1 1 0 1 3 := by decide
89theorem e_211020 : m2Num 2 1 1 0 2 0 = 8 * explicitZ 2 1 1 0 2 0 := by decide
90theorem e_211021 : m2Num 2 1 1 0 2 1 = 8 * explicitZ 2 1 1 0 2 1 := by decide
91theorem e_211022 : m2Num 2 1 1 0 2 2 = 8 * explicitZ 2 1 1 0 2 2 := by decide
92theorem e_211023 : m2Num 2 1 1 0 2 3 = 8 * explicitZ 2 1 1 0 2 3 := by decide
93theorem e_211030 : m2Num 2 1 1 0 3 0 = 8 * explicitZ 2 1 1 0 3 0 := by decide
94theorem e_211031 : m2Num 2 1 1 0 3 1 = 8 * explicitZ 2 1 1 0 3 1 := by decide
95theorem e_211032 : m2Num 2 1 1 0 3 2 = 8 * explicitZ 2 1 1 0 3 2 := by decide
96theorem e_211033 : m2Num 2 1 1 0 3 3 = 8 * explicitZ 2 1 1 0 3 3 := by decide
97theorem e_211100 : m2Num 2 1 1 1 0 0 = 8 * explicitZ 2 1 1 1 0 0 := by decide
98theorem e_211101 : m2Num 2 1 1 1 0 1 = 8 * explicitZ 2 1 1 1 0 1 := by decide
99theorem e_211102 : m2Num 2 1 1 1 0 2 = 8 * explicitZ 2 1 1 1 0 2 := by decide
100theorem e_211103 : m2Num 2 1 1 1 0 3 = 8 * explicitZ 2 1 1 1 0 3 := by decide
101theorem e_211110 : m2Num 2 1 1 1 1 0 = 8 * explicitZ 2 1 1 1 1 0 := by decide
102theorem e_211111 : m2Num 2 1 1 1 1 1 = 8 * explicitZ 2 1 1 1 1 1 := by decide
103theorem e_211112 : m2Num 2 1 1 1 1 2 = 8 * explicitZ 2 1 1 1 1 2 := by decide
104theorem e_211113 : m2Num 2 1 1 1 1 3 = 8 * explicitZ 2 1 1 1 1 3 := by decide
105theorem e_211120 : m2Num 2 1 1 1 2 0 = 8 * explicitZ 2 1 1 1 2 0 := by decide
106theorem e_211121 : m2Num 2 1 1 1 2 1 = 8 * explicitZ 2 1 1 1 2 1 := by decide
107theorem e_211122 : m2Num 2 1 1 1 2 2 = 8 * explicitZ 2 1 1 1 2 2 := by decide
108theorem e_211123 : m2Num 2 1 1 1 2 3 = 8 * explicitZ 2 1 1 1 2 3 := by decide
109theorem e_211130 : m2Num 2 1 1 1 3 0 = 8 * explicitZ 2 1 1 1 3 0 := by decide
110theorem e_211131 : m2Num 2 1 1 1 3 1 = 8 * explicitZ 2 1 1 1 3 1 := by decide
111theorem e_211132 : m2Num 2 1 1 1 3 2 = 8 * explicitZ 2 1 1 1 3 2 := by decide
112theorem e_211133 : m2Num 2 1 1 1 3 3 = 8 * explicitZ 2 1 1 1 3 3 := by decide
113theorem e_211200 : m2Num 2 1 1 2 0 0 = 8 * explicitZ 2 1 1 2 0 0 := by decide
114theorem e_211201 : m2Num 2 1 1 2 0 1 = 8 * explicitZ 2 1 1 2 0 1 := by decide
115theorem e_211202 : m2Num 2 1 1 2 0 2 = 8 * explicitZ 2 1 1 2 0 2 := by decide
116theorem e_211203 : m2Num 2 1 1 2 0 3 = 8 * explicitZ 2 1 1 2 0 3 := by decide
117theorem e_211210 : m2Num 2 1 1 2 1 0 = 8 * explicitZ 2 1 1 2 1 0 := by decide
118theorem e_211211 : m2Num 2 1 1 2 1 1 = 8 * explicitZ 2 1 1 2 1 1 := by decide
119theorem e_211212 : m2Num 2 1 1 2 1 2 = 8 * explicitZ 2 1 1 2 1 2 := by decide
120theorem e_211213 : m2Num 2 1 1 2 1 3 = 8 * explicitZ 2 1 1 2 1 3 := by decide
121theorem e_211220 : m2Num 2 1 1 2 2 0 = 8 * explicitZ 2 1 1 2 2 0 := by decide
122theorem e_211221 : m2Num 2 1 1 2 2 1 = 8 * explicitZ 2 1 1 2 2 1 := by decide
123theorem e_211222 : m2Num 2 1 1 2 2 2 = 8 * explicitZ 2 1 1 2 2 2 := by decide
124theorem e_211223 : m2Num 2 1 1 2 2 3 = 8 * explicitZ 2 1 1 2 2 3 := by decide
125theorem e_211230 : m2Num 2 1 1 2 3 0 = 8 * explicitZ 2 1 1 2 3 0 := by decide
126theorem e_211231 : m2Num 2 1 1 2 3 1 = 8 * explicitZ 2 1 1 2 3 1 := by decide
127theorem e_211232 : m2Num 2 1 1 2 3 2 = 8 * explicitZ 2 1 1 2 3 2 := by decide
128theorem e_211233 : m2Num 2 1 1 2 3 3 = 8 * explicitZ 2 1 1 2 3 3 := by decide
129theorem e_211300 : m2Num 2 1 1 3 0 0 = 8 * explicitZ 2 1 1 3 0 0 := by decide
130theorem e_211301 : m2Num 2 1 1 3 0 1 = 8 * explicitZ 2 1 1 3 0 1 := by decide
131theorem e_211302 : m2Num 2 1 1 3 0 2 = 8 * explicitZ 2 1 1 3 0 2 := by decide
132theorem e_211303 : m2Num 2 1 1 3 0 3 = 8 * explicitZ 2 1 1 3 0 3 := by decide
133theorem e_211310 : m2Num 2 1 1 3 1 0 = 8 * explicitZ 2 1 1 3 1 0 := by decide
134theorem e_211311 : m2Num 2 1 1 3 1 1 = 8 * explicitZ 2 1 1 3 1 1 := by decide
135theorem e_211312 : m2Num 2 1 1 3 1 2 = 8 * explicitZ 2 1 1 3 1 2 := by decide
136theorem e_211313 : m2Num 2 1 1 3 1 3 = 8 * explicitZ 2 1 1 3 1 3 := by decide
137theorem e_211320 : m2Num 2 1 1 3 2 0 = 8 * explicitZ 2 1 1 3 2 0 := by decide
138theorem e_211321 : m2Num 2 1 1 3 2 1 = 8 * explicitZ 2 1 1 3 2 1 := by decide
139theorem e_211322 : m2Num 2 1 1 3 2 2 = 8 * explicitZ 2 1 1 3 2 2 := by decide
140theorem e_211323 : m2Num 2 1 1 3 2 3 = 8 * explicitZ 2 1 1 3 2 3 := by decide
141theorem e_211330 : m2Num 2 1 1 3 3 0 = 8 * explicitZ 2 1 1 3 3 0 := by decide
142theorem e_211331 : m2Num 2 1 1 3 3 1 = 8 * explicitZ 2 1 1 3 3 1 := by decide
143theorem e_211332 : m2Num 2 1 1 3 3 2 = 8 * explicitZ 2 1 1 3 3 2 := by decide
144theorem e_211333 : m2Num 2 1 1 3 3 3 = 8 * explicitZ 2 1 1 3 3 3 := by decide
145theorem e_212000 : m2Num 2 1 2 0 0 0 = 8 * explicitZ 2 1 2 0 0 0 := by decide
146theorem e_212001 : m2Num 2 1 2 0 0 1 = 8 * explicitZ 2 1 2 0 0 1 := by decide
147theorem e_212002 : m2Num 2 1 2 0 0 2 = 8 * explicitZ 2 1 2 0 0 2 := by decide
148theorem e_212003 : m2Num 2 1 2 0 0 3 = 8 * explicitZ 2 1 2 0 0 3 := by decide
149theorem e_212010 : m2Num 2 1 2 0 1 0 = 8 * explicitZ 2 1 2 0 1 0 := by decide
150theorem e_212011 : m2Num 2 1 2 0 1 1 = 8 * explicitZ 2 1 2 0 1 1 := by decide
151theorem e_212012 : m2Num 2 1 2 0 1 2 = 8 * explicitZ 2 1 2 0 1 2 := by decide
152theorem e_212013 : m2Num 2 1 2 0 1 3 = 8 * explicitZ 2 1 2 0 1 3 := by decide
153theorem e_212020 : m2Num 2 1 2 0 2 0 = 8 * explicitZ 2 1 2 0 2 0 := by decide
154theorem e_212021 : m2Num 2 1 2 0 2 1 = 8 * explicitZ 2 1 2 0 2 1 := by decide
155theorem e_212022 : m2Num 2 1 2 0 2 2 = 8 * explicitZ 2 1 2 0 2 2 := by decide
156theorem e_212023 : m2Num 2 1 2 0 2 3 = 8 * explicitZ 2 1 2 0 2 3 := by decide
157theorem e_212030 : m2Num 2 1 2 0 3 0 = 8 * explicitZ 2 1 2 0 3 0 := by decide
158theorem e_212031 : m2Num 2 1 2 0 3 1 = 8 * explicitZ 2 1 2 0 3 1 := by decide
159theorem e_212032 : m2Num 2 1 2 0 3 2 = 8 * explicitZ 2 1 2 0 3 2 := by decide
160theorem e_212033 : m2Num 2 1 2 0 3 3 = 8 * explicitZ 2 1 2 0 3 3 := by decide
161theorem e_212100 : m2Num 2 1 2 1 0 0 = 8 * explicitZ 2 1 2 1 0 0 := by decide
162theorem e_212101 : m2Num 2 1 2 1 0 1 = 8 * explicitZ 2 1 2 1 0 1 := by decide
163theorem e_212102 : m2Num 2 1 2 1 0 2 = 8 * explicitZ 2 1 2 1 0 2 := by decide
164theorem e_212103 : m2Num 2 1 2 1 0 3 = 8 * explicitZ 2 1 2 1 0 3 := by decide
165theorem e_212110 : m2Num 2 1 2 1 1 0 = 8 * explicitZ 2 1 2 1 1 0 := by decide
166theorem e_212111 : m2Num 2 1 2 1 1 1 = 8 * explicitZ 2 1 2 1 1 1 := by decide
167theorem e_212112 : m2Num 2 1 2 1 1 2 = 8 * explicitZ 2 1 2 1 1 2 := by decide
168theorem e_212113 : m2Num 2 1 2 1 1 3 = 8 * explicitZ 2 1 2 1 1 3 := by decide
169theorem e_212120 : m2Num 2 1 2 1 2 0 = 8 * explicitZ 2 1 2 1 2 0 := by decide
170theorem e_212121 : m2Num 2 1 2 1 2 1 = 8 * explicitZ 2 1 2 1 2 1 := by decide
171theorem e_212122 : m2Num 2 1 2 1 2 2 = 8 * explicitZ 2 1 2 1 2 2 := by decide
172theorem e_212123 : m2Num 2 1 2 1 2 3 = 8 * explicitZ 2 1 2 1 2 3 := by decide
173theorem e_212130 : m2Num 2 1 2 1 3 0 = 8 * explicitZ 2 1 2 1 3 0 := by decide
174theorem e_212131 : m2Num 2 1 2 1 3 1 = 8 * explicitZ 2 1 2 1 3 1 := by decide
175theorem e_212132 : m2Num 2 1 2 1 3 2 = 8 * explicitZ 2 1 2 1 3 2 := by decide
176theorem e_212133 : m2Num 2 1 2 1 3 3 = 8 * explicitZ 2 1 2 1 3 3 := by decide
177theorem e_212200 : m2Num 2 1 2 2 0 0 = 8 * explicitZ 2 1 2 2 0 0 := by decide
178theorem e_212201 : m2Num 2 1 2 2 0 1 = 8 * explicitZ 2 1 2 2 0 1 := by decide
179theorem e_212202 : m2Num 2 1 2 2 0 2 = 8 * explicitZ 2 1 2 2 0 2 := by decide
180theorem e_212203 : m2Num 2 1 2 2 0 3 = 8 * explicitZ 2 1 2 2 0 3 := by decide
181theorem e_212210 : m2Num 2 1 2 2 1 0 = 8 * explicitZ 2 1 2 2 1 0 := by decide
182theorem e_212211 : m2Num 2 1 2 2 1 1 = 8 * explicitZ 2 1 2 2 1 1 := by decide
183theorem e_212212 : m2Num 2 1 2 2 1 2 = 8 * explicitZ 2 1 2 2 1 2 := by decide
184theorem e_212213 : m2Num 2 1 2 2 1 3 = 8 * explicitZ 2 1 2 2 1 3 := by decide
185theorem e_212220 : m2Num 2 1 2 2 2 0 = 8 * explicitZ 2 1 2 2 2 0 := by decide
186theorem e_212221 : m2Num 2 1 2 2 2 1 = 8 * explicitZ 2 1 2 2 2 1 := by decide
187theorem e_212222 : m2Num 2 1 2 2 2 2 = 8 * explicitZ 2 1 2 2 2 2 := by decide
188theorem e_212223 : m2Num 2 1 2 2 2 3 = 8 * explicitZ 2 1 2 2 2 3 := by decide
189theorem e_212230 : m2Num 2 1 2 2 3 0 = 8 * explicitZ 2 1 2 2 3 0 := by decide
190theorem e_212231 : m2Num 2 1 2 2 3 1 = 8 * explicitZ 2 1 2 2 3 1 := by decide
191theorem e_212232 : m2Num 2 1 2 2 3 2 = 8 * explicitZ 2 1 2 2 3 2 := by decide
192theorem e_212233 : m2Num 2 1 2 2 3 3 = 8 * explicitZ 2 1 2 2 3 3 := by decide
193theorem e_212300 : m2Num 2 1 2 3 0 0 = 8 * explicitZ 2 1 2 3 0 0 := by decide
194theorem e_212301 : m2Num 2 1 2 3 0 1 = 8 * explicitZ 2 1 2 3 0 1 := by decide
195theorem e_212302 : m2Num 2 1 2 3 0 2 = 8 * explicitZ 2 1 2 3 0 2 := by decide
196theorem e_212303 : m2Num 2 1 2 3 0 3 = 8 * explicitZ 2 1 2 3 0 3 := by decide
197theorem e_212310 : m2Num 2 1 2 3 1 0 = 8 * explicitZ 2 1 2 3 1 0 := by decide
198theorem e_212311 : m2Num 2 1 2 3 1 1 = 8 * explicitZ 2 1 2 3 1 1 := by decide
199theorem e_212312 : m2Num 2 1 2 3 1 2 = 8 * explicitZ 2 1 2 3 1 2 := by decide
200theorem e_212313 : m2Num 2 1 2 3 1 3 = 8 * explicitZ 2 1 2 3 1 3 := by decide
201theorem e_212320 : m2Num 2 1 2 3 2 0 = 8 * explicitZ 2 1 2 3 2 0 := by decide
202theorem e_212321 : m2Num 2 1 2 3 2 1 = 8 * explicitZ 2 1 2 3 2 1 := by decide
203theorem e_212322 : m2Num 2 1 2 3 2 2 = 8 * explicitZ 2 1 2 3 2 2 := by decide
204theorem e_212323 : m2Num 2 1 2 3 2 3 = 8 * explicitZ 2 1 2 3 2 3 := by decide
205theorem e_212330 : m2Num 2 1 2 3 3 0 = 8 * explicitZ 2 1 2 3 3 0 := by decide
206theorem e_212331 : m2Num 2 1 2 3 3 1 = 8 * explicitZ 2 1 2 3 3 1 := by decide
207theorem e_212332 : m2Num 2 1 2 3 3 2 = 8 * explicitZ 2 1 2 3 3 2 := by decide
208theorem e_212333 : m2Num 2 1 2 3 3 3 = 8 * explicitZ 2 1 2 3 3 3 := by decide
209theorem e_213000 : m2Num 2 1 3 0 0 0 = 8 * explicitZ 2 1 3 0 0 0 := by decide
210theorem e_213001 : m2Num 2 1 3 0 0 1 = 8 * explicitZ 2 1 3 0 0 1 := by decide
211theorem e_213002 : m2Num 2 1 3 0 0 2 = 8 * explicitZ 2 1 3 0 0 2 := by decide
212theorem e_213003 : m2Num 2 1 3 0 0 3 = 8 * explicitZ 2 1 3 0 0 3 := by decide
213theorem e_213010 : m2Num 2 1 3 0 1 0 = 8 * explicitZ 2 1 3 0 1 0 := by decide
214theorem e_213011 : m2Num 2 1 3 0 1 1 = 8 * explicitZ 2 1 3 0 1 1 := by decide
215theorem e_213012 : m2Num 2 1 3 0 1 2 = 8 * explicitZ 2 1 3 0 1 2 := by decide
216theorem e_213013 : m2Num 2 1 3 0 1 3 = 8 * explicitZ 2 1 3 0 1 3 := by decide
217theorem e_213020 : m2Num 2 1 3 0 2 0 = 8 * explicitZ 2 1 3 0 2 0 := by decide
218theorem e_213021 : m2Num 2 1 3 0 2 1 = 8 * explicitZ 2 1 3 0 2 1 := by decide
219theorem e_213022 : m2Num 2 1 3 0 2 2 = 8 * explicitZ 2 1 3 0 2 2 := by decide
220theorem e_213023 : m2Num 2 1 3 0 2 3 = 8 * explicitZ 2 1 3 0 2 3 := by decide
221theorem e_213030 : m2Num 2 1 3 0 3 0 = 8 * explicitZ 2 1 3 0 3 0 := by decide
222theorem e_213031 : m2Num 2 1 3 0 3 1 = 8 * explicitZ 2 1 3 0 3 1 := by decide
223theorem e_213032 : m2Num 2 1 3 0 3 2 = 8 * explicitZ 2 1 3 0 3 2 := by decide
224theorem e_213033 : m2Num 2 1 3 0 3 3 = 8 * explicitZ 2 1 3 0 3 3 := by decide
225theorem e_213100 : m2Num 2 1 3 1 0 0 = 8 * explicitZ 2 1 3 1 0 0 := by decide
226theorem e_213101 : m2Num 2 1 3 1 0 1 = 8 * explicitZ 2 1 3 1 0 1 := by decide
227theorem e_213102 : m2Num 2 1 3 1 0 2 = 8 * explicitZ 2 1 3 1 0 2 := by decide
228theorem e_213103 : m2Num 2 1 3 1 0 3 = 8 * explicitZ 2 1 3 1 0 3 := by decide
229theorem e_213110 : m2Num 2 1 3 1 1 0 = 8 * explicitZ 2 1 3 1 1 0 := by decide
230theorem e_213111 : m2Num 2 1 3 1 1 1 = 8 * explicitZ 2 1 3 1 1 1 := by decide
231theorem e_213112 : m2Num 2 1 3 1 1 2 = 8 * explicitZ 2 1 3 1 1 2 := by decide
232theorem e_213113 : m2Num 2 1 3 1 1 3 = 8 * explicitZ 2 1 3 1 1 3 := by decide
233theorem e_213120 : m2Num 2 1 3 1 2 0 = 8 * explicitZ 2 1 3 1 2 0 := by decide
234theorem e_213121 : m2Num 2 1 3 1 2 1 = 8 * explicitZ 2 1 3 1 2 1 := by decide
235theorem e_213122 : m2Num 2 1 3 1 2 2 = 8 * explicitZ 2 1 3 1 2 2 := by decide
236theorem e_213123 : m2Num 2 1 3 1 2 3 = 8 * explicitZ 2 1 3 1 2 3 := by decide
237theorem e_213130 : m2Num 2 1 3 1 3 0 = 8 * explicitZ 2 1 3 1 3 0 := by decide
238theorem e_213131 : m2Num 2 1 3 1 3 1 = 8 * explicitZ 2 1 3 1 3 1 := by decide
239theorem e_213132 : m2Num 2 1 3 1 3 2 = 8 * explicitZ 2 1 3 1 3 2 := by decide
240theorem e_213133 : m2Num 2 1 3 1 3 3 = 8 * explicitZ 2 1 3 1 3 3 := by decide
241theorem e_213200 : m2Num 2 1 3 2 0 0 = 8 * explicitZ 2 1 3 2 0 0 := by decide
242theorem e_213201 : m2Num 2 1 3 2 0 1 = 8 * explicitZ 2 1 3 2 0 1 := by decide
243theorem e_213202 : m2Num 2 1 3 2 0 2 = 8 * explicitZ 2 1 3 2 0 2 := by decide
244theorem e_213203 : m2Num 2 1 3 2 0 3 = 8 * explicitZ 2 1 3 2 0 3 := by decide
245theorem e_213210 : m2Num 2 1 3 2 1 0 = 8 * explicitZ 2 1 3 2 1 0 := by decide
246theorem e_213211 : m2Num 2 1 3 2 1 1 = 8 * explicitZ 2 1 3 2 1 1 := by decide
247theorem e_213212 : m2Num 2 1 3 2 1 2 = 8 * explicitZ 2 1 3 2 1 2 := by decide
248theorem e_213213 : m2Num 2 1 3 2 1 3 = 8 * explicitZ 2 1 3 2 1 3 := by decide
249theorem e_213220 : m2Num 2 1 3 2 2 0 = 8 * explicitZ 2 1 3 2 2 0 := by decide
250theorem e_213221 : m2Num 2 1 3 2 2 1 = 8 * explicitZ 2 1 3 2 2 1 := by decide
251theorem e_213222 : m2Num 2 1 3 2 2 2 = 8 * explicitZ 2 1 3 2 2 2 := by decide
252theorem e_213223 : m2Num 2 1 3 2 2 3 = 8 * explicitZ 2 1 3 2 2 3 := by decide
253theorem e_213230 : m2Num 2 1 3 2 3 0 = 8 * explicitZ 2 1 3 2 3 0 := by decide
254theorem e_213231 : m2Num 2 1 3 2 3 1 = 8 * explicitZ 2 1 3 2 3 1 := by decide
255theorem e_213232 : m2Num 2 1 3 2 3 2 = 8 * explicitZ 2 1 3 2 3 2 := by decide
256theorem e_213233 : m2Num 2 1 3 2 3 3 = 8 * explicitZ 2 1 3 2 3 3 := by decide
257theorem e_213300 : m2Num 2 1 3 3 0 0 = 8 * explicitZ 2 1 3 3 0 0 := by decide
258theorem e_213301 : m2Num 2 1 3 3 0 1 = 8 * explicitZ 2 1 3 3 0 1 := by decide
259theorem e_213302 : m2Num 2 1 3 3 0 2 = 8 * explicitZ 2 1 3 3 0 2 := by decide
260theorem e_213303 : m2Num 2 1 3 3 0 3 = 8 * explicitZ 2 1 3 3 0 3 := by decide
261theorem e_213310 : m2Num 2 1 3 3 1 0 = 8 * explicitZ 2 1 3 3 1 0 := by decide
262theorem e_213311 : m2Num 2 1 3 3 1 1 = 8 * explicitZ 2 1 3 3 1 1 := by decide
263theorem e_213312 : m2Num 2 1 3 3 1 2 = 8 * explicitZ 2 1 3 3 1 2 := by decide
264theorem e_213313 : m2Num 2 1 3 3 1 3 = 8 * explicitZ 2 1 3 3 1 3 := by decide
265theorem e_213320 : m2Num 2 1 3 3 2 0 = 8 * explicitZ 2 1 3 3 2 0 := by decide
266theorem e_213321 : m2Num 2 1 3 3 2 1 = 8 * explicitZ 2 1 3 3 2 1 := by decide
267theorem e_213322 : m2Num 2 1 3 3 2 2 = 8 * explicitZ 2 1 3 3 2 2 := by decide
268theorem e_213323 : m2Num 2 1 3 3 2 3 = 8 * explicitZ 2 1 3 3 2 3 := by decide
269theorem e_213330 : m2Num 2 1 3 3 3 0 = 8 * explicitZ 2 1 3 3 3 0 := by decide
270theorem e_213331 : m2Num 2 1 3 3 3 1 = 8 * explicitZ 2 1 3 3 3 1 := by decide
271theorem e_213332 : m2Num 2 1 3 3 3 2 = 8 * explicitZ 2 1 3 3 3 2 := by decide
272theorem e_213333 : m2Num 2 1 3 3 3 3 = 8 * explicitZ 2 1 3 3 3 3 := by decide
273
274end M2NumChunk09
275end ReggeExactMidpointM2TTIdentity4D
276end Analysis
277end Gravity
278end IndisputableMonolith
279