Realization Calculus

Download original file

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

Read the typeset paper

1 \section{Scope and conventions}
2 \label{sec:scope}
3 The central objects are sequences and polynomial equations equipped with
4 arithmetic coordinates. Residue projectors select addresses in a sequence,
5 finite differences measure compatibility between nearby addresses, and
6 valuation bounds control the passage from finite precision to a $p$-adic
7 limit. These constructions provide a common language for the Euler packet
8 results and the later lifting results. Each theorem nevertheless retains its
9 own coefficient ring, topology and nonsingularity hypotheses.
10 
11 The arithmetic framework is developed together with its completed
12 extensions. The stated external Nishibuchi conjecture is proved in its full
13 specified parameter range. The dyadic refinements and polynomial deformation theorems give stronger
14 conclusions under the hypotheses stated with each result. The native conjectures retain their original
15 identifiers, 13.2 and 13.3, when discussed as research questions, although the
16 section numbering of this consolidated manuscript is new.
17 
18 Throughout, $\N=\{0,1,2,\ldots\}$. When $p$ is prime, $\Zp$ denotes the
19 $p$-adic integers and $\Qp$ their fraction field. We normalize $v_p(p)=1$.
20 For a rational or $p$-adic quantity, a displayed lower valuation bound is
21 understood with the mathematical convention $v_p(0)=+\infty$.
22 The corresponding formal predicates are zero-safe: the quantity is zero or
23 its valuation meets the stated bound. An exact finite valuation assertion
24 requires a nonzero quantity, and this is stated where used. Congruence in
25 $\Zp$ means ideal divisibility. Thus
26 \[
27  x\equiv y\pmod{p^r}\quad\Longleftrightarrow\quad
28  x-y\in p^r\Zp.
29 \]
30 For vectors, ideal membership and congruence are coordinatewise.
31 
32 Write $\Delta_u f(n)=f(n+u)-f(n)$ and use $\Delta_u^k$ for its $k$-fold
33 iterate. Euler coefficients indexed by ordinary degree and by packet row are
34 distinguished explicitly. A packet displacement by $u$ rows is a degree
35 displacement by $Nu$ in a packet of width $N$.
36 
37 The main text presents theorem statements and their arguments. Accompanying
38 source maps identify the Lean declarations and archived files that support
39 them. The formal companion identifies the scope of each recorded build. The
40 91-check polynomial record covers the polynomial development. Separate
41 records support the arithmetic results.
42 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
43 used in Section~\ref{sec:regularity} come from Mathlib.

Back to source controls

Back to Realization Calculus