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{Arithmetic packets and coefficient transport}
2 \label{sec:foundations}
3 
4 We work with sequences, formal power series, and finite recurrence states.
5 Residue selectors isolate coefficients in a chosen congruence class, while
6 triangular transport expresses the same object in new coordinates. A valuation
7 filtration determines how many coordinates are needed at a given precision.
8 Together, these operations provide a common framework for the Euler
9 congruences and the finite lifting constructions developed later.
10 
11 The original arithmetic seed notation
12 \[
13 \mathcal S=(A,a_0,\mathcal O,\mathcal R,\{P_{N,j}\},w,\tau_p)
14 \]
15 records a coefficient ring or module, a seed, allowed operators, relations,
16 residue selectors, a depth weight, and a topology. This notation describes the
17 ingredients of the construction; a category of seed presentations and a
18 notion of equivalence still require separate definitions. We therefore state
19 each theorem for a concrete object. Section~\ref{sec:open} discusses the
20 additional structure needed for the original native conjectures.
21 
22 The Lean declarations cited in this section have namespace prefix
23 \lean{KomorebiPaperIX}. Their exact modules and source hashes are recorded in
24 the accompanying statement map. All belong to the preserved baseline
25 formalization; this section brings their statements and proofs together.
26 
27 \subsection{Residue selectors and exact reconstruction}
28 
29 Let $R$ be a commutative ring, $a:\N\to R$, $N\geq1$, and $0\leq j<N$.
30 Define
31 \[
32 (P_{N,j}a)(n)=
33 \begin{cases}
34 a(n),&n\equiv j\pmod N,\\
35 0,&\text{otherwise}.
36 \end{cases}
37 \]
38 This definition keeps the original index set. The compressed subsequence
39 $a(Nq+j)$, used below for recurrence packets, is a different representation of
40 the selected coefficients.
41 
Statement: Residue reconstruction · Go to proof · Read statement and proof side by side42 \begin{theorem}[Residue reconstruction]
43 \label{thm:residue-reconstruction}
44 The selectors satisfy
45 \[
46 P_{N,j}^2=P_{N,j},\qquad P_{N,i}P_{N,j}=0\quad(i\ne j),
47 \qquad \sum_{j=0}^{N-1}P_{N,j}=I.
48 \]
49 If $N\mid M$ and $M>0$, then
50 \[
51 P_{N,j}a=\sum_{\substack{0\leq r<M\\r\equiv j\pmod N}}P_{M,r}a.
52 \]
53 The same identities hold coefficientwise for formal power series.
54 \end{theorem}
55 
Proof block: Residue reconstruction · Go to statement · Read statement and proof side by side56 \begin{proof}
57 At each index $n$, exactly one standard residue label equals $n\bmod N$.
58 Consequently a repeated selector changes nothing, two different selectors have
59 zero composite, and the sum retains $a(n)$ exactly once. If $N\mid M$, reducing
60 $n\bmod M$ modulo $N$ gives $n\bmod N$. This proves the refinement identity
61 at every coefficient. Equality of all coefficients proves the formal-series
62 versions.
63 \end{proof}
64 
65 \begingroup\small\raggedright
66 \noindent\emph{Formal correspondence.}
67 \lean{ResiduePackets.packet_idempotent},
68 \lean{ResiduePackets.packet_orthogonal},
69 \lean{ResiduePackets.packet_reconstruction}, and
70 \lean{ResiduePackets.packet_refinement}; the series variants have the
71 prefix \lean{series_packet} in the same module.
72 The algebraic statements need no convergence hypothesis.
73 \par\endgroup
74 
75 \subsection{Formal exponential coordinates and Hurwitz multiplication}
76 
77 Over a characteristic-zero field $K$, put
78 \[
79 \mathcal E(a)=\sum_{n\geq0}\frac{a_n}{n!}t^n,
80 \qquad \mathcal D(A)_n=n![t^n]A.
81 \]
82 These inverse maps between sequences and $K[[t]]$ provide \emph{formal}
83 exponential coordinates. No analytic convergence is needed for the coefficient
84 identities below.
85 
Statement: Constructed unit-triangular coordinates · Go to proof · Read statement and proof side by side86 \begin{theorem}[Constructed unit-triangular coordinates]
87 \label{thm:egf-coordinates}
88 Let $h:\N\to K$ satisfy $h_0=1$, write $H=\mathcal E(h)$ and
89 $H^{-1}=\mathcal E(k)$, and define
90 \[
91 U_Ha=\mathcal D(H\mathcal E(a)).
92 \]
93 Then $U_H$ is an equivalence, with inverse
94 $U_H^{-1}a=\mathcal D(H^{-1}\mathcal E(a))$. Its coefficient formulas are
95 \[
96 (U_Ha)_n=\sum_{r=0}^{n}\binom nr h_r a_{n-r},\qquad
97 (U_H^{-1}a)_n=\sum_{r=0}^{n}\binom nr k_r a_{n-r}.
98 \]
99 The resulting triangular matrix has diagonal entries $1$. The transported
100 selectors
101 \[
102 \widehat P_{N,j}=U_HP_{N,j}U_H^{-1}
103 \]
104 are idempotent and pairwise orthogonal, and their sum is the identity.
105 \end{theorem}
106 
Proof block: Constructed unit-triangular coordinates · Go to statement · Read statement and proof side by side107 \begin{proof}
108 The factorials are nonzero in $K$, so encoding and decoding cancel
109 coefficientwise. The constant coefficient of $H$ is $1$; hence its formal
110 power-series inverse exists. Multiplication by $H$ and $H^{-1}$ gives the two
111 inverse laws. The ordinary product coefficient formula, multiplied by $n!$,
112 gives the displayed binomial sums. In row $n$, the coefficient of $a_n$ is
113 $h_0=1$ and coefficients of $a_q$ with $q>n$ vanish. Conjugating the identities
114 of Theorem~\ref{thm:residue-reconstruction} by the constructed equivalence proves
115 the transported projector identities.
116 \end{proof}
117 
118 \begingroup\small\raggedright
119 \noindent\emph{Formal correspondence.}
120 \lean{EGF.decode_encode}, \lean{EGF.encode_decode},
121 \lean{EGF.egf_product}, \lean{EGF.coordinateEquiv},
122 \lean{EGF.coordinate_forward}, \lean{EGF.coordinate_inverse},
123 and \lean{EGF.transported_reconstruction}, together with the idempotence and
124 orthogonality declarations in \lean{EGFCoordinates}.
125 \par\endgroup
126 
127 In characteristic $p$, factorial division is unavailable in general, but the
128 coefficient operation remains meaningful over every commutative ring:
129 \[
130 (f\star g)_n=\sum_{r=0}^{n}\binom nr f_r g_{n-r},\qquad
131 (D^d f)_n=f_{n+d},\qquad \mathbf1_n=\begin{cases}1,&n=0,\\0,&n>0.\end{cases}
132 \]
133 Here $\star$ is Hurwitz multiplication. The symbol $D^d$ denotes a coefficient
134 shift, which agrees with formal differentiation after characteristic-zero
135 encoding.
136 
Statement: Hurwitz product rules · Go to proof · Read statement and proof side by side137 \begin{theorem}[Hurwitz product rules]
138 \label{thm:hurwitz-product}
139 For $d\geq0$,
140 \[
141 D^d(f\star g)=\sum_{r=0}^{d}\binom dr(D^r f)\star(D^{d-r}g).
142 \]
143 If $R$ has prime characteristic $p$, then
144 \[
145 D^p(f\star g)=f\star D^p g+D^p f\star g.
146 \]
147 Over a field, if $g_0=1$, a sequence $b$ is constructed recursively with
148 $b\star g=\mathbf1$. If also $D^p g=Dg$ in characteristic $p$, then
149 $D^p b=Db$.
150 \end{theorem}
151 
Proof block: Hurwitz product rules · Go to statement · Read statement and proof side by side152 \begin{proof}
153 Pascal's identity proves the first product rule, and induction proves the
154 higher rule. The intermediate binomial coefficients $\binom pr$ vanish in
155 characteristic $p$. For the inverse, solve row $n$ using the coefficient of
156 $b_n$, which is $g_0=1$:
157 \[
158 b_n=\mathbf1_n-\sum_{r<n}\binom nr b_r g_{n-r}.
159 \]
160 Subtract the first and $p$th product rules for $b\star g=\mathbf1$.
161 The assumed identity for $g$ leaves
162 $(D^p b-Db)\star g=0$. A second triangular induction shows that convolution
163 with a sequence having constant coefficient $1$ has trivial kernel.
164 \end{proof}
165 
166 \begingroup\small\raggedright
167 \noindent\emph{Formal correspondence.}
168 \lean{Hurwitz.shift_convolution}, \lean{Hurwitz.prime_shift_convolution},
169 \lean{Hurwitz.convolution_left_eq_zero},
170 \lean{HurwitzInverse.inverse_convolution}, and
171 \lean{HurwitzInverse.inverse_prime_difference}.
172 Working directly with coefficient sequences avoids the undefined expression
173 $1/n!$ in $\F_p$ when $p\mid n!$.
174 \par\endgroup
175 
176 \subsection{Triangular inversion and a finite precision filtration}
177 
Statement: Forward substitution and denominator clearing · Go to proof · Read statement and proof side by side178 \begin{theorem}[Forward substitution and denominator clearing]
179 \label{thm:triangular-foundation}
180 Let $T_{nq}$ be coefficients over a field with $T_{nn}\ne0$ for every $n$.
181 For any sequence $b$, define
182 \[
183 a_n=\frac{b_n-\sum_{q<n}T_{nq}a_q}{T_{nn}}.
184 \]
185 This constructs the unique solution of
186 $\sum_{q=0}^{n}T_{nq}a_q=b_n$ for all $n$. If $T_{nq}$ and $b_n$ are integers
187 and the solution is taken over $\Q$, then
188 \[
189 \left(\prod_{r=0}^{n}T_{rr}\right)a_n\in\Z.
190 \]
191 \end{theorem}
192 
Proof block: Forward substitution and denominator clearing · Go to statement · Read statement and proof side by side193 \begin{proof}
194 The recursion uses only smaller indices, and substitution verifies each row.
195 If a second solution agrees through row $n-1$, subtracting row $n$ and
196 cancelling $T_{nn}$ proves equality at $n$. For integrality, use induction and
197 promote every earlier clearing product to $\prod_{r<n}T_{rr}$. Multiplication
198 by the additional factor $T_{nn}$ cancels the only new division.
199 \end{proof}
200 
201 \begingroup\small\raggedright
202 \noindent\emph{Formal correspondence.}
203 \lean{Triangular.solve_row}, \lean{Triangular.solve_unique}, and
204 \lean{Triangular.solve_denominator_integral}. The clearing product bounds the
205 denominator; the unscaled solution can still be nonintegral.
206 \par\endgroup
207 
208 To isolate the filtration argument, let $p$ be any element of a commutative
209 ring and let $w:\N\to\N\cup\{\infty\}$. Set $p^{[r]}=p^r$ for finite $r$
210 and $p^{[\infty]}=0$. The latter notation means the coefficient vanishes.
211 
Statement: Filtered finite reconstruction · Go to proof · Read statement and proof side by side212 \begin{theorem}[Filtered finite reconstruction]
213 \label{thm:filtered-foundation}
214 For every $n,L\in\N$ and sequences $c,S$ in that ring,
215 \[
216 \begin{split}
217 &\sum_{r=0}^{n}\binom nr c_rp^{[w(r)]}S_{n-r}\\
218 &\hspace{8mm}\equiv
219 \sum_{\substack{0\leq r\leq n\\w(r)<L}}
220 \binom nr c_rp^{[w(r)]}S_{n-r}\pmod{p^L}.
221 \end{split}
222 \]
223 Here congruence means divisibility of the difference by $p^L$ in the
224 coefficient ring. In $\Zp$, it means membership in $p^L\Zp$.
225 \end{theorem}
226 
Proof block: Filtered finite reconstruction · Go to statement · Read statement and proof side by side227 \begin{proof}
228 The difference of the two sums consists exactly of terms with $w(r)\geq L$.
229 Every such term is divisible by $p^L$, including the zero terms with infinite
230 weight. Their finite sum has the same divisibility.
231 \end{proof}
232 
233 \begingroup\small\raggedright
234 \noindent\emph{Formal correspondence.}
235 \lean{Filtered.filtered_triangular_reconstruction} and
236 \lean{Filtered.padic_filtered_reconstruction}.
237 For weights $2r$, retaining $r\leq M$ gives the bound $p^{2M+2}$ through
238 \lean{Filtered.even_weight_tail}. A sharper kernel weight can improve this
239 bound, as in the classical dyadic reconstruction later in the paper. Each
240 coefficient row is finite, so no hypothesis $w(r)\to\infty$ is needed here.
241 \par\endgroup
242 
243 \subsection{Finite Mahler coordinates and weighted differences}
244 
245 For $f:\N\to R$, define the step-$h$ forward difference and its iterates by
246 \[
247 \Delta_h f(n)=f(n+h)-f(n),\qquad \Delta_h^0 f=f,
248 \]
249 and put $c_r(f)=\Delta_1^r f(0)$. Thus the coefficients are determined by the
250 differences of $f$.
251 
Statement: Finite Newton Mahler identities · Go to proof · Read statement and proof side by side252 \begin{theorem}[Finite Newton--Mahler identities]
253 \label{thm:mahler-foundation}
254 For every $n,s,h\in\N$,
255 \[
256 \begin{aligned}
257 f(n)&=\sum_{r=0}^{n}c_r(f)\binom nr,\\
258 c_r(\Delta_1^s f)&=c_{s+r}(f),\\
259 \Delta_1^s f(n)&=\sum_{j=0}^{n}c_{s+j}(f)\binom nj,\\
260 \Delta_h^s f(n)&=\sum_{j=0}^{s}(-1)^{s-j}\binom sj f(n+jh).
261 \end{aligned}
262 \]
263 The finite interpolant
264 $I_Nf(n)=\sum_{r=0}^{N}c_r(f)\binom nr$ agrees with $f$ for $n\leq N$.
265 It has the same order-$s$ unit-step difference at $n$ whenever $n+s\leq N$.
266 For arbitrary coefficients $c_0,\ldots,c_N$, the corresponding binomial
267 interpolant has exactly those coefficients and zero coefficients above $N$.
268 \end{theorem}
269 
Proof block: Finite Newton Mahler identities · Go to statement · Read statement and proof side by side270 \begin{proof}
271 Write $E_h f(n)=f(n+h)$ for the shift operator. The unit shift is
272 $I+\Delta_1$. Expanding its $n$th power and evaluating
273 at zero gives reconstruction. Composing difference operators gives the
274 coefficient shift and applying reconstruction to $\Delta_1^s f$ gives the
275 third identity. The binomial expansion of $(E_h-I)^s$ gives the explicit
276 stencil. Binomial coefficients vanish when their lower index exceeds $n$,
277 which proves the interpolation claim. Equality of every point of the stencil
278 proves equality of differences. Repeated finite differences of $\binom nr$
279 at zero give the exact coefficient extraction.
280 \end{proof}
281 
282 \begingroup\small\raggedright
283 \noindent\emph{Formal correspondence.}
284 \lean{Mahler.finite_mahler_reconstruction},
285 \lean{Mahler.coefficient_difference},
286 \lean{Mahler.difference_from_coefficients},
287 \lean{Mahler.difference_explicit},
288 \lean{Mahler.finite_sample_difference}, and
289 \lean{Mahler.coefficient_interpolant}.
290 Finite samples determine the stencils contained in the sample interval;
291 a universal tail estimate requires additional information.
292 \par\endgroup
293 
294 For $x\in\Zp$, extend the valuation to zero by setting
295 \[
296 \operatorname{ord}_p(x)=
297 \begin{cases}v_p(x),&x\ne0,\\\infty,&x=0.\end{cases}
298 \]
299 Thus $L\leq\operatorname{ord}_p(x)$ is equivalent to $x\in p^L\Zp$.
300 
Statement: Weighted difference bound · Go to proof · Read statement and proof side by side301 \begin{theorem}[Weighted difference bound]
302 \label{thm:weighted-mahler-foundation}
303 Let $f:\N\to\Zp$ and let $w:\N\to\N\cup\{\infty\}$ satisfy
304 $w(s+j)\leq\operatorname{ord}_p(c_{s+j}(f))$ for $0\leq j\leq n$.
305 Then
306 \[
307 \operatorname{ord}_p(\Delta_1^s f(n))\geq
308 \min_{0\leq j\leq n}
309 \left\{w(s+j)+v_p\binom nj\right\}.
310 \]
311 \end{theorem}
312 
Proof block: Weighted difference bound · Go to statement · Read statement and proof side by side313 \begin{proof}
314 Apply the nonarchimedean inequality to the finite coefficient formula in
315 Theorem~\ref{thm:mahler-foundation}. For $0\leq j\leq n$, the integer
316 $\binom nj$ is positive. The order of its product with $c_{s+j}(f)$ is the
317 sum of the two orders, including the case where that coefficient is zero.
318 \end{proof}
319 
320 \begingroup\small\raggedright
321 \noindent\emph{Formal correspondence.}
322 \lean{PadicBounds.nat_le_order_iff},
323 \lean{PadicBounds.weighted_difference_bound}, and
324 \lean{PadicBounds.weighted_difference_divisibility}.
325 An expansion on all of $\Zp$ requires a convergence theorem in addition to
326 these finite algebraic identities and bounds.
327 \par\endgroup
328 
329 \subsection{Unit modes and the dyadic distinction}
330 
Statement: Differences of unit modes · Go to proof · Read statement and proof side by side331 \begin{theorem}[Differences of unit modes]
332 \label{thm:unit-modes-foundation}
333 Over every commutative ring,
334 \[
335 \Delta_h^s(u^n)=u^n(u^h-1)^s.
336 \]
337 For any prime $p$, units $u_i\in\Zp^\times$, coefficients $a_i\in\Zp$, and
338 a finite index set $I$, the sequence $f(n)=\sum_{i\in I}a_i u_i^n$ satisfies
339 \[
340 \Delta_{p-1}^s f(n)\in p^s\Zp
341 \qquad(n,s\in\N).
342 \]
343 \end{theorem}
344 
Proof block: Differences of unit modes · Go to statement · Read statement and proof side by side345 \begin{proof}
346 Induction gives the geometric identity. Reduction of a unit to $\F_p^\times$
347 gives $u_i^{p-1}=1$ modulo $p$. Taking $s$ powers supplies $p^s$ in each
348 summand. The difference operator is linear over finite sums.
349 \end{proof}
350 
351 \begingroup\small\raggedright
352 \noindent\emph{Formal correspondence.}
353 \lean{UnitModes.geometric_difference},
354 \lean{UnitModes.unit_fermat_divisibility}, and
355 \lean{UnitModes.finite_unit_modes_divisibility}.
356 The result includes $p=2$, where the displayed step is $1$. Its scope here
357 is finite sums of modes.
358 \par\endgroup
359 
Statement: Finite unit coordinates · Go to proof · Read statement and proof side by side360 \begin{theorem}[Finite unit coordinates]
361 \label{thm:finite-unit-foundation}
362 Let $p$ be prime, $L\geq0$, and
363 $a\in(\Z/p^{L+1}\Z)^\times$. Define
364 \[
365 \omega_L(a)=a^{p^L},\qquad \langle a\rangle_L=a\omega_L(a)^{-1}.
366 \]
367 Then
368 \[
369 a=\omega_L(a)\langle a\rangle_L,\qquad
370 \omega_L(a)^{p-1}=1,\qquad \langle a\rangle_L\equiv1\pmod p.
371 \]
372 The two factors are uniquely determined by these properties and are compatible
373 with reduction to lower precision.
374 For $a\in(\Z/2^{L+2}\Z)^\times$, there is instead a unique decomposition
375 \[
376 a=\epsilon(a)\langle a\rangle_4,
377 \qquad \epsilon(a)\in\{1,-1\},\qquad
378 \langle a\rangle_4\equiv1\pmod4.
379 \]
380 \end{theorem}
381 
Proof block: Finite unit coordinates · Go to statement · Read statement and proof side by side382 \begin{proof}
383 The unit-group exponent $p^L(p-1)$ gives the root identity for $\omega_L$.
384 Its residue is that of $a$, so the remaining factor has residue $1$.
385 If two $(p-1)$st roots have equal residue, raising them to $p^L$ makes them
386 equal modulo $p^{L+1}$, while each root is fixed by this exponent. This proves
387 uniqueness and then compatibility under reduction. In the dyadic construction,
388 an odd residue is exactly $1$ or $-1$ modulo $4$. Choose that sign and multiply
389 $a$ by it to obtain the principal factor. The two signs remain distinct
390 modulo $4$, which proves uniqueness.
391 \end{proof}
392 
393 \begingroup\small\raggedright
394 \noindent\emph{Formal correspondence.}
395 \lean{FiniteUnits.finite_unit_decomposition},
396 \lean{FiniteUnits.decomposition_unique},
397 \lean{UnitRefinement.omega_compatible},
398 \lean{UnitRefinement.principal_compatible}, and
399 \lean{DyadicUnits.dyadic_unit_decomposition} with
400 \lean{DyadicUnits.decomposition_unique}.
401 The finite $p=2$ version of the first construction has trivial root-of-unity
402 factor. The separate modulo-$4$ construction retains the sign that reduction
403 modulo $2$ cannot detect.
404 \par\endgroup
405 
406 \subsection{Recurrence packets and finite arithmetic synchronization}
407 
Statement: Companion jumps and packet recurrences · Go to proof · Read statement and proof side by side408 \begin{theorem}[Companion jumps and packet recurrences]
409 \label{thm:companion-foundation}
410 Let $C$ be a $d\times d$ matrix over a commutative ring and
411 $x_n=C^n x_0$. For $N,j,k\in\N$, put $b_k=x_{Nk+j}$. Then
412 \[
413 b_k=C^j(C^N)^kx_0,\qquad b_{k+1}=C^Nb_k.
414 \]
415 If $\chi_{C^N}(X)=X^d+\sum_{r<d}q_rX^r$, then
416 \[
417 b_{k+d}=-\sum_{r=0}^{d-1}q_r b_{k+r}.
418 \]
419 Every coordinate and every linear scalar observable satisfies the same
420 recurrence. No invertibility or diagonalization hypothesis is required.
421 \end{theorem}
422 
Proof block: Companion jumps and packet recurrences · Go to statement · Read statement and proof side by side423 \begin{proof}
424 The jump identity follows from the power law for one matrix. Apply the
425 Cayley--Hamilton identity $\chi_{C^N}(C^N)=0$ to the state $b_k$.
426 The leading coefficient is $1$, so the final state can be isolated. A linear
427 observable preserves the resulting finite sum.
428 \end{proof}
429 
430 \begingroup\small\raggedright
431 \noindent\emph{Formal correspondence.}
432 \lean{Companion.companion_jump},
433 \lean{Companion.packet_charpoly_recurrence}, and
434 \lean{Companion.packet_observable_recurrence}.
435 The source-sequence versions derive the packet recurrence from the relation
436 $x_{n+1}=Cx_n$.
437 For the Fibonacci matrix $C=\left(\begin{smallmatrix}1&1\\1&0\end{smallmatrix}\right)$,
438 its jump trace is the Lucas number $L_N$ and its determinant is $(-1)^N$.
439 Thus
440 \[
441 F_{N(k+2)+j}=L_NF_{N(k+1)+j}-(-1)^NF_{Nk+j}.
442 \]
443 This specialization is
444 \lean{FibonacciPackets.fibonacci_packet_recurrence}; it is derived from the
445 Fibonacci state.
446 \par\endgroup
447 
Statement: Dyadic odd packet factorization · Go to proof · Read statement and proof side by side448 \begin{theorem}[Dyadic--odd packet factorization]
449 \label{thm:crt-foundation}
450 Let $a\geq0$ and let $M$ be a positive odd integer. The Chinese remainder map
451 is a ring isomorphism
452 \[
453 \Z/(2^aM)\Z\simeq\Z/2^a\Z\times\Z/M\Z.
454 \]
455 For $0\leq r<2^aM$ and any coefficient sequence $f$,
456 \[
457 P_{2^aM,r}f
458 =P_{2^a,r\bmod 2^a}\,P_{M,r\bmod M}f.
459 \]
460 The same identity holds for formal-series coefficient selectors.
461 \end{theorem}
462 
Proof block: Dyadic odd packet factorization · Go to statement · Read statement and proof side by side463 \begin{proof}
464 The two moduli are coprime. An index has the prescribed combined residue
465 exactly when it has both component residues. Applying this equivalence to
466 the indicator defining each selector proves the formula.
467 \end{proof}
468 
469 \begingroup\small\raggedright
470 \noindent\emph{Formal correspondence.}
471 \lean{CRTPackets.addressEquiv}, \lean{CRTPackets.residue_equivalence},
472 \lean{CRTPackets.packet_factorization}, and
473 \lean{CRTPackets.series_packet_factorization}.
474 This theorem synchronizes finite arithmetic addresses. The passage from a
475 family of $p$-adic objects to a global integer object is a separate question,
476 discussed in Section~\ref{subsec:native133}.
477 \par\endgroup
478 
479 \subsection{Polyphase notation retained from the recovered manuscript}
480 \label{subsec:polyphase-exposition}
481 
482 The recovered Annals text develops a broader polyphase vocabulary. We explain
483 it through elementary identities with explicit algebraic derivations. These
484 identities have not been separately formalized in Lean for this consolidation.
485 For a sequence $a$ and $M\geq1$, let $a_r^{[M]}(q)=a_{Mq+r}$ for $0\leq r<M$.
486 If $A(z)=\sum_n a_nz^n$ and $A_r(w)=\sum_q a_{Mq+r}w^q$ are ordinary generating
487 functions, then unique quotient and remainder give
488 \[
489 A(z)=\sum_{r=0}^{M-1}z^rA_r(z^M),\qquad
490 \bigl(a_r^{[M]}\bigr)_s^{[N]}=a_{r+Ms}^{[MN]}.
491 \]
492 For ordinary Cauchy multiplication, the phase-$r$ product has a term without a
493 carry and a term with one carry:
494 \[
495 C_r(w)=\sum_{u+v=r}A_u(w)B_v(w)
496 +w\sum_{u+v=r+M}A_u(w)B_v(w),\qquad 0\leq u,v<M.
497 \]
498 Adding the two phase addresses gives the formula. It describes ordinary
499 Cauchy multiplication; Hurwitz convolution has its own binomial weights.
500 
501 For $M\geq1$ and $s,r,k\in\N$, define the affine Mahler kernel by
502 \[
503 \Theta_{M,s}(r,k)=[z^r](1+z)^s\bigl((1+z)^M-1\bigr)^k
504 =\sum_{j=0}^{k}(-1)^{k-j}\binom kj\binom{Mj+s}{r}.
505 \]
506 It vanishes unless $k\leq r\leq Mk+s$. For a finite binomial expansion
507 $f(n)=\sum_{r=0}^{D}c_r\binom nr$, the $k$th Newton coefficient of
508 $g(q)=f(Mq+s)$ is therefore
509 \[
510 c_k(g)=\sum_{r=k}^{\min(D,Mk+s)}c_r\Theta_{M,s}(r,k).
511 \]
512 Indeed, insert the finite stencil for $\Delta_1^k g(0)$ and interchange its
513 two finite sums. Coefficient extraction of the binomial expansion of
514 $((1+z)^M-1)^k$ gives the kernel. In the binary zero-address case,
515 \[
516 \Theta_{2,0}(k+j,k)=2^{k-j}\binom kj\qquad(0\leq j\leq k),
517 \]
518 since $(2z+z^2)^k=z^k(2+z)^k$.
519 Exact valuations for the general kernel remain to be determined. The
520 recovered infinite analytic extensions and stronger historical identities
521 lie beyond these finite derivations; their status is discussed in
522 Section~\ref{subsec:historical-scope}.

Back to source controls

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