Paper IX: Arithmetic Packets, Dyadic Towers, and Local Polynomial Deformation

Download original file

This is the original TeX manuscript source. Use the paper’s PDF for typeset equations.

Read the typeset paper

Read this chapter with formatted equations

1 \section{Formal evidence and reproduction}
2 \label{sec:verification}
3 
4 The verification record supports the manuscript in several ways. The Lean source states the quantified theorem and its hypotheses. A
5 compiler report records acceptance of that source by a specified Lean and
6 Mathlib environment. An axiom audit identifies the axioms used by the resulting
7 named declarations. Statement contracts and mathematical controls check
8 selected interfaces and boundary cases. Finally, source correspondence reviews
9 compare the formal objects with the intended mathematical statement. Each check has a specific role: numerical examples test particular cases,
10 whereas a universal claim requires a proof, and correspondence with an
11 external conjecture requires a comparison of the statements.
12 
13 This edition revises the exposition and checks the evidence index against
14 the preserved sources. The Lean sources are unchanged. Their compiler
15 acceptance is supported by the earlier successful reports, whose source and
16 log hashes are checked by the accompanying index. The most recent compilation
17 covers local analytic regularity and its polynomial dependencies; earlier
18 reports cover the arithmetic and native obstruction developments.
19 
20 The proofreading pass also restores several results omitted from the first
21 consolidation and records the comparison with the original paper. Its
22 coverage matrix and semantic review appear in
23 \texttt{consolidation/editorial/}. The Bernoulli boundary is accompanied by
24 a classical derivation, without a claim of a dedicated Lean certificate.
25 The reviews distinguish this addition from restored results already present
26 in the checked sources.
27 
28 \subsection{Verification frontiers}
29 
30 Table~\ref{tab:verification-frontiers} gives the recorded scope of each major
31 verification frontier. An \emph{inventoried module} is a source file in that
32 frontier's formalization list. Older lists sometimes include files of examples
33 or positive controls in this group. A \emph{check} is an entry in the report's
34 run list, including expected rejection of invalid claims. An \emph{axiom
35 closure} is the recorded axiom dependency set of an explicitly named
36 declaration; definitions and abbreviations contribute to this count as well
37 as theorems. None of these columns is a count of distinct mathematical results
38 across the paper.
39 
40 \begin{table}[htbp]
41 \centering
42 \small
43 \begin{tabular}{@{}lrrr@{}}
44 \toprule
45 Preserved frontier & Modules & Checks & Axiom closures\\
46 \midrule
47 Original completion baseline & 79 & $79+37+3$ & 1000\\
48 Dyadic strengthening and isometry & 22 & 38 & 246\\
49 Standalone finite affine obstruction & 2 & 4 & 17\\
50 Shared correction quotient & 6 & 13 & 60\\
51 Polynomial one-step lifting & 9 & 18 & 91\\
52 Exact polynomial lift counts & 9 & 17 & 106\\
53 Smooth infinite towers & 14 & 22 & 127\\
54 Coefficient deformation & 17 & 26 & 159\\
55 Continuous parameter charts & 25 & 40 & 244\\
56 Weighted lifting & 30 & 50 & 304\\
57 First-order root motion & 35 & 58 & 326\\
58 Prescribed parameter obstruction & 39 & 65 & 375\\
59 Prescribed parameter towers & 45 & 74 & 408\\
60 Joint coefficient and parameter motion & 49 & 82 & 460\\
61 Local analytic regularity & 55 & 91 & 515\\
62 \bottomrule
63 \end{tabular}
64 \caption{Recorded verification scopes. Rows overlap extensively through
65 inherited sources and must not be added. The baseline separates 79 module
66 checks, 37 control checks, and three additional recorded runs; its nine
67 dependency revision comparisons are recorded separately.}
68 \label{tab:verification-frontiers}
69 \end{table}
70 
71 The baseline inventory contains 836 theorem commands, 162 definitions and two
72 abbreviations, matching its 1000 audited names. The latest polynomial inventory
73 contains 322 theorem commands, 76 definitions and seven abbreviations in its
74 55 formalization modules. Its eight positive-control support modules and
75 13 statement-contract modules bring the full audit to 415 theorem commands,
76 92 definitions and eight abbreviations, hence 515 closures. The 91 checks also
77 include 12 negative controls. Six new regularity modules contribute 30 theorem
78 commands and eight definitions; all 49 inherited formalization modules are
79 unchanged in that release.
80 
81 The arithmetic strengthening inventory exposes a small historical metadata
82 error. Its summary fields say 179 theorems and 12 definitions, while its
83 module entries list 215 theorem commands, ten lemma commands,
84 20 definitions and one abbreviation. These 246 named entries exactly match
85 the preserved axiom audit. The consolidation uses the entries and audit, and
86 records the stale summary fields explicitly. The original inventory remains
87 unchanged as historical evidence. This is a correction to the reporting
88 metadata, not a newly discovered proof or a modification of a checked theorem.
89 
90 \subsection{Claim-to-source correspondence}
91 
92 The source references attached to the mathematical sections identify the
93 principal declarations for each result. Their complete names, exact source
94 hashes, roles and verification frontiers are collected in
95 \texttt{consolidation/audit/DECLARATIONS.csv}. The accompanying
96 \nolinkurl{consolidation/audit/EVIDENCE_INDEX.json} records the corresponding inventories,
97 reports and retained logs. In particular, the following interfaces distinguish
98 the principal completed results from generic auxiliary lemmas:
99 \begin{itemize}
100 \item The external conjecture is assembled by
101 \lean{NishibuchiCompletion.conjecture_3_9} in the original completion
102 baseline. Its coefficient identification, integrality, parameter split and
103 explicit threshold are part of that proof chain.
104 \item Exact $N=4$ packet periods are supplied by
105 \lean{DyadicFourLeastPeriods.least_packet_period}; the isometric extension
106 is supplied by \lean{DyadicFourIsometry.existsUnique_isometry}. The
107 normalization of the original coefficients is an explicit part of these
108 interfaces.
109 \item The classical sharp edge tower is supplied by
110 \lean{DyadicSharpTower.dyadic_supercongruence_sharp}, together with its
111 first omitted error valuation. Its optimality concerns the stated uniform
112 truncation bound.
113 \item Prescribed parameter lifting uses the actual residual and actual
114 partial Jacobians in
115 \lean{PolynomialPrescribedObstruction.prescribed_lift_iff_obstruction_zero}.
116 The quotient criterion and exact lift counts are not assumptions of the
117 later tower results.
118 \item Joint deformation is supplied by
119 \lean{PolynomialJointDeformation.exists_unique_joint_deformation}.
120 Local regularity is supplied by
121 \lean{PolynomialAnalyticImplicit.exists_analytic_implicit}, with the
122 actual polynomial derivative and the derivative formula $-J^{-1}K$.
123 \item \lean{PolynomialAnalyticSelection.continuous_selection_regularity}
124 transfers the analytic germ and strict derivative to any continuous local
125 root selection satisfying the stated root and base-point conditions.
126 \end{itemize}
127 Here arithmetic declaration names have namespace prefix
128 \texttt{KomorebiPaperIX.}; polynomial and native declarations have prefix
129 \texttt{Komorebi.}. The section maps and CSV retain the full names.
130 
131 The declaration index covers every explicitly named theorem, lemma,
132 definition and abbreviation in the 14 release-frontier inventories, together
133 with the earlier standalone affine report. Byte-identical copies of a source
134 file are collapsed, while all their locations remain recorded. If the same
135 qualified name occurs in different source versions, the versions remain
136 separate and are marked. Anonymous examples, compiler-generated declarations,
137 failed development attempts, and the contents of earlier nested historical
138 snapshots are not counted as named results in this index. Negative-control
139 source files are checked for integrity but are not recorded as proved
140 mathematical assertions. Consequently, the number of CSV rows must not be
141 quoted as a global unique theorem count.
142 
143 \subsection{External statement and library dependencies}
144 
145 The original conjecture correspondence was reviewed against Nishibuchi's
146 arXiv version \texttt{2605.10677v2}, dated 1 June 2026. The retained source
147 record identifies the official version, the full title, the PDF checksum and
148 the extracted-text checksum. The detailed review compares Definition~2.1,
149 Notation~3.2 and Conjecture~3.9 with the actual reciprocal EGF coefficients,
150 the factor $j!$, the residue range, the degree displacement, and the threshold
151 in the formal capstone. Nishibuchi's conjecture is the conclusion to be
152 proved; it is not an axiom imported into Lean.
153 
154 The full external paper is not redistributed in this source release.
155 Consolidation preserves the earlier source correspondence audit and its
156 version record. The earlier consolidation recorded a blocked request to the official arXiv endpoints.
157 For the preserved prior edition, the official unversioned PDF was inspected;
158 its internal version is v2, dated 1 June 2026. Definition 2.1 and Remark 2.3
159 (printed page 3), Notation 3.2 (page 5), and Conjecture 3.9 (page 8)
160 confirm the parameter, index, degree-displacement and normalization match.
161 Some direct versioned-endpoint requests were blocked in that earlier check. The later strengthening source review reached the primary PDF and HTML through the official record and confirmed the same v2 statement. These are dated source-access records, not mathematical hypotheses.
162 This source check is distinct from the inherited compiler acceptance.
163 No broad literature or priority claim is made.
164 
165 The mathematical environment is Lean \texttt{4.34.0-rc2}, with Mathlib revision
166 \nolinkurl{aeb72f1e9981b6d35b426b16dca7759be3e7ba06}.
167 The allowed axiom dependencies are
168 \texttt{propext}, \texttt{Classical.choice} and \texttt{Quot.sound}.
169 The reports do not describe a rebuild of Mathlib from source. The local
170 regularity audit separately records the applicable Mathlib analytic inverse
171 and strict derivative interfaces and their hypotheses. In particular, the
172 field-valued analysis is performed over a complete nontrivially normed field;
173 its integral specialization embeds the data into $\Qp$. It does not use
174 $\Zp$ as a vector space over $\Qp$.
175 
176 \subsection{Reproduction and limits of the consolidation check}
177 
178 The archive contains the mathematical sources, verifier scripts, controls,
179 contracts, prior logs and exact inventories. The pinned Lean and Mathlib kit
180 is supplied separately. From the consolidated archive root, the latest
181 polynomial gate can be reproduced with a new output directory:
182 \begin{verbatim}
183 python3 replay_paper9_regularity.py \
184   --kit /absolute/path/to/pinned-kit \
185   --output /absolute/path/to/new-polynomial-run
186 \end{verbatim}
187 The preserved arithmetic, native and shared-correction chain has a separate
188 entry point:
189 \begin{verbatim}
190 python3 replay_shared_correction.py --all \
191   --kit /absolute/path/to/pinned-kit \
192   --output /absolute/path/to/new-arithmetic-run
193 \end{verbatim}
194 These commands reproduce the recorded checks; they were not rerun during
195 manuscript consolidation or proofreading. The second command rebuilds
196 the preserved baseline before the arithmetic continuation. Each output path
197 must be new. The reports retain the original full commands, runtime
198 fingerprints and output hashes. The executable-path compatibility adapter
199 used in the recorded environment restores runtime path discovery; it does
200 not alter Lean's mathematical kernel or the source statements.
201 
202 For the narrower evidence reconciliation carried out for this edition, use
203 \begin{verbatim}
204 python3 consolidation/tools/evidence_index.py \
205   --source . --output /absolute/path/to/new-evidence-index
206 \end{verbatim}
207 This check compared 644 source-file occurrences with their recorded hashes
208 and 713 retained log occurrences with their recorded hashes. Four additional
209 logs from the older standalone affine report were fingerprinted, but that
210 legacy report does not contain prior log hashes; those four are not promoted
211 to hash comparisons. Every named declaration in the selected inventories
212 matches the appropriate recorded standard-axiom dependency set. These are
213 integrity and provenance checks, not another Lean compilation.
214 
215 Expected negative-control failures are retained as evidence that specific
216 invalid strengthenings are rejected. Examples include an unjustified extra
217 precision digit, omitted parameter terms, a wrong derivative sign, and
218 uniqueness without the appropriate hypotheses. Development failures and
219 interrupted runs remain historical records; only the successful designated
220 release reports support the verification table. Only accepted declarations in the designated successful reports support
221 claims of formal verification.
222 
223 Finally, the proof of the original stated conjecture does not resolve every
224 extension mentioned in this manuscript. The open questions concerning
225 rationally rank-deficient singular points, presentation invariance, global
226 or completed descent, and further exact arithmetic have no certificate
227 supplied by these counts. Section~\ref{sec:open} states the remaining implications explicitly.
228 
229 \subsection{Inherited checks for the prior final edition}
230 The preserved prior final-edition review reconstructed the arguments in its 54 written
231 proof blocks under their stated hypotheses. The two expanded paragraphs
232 in the all-address proof make the inverse-flatness commutator and the
233 coefficient-extraction saturation explicit. The recovered historical text
234 received five local repairs: integral observation vectors for matrix
235 congruences, positive precision for matrix amplification, integral Mahler
236 coefficients for the sparsification consequence, the corrected modulo-seven
237 example, and the even-subsequence range for source changes. Its remaining
238 historical and external-source evidence limits are retained in
239 Appendix~\ref{app:recovered}; preservation of its 82 proof bodies is not
240 a blanket formal certificate.
241 
242 An independent Python gate using arbitrary-precision integers and
243 \texttt{fractions.Fraction} passed 116,492 deterministic assertions in nine
244 finite families: packet construction, foundational identities, divisor-branch
245 congruences, four-packet sharpness, classical truncations, polynomial digit
246 fibers, shared affine quotients, finite towers and charts, and weighted
247 deformation. Nineteen invalid strengthenings were rejected by concrete
248 controls. The exact ranges, coefficient domains, scripts and output hashes
249 are in the accompanying \nolinkurl{verification/computation} manifests.
250 These finite tests do not establish a universal theorem.
251 
252 The unchanged early-row script separately reproduced 312 finite period
253 cases and its odd-prime row-zero boundary control. Other research-script
254 replays, unchanged baseline regression gates and recovered-text controls
255 are recorded separately in the same audit directory; their totals are
256 not added to the independent gate. Lean and Lake were unavailable in this
257 execution environment. No fresh compiler run, infinite $p$-adic computation,
258 analytic-continuation computation or hardware benchmark is asserted.
259 
260 
261 \subsection{Checks for the strengthened Euler edition}
262 The new proof routes are recorded in the threshold-free strengthening checkpoint, whose manifest pins 52 files. Its six principal proof audits are internal computational-assistant reviews and identify the exact proof revisions they checked. The manuscript delta review compares the new chapters and current scope statements with those proofs. It does not replace the earlier Lean kernel or constitute external peer review.
263 
264 The dedicated arithmetic experiment computed the four reciprocal rows through index 512 modulo $2^{4096}$, with independent exact-rational inversion through index 16. It checked 525,312 first differences, 1,141,424 repeated-step factorial bounds, 139,000 mixed-step bounds, and 2,048 Newton coefficients. The supplemental experiments cover additional mixed-step and sharpness cases and retain their separate tested ranges. Their outputs and source hashes are preserved under \nolinkurl{preserved/threshold_free/computation}. All these are bounded implementation checks; the written arguments establish the universal claims.
265 
266 The visual guide has its own exact computation contract and figure manifest. Its modular recurrence is compared with independent rational inversion, and each theorem-derived plot is marked as such. The fresh static Lean review reconciles the unchanged formal sources and inherited compiler logs, with counts stated in the Lean guide. No Lean or Lake executable was available for this release, and no new compiler acceptance is asserted for the new proof routes.
267 
268 The release includes the editable three-document sources, exact figure generator, the strengthened proof checkpoint, unchanged earlier source packages, and manifests for the final outputs. PDF compilation, figure arithmetic, manifest validation, source reconciliation, and written proof auditing are separate checks with separate scopes.

Back to source controls

Back to Paper IX: Arithmetic Packets, Dyadic Towers, and Local Polynomial Deformation