Realization Calculus

Download original file

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

Included manuscript sections

• edition_summary.tex
• historical_references.tex
• 00_scope.tex
• 10_foundations.tex
• 20_arithmetic.tex
• 30_lifting.tex
• 40_regularity.tex
• 50_open_questions.tex
• 60_verification.tex
• 70_continuation.tex
• 71_native.tex
• 72_recovered.tex
• 73_supplements.tex
• root_scope.tex
• strengthening.tex
• worked_atlas.tex

Read the typeset paper

1 \documentclass[11pt]{article}
2 \usepackage[a4paper,margin=27mm,headheight=15pt]{geometry}
3 \usepackage[T1]{fontenc}
4 \usepackage[utf8]{inputenc}
5 \usepackage{lmodern,microtype,bm,graphicx}
6 \usepackage{amsmath,amssymb,amsthm,mathtools,mathrsfs}
7 \usepackage{booktabs,array,longtable,tabularx,enumitem}
8 \usepackage{xcolor,fancyhdr,xurl,hyperref}
9 \definecolor{paperink}{HTML}{185B58}
10 \hypersetup{colorlinks=true,linkcolor=paperink,citecolor=paperink,urlcolor=paperink,
11   pdftitle={Euler Congruences: Completion, Factorial Strengthening and Sharp Dyadic Geometry},
12   pdfauthor={Komorebi P.},pdfsubject={Generalized Euler congruences, factorial precision, sharp dyadic periods, formal coverage and remaining tail simplicity}}
13 \newcommand{\N}{\mathbb N}
14 \newcommand{\Z}{\mathbb Z}
15 \newcommand{\Q}{\mathbb Q}
16 \newcommand{\F}{\mathbb F}
17 \newcommand{\Zp}{\mathbb Z_p}
18 \newcommand{\Qp}{\mathbb Q_p}
19 \DeclareMathOperator{\coker}{coker}
20 \DeclareMathOperator{\im}{im}
21 \DeclareMathOperator{\rank}{rank}
22 \newcommand{\lean}[1]{{\footnotesize\nolinkurl{#1}}}
23 \newtheorem{theorem}{Theorem}[section]
24 \newtheorem{proposition}[theorem]{Proposition}
25 \newtheorem{lemma}[theorem]{Lemma}
26 \newtheorem{corollary}[theorem]{Corollary}
27 \theoremstyle{definition}
28 \newtheorem{definition}[theorem]{Definition}
29 \newtheorem{example}[theorem]{Example}
30 \theoremstyle{remark}
31 \newtheorem{remark}[theorem]{Remark}
32 \numberwithin{equation}{section}
33 \setlength{\parskip}{3pt}
34 \setlength{\emergencystretch}{2em}
35 \setlist{itemsep=2pt,topsep=5pt}
36 \allowdisplaybreaks[1]
37 \pagestyle{fancy}
38 \fancyhf{}
39 \fancyhead[L]{\small\scshape Euler congruences / Chapter IX}
40 \fancyhead[R]{\small\scshape Final strengthened edition}
41 \fancyfoot[L]{\small Komorebi P.}
42 \fancyfoot[R]{\thepage}
43 
44 \title{\textbf{Euler Congruences}\\[5pt]
45   \Large Completion, Factorial Strengthening,\\ and Sharp Dyadic Geometry\\[7pt]
46   \large Projector-Resolved Seed Calculus IX}
47 \author{Komorebi P.}
48 \date{}
49 
50 \usepackage[nameinlink,noabbrev]{cleveref}
51 
52 \providecommand{\tightlist}{\setlength{\itemsep}{0pt}\setlength{\parskip}{0pt}}
53 \providecommand{\passthrough}[1]{#1}
54 \newcommand{\mcode}[1]{\ifmmode\text{\nolinkurl{#1}}\else\nolinkurl{#1}\fi}
55 \definecolor{ink}{HTML}{185B58}
56 \newcommand{\ZZ}{\mathbb Z}\newcommand{\QQ}{\mathbb Q}\newcommand{\FF}{\mathbb F}\newcommand{\NN}{\mathbb N}
57 \newcommand{\Wp}{\mathcal W_p}\newcommand{\Hp}{\mathcal H(\Z_p)}
58 \newcommand{\ordp}{\operatorname{ord}_p}\newcommand{\ord}{\operatorname{ord}}
59 \newcommand{\coef}[2]{[#1^{#2}]}\newcommand{\target}[1]{{\footnotesize\nolinkurl{#1}}}
60 \newcommand{\pageheading}[2]{{\large\bfseries\color{ink}#1}\par{\small #2}\par\medskip}
61 \newcommand{\sech}{\operatorname{sech}}\newcommand{\fall}[2]{(#1)_{#2}}
62 \newcommand{\EE}{\mathcal E}\newcommand{\PP}{\mathcal P}\newcommand{\code}[1]{{\small\nolinkurl{#1}}}
63 \newcommand{\Hcal}{\mathcal H}\newcommand{\Ecal}{\mathcal E}\newcommand{\Ccal}{\mathcal C}\newcommand{\Pcal}{\mathcal P}\newcommand{\Scal}{\mathcal S}\newcommand{\Ocal}{\mathcal O}\newcommand{\Rcal}{\mathcal R}\newcommand{\Vcal}{\mathcal V}\newcommand{\Wcal}{\mathcal W}
64 \newcommand{\End}{\operatorname{End}}\newcommand{\Ker}{\operatorname{Ker}}\newcommand{\Res}{\operatorname{Res}}\newcommand{\vp}{v_p}\newcommand{\vTwo}{v_2}\newcommand{\sTwo}{s_2}\newcommand{\DeltaH}{\Delta_h}\newcommand{\abs}[1]{\left\lvert#1\right\rvert}\newcommand{\norm}[1]{\left\lVert#1\right\rVert}\newcommand{\one}{\bm 1}\newcommand{\starh}{\mathbin{\star}}\newcommand{\e}{\mathrm e}
65 \newtheorem{histtheorem}[theorem]{Historical theorem}
66 \crefname{histtheorem}{historical theorem}{historical theorems}
67 \newtheorem{histproposition}[theorem]{Historical proposition}
68 \crefname{histproposition}{historical proposition}{historical propositions}
69 \newtheorem{histlemma}[theorem]{Historical lemma}
70 \crefname{histlemma}{historical lemma}{historical lemmas}
71 \newtheorem{histcorollary}[theorem]{Historical corollary}
72 \crefname{histcorollary}{historical corollary}{historical corollaries}
73 \newtheorem{histdefinition}[theorem]{Historical definition}
74 \crefname{histdefinition}{historical definition}{historical definitions}
75 \newtheorem{histexample}[theorem]{Historical example}
76 \crefname{histexample}{historical example}{historical examples}
77 \newtheorem{histremark}[theorem]{Historical remark}
78 \crefname{histremark}{historical remark}{historical remarks}
79 \newtheorem{histstandardfact}[theorem]{Historical standard fact}
80 \crefname{histstandardfact}{historical standardfact}{historical standardfacts}
81 
82 
83 % Operation Komorebi: shared publication profile.
84 \usepackage{komorebi-publication}
85 \renewcommand{\KomorebiTitle}{Euler Congruences}
86 \renewcommand{\KomorebiSubtitle}{Completion, factorial strengthening, and sharp dyadic geometry}
87 \renewcommand{\KomorebiSeries}{Chapter IX}
88 \renewcommand{\KomorebiKind}{Mathematical text}
89 \renewcommand{\KomorebiEdition}{}
90 \renewcommand{\KomorebiShortTitle}{Chapter IX}
91 \renewcommand{\KomorebiTitleSize}{38}
92 \renewcommand{\KomorebiTitleLeading}{43}
93 \renewcommand{\KomorebiProfile}{classical}
94 \renewcommand{\KomorebiOrientation}{portrait}
95 \KomorebiSetup
96 \begin{document}
97 \KomorebiCover
98 
99 \relax
100 \begin{abstract}
101 We prove Nishibuchi's generalized Euler congruence conjecture in its full stated parameter range and develop sharper arithmetic consequences. For every prime-power packet width, a charged Hurwitz differential operator transfers integral difference estimates through the reciprocal generating series. In the dyadic case this gives mixed finite-difference bounds at every row, without a starting threshold. For the four addresses of width four, a divided-power argument adds the factorial gain $v_2(k!)$, determines every repeated-step valuation in addresses zero and one, and gives a stronger address-two estimate with exact values at all power-of-two orders. The corresponding first differences yield least periods and bijective isometric continuations onto explicit dyadic residue classes. We also determine exact Taylor radii for three addresses. The manuscript retains the complete earlier arithmetic, lifting, deformation, and analytic-regularity development, with detailed mathematical appendices. A separate appendix states the precise remaining simplicity problem for ordinary Euler tails. Formal coverage is explicit: the external conjecture and several four-address results have inherited Lean verification. The new factorial, mixed-step, all-rank, and radius arguments are written proofs with recorded audits and exact computational checks, and await dedicated Lean formalization.
102 \end{abstract}
103 \input{../edition_summary.tex}
104 
105 
106 \input{parts/00_scope}
107 \clearpage
108 {\small\setlength{\parskip}{0pt}\tableofcontents}
109 \clearpage
110 \input{parts/10_foundations}
111 \input{parts/20_arithmetic}
112 \clearpage
113 \input{../strengthening.tex}
114 \clearpage
115 \input{parts/30_lifting}
116 \input{parts/40_regularity}
117 \input{parts/50_open_questions}
118 \input{parts/60_verification}
119 
120 \clearpage
121 \appendix
122 \input{../root_scope.tex}
123 \input{parts/70_continuation}
124 \input{parts/71_native}
125 \input{parts/72_recovered}
126 \input{parts/73_supplements}
127 \clearpage\def\IXMainAtlas{1}\def\AtlasFigDir{../../figures/worked}\input{../worked_atlas.tex}\clearpage
128 \begin{thebibliography}{99}
129 \bibitem{Nishibuchi}
130 Yuta Nishibuchi,
131 \emph{$p$-adic Congruences of Generalized Euler Numbers and Relations to Even
132 Zeta Values}, arXiv:2605.10677v2, 1 June 2026.
133 \url{https://arxiv.org/abs/2605.10677v2}.
134 The comparison to Conjecture 3.9 uses the source review and fixed-version
135 record preserved with this edition.
136 
137 \bibitem{gessel}
138 Ira M. Gessel, \emph{Applications of the classical umbral calculus},
139 arXiv:math/0108121v3, 22 November 2001, Section 9, in particular the Frobenius Euler congruence and the derivation following Theorem 9.2.
140 \url{https://arxiv.org/abs/math/0108121}.
141 The normalization and quantifiers of the ordinary Euler input were checked against the primary PDF in the strengthening checkpoint.
142 
143 \bibitem{DLMF24}
144 NIST Digital Library of Mathematical Functions, \S24.10(i),
145 Eq.\ 24.10.1 (Bernoulli denominator theorem).
146 \url{https://dlmf.nist.gov/24.10.E1}. The official primary entry was inspected
147 for the positive even-index denominator specialization in this edition.
148 
149 \bibitem{Mathlib}
150 The Mathlib Community,
151 \emph{Mathlib}, source revision
152 \nolinkurl{aeb72f1e9981b6d35b426b16dca7759be3e7ba06},
153 used with Lean 4.34.0-rc2.
154 In particular, the polynomial, strict inverse-function and analytic
155 inverse-function developments cited in Section~\ref{sec:regularity}.
156 The exact local source paths and dependency records accompany the release.
157 
158 \bibitem{PaperIXArchive}
159 Komorebi P.,
160 \emph{Projector-Resolved Seed Calculus IX: original manuscript, formal
161 supplements and cumulative continuation sources}, preserved source collection,
162 consolidated 8 September 2026.
163 The original 28-page status-corrected manuscript and all subsequent release
164 records remain in the accompanying archive.
165 
166 \medskip\noindent\textbf{Recovered historical references.}
167 The bibliography underlying Appendix~\ref{app:recovered} has been recovered
168 from the original source package. Its 22 citation keys are retained below,
169 with bibliographic identities checked against publisher and author records.
170 This repairs the source attributions. It does not enlarge the historical
171 chapter's stated proof or formalization scope.
172 \input{historical_references.tex}
173 \end{thebibliography}
174 \end{document}

Back to source controls

Back to Realization Calculus