Current guide: source locations, correspondence, and replay limits
Paper IX: Arithmetic Packets, Dyadic Towers, and Local Polynomial Deformation
README.md
1 # Euler Congruences — final strengthened Lean guide
2
3 Author: Komorebi P. Current release: 20 October 2026. Mathematical baseline retained from the October 10 reading edition.
4
5 This guide adds a current claim/coverage chapter to the complete retained Paper IX Lean companion. It distinguishes the compiled historical Nishibuchi completion, the already formalized N=4 all-row/common-step congruences and sharp first-period/isometry results, and the new general-modulus, mixed factorial, higher exactness and analytic-radius proofs that do not yet have compiled Lean endpoints.
6
7 The retained guide contains eleven teaching chapters, 47 exact contiguous Lean excerpts comprising 623 raw source lines, the full 1,876-row declaration/source-version catalog under 199 canonical source files, the latest 55-module polynomial dependency map, and a crosswalk for 62 preceding-manuscript statements / 202 source links. The current opening is a twelfth instructional chapter. The current crosswalk resolves all 62 entries against the 232-page final monograph and its current SHA-256. The 202 original formal source links remain unchanged; guide locators resolve in this 139-page reader.
8
9 ## Build the PDF
10
11 From this directory:
12
13 ```sh
14 python3 build.py
15 ```
16
17 The isolated builder uses XeLaTeX, `SOURCE_DATE_EPOCH=1791590400`, the copied chapters/generated tables/excerpts and packaged publication style, and no Lean runtime. It writes `Paper_IX_Lean_Guide_Final.pdf` here and build logs under `qa/`. `preamble.tex` uses the P052, DejaVu and Latin Modern fonts recorded in the build. Do not substitute pdfLaTeX for XeLaTeX. See the root `FONT_DEPENDENCIES.txt` for the external font requirements and tested selectors.
18
19 ## Repeat the static evidence review
20
21 From this directory in the final package:
22
23 ```sh
24 python3 audit_sources.py \
25 --source ../../preserved/PRSC_IX_Consolidated_Manuscript \
26 --output audit/a_new_static_run
27 python3 verify_guide.py \
28 --source ../../preserved/PRSC_IX_Consolidated_Manuscript
29 ```
30
31 The catalog source paths are relative to that preserved root. A path containing `!` identifies an exact ZIP member. The 0.11.0 Nishibuchi completion sources are preserved within the baseline ZIP; later width-four all-row/period/isometry endpoints are under `strengthening/formalization`.
32
33 The fresh static reconciliation in `audit/current_reconciliation/` matched 15 inherited frontiers, 644 source hashes, 713 recorded log hashes, all 202 source links, the catalog, and 515 exact strict axiom records at the latest polynomial frontier. The unchanged Python declaration/axiom parser regression was rerun. Twelve retained negative-control logs retain matching recorded rejection diagnostics. Four older affine logs lack a digest in their original report and retain that limit. Historical compiler evidence and old document QA are retained separately; old document hashes and counts do not describe this revised PDF.
34
35 No Lean or Lake executable is present and neither was executed for this guide. Historical compilation records use Lean 4.34.0-rc2 and pinned Mathlib revision `aeb72f1e9981b6d35b426b16dca7759be3e7ba06`. The new paper's proof audits and bounded exact computations do not count as new kernel compilation. This release adds no `.lean` proof files and no placeholder theorems for the new results.
36
37 The raw `.lean.txt` excerpt assets retain their original source characters. Display `.render.txt` assets only adapt verbatim escaping and otherwise unsupported glyphs; the raw Lean proof files are unchanged. `audit/EXCERPTS.json` records original locators, hashes and ranges. The complete guide verifier checks all 47 excerpt identities, their unique teaching uses, catalog identifiers present in the PDF, embedded fonts, cross-references and layout warnings.
38
39 The current chapter does not close unrestricted native presentation invariance, completed/global compatibility, singular persistence, or a universal exact higher-order law for addresses two and three. Previously proved and still open arithmetic subfamilies are separated in the main paper's final theorem register.