IndisputableMonolith.Loom.CertificateData
IndisputableMonolith/Loom/CertificateData.lean · 408 lines · 9 declarations
show as:
view math explainer →
1import IndisputableMonolith.Loom.Core
2
3/-!
4# The measured certificate, as Lean data
5
6Generated by Loom/lean/emit_lean_data.py from Loom/lean/certificate.json.
7Do not edit by hand; regenerate.
8
9`base` is the homomorphism from the free group of rank five into the
10determinant one subgroup of the two by two matrices over ZMod 3 that the search
11found. `autTables` holds, for each of the forty eight automorphisms of Q3, the
12composite homomorphism, so a gauge image of an utterance is read by changing the
13table rather than by rewriting the words. `Table.ok` is decidable and every one
14of these tables is checked by it in the separation module, so a transcription
15error here cannot become a theorem.
16
17What Lean takes on trust is only the PROVENANCE of the forty eight tables, that
18they are the images of the generators under the automorphism group of the cube.
19That is measured in Loom/config/loom_configuration.py, whose self tests recover
20two facts nobody put into them (twelve oriented faces at walk length four, and
21ninety six Hamiltonian walks forming one class under gauge).
22
23The two configurations are the encoder's output for the witness pair under the
24codebook {'door': -1, 'key': 3, 'opens': 4, 'locks': 5}, which was chosen by exhaustive search so that no
25length statistic can separate the pair: both cost 142 acts with per loop
26multiset [4, 8, 8, 16, 18, 40, 48].
27
28The measured separation this data is here to make kernel checkable: the depth
29one reading of the two is IDENTICAL ([0, 0, 2, 2, 2, 2, 2]), the
30abelianised reading is identical too, and only the depth two reading differs
31([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 2, 2, 2] against [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 2]).
32
33A SECOND pair follows, `cfgC` and `cfgD`, under its own codebook
34{'door': 1, 'key': 3, 'opens': -4, 'locks': 5}. It is the stronger claim: the flagship is
35conflated by a bag of ground relations but seen by a reading that also carries
36parent to child labels, while this pair is conflated by that reading too, and
37its two members are separated by an explicit model rather than by a syntactic
38criterion. Both cost 88 acts with per loop multiset
39[4, 4, 8, 8, 16, 22, 26], depth one is identical
40([0, 0, 1, 2, 2, 2, 2]), and one homomorphism certifies both pairs.
41-/
42
43namespace IndisputableMonolith
44namespace Loom
45namespace Certificate
46
47/-- The homomorphism the search found. -/
48def base : Table :=
49 [(⟨2, 2, 1, 0⟩, ⟨0, 1, 2, 2⟩),
50 (⟨1, 1, 1, 2⟩, ⟨2, 2, 2, 1⟩),
51 (⟨2, 1, 2, 0⟩, ⟨0, 2, 1, 2⟩),
52 (⟨1, 2, 2, 2⟩, ⟨2, 1, 1, 1⟩),
53 (⟨1, 0, 1, 1⟩, ⟨1, 0, 2, 1⟩)]
54
55/-- The codebook the blinding search chose, in the name order the
56separation module indexes by: ['door', 'key', 'opens', 'locks']. Which codebook is used is a free
57convention (`invariant_substConfig` is why), and this one is the one under
58which no length statistic separates the pair. -/
59def cbData : List Int :=
60 [-1, 3, 4, 5]
61
62/-- Every door has some key that opens it, and one master key locks every door. -/
63def cfgA : Config :=
64 [[2],
65 [-1],
66 [-1, -3, 1],
67 [-1, -3, 4, 3, -1, 4, 3, 1],
68 [-3],
69 [-3, -1, 3],
70 [-3, -1, 5, 3, -1, 5, 1, 3]]
71
72/-- Every door has some key that locks it, and one master key opens every door. -/
73def cfgB : Config :=
74 [[2],
75 [-1],
76 [-1, -3, 1],
77 [-1, -3, 5, 3, -1, 5, 3, 1],
78 [-3],
79 [-3, -1, 3],
80 [-3, -1, 4, 3, -1, 4, 1, 3]]
81
82/-- The codebook for the second witness, the one that also defeats a
83reading which carries parent to child labels. -/
84def cbData2 : List Int :=
85 [1, 3, -4, 5]
86
87/-- Some door is opened by every key, and every door opens every key. -/
88def cfgC : Config :=
89 [[2],
90 [-1],
91 [-1, 3, 1],
92 [-1, 3, 5, 1, 3, 5, -3, 1],
93 [1],
94 [1, 3, -1],
95 [1, 3, -4, 1, 3, -4, -3, -1]]
96
97/-- Some door opens every key, and every key opens every door. -/
98def cfgD : Config :=
99 [[2],
100 [-1],
101 [-1, 3, 1],
102 [-1, 3, -4, 1, 3, -4, -3, 1],
103 [1],
104 [1, 3, -1],
105 [1, 3, 5, 1, 3, 5, -3, -1]]
106
107/-- The forty eight composite homomorphisms, one per automorphism of Q3. -/
108def autTables : List Table :=
109 [[(⟨2, 2, 1, 0⟩, ⟨0, 1, 2, 2⟩),
110 (⟨1, 1, 1, 2⟩, ⟨2, 2, 2, 1⟩),
111 (⟨2, 1, 2, 0⟩, ⟨0, 2, 1, 2⟩),
112 (⟨1, 2, 2, 2⟩, ⟨2, 1, 1, 1⟩),
113 (⟨1, 0, 1, 1⟩, ⟨1, 0, 2, 1⟩)],
114 [(⟨0, 1, 2, 2⟩, ⟨2, 2, 1, 0⟩),
115 (⟨2, 0, 1, 2⟩, ⟨2, 0, 2, 2⟩),
116 (⟨0, 2, 1, 0⟩, ⟨0, 1, 2, 0⟩),
117 (⟨2, 2, 2, 1⟩, ⟨1, 1, 1, 2⟩),
118 (⟨0, 1, 2, 2⟩, ⟨2, 2, 1, 0⟩)],
119 [(⟨0, 1, 2, 2⟩, ⟨2, 2, 1, 0⟩),
120 (⟨2, 2, 2, 1⟩, ⟨1, 1, 1, 2⟩),
121 (⟨0, 1, 2, 0⟩, ⟨0, 2, 1, 0⟩),
122 (⟨0, 2, 1, 1⟩, ⟨1, 1, 2, 0⟩),
123 (⟨2, 1, 2, 0⟩, ⟨0, 2, 1, 2⟩)],
124 [(⟨2, 2, 1, 0⟩, ⟨0, 1, 2, 2⟩),
125 (⟨0, 1, 2, 1⟩, ⟨1, 2, 1, 0⟩),
126 (⟨2, 0, 2, 2⟩, ⟨2, 0, 1, 2⟩),
127 (⟨1, 1, 2, 0⟩, ⟨0, 2, 1, 1⟩),
128 (⟨1, 0, 1, 1⟩, ⟨1, 0, 2, 1⟩)],
129 [(⟨1, 0, 1, 1⟩, ⟨1, 0, 2, 1⟩),
130 (⟨2, 2, 2, 1⟩, ⟨1, 1, 1, 2⟩),
131 (⟨0, 2, 1, 2⟩, ⟨2, 1, 2, 0⟩),
132 (⟨2, 1, 1, 1⟩, ⟨1, 2, 2, 2⟩),
133 (⟨2, 2, 1, 0⟩, ⟨0, 1, 2, 2⟩)],
134 [(⟨1, 0, 2, 1⟩, ⟨1, 0, 1, 1⟩),
135 (⟨1, 1, 2, 0⟩, ⟨0, 2, 1, 1⟩),
136 (⟨0, 2, 1, 0⟩, ⟨0, 1, 2, 0⟩),
137 (⟨2, 2, 2, 1⟩, ⟨1, 1, 1, 2⟩),
138 (⟨1, 0, 2, 1⟩, ⟨1, 0, 1, 1⟩)],
139 [(⟨1, 0, 2, 1⟩, ⟨1, 0, 1, 1⟩),
140 (⟨1, 1, 1, 2⟩, ⟨2, 2, 2, 1⟩),
141 (⟨0, 1, 2, 0⟩, ⟨0, 2, 1, 0⟩),
142 (⟨2, 1, 0, 2⟩, ⟨2, 2, 0, 2⟩),
143 (⟨1, 1, 0, 1⟩, ⟨1, 2, 0, 1⟩)],
144 [(⟨1, 0, 1, 1⟩, ⟨1, 0, 2, 1⟩),
145 (⟨2, 2, 0, 2⟩, ⟨2, 1, 0, 2⟩),
146 (⟨2, 0, 1, 2⟩, ⟨2, 0, 2, 2⟩),
147 (⟨1, 2, 1, 0⟩, ⟨0, 1, 2, 1⟩),
148 (⟨0, 2, 1, 2⟩, ⟨2, 1, 2, 0⟩)],
149 [(⟨1, 1, 2, 0⟩, ⟨0, 2, 1, 1⟩),
150 (⟨2, 0, 2, 2⟩, ⟨2, 0, 1, 2⟩),
151 (⟨2, 2, 2, 1⟩, ⟨1, 1, 1, 2⟩),
152 (⟨1, 1, 0, 1⟩, ⟨1, 2, 0, 1⟩),
153 (⟨1, 2, 2, 2⟩, ⟨2, 1, 1, 1⟩)],
154 [(⟨0, 2, 1, 1⟩, ⟨1, 1, 2, 0⟩),
155 (⟨2, 2, 2, 1⟩, ⟨1, 1, 1, 2⟩),
156 (⟨2, 0, 2, 2⟩, ⟨2, 0, 1, 2⟩),
157 (⟨0, 2, 1, 2⟩, ⟨2, 1, 2, 0⟩),
158 (⟨2, 1, 1, 1⟩, ⟨1, 2, 2, 2⟩)],
159 [(⟨2, 1, 1, 1⟩, ⟨1, 2, 2, 2⟩),
160 (⟨1, 2, 1, 0⟩, ⟨0, 1, 2, 1⟩),
161 (⟨1, 1, 1, 2⟩, ⟨2, 2, 2, 1⟩),
162 (⟨2, 2, 1, 0⟩, ⟨0, 1, 2, 2⟩),
163 (⟨2, 1, 0, 2⟩, ⟨2, 2, 0, 2⟩)],
164 [(⟨1, 2, 2, 2⟩, ⟨2, 1, 1, 1⟩),
165 (⟨1, 1, 1, 2⟩, ⟨2, 2, 2, 1⟩),
166 (⟨1, 2, 1, 0⟩, ⟨0, 1, 2, 1⟩),
167 (⟨1, 0, 2, 1⟩, ⟨1, 0, 1, 1⟩),
168 (⟨2, 2, 0, 2⟩, ⟨2, 1, 0, 2⟩)],
169 [(⟨2, 2, 0, 2⟩, ⟨2, 1, 0, 2⟩),
170 (⟨0, 2, 1, 1⟩, ⟨1, 1, 2, 0⟩),
171 (⟨0, 2, 1, 2⟩, ⟨2, 1, 2, 0⟩),
172 (⟨1, 1, 0, 1⟩, ⟨1, 2, 0, 1⟩),
173 (⟨0, 2, 1, 0⟩, ⟨0, 1, 2, 0⟩)],
174 [(⟨2, 1, 0, 2⟩, ⟨2, 2, 0, 2⟩),
175 (⟨1, 1, 1, 2⟩, ⟨2, 2, 2, 1⟩),
176 (⟨1, 1, 2, 0⟩, ⟨0, 2, 1, 1⟩),
177 (⟨1, 2, 0, 1⟩, ⟨1, 1, 0, 1⟩),
178 (⟨1, 2, 2, 2⟩, ⟨2, 1, 1, 1⟩)],
179 [(⟨1, 2, 2, 2⟩, ⟨2, 1, 1, 1⟩),
180 (⟨2, 1, 0, 2⟩, ⟨2, 2, 0, 2⟩),
181 (⟨2, 1, 2, 0⟩, ⟨0, 2, 1, 2⟩),
182 (⟨1, 0, 1, 1⟩, ⟨1, 0, 2, 1⟩),
183 (⟨2, 0, 1, 2⟩, ⟨2, 0, 2, 2⟩)],
184 [(⟨2, 1, 1, 1⟩, ⟨1, 2, 2, 2⟩),
185 (⟨2, 2, 2, 1⟩, ⟨1, 1, 1, 2⟩),
186 (⟨2, 2, 0, 2⟩, ⟨2, 1, 0, 2⟩),
187 (⟨0, 1, 2, 2⟩, ⟨2, 2, 1, 0⟩),
188 (⟨1, 1, 2, 0⟩, ⟨0, 2, 1, 1⟩)],
189 [(⟨0, 1, 2, 2⟩, ⟨2, 2, 1, 0⟩),
190 (⟨0, 1, 2, 1⟩, ⟨1, 2, 1, 0⟩),
191 (⟨1, 0, 1, 1⟩, ⟨1, 0, 2, 1⟩),
192 (⟨2, 1, 0, 2⟩, ⟨2, 2, 0, 2⟩),
193 (⟨2, 1, 2, 0⟩, ⟨0, 2, 1, 2⟩)],
194 [(⟨2, 2, 1, 0⟩, ⟨0, 1, 2, 2⟩),
195 (⟨2, 2, 0, 2⟩, ⟨2, 1, 0, 2⟩),
196 (⟨1, 1, 1, 2⟩, ⟨2, 2, 2, 1⟩),
197 (⟨0, 1, 2, 0⟩, ⟨0, 2, 1, 0⟩),
198 (⟨1, 2, 0, 1⟩, ⟨1, 1, 0, 1⟩)],
199 [(⟨2, 2, 1, 0⟩, ⟨0, 1, 2, 2⟩),
200 (⟨2, 1, 1, 1⟩, ⟨1, 2, 2, 2⟩),
201 (⟨2, 2, 2, 1⟩, ⟨1, 1, 1, 2⟩),
202 (⟨1, 2, 1, 0⟩, ⟨0, 1, 2, 1⟩),
203 (⟨2, 2, 1, 0⟩, ⟨0, 1, 2, 2⟩)],
204 [(⟨0, 1, 2, 2⟩, ⟨2, 2, 1, 0⟩),
205 (⟨1, 1, 1, 2⟩, ⟨2, 2, 2, 1⟩),
206 (⟨2, 2, 0, 2⟩, ⟨2, 1, 0, 2⟩),
207 (⟨2, 1, 1, 1⟩, ⟨1, 2, 2, 2⟩),
208 (⟨1, 1, 0, 1⟩, ⟨1, 2, 0, 1⟩)],
209 [(⟨1, 0, 2, 1⟩, ⟨1, 0, 1, 1⟩),
210 (⟨2, 0, 1, 2⟩, ⟨2, 0, 2, 2⟩),
211 (⟨1, 1, 0, 1⟩, ⟨1, 2, 0, 1⟩),
212 (⟨1, 2, 1, 0⟩, ⟨0, 1, 2, 1⟩),
213 (⟨0, 1, 2, 2⟩, ⟨2, 2, 1, 0⟩)],
214 [(⟨1, 0, 1, 1⟩, ⟨1, 0, 2, 1⟩),
215 (⟨2, 0, 2, 2⟩, ⟨2, 0, 1, 2⟩),
216 (⟨1, 1, 1, 2⟩, ⟨2, 2, 2, 1⟩),
217 (⟨0, 2, 1, 0⟩, ⟨0, 1, 2, 0⟩),
218 (⟨0, 2, 1, 2⟩, ⟨2, 1, 2, 0⟩)],
219 [(⟨1, 0, 1, 1⟩, ⟨1, 0, 2, 1⟩),
220 (⟨1, 2, 2, 2⟩, ⟨2, 1, 1, 1⟩),
221 (⟨2, 2, 2, 1⟩, ⟨1, 1, 1, 2⟩),
222 (⟨2, 1, 0, 2⟩, ⟨2, 2, 0, 2⟩),
223 (⟨1, 0, 1, 1⟩, ⟨1, 0, 2, 1⟩)],
224 [(⟨1, 0, 2, 1⟩, ⟨1, 0, 1, 1⟩),
225 (⟨1, 1, 1, 2⟩, ⟨2, 2, 2, 1⟩),
226 (⟨2, 0, 2, 2⟩, ⟨2, 0, 1, 2⟩),
227 (⟨2, 1, 1, 1⟩, ⟨1, 2, 2, 2⟩),
228 (⟨2, 1, 2, 0⟩, ⟨0, 2, 1, 2⟩)],
229 [(⟨2, 1, 1, 1⟩, ⟨1, 2, 2, 2⟩),
230 (⟨1, 1, 1, 2⟩, ⟨2, 2, 2, 1⟩),
231 (⟨1, 0, 1, 1⟩, ⟨1, 0, 2, 1⟩),
232 (⟨1, 2, 0, 1⟩, ⟨1, 1, 0, 1⟩),
233 (⟨1, 2, 1, 0⟩, ⟨0, 1, 2, 1⟩)],
234 [(⟨2, 0, 1, 2⟩, ⟨2, 0, 2, 2⟩),
235 (⟨2, 2, 2, 1⟩, ⟨1, 1, 1, 2⟩),
236 (⟨2, 1, 2, 0⟩, ⟨0, 2, 1, 2⟩),
237 (⟨0, 1, 2, 2⟩, ⟨2, 2, 1, 0⟩),
238 (⟨1, 2, 2, 2⟩, ⟨2, 1, 1, 1⟩)],
239 [(⟨0, 1, 2, 0⟩, ⟨0, 2, 1, 0⟩),
240 (⟨2, 2, 0, 2⟩, ⟨2, 1, 0, 2⟩),
241 (⟨0, 2, 1, 2⟩, ⟨2, 1, 2, 0⟩),
242 (⟨1, 1, 0, 1⟩, ⟨1, 2, 0, 1⟩),
243 (⟨0, 1, 2, 1⟩, ⟨1, 2, 1, 0⟩)],
244 [(⟨2, 0, 2, 2⟩, ⟨2, 0, 1, 2⟩),
245 (⟨2, 1, 0, 2⟩, ⟨2, 2, 0, 2⟩),
246 (⟨1, 0, 2, 1⟩, ⟨1, 0, 1, 1⟩),
247 (⟨1, 2, 0, 1⟩, ⟨1, 1, 0, 1⟩),
248 (⟨2, 2, 2, 1⟩, ⟨1, 1, 1, 2⟩)],
249 [(⟨2, 1, 1, 1⟩, ⟨1, 2, 2, 2⟩),
250 (⟨1, 1, 1, 2⟩, ⟨2, 2, 2, 1⟩),
251 (⟨1, 1, 2, 0⟩, ⟨0, 2, 1, 1⟩),
252 (⟨0, 2, 1, 2⟩, ⟨2, 1, 2, 0⟩),
253 (⟨2, 1, 0, 2⟩, ⟨2, 2, 0, 2⟩)],
254 [(⟨1, 1, 2, 0⟩, ⟨0, 2, 1, 1⟩),
255 (⟨2, 2, 2, 1⟩, ⟨1, 1, 1, 2⟩),
256 (⟨2, 2, 0, 2⟩, ⟨2, 1, 0, 2⟩),
257 (⟨1, 0, 2, 1⟩, ⟨1, 0, 1, 1⟩),
258 (⟨1, 2, 2, 2⟩, ⟨2, 1, 1, 1⟩)],
259 [(⟨0, 2, 1, 0⟩, ⟨0, 1, 2, 0⟩),
260 (⟨2, 0, 2, 2⟩, ⟨2, 0, 1, 2⟩),
261 (⟨2, 0, 0, 2⟩, ⟨2, 0, 0, 2⟩),
262 (⟨2, 1, 2, 0⟩, ⟨0, 2, 1, 2⟩),
263 (⟨2, 2, 0, 2⟩, ⟨2, 1, 0, 2⟩)],
264 [(⟨0, 2, 1, 1⟩, ⟨1, 1, 2, 0⟩),
265 (⟨2, 0, 1, 2⟩, ⟨2, 0, 2, 2⟩),
266 (⟨2, 0, 0, 2⟩, ⟨2, 0, 0, 2⟩),
267 (⟨1, 2, 0, 1⟩, ⟨1, 1, 0, 1⟩),
268 (⟨1, 2, 2, 2⟩, ⟨2, 1, 1, 1⟩)],
269 [(⟨0, 2, 1, 1⟩, ⟨1, 1, 2, 0⟩),
270 (⟨1, 1, 1, 2⟩, ⟨2, 2, 2, 1⟩),
271 (⟨0, 1, 2, 0⟩, ⟨0, 2, 1, 0⟩),
272 (⟨2, 2, 0, 2⟩, ⟨2, 1, 0, 2⟩),
273 (⟨1, 1, 1, 2⟩, ⟨2, 2, 2, 1⟩)],
274 [(⟨1, 1, 2, 0⟩, ⟨0, 2, 1, 1⟩),
275 (⟨2, 1, 1, 1⟩, ⟨1, 2, 2, 2⟩),
276 (⟨1, 2, 1, 0⟩, ⟨0, 1, 2, 1⟩),
277 (⟨0, 2, 1, 0⟩, ⟨0, 1, 2, 0⟩),
278 (⟨2, 1, 1, 1⟩, ⟨1, 2, 2, 2⟩)],
279 [(⟨1, 2, 2, 2⟩, ⟨2, 1, 1, 1⟩),
280 (⟨2, 1, 1, 1⟩, ⟨1, 2, 2, 2⟩),
281 (⟨1, 1, 1, 2⟩, ⟨2, 2, 2, 1⟩),
282 (⟨1, 1, 2, 0⟩, ⟨0, 2, 1, 1⟩),
283 (⟨2, 0, 1, 2⟩, ⟨2, 0, 2, 2⟩)],
284 [(⟨2, 1, 1, 1⟩, ⟨1, 2, 2, 2⟩),
285 (⟨1, 2, 2, 2⟩, ⟨2, 1, 1, 1⟩),
286 (⟨2, 1, 0, 2⟩, ⟨2, 2, 0, 2⟩),
287 (⟨0, 2, 1, 0⟩, ⟨0, 1, 2, 0⟩),
288 (⟨2, 0, 2, 2⟩, ⟨2, 0, 1, 2⟩)],
289 [(⟨2, 1, 0, 2⟩, ⟨2, 2, 0, 2⟩),
290 (⟨2, 2, 0, 2⟩, ⟨2, 1, 0, 2⟩),
291 (⟨1, 0, 2, 1⟩, ⟨1, 0, 1, 1⟩),
292 (⟨0, 1, 2, 1⟩, ⟨1, 2, 1, 0⟩),
293 (⟨0, 2, 1, 0⟩, ⟨0, 1, 2, 0⟩)],
294 [(⟨2, 2, 0, 2⟩, ⟨2, 1, 0, 2⟩),
295 (⟨2, 1, 0, 2⟩, ⟨2, 2, 0, 2⟩),
296 (⟨2, 0, 1, 2⟩, ⟨2, 0, 2, 2⟩),
297 (⟨1, 1, 1, 2⟩, ⟨2, 2, 2, 1⟩),
298 (⟨0, 1, 2, 0⟩, ⟨0, 2, 1, 0⟩)],
299 [(⟨2, 1, 1, 1⟩, ⟨1, 2, 2, 2⟩),
300 (⟨0, 1, 2, 1⟩, ⟨1, 2, 1, 0⟩),
301 (⟨1, 2, 0, 1⟩, ⟨1, 1, 0, 1⟩),
302 (⟨2, 0, 1, 2⟩, ⟨2, 0, 2, 2⟩),
303 (⟨0, 1, 2, 1⟩, ⟨1, 2, 1, 0⟩)],
304 [(⟨1, 2, 2, 2⟩, ⟨2, 1, 1, 1⟩),
305 (⟨2, 2, 0, 2⟩, ⟨2, 1, 0, 2⟩),
306 (⟨0, 1, 2, 1⟩, ⟨1, 2, 1, 0⟩),
307 (⟨0, 1, 2, 0⟩, ⟨0, 2, 1, 0⟩),
308 (⟨2, 2, 0, 2⟩, ⟨2, 1, 0, 2⟩)],
309 [(⟨1, 2, 2, 2⟩, ⟨2, 1, 1, 1⟩),
310 (⟨1, 1, 2, 0⟩, ⟨0, 2, 1, 1⟩),
311 (⟨0, 1, 2, 2⟩, ⟨2, 2, 1, 0⟩),
312 (⟨1, 1, 1, 2⟩, ⟨2, 2, 2, 1⟩),
313 (⟨0, 1, 2, 1⟩, ⟨1, 2, 1, 0⟩)],
314 [(⟨2, 0, 2, 2⟩, ⟨2, 0, 1, 2⟩),
315 (⟨0, 2, 1, 1⟩, ⟨1, 1, 2, 0⟩),
316 (⟨2, 2, 1, 0⟩, ⟨0, 1, 2, 2⟩),
317 (⟨0, 2, 1, 0⟩, ⟨0, 1, 2, 0⟩),
318 (⟨1, 1, 1, 2⟩, ⟨2, 2, 2, 1⟩)],
319 [(⟨0, 2, 1, 0⟩, ⟨0, 1, 2, 0⟩),
320 (⟨1, 2, 1, 0⟩, ⟨0, 1, 2, 1⟩),
321 (⟨0, 1, 2, 2⟩, ⟨2, 2, 1, 0⟩),
322 (⟨0, 1, 2, 1⟩, ⟨1, 2, 1, 0⟩),
323 (⟨0, 2, 1, 1⟩, ⟨1, 1, 2, 0⟩)],
324 [(⟨2, 0, 1, 2⟩, ⟨2, 0, 2, 2⟩),
325 (⟨0, 1, 2, 1⟩, ⟨1, 2, 1, 0⟩),
326 (⟨1, 0, 1, 1⟩, ⟨1, 0, 2, 1⟩),
327 (⟨1, 2, 1, 0⟩, ⟨0, 1, 2, 1⟩),
328 (⟨1, 1, 1, 2⟩, ⟨2, 2, 2, 1⟩)],
329 [(⟨1, 2, 2, 2⟩, ⟨2, 1, 1, 1⟩),
330 (⟨2, 2, 2, 1⟩, ⟨1, 1, 1, 2⟩),
331 (⟨2, 0, 1, 2⟩, ⟨2, 0, 2, 2⟩),
332 (⟨1, 1, 1, 2⟩, ⟨2, 2, 2, 1⟩),
333 (⟨2, 2, 0, 2⟩, ⟨2, 1, 0, 2⟩)],
334 [(⟨0, 2, 1, 1⟩, ⟨1, 1, 2, 0⟩),
335 (⟨1, 1, 1, 2⟩, ⟨2, 2, 2, 1⟩),
336 (⟨0, 1, 2, 1⟩, ⟨1, 2, 1, 0⟩),
337 (⟨2, 2, 2, 1⟩, ⟨1, 1, 1, 2⟩),
338 (⟨2, 1, 1, 1⟩, ⟨1, 2, 2, 2⟩)],
339 [(⟨0, 1, 2, 0⟩, ⟨0, 2, 1, 0⟩),
340 (⟨1, 2, 2, 2⟩, ⟨2, 1, 1, 1⟩),
341 (⟨2, 0, 0, 2⟩, ⟨2, 0, 0, 2⟩),
342 (⟨0, 2, 1, 1⟩, ⟨1, 1, 2, 0⟩),
343 (⟨2, 0, 2, 2⟩, ⟨2, 0, 1, 2⟩)],
344 [(⟨1, 1, 2, 0⟩, ⟨0, 2, 1, 1⟩),
345 (⟨2, 1, 1, 1⟩, ⟨1, 2, 2, 2⟩),
346 (⟨2, 0, 0, 2⟩, ⟨2, 0, 0, 2⟩),
347 (⟨2, 0, 2, 2⟩, ⟨2, 0, 1, 2⟩),
348 (⟨0, 2, 1, 0⟩, ⟨0, 1, 2, 0⟩)]]
349
350set_option maxHeartbeats 2000000 in
351/-- The action of the forty eight automorphisms of Q3 on the five free
352generators, as words. This is the only datum whose provenance Lean takes on
353trust; everything the separation theorem needs is computed from it inside Lean,
354so `autTables` above is a convenience and not a trusted input. -/
355def autSubst : List (List Word) :=
356 [[[1], [2], [3], [4], [5]],
357 [[-1], [3, 5, -4, -1], [2, 5, -4, -1], [1, -4, -1], [1, 4, -5, -4, -1]],
358 [[-1], [-2], [4, -2], [3, -2], [2, -5, -2]],
359 [[1], [4, -5, -3, 1], [-5, -3, 1], [-1, 2, -3, 1], [-1, 3, 5, -3, 1]],
360 [[5], [-2], [-3], [-4], [1]],
361 [[-5], [-3, 1, 4, -5], [-2, 1, 4, -5], [5, 4, -5], [5, -4, -1, 4, -5]],
362 [[-5], [2], [-4, 2], [-3, 2], [-2, -1, 2]],
363 [[5], [-4, -1, 3, 5], [-1, 3, 5], [-5, -2, 3, 5], [-5, -3, 1, 3, 5]],
364 [[2, -3], [1, 4, -5, -3], [4, -5, -3], [3, -5, -3], [3, 5, -4, -5, -3]],
365 [[3, -2], [-2], [1, -2], [2, 5, -2], [2, 4, -2]],
366 [[-4], [-1, 3, 5, -4], [3, 5, -4], [4, 5, -4], [4, -5, -3, 2, 5, -4]],
367 [[4], [2], [-1, 2], [-5], [-2, 3]],
368 [[-2, 3], [5, -4, -1, 3], [-4, -1, 3], [-3, -1, 3], [-3, 1, 4, -1, 3]],
369 [[-3, 2], [2], [5, 2], [-2, 1, 2], [-2, -4, 2]],
370 [[4], [-5, -3, 1, 4], [-3, 1, 4], [-4, 1, 4], [-4, -1, 3, -2, 1, 4]],
371 [[-4], [-2], [-5, -2], [-1], [2, -3]],
372 [[-1], [2, 5, -3, -1], [1, -3, -1], [1, 4, -3, -1], [1, 3, -5, -3, -1]],
373 [[1], [3, -5, -2, 1], [4, -5, -2, 1], [-5, -2, 1], [-1, 2, 5, -2, 1]],
374 [[1], [-5, -4, 1], [-1, 2, -4, 1], [-1, 3, -4, 1], [-1, 4, 5, -4, 1]],
375 [[-1], [4, 5, -1], [3, 5, -1], [2, 5, -1], [1, -5, -1]],
376 [[-5], [-2, 1, 3, -5], [5, 3, -5], [5, -4, 3, -5], [5, -3, -1, 3, -5]],
377 [[5], [-3, -1, 2, 5], [-4, -1, 2, 5], [-1, 2, 5], [-5, -2, 1, 2, 5]],
378 [[5], [-1, 4, 5], [-5, -2, 4, 5], [-5, -3, 4, 5], [-5, -4, 1, 4, 5]],
379 [[-5], [-4, 1, -5], [-3, 1, -5], [-2, 1, -5], [5, -1, -5]],
380 [[2, 5, -1], [4, 5, -1], [1, 4, 5, -1], [1, 5, -1], [1, -5, -4, 3, 5, -1]],
381 [[3, -4], [1, -5, -4], [-5, -4], [4, -5, -4], [4, 5, -1, 2, -4]],
382 [[-5, -2, 1], [3, -5, -2, 1], [-1, 3, -5, -2, 1], [-1, 2, -5, -2, 1], [-1, 2, 5, -3, 4, -5, -2, 1]],
383 [[4, -3], [-1, 2, 5, -3], [2, 5, -3], [3, 5, -3], [3, -5, -2, 1, -3]],
384 [[-2, 1, -5], [-4, 1, -5], [5, -4, 1, -5], [5, 1, -5], [5, -1, 4, -3, 1, -5]],
385 [[-3, 4], [5, -1, 4], [-1, 4], [-4, -1, 4], [-4, 1, -5, -2, 4]],
386 [[-1, 2, 5], [-3, -1, 2, 5], [-5, -3, -1, 2, 5], [-5, -2, -1, 2, 5], [-5, -2, 1, 3, -4, -1, 2, 5]],
387 [[-4, 3], [-5, -2, 1, 3], [-2, 1, 3], [-3, 1, 3], [-3, -1, 2, 5, 3]],
388 [[3, -2], [1, -4, 3, -2], [2, 5, -4, 3, -2], [2, -4, 3, -2], [2, -3, 4, 3, -2]],
389 [[2, -3], [4, -1, 2, -3], [3, -1, 2, -3], [3, 5, -1, 2, -3], [3, -2, 1, -4, -1, 2, -3]],
390 [[4], [-1, 2, -3, 4], [-5, -3, 4], [-3, 4], [-4, 3, -2, 4]],
391 [[-4], [3, -2, 1, -4], [4, -2, 1, -4], [4, -5, -2, 1, -4], [4, -1, 2, -3, 1, -4]],
392 [[-3, 2], [5, 4, -3, 2], [-2, 1, 4, -3, 2], [-2, 4, -3, 2], [-2, 3, -4, -3, 2]],
393 [[-2, 3], [-4, -5, -2, 3], [-3, -5, -2, 3], [-3, 1, -5, -2, 3], [-3, 2, 5, 4, -5, -2, 3]],
394 [[-4], [-5, -2, 3, -4], [-1, 3, -4], [3, -4], [4, -3, 2, -4]],
395 [[4], [-3, 2, 5, 4], [-4, 2, 5, 4], [-4, -1, 2, 5, 4], [-4, -5, -2, 3, 5, 4]],
396 [[1, -5, -2], [3, -4, -5, -2], [2, -4, -5, -2], [2, 5, -4, -5, -2], [2, 5, 4, -3, -5, -2]],
397 [[4, -3], [2, 5, 4, -3], [3, 5, 4, -3], [3, 4, -3], [3, -4, -5, -2, 1, 4, -3]],
398 [[-1, 2, 5], [4, -3, 2, 5], [-3, 2, 5], [-5, -3, 2, 5], [-5, -2, 3, -4, 2, 5]],
399 [[3, -4], [-5, -2, 3, -4], [4, -5, -2, 3, -4], [4, -2, 3, -4], [4, -3, 2, 5, -1, 3, -4]],
400 [[5, -1, 2], [-3, 4, -1, 2], [-2, 4, -1, 2], [-2, 1, 4, -1, 2], [-2, 1, -4, 3, -1, 2]],
401 [[-4, 3], [-2, 1, -4, 3], [-3, 1, -4, 3], [-3, -4, 3], [-3, 4, -1, 2, 5, -4, 3]],
402 [[-5, -2, 1], [-4, 3, -2, 1], [3, -2, 1], [-1, 3, -2, 1], [-1, 2, -3, 4, -2, 1]],
403 [[-3, 4], [-1, 2, -3, 4], [-4, -1, 2, -3, 4], [-4, 2, -3, 4], [-4, 3, -2, 1, -5, -3, 4]]]
404
405end Certificate
406end Loom
407end IndisputableMonolith
408