2 Arithmetic packets and coefficient transport
On this page · Permalink · Source line 1
We work with sequences, formal power series, and finite recurrence states. Residue selectors isolate coefficients in a chosen congruence class, while triangular transport expresses the same object in new coordinates. A valuation filtration determines how many coordinates are needed at a given precision. Together, these operations provide a common framework for the Euler congruences and the finite lifting constructions developed later.
The original arithmetic seed notation
records a coefficient ring or module, a seed, allowed operators, relations, residue selectors, a depth weight, and a topology. This notation describes the ingredients of the construction; a category of seed presentations and a notion of equivalence still require separate definitions. We therefore state each theorem for a concrete object. Section 12 discusses the additional structure needed for the original native conjectures.
The Lean declarations cited in this section have namespace prefix KomorebiPaperIX. Their exact modules and source hashes are recorded in the accompanying statement map. All belong to the preserved baseline formalization; this section brings their statements and proofs together.
2.1 Residue selectors and exact reconstruction
On this page · Permalink · Source line 27
Let \(R\) be a commutative ring, \(a:{\mathbb N}\to R\), \(N\geq1\), and \(0\leq j<N\). Define
This definition keeps the original index set. The compressed subsequence \(a(Nq+j)\), used below for recurrence packets, is a different representation of the selected coefficients.
Theorem 2.1: Residue reconstruction
The selectors satisfy
If \(N\mid M\) and \(M>0\), then
The same identities hold coefficientwise for formal power series.
Read proof · Read statement and proof side by side · Permalink · Source line 42 · Claim record · Lean coverage · Code · Worked examples
Proof of Theorem 2.1
At each index \(n\), exactly one standard residue label equals \(n\bmod N\). Consequently a repeated selector changes nothing, two different selectors have zero composite, and the sum retains \(a(n)\) exactly once. If \(N\mid M\), reducing \(n\bmod M\) modulo \(N\) gives \(n\bmod N\). This proves the refinement identity at every coefficient. Equality of all coefficients proves the formal-series versions.
Back to statement · Read statement and proof side by side · Permalink · Source line 56 · Claim record · Lean coverage · Code · Worked examples
Formal correspondence. ResiduePackets.packet_idempotent, ResiduePackets.packet_orthogonal, ResiduePackets.packet_reconstruction, and ResiduePackets.packet_refinement; the series variants have the prefix series_packet in the same module. The algebraic statements need no convergence hypothesis.
2.2 Formal exponential coordinates and Hurwitz multiplication
On this page · Permalink · Source line 75
Over a characteristic-zero field \(K\), put
These inverse maps between sequences and \(K[[t]]\) provide formal exponential coordinates. No analytic convergence is needed for the coefficient identities below.
Theorem 2.2: Constructed unit-triangular coordinates
Let \(h:{\mathbb N}\to K\) satisfy \(h_0=1\), write \(H=\mathcal E(h)\) and \(H^{-1}=\mathcal E(k)\), and define
Then \(U_H\) is an equivalence, with inverse \(U_H^{-1}a=\mathcal D(H^{-1}\mathcal E(a))\). Its coefficient formulas are
The resulting triangular matrix has diagonal entries \(1\). The transported selectors
are idempotent and pairwise orthogonal, and their sum is the identity.
Read proof · Read statement and proof side by side · Permalink · Source line 86 · Claim record · Lean coverage · Code · Worked examples
Proof of Theorem 2.2
The factorials are nonzero in \(K\), so encoding and decoding cancel coefficientwise. The constant coefficient of \(H\) is \(1\); hence its formal power-series inverse exists. Multiplication by \(H\) and \(H^{-1}\) gives the two inverse laws. The ordinary product coefficient formula, multiplied by \(n!\), gives the displayed binomial sums. In row \(n\), the coefficient of \(a_n\) is \(h_0=1\) and coefficients of \(a_q\) with \(q>n\) vanish. Conjugating the identities of Theorem 2.1 by the constructed equivalence proves the transported projector identities.
Back to statement · Read statement and proof side by side · Permalink · Source line 107 · Claim record · Lean coverage · Code · Worked examples
Formal correspondence. EGF.decode_encode, EGF.encode_decode, EGF.egf_product, EGF.coordinateEquiv, EGF.coordinate_forward, EGF.coordinate_inverse, and EGF.transported_reconstruction, together with the idempotence and orthogonality declarations in EGFCoordinates.
In characteristic \(p\), factorial division is unavailable in general, but the coefficient operation remains meaningful over every commutative ring:
Here \(\star\) is Hurwitz multiplication. The symbol \(D^d\) denotes a coefficient shift, which agrees with formal differentiation after characteristic-zero encoding.
Theorem 2.3: Hurwitz product rules
For \(d\geq0\),
If \(R\) has prime characteristic \(p\), then
Over a field, if \(g_0=1\), a sequence \(b\) is constructed recursively with \(b\star g=\mathbf1\). If also \(D^p g=Dg\) in characteristic \(p\), then \(D^p b=Db\).
Read proof · Read statement and proof side by side · Permalink · Source line 137 · Claim record · Lean coverage · Code · Worked examples
Proof of Theorem 2.3
Pascal's identity proves the first product rule, and induction proves the higher rule. The intermediate binomial coefficients \(\binom pr\) vanish in characteristic \(p\). For the inverse, solve row \(n\) using the coefficient of \(b_n\), which is \(g_0=1\):
Subtract the first and \(p\)th product rules for \(b\star g=\mathbf1\). The assumed identity for \(g\) leaves \((D^p b-Db)\star g=0\). A second triangular induction shows that convolution with a sequence having constant coefficient \(1\) has trivial kernel.
Back to statement · Read statement and proof side by side · Permalink · Source line 152 · Claim record · Lean coverage · Code · Worked examples
Formal correspondence. Hurwitz.shift_convolution, Hurwitz.prime_shift_convolution, Hurwitz.convolution_left_eq_zero, HurwitzInverse.inverse_convolution, and HurwitzInverse.inverse_prime_difference. Working directly with coefficient sequences avoids the undefined expression \(1/n!\) in \({\mathbb F}_p\) when \(p\mid n!\).
2.3 Triangular inversion and a finite precision filtration
On this page · Permalink · Source line 176
Theorem 2.4: Forward substitution and denominator clearing
Let \(T_{nq}\) be coefficients over a field with \(T_{nn}\ne0\) for every \(n\). For any sequence \(b\), define
This constructs the unique solution of \(\sum_{q=0}^{n}T_{nq}a_q=b_n\) for all \(n\). If \(T_{nq}\) and \(b_n\) are integers and the solution is taken over \({\mathbb Q}\), then
Read proof · Visual guide: Compute the reciprocal before estimating it · Read statement and proof side by side · Permalink · Source line 178 · Claim record · Lean coverage · Code · Worked examples
Proof of Theorem 2.4
The recursion uses only smaller indices, and substitution verifies each row. If a second solution agrees through row \(n-1\), subtracting row \(n\) and cancelling \(T_{nn}\) proves equality at \(n\). For integrality, use induction and promote every earlier clearing product to \(\prod_{r<n}T_{rr}\). Multiplication by the additional factor \(T_{nn}\) cancels the only new division.
Back to statement · Read statement and proof side by side · Permalink · Source line 193 · Claim record · Lean coverage · Code · Worked examples
Formal correspondence. Triangular.solve_row, Triangular.solve_unique, and Triangular.solve_denominator_integral. The clearing product bounds the denominator; the unscaled solution can still be nonintegral.
To isolate the filtration argument, let \(p\) be any element of a commutative ring and let \(w:{\mathbb N}\to{\mathbb N}\cup\{\infty\}\). Set \(p^{[r]}=p^r\) for finite \(r\) and \(p^{[\infty]}=0\). The latter notation means the coefficient vanishes.
Theorem 2.5: Filtered finite reconstruction
For every \(n,L\in{\mathbb N}\) and sequences \(c,S\) in that ring,
Here congruence means divisibility of the difference by \(p^L\) in the coefficient ring. In \({\mathbb Z_p}\), it means membership in \(p^L{\mathbb Z_p}\).
Read proof · Read statement and proof side by side · Permalink · Source line 212 · Claim record · Lean coverage · Code · Worked examples
Proof of Theorem 2.5
The difference of the two sums consists exactly of terms with \(w(r)\geq L\). Every such term is divisible by \(p^L\), including the zero terms with infinite weight. Their finite sum has the same divisibility.
Back to statement · Read statement and proof side by side · Permalink · Source line 227 · Claim record · Lean coverage · Code · Worked examples
Formal correspondence. Filtered.filtered_triangular_reconstruction and Filtered.padic_filtered_reconstruction. For weights \(2r\), retaining \(r\leq M\) gives the bound \(p^{2M+2}\) through Filtered.even_weight_tail. A sharper kernel weight can improve this bound, as in the classical dyadic reconstruction later in the paper. Each coefficient row is finite, so no hypothesis \(w(r)\to\infty\) is needed here.
2.4 Finite Mahler coordinates and weighted differences
On this page · Permalink · Source line 243
For \(f:{\mathbb N}\to R\), define the step-\(h\) forward difference and its iterates by
and put \(c_r(f)=\Delta_1^r f(0)\). Thus the coefficients are determined by the differences of \(f\).
Theorem 2.6: Finite Newton–Mahler identities
For every \(n,s,h\in{\mathbb N}\),
The finite interpolant \(I_Nf(n)=\sum_{r=0}^{N}c_r(f)\binom nr\) agrees with \(f\) for \(n\leq N\). It has the same order-\(s\) unit-step difference at \(n\) whenever \(n+s\leq N\). For arbitrary coefficients \(c_0,\ldots,c_N\), the corresponding binomial interpolant has exactly those coefficients and zero coefficients above \(N\).
Read proof · Read statement and proof side by side · Permalink · Source line 252 · Claim record · Lean coverage · Code · Worked examples
Proof of Theorem 2.6
Write \(E_h f(n)=f(n+h)\) for the shift operator. The unit shift is \(I+\Delta_1\). Expanding its \(n\)th power and evaluating at zero gives reconstruction. Composing difference operators gives the coefficient shift and applying reconstruction to \(\Delta_1^s f\) gives the third identity. The binomial expansion of \((E_h-I)^s\) gives the explicit stencil. Binomial coefficients vanish when their lower index exceeds \(n\), which proves the interpolation claim. Equality of every point of the stencil proves equality of differences. Repeated finite differences of \(\binom nr\) at zero give the exact coefficient extraction.
Back to statement · Read statement and proof side by side · Permalink · Source line 270 · Claim record · Lean coverage · Code · Worked examples
Formal correspondence. Mahler.finite_mahler_reconstruction, Mahler.coefficient_difference, Mahler.difference_from_coefficients, Mahler.difference_explicit, Mahler.finite_sample_difference, and Mahler.coefficient_interpolant. Finite samples determine the stencils contained in the sample interval; a universal tail estimate requires additional information.
For \(x\in{\mathbb Z_p}\), extend the valuation to zero by setting
Thus \(L\leq\operatorname{ord}_p(x)\) is equivalent to \(x\in p^L{\mathbb Z_p}\).
Theorem 2.7: Weighted difference bound
Let \(f:{\mathbb N}\to{\mathbb Z_p}\) and let \(w:{\mathbb N}\to{\mathbb N}\cup\{\infty\}\) satisfy \(w(s+j)\leq\operatorname{ord}_p(c_{s+j}(f))\) for \(0\leq j\leq n\). Then
Read proof · Read statement and proof side by side · Permalink · Source line 301 · Claim record · Lean coverage · Code · Worked examples
Proof of Theorem 2.7
Apply the nonarchimedean inequality to the finite coefficient formula in Theorem 2.6. For \(0\leq j\leq n\), the integer \(\binom nj\) is positive. The order of its product with \(c_{s+j}(f)\) is the sum of the two orders, including the case where that coefficient is zero.
Back to statement · Read statement and proof side by side · Permalink · Source line 313 · Claim record · Lean coverage · Code · Worked examples
Formal correspondence. PadicBounds.nat_le_order_iff, PadicBounds.weighted_difference_bound, and PadicBounds.weighted_difference_divisibility. An expansion on all of \({\mathbb Z_p}\) requires a convergence theorem in addition to these finite algebraic identities and bounds.
2.5 Unit modes and the dyadic distinction
On this page · Permalink · Source line 329
Theorem 2.8: Differences of unit modes
Over every commutative ring,
For any prime \(p\), units \(u_i\in{\mathbb Z_p}^\times\), coefficients \(a_i\in{\mathbb Z_p}\), and a finite index set \(I\), the sequence \(f(n)=\sum_{i\in I}a_i u_i^n\) satisfies
Read proof · Read statement and proof side by side · Permalink · Source line 331 · Claim record · Lean coverage · Code · Worked examples
Proof of Theorem 2.8
Induction gives the geometric identity. Reduction of a unit to \({\mathbb F}_p^\times\) gives \(u_i^{p-1}=1\) modulo \(p\). Taking \(s\) powers supplies \(p^s\) in each summand. The difference operator is linear over finite sums.
Back to statement · Read statement and proof side by side · Permalink · Source line 345 · Claim record · Lean coverage · Code · Worked examples
Formal correspondence. UnitModes.geometric_difference, UnitModes.unit_fermat_divisibility, and UnitModes.finite_unit_modes_divisibility. The result includes \(p=2\), where the displayed step is \(1\). Its scope here is finite sums of modes.
Theorem 2.9: Finite unit coordinates
Let \(p\) be prime, \(L\geq0\), and \(a\in({\mathbb Z}/p^{L+1}{\mathbb Z})^\times\). Define
Then
The two factors are uniquely determined by these properties and are compatible with reduction to lower precision. For \(a\in({\mathbb Z}/2^{L+2}{\mathbb Z})^\times\), there is instead a unique decomposition
Read proof · Read statement and proof side by side · Permalink · Source line 360 · Claim record · Lean coverage · Code · Worked examples
Proof of Theorem 2.9
The unit-group exponent \(p^L(p-1)\) gives the root identity for \(\omega_L\). Its residue is that of \(a\), so the remaining factor has residue \(1\). If two \((p-1)\)st roots have equal residue, raising them to \(p^L\) makes them equal modulo \(p^{L+1}\), while each root is fixed by this exponent. This proves uniqueness and then compatibility under reduction. In the dyadic construction, an odd residue is exactly \(1\) or \(-1\) modulo \(4\). Choose that sign and multiply \(a\) by it to obtain the principal factor. The two signs remain distinct modulo \(4\), which proves uniqueness.
Back to statement · Read statement and proof side by side · Permalink · Source line 382 · Claim record · Lean coverage · Code · Worked examples
Formal correspondence. FiniteUnits.finite_unit_decomposition, FiniteUnits.decomposition_unique, UnitRefinement.omega_compatible, UnitRefinement.principal_compatible, and DyadicUnits.dyadic_unit_decomposition with DyadicUnits.decomposition_unique. The finite \(p=2\) version of the first construction has trivial root-of-unity factor. The separate modulo-\(4\) construction retains the sign that reduction modulo \(2\) cannot detect.
2.6 Recurrence packets and finite arithmetic synchronization
On this page · Permalink · Source line 406
Theorem 2.10: Companion jumps and packet recurrences
Let \(C\) be a \(d\times d\) matrix over a commutative ring and \(x_n=C^n x_0\). For \(N,j,k\in{\mathbb N}\), put \(b_k=x_{Nk+j}\). Then
If \(\chi_{C^N}(X)=X^d+\sum_{r<d}q_rX^r\), then
Every coordinate and every linear scalar observable satisfies the same recurrence. No invertibility or diagonalization hypothesis is required.
Read proof · Read statement and proof side by side · Permalink · Source line 408 · Claim record · Lean coverage · Code · Worked examples
Proof of Theorem 2.10
The jump identity follows from the power law for one matrix. Apply the Cayley–Hamilton identity \(\chi_{C^N}(C^N)=0\) to the state \(b_k\). The leading coefficient is \(1\), so the final state can be isolated. A linear observable preserves the resulting finite sum.
Back to statement · Read statement and proof side by side · Permalink · Source line 423 · Claim record · Lean coverage · Code · Worked examples
Formal correspondence. Companion.companion_jump, Companion.packet_charpoly_recurrence, and Companion.packet_observable_recurrence. The source-sequence versions derive the packet recurrence from the relation \(x_{n+1}=Cx_n\). For the Fibonacci matrix \(C=\left(\begin{smallmatrix}1&1\\1&0\end{smallmatrix}\right)\), its jump trace is the Lucas number \(L_N\) and its determinant is \((-1)^N\). Thus
This specialization is FibonacciPackets.fibonacci_packet_recurrence; it is derived from the Fibonacci state.
Theorem 2.11: Dyadic–odd packet factorization
Let \(a\geq0\) and let \(M\) be a positive odd integer. The Chinese remainder map is a ring isomorphism
For \(0\leq r<2^aM\) and any coefficient sequence \(f\),
The same identity holds for formal-series coefficient selectors.
Read proof · Read statement and proof side by side · Permalink · Source line 448 · Claim record · Lean coverage · Code · Worked examples
Proof of Theorem 2.11
The two moduli are coprime. An index has the prescribed combined residue exactly when it has both component residues. Applying this equivalence to the indicator defining each selector proves the formula.
Back to statement · Read statement and proof side by side · Permalink · Source line 463 · Claim record · Lean coverage · Code · Worked examples
Formal correspondence. CRTPackets.addressEquiv, CRTPackets.residue_equivalence, CRTPackets.packet_factorization, and CRTPackets.series_packet_factorization. This theorem synchronizes finite arithmetic addresses. The passage from a family of \(p\)-adic objects to a global integer object is a separate question, discussed in Section 12.3.
2.7 Polyphase notation retained from the recovered manuscript
On this page · Permalink · Source line 479
The recovered Annals text develops a broader polyphase vocabulary. We explain it through elementary identities with explicit algebraic derivations. These identities have not been separately formalized in Lean for this consolidation. For a sequence \(a\) and \(M\geq1\), let \(a_r^{[M]}(q)=a_{Mq+r}\) for \(0\leq r<M\). If \(A(z)=\sum_n a_nz^n\) and \(A_r(w)=\sum_q a_{Mq+r}w^q\) are ordinary generating functions, then unique quotient and remainder give
For ordinary Cauchy multiplication, the phase-\(r\) product has a term without a carry and a term with one carry:
Adding the two phase addresses gives the formula. It describes ordinary Cauchy multiplication; Hurwitz convolution has its own binomial weights.
For \(M\geq1\) and \(s,r,k\in{\mathbb N}\), define the affine Mahler kernel by
It vanishes unless \(k\leq r\leq Mk+s\). For a finite binomial expansion \(f(n)=\sum_{r=0}^{D}c_r\binom nr\), the \(k\)th Newton coefficient of \(g(q)=f(Mq+s)\) is therefore
Indeed, insert the finite stencil for \(\Delta_1^k g(0)\) and interchange its two finite sums. Coefficient extraction of the binomial expansion of \(((1+z)^M-1)^k\) gives the kernel. In the binary zero-address case,
since \((2z+z^2)^k=z^k(2+z)^k\). Exact valuations for the general kernel remain to be determined. The recovered infinite analytic extensions and stronger historical identities lie beyond these finite derivations; their status is discussed in Section 12.5.