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 \clearpage\subsection{Singular Amice Supplement}\label{app:sup9}
2 \noindent\textbf{Checkpoint scope.} This complete source body retains the status of its dated original supplement. Earlier pending or partial-coverage labels are historical; the final core records their resolution.\par\medskip
3 \subsubsection*{Scope and result}
4 Let $p$ be prime, let $m\mid p-1$, and put $N=mp$. For $1\le a<m$, put $c=ap$ and define the original exponential section and ratio by
5 \[
6  H_{N,c}(t)=\sum_{n\ge0}\frac{t^{Nn+c}}{(Nn+c)!},\qquad
7  R_c(t)=\frac{tH_{N,c-1}(t)}{H_{N,c}(t)}.
8 \]
9 The quotient is interpreted after removing its forced zero. This block proves, for the actual rational coefficients $\alpha_d$,
10 \[
11  R_{ap}(\log(1+T))=\sum_{d\ge0}\alpha_dT^d,
12  \qquad
13  \boxed{\alpha_d=0\ \text{or}\ v_p(\alpha_d)\ge-\left\lfloor d/p\right\rfloor.}
14 \]
15 Equivalently, every $p^{\lfloor d/p\rfloor}\alpha_d$ belongs to the actual completed ring $\Z_p$. The zero-safe alternative is explicit in the formal rational statement.
16 
17 This is the weighted estimate of Proposition 4.7 in the supporting argument. It is \textbf{not yet the singular higher finite-difference theorem}. The full all-residue Paper IX Theorem 7.5 remains pending, and full manuscript coverage stays at \textbf{23 of 24}.
18 
19 \begin{center}\begin{tabular}{lrr}\toprule
20 Inventory & v0.8.0 & This release\\\midrule
21 Proof modules &47&57\\
22 Explicit theorem declarations &526&630\\
23 Explicit definitions audited separately &107&128\\
24 Fully covered manuscript items &23/24&23/24\\\bottomrule
25 \end{tabular}\end{center}
26 The 104 added declarations include 30 declarations in four previously compiled research modules, now included in the cumulative audit, and 74 declarations in six new modules. They include supporting lemmas and examples, not independent discoveries. All 47 earlier checked proof modules are preserved byte for byte.
27 
28 \textbf{No hidden estimate.} The final weighted-ratio theorem assumes primality, the modulus divisibility and the specified residue bounds. It does not assume weighted section membership, reciprocal closure, the ratio identity, a Mahler pairing or the desired higher-difference bound. Pages 2--5 describe the constructed objects and proved bridges.
29 \par\medskip
30 \subsubsection*{1. Integral cyclic coefficients}
31 Work first in an arbitrary commutative ring $R$. If $z^p=1$, set
32 \[
33  I=(p,z-1),\qquad P=(p).
34 \]
35 Expanding $((z-1)+1)^p=1$ and using divisibility of every interior binomial coefficient in prime row $p$ gives
36 \[
37  (z-1)^p\in PI.
38 \]
39 Every other degree-$p$ product of the two generators of $I$ also belongs to $PI$. The formal ideal proof therefore establishes
40 \[
41  \boxed{I^p\subseteq PI.}
42 \]
43 For $q=p\lfloor q/p\rfloor+(q\bmod p)$, strong induction and the factorial valuation identity give
44 \[
45  \boxed{I^q\subseteq P^{v_p(q!)}}.
46 \]
47 In detail, write $b=\lfloor q/p\rfloor$. Then
48 \[
49  I^q\subseteq P^b I^b\subseteq P^{b+v_p(b!)}=P^{v_p(q!)}.
50 \]
51 No integral-domain hypothesis or division in a field is used here.
52 
53 Now take the integral cyclic group ring
54 \[
55  R_N=\Z[\Z/N\Z],\qquad x=[1],\qquad x^N=1,
56 \]
57 and assume $N\mid p(p-1)$. Thus $(x^{p-1})^p=1$. Each genuine consecutive block
58 \[
59  \prod_{i=0}^{p-1}\bigl(x-(pb+i)\bigr)
60 \]
61 belongs to $(p,x^{p-1}-1)$. This follows from the actual polynomial identity
62 \[
63  \prod_{i\in\F_p}(X-i)=X^p-X
64 \]
65 modulo $p$, not from a hypothesized valuation of the product.
66 
67 For the falling factorial $(x)_d=\prod_{i=0}^{d-1}(x-i)$, grouping into consecutive blocks gives
68 \[
69  (x)_d\in I^{\lfloor d/p\rfloor}
70  \subseteq\bigl(p^{v_p(\lfloor d/p\rfloor!)}\bigr).
71 \]
72 Every integral residue coordinate therefore satisfies
73 \[
74  \boxed{p^{v_p(\lfloor d/p\rfloor!)}\mid [(r)](x)_d\quad\text{in }\Z.}
75 \]
76 Dividing a coordinate by $d!$ is done only afterward, using
77 $v_p(d!)=\lfloor d/p\rfloor+v_p(\lfloor d/p\rfloor!)$. This establishes the weighted denominator estimate before any field-valued divisibility could make it vacuous.
78 
79 \textbf{Modules.} \mcode{CyclotomicFiltration}, \mcode{PrimeBlockPolynomial}, and \mcode{CyclicAmiceCoefficients}.
80 \par\medskip
81 \subsubsection*{2. Connection to the actual section}
82 An integral coordinate estimate becomes relevant only after connecting it to the manuscript's generating functions. For a residue $r\in\Z/N\Z$, define
83 \[
84  H_r(t)=\sum_{d\ge0}\mathbf1_{d\equiv r\ (N)}\frac{t^d}{d!},
85  \qquad F_r(T)=H_r(\log(1+T)).
86 \]
87 The implementation uses the actual formal logarithm and substitution in $\Q[[T]]$. It proves
88 \[
89  H_r'=H_{r-1},\qquad (1+T)F_r'=F_{r-1},
90 \]
91 and hence the coefficient recurrence
92 \[
93  (d+1)\coef{T}{d+1}F_r
94  =\coef{T}{d}F_{r-1}-d\coef{T}{d}F_r.
95 \]
96 The initial values are $F_r(0)=\mathbf1_{r=0}$.
97 
98 Independently, let $b_{d,r}$ be the residue-$r$ coordinate of $(x)_d$ in $R_N$. Actual group-ring multiplication gives
99 \[
100  b_{0,r}=\mathbf1_{r=0},\qquad
101  b_{d+1,r}=b_{d,r-1}-d\,b_{d,r}.
102 \]
103 Induction comparing these two recurrences proves
104 \[
105  \boxed{d!\coef{T}{d}H_r(\log(1+T))=b_{d,r}.}
106 \]
107 Thus the cyclic coefficient is not an unrelated stand-in for a section coefficient. For the canonical label $0\le c<N$, the formal section is also proved equal to the original \mcode{ExponentialSection.}\allowbreak\mcode{originalSection} used in the existing Euler project.
108 
109 \subsection*{Weighted membership}
110 The class used in the formalization is
111 \[
112  \Wp=\left\{F\in\Q_p[[T]]:
113  p^{\lfloor d/p\rfloor}\coef{T}{d}F\in\Z_p\ \text{for every }d\right\}.
114 \]
115 The integral-coordinate estimate from page 2 now proves
116 \[
117  \boxed{H_r(\log(1+T))\in\Wp}
118 \]
119 for every residue $r$, including the singular ones. Rational coefficients are mapped into $\Q_p$ by the actual coefficient ring homomorphism.
120 
121 The same source package retains the earlier independent formal identity
122 \[
123  d!\coef{T}{d}\exp(x\log(1+T))=(x)_d
124 \]
125 over a commutative $\Q$-algebra. The section bridge above does not rely on selecting or averaging roots in a cyclotomic extension.
126 
127 \textbf{Principal targets.}\par \mcode{factorial_coeff_section}; \mcode{section_weighted_integral};\par \mcode{weighted_section}.
128 \par\medskip
129 \subsubsection*{3. Weighted closure and the normalized denominator}
130 Let $w(d)=\lfloor d/p\rfloor$. Since $w(i)+w(d-i)\le w(d)$, the coefficient formula for a product proves closure of $\Wp$ under multiplication. Additive closure is immediate. For $U\in\Wp$ with $U(0)=1$, strong induction in the actual reciprocal coefficient recurrence proves
131 \[
132  \boxed{U^{-1}\in\Wp.}
133 \]
134 This inverse property is a theorem, not an additional field in a structure encoding weighted series.
135 
136 \subsection*{Differentiation and the Euler field}
137 The derivative coefficient is $(d+1)a_{d+1}$. If $p\nmid d+1$, the adjacent weights agree. If $p\mid d+1$, the integer factor $d+1$ compensates for the one-unit weight increase. Therefore ordinary differentiation preserves $\Wp$.
138 
139 For the actual logarithm, its coefficient denominator is $d$, and the proved inequality
140 \[
141  v_p(d)\le\lfloor d/p\rfloor\qquad(d>0)
142 \]
143 implies $\log(1+T)\in\Wp$. Consequently
144 \[
145  L_TF=\log(1+T)(1+T)F'
146 \]
147 also preserves $\Wp$.
148 
149 \subsection*{Removing a singular forced zero}
150 Put $c=ap<N$ and define the actual normalized kernel
151 \[
152  K_c(t)=c!\sum_{n\ge0}\frac{t^{Nn}}{(Nn+c)!},\qquad K_c(0)=1.
153 \]
154 Let $\ell(T)=\log(1+T)/T$, defined by shifting logarithm coefficients, not by inverting $T$. Set
155 \[
156  U(T)=\ell(T)^cK_c(\log(1+T)).
157 \]
158 The formal proof establishes $U(0)=1$ and the exact factorization
159 \[
160  H_{N,c}(\log(1+T))=\frac{T^c}{c!}U(T).
161 \]
162 It follows coefficientwise that
163 \[
164  \coef{T}{d}U=c!\coef{T}{d+c}H_{N,c}(\log(1+T)).
165 \]
166 Because $p^a\mid(ap)!$ and $\lfloor(d+ap)/p\rfloor=a+\lfloor d/p\rfloor$, the already proved section estimate gives $U\in\Wp$. Thus $U^{-1}\in\Wp$ as well. The factorial divisibility is derived from the pinned Legendre valuation theorem.
167 
168 \textbf{Boundary.} The original positive-address section has zero constant coefficient. It is not the series to which unit inverse closure is applied.
169 \par\medskip
170 \subsubsection*{4. The singular ratio estimate}
171 For a positive address $c$, the rational ratio is independently constructed from the original kernels:
172 \[
173  R_c(t)=c\,K_{c-1}(t)K_c(t)^{-1}.
174 \]
175 The scalar factor $c$ is necessary. The source proves the cleared identity
176 \[
177  \boxed{R_c(t)H_{N,c}(t)=tH_{N,c-1}(t).}
178 \]
179 This connects the constructed object to the original unnormalized ratio $A_{c-1}/A_c$. It does not assign the desired transformed formula as its definition.
180 
181 After actual logarithmic substitution and the chain rule,
182 \[
183  R_c(\log(1+T))H_{N,c}(\log(1+T))
184  =L_TH_{N,c}(\log(1+T)).
185 \]
186 Insert the proved factorization $H_{N,c}(\log(1+T))=T^cU/c!$. Leibniz differentiation and cancellation of that nonzero section give
187 \[
188  \boxed{R_c(\log(1+T))
189  =c(1+T)\ell(T)+(L_TU)U^{-1}.}
190 \]
191 All differentiation, substitution, nonzeroness and cancellation obligations are proved in the source.
192 
193 For $c=ap$, the second summand belongs to $\Wp$ by the closure results on page 4. The first does too: shifting the logarithm coefficient loses at most one unit of the floor weight, so $p\ell(T)\in\Wp$, and the integer $a$ supplies the remaining factor. Therefore
194 \[
195  \boxed{R_{ap}(\log(1+T))\in\Wp.}
196 \]
197 The final rational coefficient theorem states the bound with an explicit zero alternative. No finite-valued default valuation at zero is used as the meaning of unlimited precision.
198 
199 \subsection*{Checks that prevent a normalization mistake}
200 The source proves that the actual ratio has constant coefficient $c$, not one. In the concrete case $N=6,c=3$, the universal theorem gives weighted membership and the constant coefficient is proved to be $3$.
201 
202 It also derives $\coef{T}{3}H_{3,0}(\log(1+T))=1/6$ from the actual differential recurrence and checks its valuation $v_3(1/6)=-1$. Thus weighted membership does not mean ordinary coefficient integrality. This value attains the allowed floor weight at degree three.
203 
204 \textbf{Principal target.} \mcode{SingularRatioAmice.paper_singular_amice_estimate}. The theorem's assumptions contain only the declared arithmetic parameter conditions.
205 \par\medskip
206 \subsubsection*{5. Verification and the remaining theorem}
207 The cumulative inventory consists of 57 modules, 630 explicit theorem declarations and 128 explicit definitions. The release verifier compiles every module in dependency order into a new directory, treats warnings as errors, and requests a transitive axiom report for all 758 listed declarations. The allowed axioms remain \mcode{propext}, \mcode{Classical.choice} and \mcode{Quot.sound}.
208 
209 The verifier retains the previous 27 invalid-proof controls and adds two: incorrectly promoting a weighted coefficient to an integral one, and incorrectly normalizing the singular ratio constant to one. Missing imports, panics and timeouts do not qualify as successful negative controls. The preserved source checker rejects proof placeholders, added axioms and selected kernel-bypass constructs.
210 
211 The Python infrastructure suite now contains 209 tests. Four old cumulative-count assertions initially failed against the extended inventory. Their original files and failed test output are preserved; the historical tests now inspect the frozen eighth-block inventory where appropriate, while current-corpus tests enforce the new counts.
212 
213 \subsection*{Independent finite regressions}
214 The new exact-rational regression program is a separate implementation, not Lean extraction. Its checked scope is:
215 \begin{center}\begin{tabular}{lr}\toprule
216 Finite check & Count\\\midrule
217 Integral cyclic-coordinate numerator tests &17,775\\
218 Corresponding section-weight tests &17,775\\
219 Direct logarithmic composition comparisons &24\\
220 Singular ratio families &13\\
221 Singular ratio coefficient comparisons &597\\
222 Weighted product, inverse and derivative cases &120\\\bottomrule
223 \end{tabular}\end{center}
224 For $p=3,N=6,c=3$, this independent computation obtains the degree-six ratio coefficient $1/10080$, with valuation $-2$, attaining the allowed weight. This particular coefficient calculation is recorded as a finite regression, not as a new Lean theorem. A violating modulus $p=3,N=4$ yields a section coefficient of valuation $-4$ at degree nine, showing that the modulus divisibility hypothesis cannot simply be discarded.
225 
226 \subsection*{What has not been proved by this block}
227 To obtain the singular higher-difference theorem, the weighted coefficient estimate must still be connected to the dual Mahler polynomial filtration and its integral pairing. The argument must then establish the required ratio flatness, propagate between singular indices, and assemble the original all-residue Euler family. None of these obligations is replaced by the finite regression tests.
228 
229 The full manuscript register remains 23/24. Neither conjecture is resolved. The original manuscript is unchanged. Mathlib's pinned compiled cache is reused, not independently rebuilt. Frozen compiler logs, source hashes, failed drafts and fresh-extraction results accompany the release; its machine-readable audit is authoritative about the runs actually performed.

Back to source controls

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