Paper XII: Patching Support, Hecke Packets, and Conditional Automorphic Completion

Download original file

This is the original source text. Reading it does not run or verify the program.

Read the typeset paper

1 {
2   "date": "2026-10-06",
3   "source_tex_name": "Paper_XII_Revised_Formalization_Complete_v0.17.0.tex",
4   "source_tex_sha256": "5b1aa5b7d8919d60b53cd85fd900dc4ab98fdcd52991f1f48380535ab7243cc4",
5   "evidence_record": "formal_release/REVISED_COVERAGE.json; provenance/Paper_XII_v0.17.1_Status.md",
6   "scope": "Reading-entry coverage for the historical revised contract; not a new formal proof map.",
7   "revised_census": {
8     "complete": 49,
9     "partial": 0,
10     "unchecked": 0
11   },
12   "original_census": {
13     "complete": 41,
14     "partial": 7,
15     "unchecked": 1
16   },
17   "claims": [
18     {
19       "number": "3.1",
20       "label": "thm:tensor_quotient",
21       "source_line": 222,
22       "guide_pages": [
23         3,
24         5,
25         19
26       ],
27       "inherited_revised_status": "complete",
28       "inherited_amendment": false,
29       "original_wording_status": "complete"
30     },
31     {
32       "number": "3.2",
33       "label": "cor:simultaneous_local",
34       "source_line": 258,
35       "guide_pages": [
36         4,
37         19,
38         24
39       ],
40       "inherited_revised_status": "complete",
41       "inherited_amendment": false,
42       "original_wording_status": "complete"
43     },
44     {
45       "number": "3.3",
46       "label": "prop:global_local_basechange",
47       "source_line": 266,
48       "guide_pages": [
49         4,
50         19
51       ],
52       "inherited_revised_status": "complete",
53       "inherited_amendment": false,
54       "original_wording_status": "complete"
55     },
56     {
57       "number": "3.4",
58       "label": "prop:local_idempotent",
59       "source_line": 290,
60       "guide_pages": [
61         9,
62         14,
63         21
64       ],
65       "inherited_revised_status": "complete",
66       "inherited_amendment": false,
67       "original_wording_status": "complete"
68     },
69     {
70       "number": "4.2",
71       "label": "thm:s3_adequacy",
72       "source_line": 340,
73       "guide_pages": [
74         20
75       ],
76       "inherited_revised_status": "complete",
77       "inherited_amendment": false,
78       "original_wording_status": "complete"
79     },
80     {
81       "number": "5.1",
82       "label": "prop:group_algebra_transfer",
83       "source_line": 436,
84       "guide_pages": [
85         21
86       ],
87       "inherited_revised_status": "complete",
88       "inherited_amendment": false,
89       "original_wording_status": "complete"
90     },
91     {
92       "number": "5.2",
93       "label": "thm:residual_augmentation_algebra",
94       "source_line": 451,
95       "guide_pages": [
96         14,
97         21
98       ],
99       "inherited_revised_status": "complete",
100       "inherited_amendment": false,
101       "original_wording_status": "complete"
102     },
103     {
104       "number": "5.3",
105       "label": "cor:no_residual_character_splitting",
106       "source_line": 478,
107       "guide_pages": [
108         14,
109         21
110       ],
111       "inherited_revised_status": "complete",
112       "inherited_amendment": false,
113       "original_wording_status": "complete"
114     },
115     {
116       "number": "5.4",
117       "label": "thm:coinvariant_recovery",
118       "source_line": 490,
119       "guide_pages": [
120         14,
121         21
122       ],
123       "inherited_revised_status": "complete",
124       "inherited_amendment": false,
125       "original_wording_status": "complete"
126     },
127     {
128       "number": "6.2",
129       "label": "thm:finite_module_support",
130       "source_line": 547,
131       "guide_pages": [
132         6,
133         9,
134         10
135       ],
136       "inherited_revised_status": "complete",
137       "inherited_amendment": false,
138       "original_wording_status": "complete"
139     },
140     {
141       "number": "6.3",
142       "label": "thm:fitting_support",
143       "source_line": 570,
144       "guide_pages": [
145         6,
146         7
147       ],
148       "inherited_revised_status": "complete",
149       "inherited_amendment": false,
150       "original_wording_status": "complete"
151     },
152     {
153       "number": "6.4",
154       "label": "thm:higher_fitting_strata",
155       "source_line": 590,
156       "guide_pages": [
157         6,
158         7
159       ],
160       "inherited_revised_status": "complete",
161       "inherited_amendment": false,
162       "original_wording_status": "complete"
163     },
164     {
165       "number": "6.5",
166       "label": "prop:fitting_base_change",
167       "source_line": 619,
168       "guide_pages": [
169         8
170       ],
171       "inherited_revised_status": "complete",
172       "inherited_amendment": false,
173       "original_wording_status": "complete"
174     },
175     {
176       "number": "6.7",
177       "label": "thm:near_faithful_full_support",
178       "source_line": 638,
179       "guide_pages": [
180         10
181       ],
182       "inherited_revised_status": "complete",
183       "inherited_amendment": false,
184       "original_wording_status": "complete"
185     },
186     {
187       "number": "6.8",
188       "label": "cor:every_component_support",
189       "source_line": 656,
190       "guide_pages": [
191         10,
192         17
193       ],
194       "inherited_revised_status": "complete",
195       "inherited_amendment": false,
196       "original_wording_status": "complete"
197     },
198     {
199       "number": "6.9",
200       "label": "thm:quotient_support",
201       "source_line": 664,
202       "guide_pages": [
203         10
204       ],
205       "inherited_revised_status": "complete",
206       "inherited_amendment": false,
207       "original_wording_status": "complete"
208     },
209     {
210       "number": "6.11",
211       "label": "thm:ordinary_support_descent",
212       "source_line": 702,
213       "guide_pages": [
214         10,
215         17
216       ],
217       "inherited_revised_status": "complete",
218       "inherited_amendment": false,
219       "original_wording_status": "complete"
220     },
221     {
222       "number": "6.12",
223       "label": "cor:componentwise_occupancy",
224       "source_line": 725,
225       "guide_pages": [
226         10,
227         17,
228         26,
229         27
230       ],
231       "inherited_revised_status": "complete",
232       "inherited_amendment": true,
233       "original_wording_status": "unchecked"
234     },
235     {
236       "number": "6.16",
237       "label": "thm:derived_quotient_support",
238       "source_line": 797,
239       "guide_pages": [
240         11
241       ],
242       "inherited_revised_status": "complete",
243       "inherited_amendment": false,
244       "original_wording_status": "complete"
245     },
246     {
247       "number": "6.18",
248       "label": "thm:derived_support_descent",
249       "source_line": 837,
250       "guide_pages": [
251         11,
252         17
253       ],
254       "inherited_revised_status": "complete",
255       "inherited_amendment": false,
256       "original_wording_status": "complete"
257     },
258     {
259       "number": "6.19",
260       "label": "cor:derived_degree_survives",
261       "source_line": 861,
262       "guide_pages": [
263         11,
264         17
265       ],
266       "inherited_revised_status": "complete",
267       "inherited_amendment": false,
268       "original_wording_status": "complete"
269     },
270     {
271       "number": "7.1",
272       "label": "thm:rt_support_transport",
273       "source_line": 884,
274       "guide_pages": [
275         8,
276         17
277       ],
278       "inherited_revised_status": "complete",
279       "inherited_amendment": false,
280       "original_wording_status": "complete"
281     },
282     {
283       "number": "7.2",
284       "label": "cor:rt_full_support",
285       "source_line": 914,
286       "guide_pages": [
287         8,
288         17
289       ],
290       "inherited_revised_status": "complete",
291       "inherited_amendment": false,
292       "original_wording_status": "complete"
293     },
294     {
295       "number": "7.3",
296       "label": "prop:quotient_erases_component",
297       "source_line": 922,
298       "guide_pages": [
299         9
300       ],
301       "inherited_revised_status": "complete",
302       "inherited_amendment": false,
303       "original_wording_status": "complete"
304     },
305     {
306       "number": "7.4",
307       "label": "thm:field_fiber_criterion",
308       "source_line": 938,
309       "guide_pages": [
310         13,
311         17
312       ],
313       "inherited_revised_status": "complete",
314       "inherited_amendment": false,
315       "original_wording_status": "complete"
316     },
317     {
318       "number": "7.5",
319       "label": "cor:supported_hecke_fiber",
320       "source_line": 960,
321       "guide_pages": [
322         13,
323         17
324       ],
325       "inherited_revised_status": "complete",
326       "inherited_amendment": false,
327       "original_wording_status": "complete"
328     },
329     {
330       "number": "8.2",
331       "label": "thm:canonical_hecke_packets",
332       "source_line": 1005,
333       "guide_pages": [
334         12,
335         13
336       ],
337       "inherited_revised_status": "complete",
338       "inherited_amendment": false,
339       "original_wording_status": "complete"
340     },
341     {
342       "number": "8.3",
343       "label": "cor:simultaneous_generalized_eigenspaces",
344       "source_line": 1026,
345       "guide_pages": [
346         12
347       ],
348       "inherited_revised_status": "complete",
349       "inherited_amendment": false,
350       "original_wording_status": "complete"
351     },
352     {
353       "number": "8.4",
354       "label": "cor:rank_trace_detection",
355       "source_line": 1054,
356       "guide_pages": [
357         12,
358         13,
359         14
360       ],
361       "inherited_revised_status": "complete",
362       "inherited_amendment": false,
363       "original_wording_status": "complete"
364     },
365     {
366       "number": "8.7",
367       "label": "thm:nested_finite_carrier",
368       "source_line": 1112,
369       "guide_pages": [
370         16
371       ],
372       "inherited_revised_status": "complete",
373       "inherited_amendment": false,
374       "original_wording_status": "complete"
375     },
376     {
377       "number": "8.8",
378       "label": "cor:finite_witness_incompatibility",
379       "source_line": 1134,
380       "guide_pages": [
381         16
382       ],
383       "inherited_revised_status": "complete",
384       "inherited_amendment": false,
385       "original_wording_status": "complete"
386     },
387     {
388       "number": "8.10",
389       "label": "lem:stable_core_surjectivity",
390       "source_line": 1167,
391       "guide_pages": [
392         15
393       ],
394       "inherited_revised_status": "complete",
395       "inherited_amendment": false,
396       "original_wording_status": "complete"
397     },
398     {
399       "number": "8.11",
400       "label": "thm:nonzero_stable_core",
401       "source_line": 1190,
402       "guide_pages": [
403         15
404       ],
405       "inherited_revised_status": "complete",
406       "inherited_amendment": false,
407       "original_wording_status": "complete"
408     },
409     {
410       "number": "8.12",
411       "label": "cor:surjective_inverse_system",
412       "source_line": 1210,
413       "guide_pages": [
414         15
415       ],
416       "inherited_revised_status": "complete",
417       "inherited_amendment": false,
418       "original_wording_status": "complete"
419     },
420     {
421       "number": "9.3",
422       "label": "thm:support_gives_hecke_system",
423       "source_line": 1280,
424       "guide_pages": [
425         13,
426         17
427       ],
428       "inherited_revised_status": "complete",
429       "inherited_amendment": false,
430       "original_wording_status": "complete"
431     },
432     {
433       "number": "9.4",
434       "label": "thm:pointwise_galois_realization",
435       "source_line": 1303,
436       "guide_pages": [
437         17,
438         26
439       ],
440       "inherited_revised_status": "complete",
441       "inherited_amendment": true,
442       "original_wording_status": "partial"
443     },
444     {
445       "number": "9.5",
446       "label": "cor:full_support_pointwise_automorphy",
447       "source_line": 1339,
448       "guide_pages": [
449         17,
450         26
451       ],
452       "inherited_revised_status": "complete",
453       "inherited_amendment": true,
454       "original_wording_status": "partial"
455     },
456     {
457       "number": "9.6",
458       "label": "thm:derived_pointwise_realization",
459       "source_line": 1351,
460       "guide_pages": [
461         11,
462         17,
463         26
464       ],
465       "inherited_revised_status": "complete",
466       "inherited_amendment": true,
467       "original_wording_status": "partial"
468     },
469     {
470       "number": "10.3",
471       "label": "thm:companion_branch_criterion",
472       "source_line": 1405,
473       "guide_pages": [
474         22
475       ],
476       "inherited_revised_status": "complete",
477       "inherited_amendment": false,
478       "original_wording_status": "complete"
479     },
480     {
481       "number": "10.4",
482       "label": "cor:empty_companion_obstruction",
483       "source_line": 1419,
484       "guide_pages": [
485         22
486       ],
487       "inherited_revised_status": "complete",
488       "inherited_amendment": false,
489       "original_wording_status": "complete"
490     },
491     {
492       "number": "10.5",
493       "label": "thm:simultaneous_companion_completion",
494       "source_line": 1454,
495       "guide_pages": [
496         23,
497         24,
498         26,
499         27
500       ],
501       "inherited_revised_status": "complete",
502       "inherited_amendment": true,
503       "original_wording_status": "partial"
504     },
505     {
506       "number": "10.7",
507       "label": "thm:one_member_propagation",
508       "source_line": 1485,
509       "guide_pages": [
510         17,
511         26
512       ],
513       "inherited_revised_status": "complete",
514       "inherited_amendment": false,
515       "original_wording_status": "complete"
516     },
517     {
518       "number": "10.9",
519       "label": "prop:finite_frobenius_separator",
520       "source_line": 1508,
521       "guide_pages": [
522         25
523       ],
524       "inherited_revised_status": "complete",
525       "inherited_amendment": false,
526       "original_wording_status": "complete"
527     },
528     {
529       "number": "11.1",
530       "label": "prop:dyadic_sign_projectors",
531       "source_line": 1542,
532       "guide_pages": [
533         14
534       ],
535       "inherited_revised_status": "complete",
536       "inherited_amendment": false,
537       "original_wording_status": "complete"
538     },
539     {
540       "number": "11.2",
541       "label": "cor:dyadic_coinvariant_recovery",
542       "source_line": 1572,
543       "guide_pages": [
544         14,
545         21
546       ],
547       "inherited_revised_status": "complete",
548       "inherited_amendment": false,
549       "original_wording_status": "complete"
550     },
551     {
552       "number": "12.2",
553       "label": "thm:ordinary_conditional_completion",
554       "source_line": 1625,
555       "guide_pages": [
556         17,
557         26
558       ],
559       "inherited_revised_status": "complete",
560       "inherited_amendment": true,
561       "original_wording_status": "partial"
562     },
563     {
564       "number": "12.4",
565       "label": "thm:derived_conditional_completion",
566       "source_line": 1657,
567       "guide_pages": [
568         11,
569         17,
570         26
571       ],
572       "inherited_revised_status": "complete",
573       "inherited_amendment": true,
574       "original_wording_status": "partial"
575     },
576     {
577       "number": "12.5",
578       "label": "thm:system_completion",
579       "source_line": 1675,
580       "guide_pages": [
581         17,
582         26
583       ],
584       "inherited_revised_status": "complete",
585       "inherited_amendment": false,
586       "original_wording_status": "complete"
587     },
588     {
589       "number": "12.6",
590       "label": "thm:five_gate_completion",
591       "source_line": 1696,
592       "guide_pages": [
593         17,
594         26
595       ],
596       "inherited_revised_status": "complete",
597       "inherited_amendment": true,
598       "original_wording_status": "partial"
599     }
600   ],
601   "external_facts": [
602     {
603       "number": "2.2",
604       "label": "fact:represented_deformation",
605       "title": "Represented deformation problem"
606     },
607     {
608       "number": "2.3",
609       "label": "fact:automorphy_package",
610       "title": "Automorphy lifting package"
611     },
612     {
613       "number": "4.1",
614       "label": "fact:adequacy",
615       "title": "Adequate image"
616     },
617     {
618       "number": "5.5",
619       "label": "fact:iwasawa_limit",
620       "title": "Iwasawa limit"
621     },
622     {
623       "number": "6.15",
624       "label": "fact:derived_support_cohomology",
625       "title": "Cohomological description of derived support"
626     },
627     {
628       "number": "8.1",
629       "label": "fact:artin_decomposition",
630       "title": "Artin decomposition"
631     },
632     {
633       "number": "9.2",
634       "label": "fact:chebotarev_brauer_nesbitt",
635       "title": "Chebotarev and Brauer Nesbitt identification"
636     },
637     {
638       "number": "10.6",
639       "label": "fact:strict_compatibility",
640       "title": "Strict compatibility and one member determination"
641     }
642   ]
643 }

Back to source controls

Back to Paper XII: Patching Support, Hecke Packets, and Conditional Automorphic Completion