EXACT_CHECKS.json
Paper XII: Patching Support, Hecke Packets, and Conditional Automorphic Completion
EXACT_CHECKS.json
This is the original source text. Reading it does not run or verify the program.
1 {
2 "scope": "Exact illustrative-example checks, not a new Lean verification or theorem census.",
3 "python_version": "3.12.14",
4 "sympy_version": "1.14.0",
5 "script_sha256": "bb7809b2c40f79def2ef2bf1983e17bf067893948e077a8d766de1c2dc88df52",
6 "status": "PASS",
7 "check_count": 46,
8 "checks": [
9 {
10 "name": "local_points_order_three",
11 "status": "PASS",
12 "detail": {
13 "candidate_count": 625,
14 "accepted_count": 5,
15 "accepted": [
16 [
17 0,
18 0,
19 0,
20 0
21 ],
22 [
23 0,
24 1,
25 0,
26 1
27 ],
28 [
29 0,
30 2,
31 0,
32 2
33 ],
34 [
35 0,
36 3,
37 0,
38 3
39 ],
40 [
41 0,
42 4,
43 0,
44 4
45 ]
46 ]
47 }
48 },
49 {
50 "name": "local_points_order_two",
51 "status": "PASS",
52 "detail": {
53 "candidate_count": 25,
54 "accepted_count": 5,
55 "image_of_order_three": [
56 [
57 0,
58 0
59 ]
60 ],
61 "nonzero_tangent_directions_with_no_lift": 4
62 }
63 },
64 {
65 "name": "quotient_monomial_window",
66 "status": "PASS",
67 "detail": {
68 "window_total_degree_less_than": 6,
69 "shown": 21,
70 "surviving_O_basis": [
71 [
72 0,
73 0
74 ],
75 [
76 1,
77 0
78 ]
79 ]
80 }
81 },
82 {
83 "name": "adic_prefix_compatibility",
84 "status": "PASS",
85 "detail": [
86 {
87 "n": 1,
88 "modulus": 5,
89 "a": 1,
90 "b": 1,
91 "ring_cardinality": 25
92 },
93 {
94 "n": 2,
95 "modulus": 25,
96 "a": 11,
97 "b": 16,
98 "ring_cardinality": 625
99 },
100 {
101 "n": 3,
102 "modulus": 125,
103 "a": 11,
104 "b": 16,
105 "ring_cardinality": 15625
106 },
107 {
108 "n": 4,
109 "modulus": 625,
110 "a": 11,
111 "b": 266,
112 "ring_cardinality": 390625
113 },
114 {
115 "n": 5,
116 "modulus": 3125,
117 "a": 1261,
118 "b": 2766,
119 "ring_cardinality": 9765625
120 },
121 {
122 "n": 6,
123 "modulus": 15625,
124 "a": 4386,
125 "b": 5891,
126 "ring_cardinality": 244140625
127 }
128 ]
129 },
130 {
131 "name": "fitting_matrix_index_0",
132 "status": "PASS",
133 "detail": {
134 "generators": [
135 "x*y"
136 ]
137 }
138 },
139 {
140 "name": "presentation_stabilization_index_0",
141 "status": "PASS",
142 "detail": "Explicit diag(x,y) versus diag(x,y,1), not a proof of general presentation independence."
143 },
144 {
145 "name": "fitting_matrix_index_1",
146 "status": "PASS",
147 "detail": {
148 "generators": [
149 "x",
150 "0",
151 "0",
152 "y"
153 ]
154 }
155 },
156 {
157 "name": "presentation_stabilization_index_1",
158 "status": "PASS",
159 "detail": "Explicit diag(x,y) versus diag(x,y,1), not a proof of general presentation independence."
160 },
161 {
162 "name": "fitting_matrix_index_2",
163 "status": "PASS",
164 "detail": {
165 "generators": [
166 "1"
167 ]
168 }
169 },
170 {
171 "name": "presentation_stabilization_index_2",
172 "status": "PASS",
173 "detail": "Explicit diag(x,y) versus diag(x,y,1), not a proof of general presentation independence."
174 },
175 {
176 "name": "nilpotent_fitting_ideals",
177 "status": "PASS",
178 "detail": {
179 "F0": "(x^2 y)",
180 "F1": "(x^2,y)"
181 }
182 },
183 {
184 "name": "fiber_rank_1_1",
185 "status": "PASS",
186 "detail": {
187 "point": [
188 1,
189 1
190 ],
191 "fiber_dimension": 0
192 }
193 },
194 {
195 "name": "fiber_rank_0_1",
196 "status": "PASS",
197 "detail": {
198 "point": [
199 0,
200 1
201 ],
202 "fiber_dimension": 1
203 }
204 },
205 {
206 "name": "fiber_rank_1_0",
207 "status": "PASS",
208 "detail": {
209 "point": [
210 1,
211 0
212 ],
213 "fiber_dimension": 1
214 }
215 },
216 {
217 "name": "fiber_rank_0_0",
218 "status": "PASS",
219 "detail": {
220 "point": [
221 0,
222 0
223 ],
224 "fiber_dimension": 2
225 }
226 },
227 {
228 "name": "diagonal_base_change_0",
229 "status": "PASS",
230 "detail": {
231 "expected": [
232 "t**2"
233 ]
234 }
235 },
236 {
237 "name": "diagonal_base_change_1",
238 "status": "PASS",
239 "detail": {
240 "expected": [
241 "t"
242 ]
243 }
244 },
245 {
246 "name": "diagonal_base_change_2",
247 "status": "PASS",
248 "detail": {
249 "expected": [
250 "1"
251 ]
252 }
253 },
254 {
255 "name": "coordinate_change_invertible",
256 "status": "PASS",
257 "detail": "Over characteristic not equal to 2; the geometric plate uses real coordinates."
258 },
259 {
260 "name": "coordinate_change_fitting",
261 "status": "PASS",
262 "detail": {
263 "F0": "(a^2-b^2)",
264 "F1": "(a,b)"
265 }
266 },
267 {
268 "name": "CRT_polynomial_congruences",
269 "status": "PASS",
270 "detail": {
271 "p_plus": "-3*z**4/16 - z**3/4 + 3*z**2/8 + 3*z/4 + 5/16",
272 "modulus": "z**5 + z**4 - 2*z**3 - 2*z**2 + z + 1"
273 }
274 },
275 {
276 "name": "CRT_matrix_projectors",
277 "status": "PASS",
278 "detail": {
279 "ranks": [
280 2,
281 3
282 ],
283 "traces": [
284 "2",
285 "3"
286 ]
287 }
288 },
289 {
290 "name": "ordinary_vs_generalized",
291 "status": "PASS",
292 "detail": {
293 "ordinary": [
294 1,
295 1
296 ],
297 "generalized": [
298 2,
299 3
300 ]
301 }
302 },
303 {
304 "name": "packet_residue_fibers",
305 "status": "PASS",
306 "detail": "Regular local packet dimensions 2 and 3, residue fibers each dimension 1."
307 },
308 {
309 "name": "empty_packet_example",
310 "status": "PASS",
311 "detail": "The supplied T-module T_+ is not faithful on the second factor."
312 },
313 {
314 "name": "dyadic_idempotents",
315 "status": "PASS",
316 "detail": [
317 [
318 0,
319 0
320 ],
321 [
322 1,
323 0
324 ]
325 ]
326 },
327 {
328 "name": "dyadic_involution",
329 "status": "PASS",
330 "detail": "Multiplication by g=1+d has g^2=1 over F_2 and a nonzero nilpotent part."
331 },
332 {
333 "name": "trace_not_occupancy_in_characteristic_two",
334 "status": "PASS",
335 "detail": {
336 "idempotent": "I_2",
337 "rank_over_F2": 2,
338 "trace_over_F2": 0
339 }
340 },
341 {
342 "name": "stable_core_identities",
343 "status": "PASS",
344 "detail": {
345 "P_power_image_dimensions": [
346 3,
347 1,
348 1,
349 1,
350 1
351 ],
352 "N_power_image_dimensions": [
353 3,
354 2,
355 1,
356 0,
357 0
358 ]
359 }
360 },
361 {
362 "name": "fixed_carrier_nested_projectors",
363 "status": "PASS",
364 "detail": {
365 "dimensions": [
366 5,
367 4,
368 4,
369 2,
370 1,
371 1,
372 1,
373 1
374 ],
375 "a_plateau_precedes_a_later_drop": true,
376 "definition_after_level_5": "constant projector onto e_1"
377 }
378 },
379 {
380 "name": "derived_fiber_dimensions",
381 "status": "PASS",
382 "detail": "C=[k[t] --t--> k[t]] in degrees 0,1; all a != 0 give an isomorphism."
383 },
384 {
385 "name": "S3_group_relations_F7",
386 "status": "PASS",
387 "detail": "Exact defining relations modulo 7."
388 },
389 {
390 "name": "S3_projector_pairings_F7",
391 "status": "PASS",
392 "detail": {
393 "pairings_mod_7": [
394 3,
395 6
396 ]
397 }
398 },
399 {
400 "name": "S3_projector_idempotence_F7",
401 "status": "PASS",
402 "detail": "Printed canonical projectors are idempotent."
403 },
404 {
405 "name": "S3_canonical_formula_F7",
406 "status": "PASS",
407 "detail": "Inverses of 2-4 and 1-(-1) are 3 and 4 in F7."
408 },
409 {
410 "name": "S3_adjoint_basis_F7",
411 "status": "PASS",
412 "detail": "Columns Z,A,B have determinant 3 modulo 7."
413 },
414 {
415 "name": "S3_eigenvalue_polynomials_F7",
416 "status": "PASS",
417 "detail": "Characteristic polynomials split as printed."
418 },
419 {
420 "name": "augmentation_binomial_relations_F2",
421 "status": "PASS",
422 "detail": "C4 x C2 relations in F2."
423 },
424 {
425 "name": "augmentation_basis_and_nilpotence",
426 "status": "PASS",
427 "detail": {
428 "basis_exponents": [
429 [
430 0,
431 0
432 ],
433 [
434 1,
435 0
436 ],
437 [
438 2,
439 0
440 ],
441 [
442 3,
443 0
444 ],
445 [
446 0,
447 1
448 ],
449 [
450 1,
451 1
452 ],
453 [
454 2,
455 1
456 ],
457 [
458 3,
459 1
460 ]
461 ],
462 "nilpotence_bound": 5
463 }
464 },
465 {
466 "name": "conjugate_involution_frame",
467 "status": "PASS",
468 "detail": "Both frames satisfy A^2=I."
469 },
470 {
471 "name": "frame_reduction_mismatch",
472 "status": "PASS",
473 "detail": "Compatible conjugacy classes need not give compatible arbitrary frames."
474 },
475 {
476 "name": "compatible_diagonal_representatives",
477 "status": "PASS",
478 "detail": "Prefixes checked through level 6; the all-level formula is reduction of one integral D."
479 },
480 {
481 "name": "involution_equations",
482 "status": "PASS",
483 "detail": "Four exact entries of A^2-I."
484 },
485 {
486 "name": "frame_sensitive_entry",
487 "status": "PASS",
488 "detail": "a12=0 is not invariant under admissible change of frame."
489 },
490 {
491 "name": "trace_separator_exact_solution",
492 "status": "PASS",
493 "detail": {
494 "determinant": -2,
495 "multiplicities": [
496 3,
497 2
498 ]
499 }
500 },
501 {
502 "name": "trace_separator_dyadic_failure",
503 "status": "PASS",
504 "detail": "The same sample rows merge in characteristic two."
505 }
506 ],
507 "limits": [
508 "Finite arithmetic enumerations are exhaustive only for their stated finite models.",
509 "Uniform algebraic conclusions and infinite-limit claims have explicit arguments in the appendix.",
510 "No test verifies external arithmetic existence, classicality, or automorphy inputs.",
511 "No new examples have been formalized in Lean by this editorial release."
512 ]
513 }
Other PDFs for this work
Original file and source record
This copy matches the recorded source file. Its publication here does not change the work’s review status.
SHA-256: f402ba5c9be0c5aeb68e245d864a1847b5a8ffff378076960d92d14aa8d94626
Back to Paper XII: Patching Support, Hecke Packets, and Conditional Automorphic Completion