Scope and conventions

The central objects are sequences and polynomial equations equipped with arithmetic coordinates. Residue projectors select addresses in a sequence, finite differences measure compatibility between nearby addresses, and valuation bounds control the passage from finite precision to a \(p\)-adic limit. These constructions provide a common language for the Euler packet results and the later lifting results. Each theorem nevertheless retains its own coefficient ring, topology, and nonsingularity hypotheses.

This edition integrates the original arithmetic framework with the completed extensions. The stated external Nishibuchi conjecture is proved in its full specified parameter range. The dyadic refinements and polynomial deformation theorems give stronger conclusions under the hypotheses stated with each result. The native conjectures retain their original identifiers, 13.2 and 13.3, when discussed as research questions, although the section numbering of this consolidated manuscript is new.

Throughout, \({\mathbb N}=\{0,1,2,\ldots\}\). When \(p\) is prime, \({\mathbb Z_p}\) denotes the \(p\)-adic integers and \({\mathbb Q_p}\) their fraction field. We normalize \(v_p(p)=1\). For a rational or \(p\)-adic quantity, a displayed lower valuation bound is understood with the mathematical convention \(v_p(0)=+\infty\). The corresponding formal predicates are zero-safe: the quantity is zero or its valuation meets the stated bound. An exact finite valuation assertion requires a nonzero quantity, and this is stated where used. Congruence in \({\mathbb Z_p}\) means ideal divisibility. Thus

For vectors, ideal membership and congruence are coordinatewise.

Write \(\Delta_u f(n)=f(n+u)-f(n)\) and use \(\Delta_u^k\) for its \(k\)-fold iterate. Euler coefficients indexed by ordinary degree and by packet row are distinguished explicitly. A packet displacement by \(u\) rows is a degree displacement by \(Nu\) in a packet of width \(N\).

The main text presents theorem statements and their arguments; accompanying source maps identify the Lean declarations and archived files that support them. The verification record keeps the original dates and scope of each build. In particular, the latest 91-check polynomial build covers the polynomial development, while earlier builds support the arithmetic results. The inherited formal development is retained without adding Lean declarations. The strengthening chapters add written proofs and clearly mark their formalization boundary; no historical-priority claim is made. The analytic inverse-function results used in Section 11 come from Mathlib.

Permalink · Source line 3