Historical formal replay instructions (September 2026)
Paper XII: Patching Support, Hecke Packets, and Conditional Automorphic Completion
README.md
1 # Patching Support, Hecke Packets, and Conditional Automorphic Completion
2
3 Komorebi P. — Paper XII — v0.17.1 independent re-verification
4
5
6 Verified September 11, 2026 (America/Chicago). Exact UTC times are in the audit.
7
8 **Revised manuscript: 49/49 internal claims complete, 0 partial, 0 unchecked.**
9 **Original wording: 41 complete, 7 partial, 1 unchecked.**
10
11 Claims 3.1 and 3.3 are verified on actual completed objects, with their topologies,
12 canonical factor maps, coefficient-algebra structure, locality, and point naturality.
13 There are no remaining internal obligations in the revised contract. The eight
14 inherited amendments and all external arithmetic inputs remain separate.
15
16 ## Correction of the conflicting conversation status
17
18 The later 47/49 retraction was incorrect: it overlooked the full saved v0.17.0
19 archive. This release recovers those existing proofs and independently rechecks
20 them. It does not count the already-written 146-theorem completion block as new
21 work in this run. All 96 production sources are unchanged.
22
23 ## Fresh evidence
24
25 - 96 production modules rebuilt with warnings as errors.
26 - 1,229 production named declarations passed transitive axiom audits.
27 - All three deliberate invalid-proof controls were rejected as expected.
28 - All 96 regenerated compiled-object hashes match the earlier successful release.
29 - All 291 unique targets in the 49-claim map occur in the fresh audit.
30 - Three supplementary contract theorems passed against the fresh objects: exact
31 completed kernel, full tensor-quotient interface, and the Noetherian local
32 coefficient-algebra point-factorization interface.
33
34 Only propext, Classical.choice, and Quot.sound occur in the audited dependencies.
35 The pinned Mathlib cache was used, not rebuilt. The source census remains
36 748 own named theorem declarations plus 81 reused Paper X theorems. The
37 three supplementary release checks are reported separately, not added to the
38 manuscript count.
39
40 ## Reproduce
41
42 ```bash
43 bash Run-Reverified.sh /path/to/Komorebi_Portable_Lean_4.34.0-rc2
44 ```
45
46 This cleans and rebuilds the cumulative project, then runs the supplementary
47 checks. The kit is separate. Native Windows behavior is not claimed; the
48 provided toolchain is Linux/WSL oriented.
49
50 ## Retained boundary
51
52 Representability, residual automorphic occupancy, applicable arithmetic patching
53 and classicality results, attached representations, Frobenius density,
54 semisimplification, and general Brauer–Nesbitt inputs remain external. This is
55 not an unconditional universal companion or unrestricted Langlands theorem.
56 The manuscript and its existing graphics are unchanged in this evidence release.
57
58 ## Contents
59
60 `lean/` contains all cumulative production source. `build/` contains objects
61 regenerated in the current run. `verification.json` and `logs/` are the fresh
62 full-project compiler and axiom records. `final_claims_check.json` and
63 `checks/FinalClaimsConsumer.lean` are the supplemental end-to-end checks.
64 `REVERIFICATION.json` reconciles the status and checks the exact claim-map
65 coverage. `CURRENT_REPLAY_REVIEW.md` describes the mathematical interpretation.
66 `CURRENT_FAILURES.md` records corrected development failures.
67
68 `paper/` preserves the editable v0.17.0 manuscript, figures, and PDF unchanged.
69 `upstream/v0.17_records/` preserves the previous release's metadata as history,
70 not as fresh evidence. `REVISED_COVERAGE.json` and `coverage.json` retain the
71 revised-versus-original boundary. No font files or toolchain are redistributed.