Congruential Euler packets and their arithmetic

Proof of Proposition 3.2

Proceed by induction in the recurrence (3.3). For every \(q<n\), the product \(D_{N,j}(q)\) divides \(D_{N,j}(n-1)\). Multiplying the recurrence by \(D_{N,j}(n-1)\) therefore makes every previous term integral. The diagonal factor completes the product \(D_{N,j}(n)\), proving the claim. At \(n=0\), both factors are one. This gives a uniform denominator bound without requiring integrality of the normalized coefficients themselves. The Lean statements are KomorebiPaperIX.Congruential.clearing_product and KomorebiPaperIX.Congruential.universal_denominator_clearing.

Back to statement · Read statement and proof side by side · Permalink · Source line 65 · Claim record · Lean coverage · Code · Worked examples

Proof of Proposition 3.5

Lucas reduction separates the lowest base-\(p\) digits, which are \(j\) and zero in the upper and lower arguments. Their binomial contribution is one, leaving the displayed reduced row. On the diagonal the reduced coefficient is one. The recurrence (3.3) therefore constructs an integral packet by successive division by units in \({\mathbb Z}_p\). After reduction, every address satisfies the same triangular system over \({\mathbb F}_p\). Its diagonal entries are one, so its solution is unique. This proves both the common reduction and the congruence between addresses. The row reduction is KomorebiPaperIX.StandardWindow.lucas_row_reduction. The integral identification and the two reduction statements are KomorebiPaperIX.WindowIndependence.standard_window_integral, KomorebiPaperIX.WindowIndependence.coeffPadic_coe, KomorebiPaperIX.WindowIndependence.residue_independence, and KomorebiPaperIX.WindowIndependence.two_window_addresses_congruent.

Back to statement · Read statement and proof side by side · Permalink · Source line 146 · Claim record · Lean coverage · Code · Worked examples

Proof of Theorem 3.7

Work in the Hurwitz integral ring of formal series

For \(D=d/dt\), let \(B_p=(D^{p^2}-D^p)/p\). Call \(F\) flat if \(B_p^sF\in\mathcal H_p\) for every \(s\ge0\). We will prove that \(j!\mathcal P_{N,j}\) is flat at every address. The main difficulty is to include the addresses at which the usual unit-pivot argument fails.

Set

The denominator of this last quotient has nonzero constant coefficient. The section identities give

Cancellation of consecutive source sections proves the product identity and ties the ratios directly to the family under study.

At the singular addresses \(c=ap\), \(1\le a<m\), use the weighted ring

The key estimate is \(R_{ap}(\log(1+T))\in\mathcal W_p\). Its arithmetic input comes from the cyclic group ring \({\mathbb Z}[{\mathbb Z}/N{\mathbb Z}]\). For its canonical element \(x\) and \(I=(p,x^{p-1}-1)\), the relation \((x^{p-1})^p=1\) implies \(I^p\subseteq(p)I\). Induction yields \(I^q\subseteq(p^{v_p(q!)})\). Grouping the falling factorial \((x)_d=\prod_{i=0}^{d-1}(x-i)\) into consecutive blocks of length \(p\) then gives an integral residue-coordinate factor \(p^{v_p(\lfloor d/p\rfloor!)}\). The identity

accounts for precisely the weight in \(\mathcal W_p\) after dividing by \(d!\). Comparison of the section and group-ring recurrences identifies these coordinates with the logarithmically substituted section.

To pass from the section to the singular ratio, factor out its initial zero: for \(c=ap\), the section has the form

The weight of \(c!\) compensates for the coefficient shift by \(c\). The weighted ring is closed under inversion of series with constant coefficient one and under \(L_T=\log(1+T)(1+T)d/dT\). With \(\ell(T)=\log(1+T)/T\), interpreted by coefficient shifting, differentiation of the displayed factorization gives

Since \(p\ell(T)\in\mathcal W_p\) and \(p\mid c\), both terms are weighted. This is the singular estimate KomorebiPaperIX.SingularRatioAmice.paper_singular_amice_estimate.

To deduce flatness from the weighted estimate, use \(\Theta=(1+T)d/dT\). Both \(\Theta\) and \((\Theta^{p^2}-\Theta^p)/p\) preserve \(\mathcal W_p\). For the first operator, its coefficient formula is \((d+1)a_{d+1}+da_d\); whenever the floor weight rises, the factor \(d+1\) provides the missing \(p\). For the second operator, the proof uses its full Leibniz correction and the scalar congruence \(p^2\mid b^{p^2}-b^p\). Weighted monomials factor as

The operator preserves these monomials and hence finite weighted polynomials. Each fixed output coefficient depends on only finitely many input coefficients, which extends the result to the formal series. Substitution \(T=e^t-1\) intertwines \(D\) with \(\Theta\) and maps \(\mathcal W_p\) into \(\mathcal H_p\), because

It follows that the singular ratios are flat. This transfer is proved in KomorebiPaperIX.WeightedDworkTransfer.singular_ratio_flat.

At a nonsingular address \(2\le c<N\) with \(p\nmid c\), differentiation of the section identities gives

Writing \(q=R_{c-1}-(c-1)\) and \(y=R_c-c\), this becomes

On degrees divisible by \(p\), the inverse of \(tD+c\) divides the degree-\(d\) coefficient by the unit \(d+c\). Starting with \(y_0=0\), form

Flatness and support are preserved. Indeed, put \(E_c=tD+c\) and \(C_p=pD^{p^2}-D^p\). The commutator is \([B_p,E_c]=C_p\), and iteration gives

For the inverse equation \(E_cy=f\), induction on \(r\) makes the correction term Hurwitz-integral. Both operators preserve support in degrees divisible by \(p\). On that support the degree multiplier \(d+c\) is a unit, so integrality of \(E_cB_p^ry\) implies integrality of \(B_p^ry\). Thus the inverse preserves full flatness, as well as support. Since the difference of two right sides factors as \((z-y)(q-z-y)\) and its second factor has zero constant term, agreement with the solution gains one coefficient at each iteration. Consequently \([t^d]y_s=[t^d]y\) for \(d\le s\). Every coefficient of \(B_p^r y\) can therefore be read from a sufficiently long finite iterate. The argument is entirely formal. This is the content of KomorebiPaperIX.RiccatiFlatPropagation.riccati_solution_flat.

The standard window supplies the initial ratio \(R_1\). The weighted estimate handles \(p\mid c\), and Riccati propagation handles \(p\nmid c\). Flatness is closed under products, so the exact factorization establishes flatness of \(j!\mathcal P_{N,j}\). Extracting its supported Hurwitz coefficients and applying the proved saturation and step-multiple lemmas yields (3.5)–(3.6).

Here is the coefficient extraction explicitly. If \(a_d=d![t^d]F\), then

For \(F=j!\mathcal P_{N,j}\) and \(k\le mn\), take \(d=mpn-pk\). Support in multiples of \(mp\) turns this into \(p^{-k}\Delta_h^kU_{N,j}(n)\), so flatness gives divisibility by \(p^k\). For \(k>mn\), expand \(\Delta_h^{k-mn}\) applied to \(\Delta_h^{mn}U_{N,j}(n)\); every shifted row is at least \(n\), so each summand is divisible by \(p^{mn}\). Finally \(\Delta_{uh}=((I+\Delta_h)^u-I)\), whose \(k\)th power for \(u>0\) is an integral combination of powers of \(\Delta_h\) of order at least \(k\). The case \(u=0\) gives zero for \(k>0\), and order zero is the original integral coefficient. This proves the bound for all \(u\) and \(k\). Finally \(\Delta_{uh}^kU_{N,j}=j!\Delta_{uh}^kC_{N,j}\) gives (3.7), with the zero case retained. The resulting statements are KomorebiPaperIX.AllResidueEuler.all_residue_flat, KomorebiPaperIX.AllResidueEuler.global_unnormalized_bound, and KomorebiPaperIX.AllResidueEuler.global_normalized_precision.

Back to statement · Read statement and proof side by side · Permalink · Source line 203 · Claim record · Lean coverage · Code · Worked examples

Proof of Corollary 3.9

Since \(j<p\), the factorial \(j!\) is a unit in \({\mathbb Z}_p\). Also \(mn\ge1\). The order-one case of Theorem 3.7 therefore gives valuation at least one for the normalized difference at every step \(uh\). This proves the congruence, and Proposition 3.5 identifies its reduction with the equality for \(\overline C_m\). The preserved Lean development also proves this period directly from the Hurwitz inverse in characteristic \(p\): KomorebiPaperIX.WindowPeriod.uniform_standard_window_period, KomorebiPaperIX.WindowPeriod.multiple_period, and KomorebiPaperIX.WindowPeriod.standard_window_period_divisibility.

Back to statement · Read statement and proof side by side · Permalink · Source line 399 · Claim record · Lean coverage · Code · Worked examples

Proof of Lemma 3.10

The finite Newton expansion gives

Terms with \(k\ge r\) have the required factor from the difference. For \(1\le k<r\), the identity

and \(v_p(k)<k\) imply \(p^r\mid\binom{p^{r-1}}k p^k\) in \({\mathbb Z}\). Mapping that integer divisibility to \(R\) proves the claim term by term. The argument includes \(r=1\). The declaration is KomorebiPaperIX.PeriodFromDifferences.prime_power_period.

Back to statement · Read statement and proof side by side · Permalink · Source line 422 · Claim record · Lean coverage · Code · Worked examples

Proof : Proof of Theorem 3.6

On the divisor branch, \(m\mid q\) and the packet step \(q/m\) is an integer multiple of \(h=(p-1)/m\). If \(r\le mn\), Theorem 3.7 supplies the hypotheses of Lemma 3.10. Its packet displacement is \(p^{r-1}q/m\), which converts to the original degree as follows:

The choice \(n\ge r\) implies \(mn\ge r\) because \(m\ge1\).

For an odd prime, \(2\mid p-1\), so the option \(m=2\) introduces no further case. The sole remaining branch is \(p=2,m=2,N=4\). The all-row theorem proved next gives \(2^k\mid\Delta_1^kC_{4,j}(n)\) at every row and address. After multiplying by \(j!\), Lemma 3.10 gives packet period \(2^{r-1}\) and degree displacement \(4\cdot2^{r-1}=2^{r+1}=qp^r\). It also gives integrality. Hence the complete statement follows. The formal degree conversion is KomorebiPaperIX.NishibuchiCompletion.original_degree_shift; the all-parameter degree theorem is KomorebiPaperIX.NishibuchiCompletion.full_period_degree.

Permalink · Source line 441

Proof of Theorem 3.11

The Hurwitz coefficients of the normalized source \(K_{4,j}\) at degrees \(4n\) are

Their explicit expressions are

Every denominator is odd. An affine sequence with even slope satisfies \(2^k\mid\Delta_1^k f(n)\) for every \(k,n\). The exact product identity

proves closure of this property under products. Applying the formula with the factors interchanged to \(fg=1\) isolates \(f(n+s)\Delta_1^sg(n)\). Multiplication by \(f(n+s)^{-1}\) and induction then prove closure under pointwise unit inverses. Thus all four \(g_j\) have the property. The explicit formulas and difference bounds are formalized in KomorebiPaperIX.DyadicFourKernel.source_coe and KomorebiPaperIX.DyadicFourKernel.source_kummer.

For an integer charge \(c\), put

A series is flat of charge \(c\) when applying any power \(A_c^s\) to it gives an element of \(\mathcal H_2\). The required product formula is

All middle coefficients are integral. Derivatives preserve \(\mathcal H_2\) and commute with \(A_c\). Induction on the number of iterations in (3.11) proves that multiplication adds charges. If \(FG=1\), the same formula yields

Induction, starting from the independently established integrality of the reciprocal \(G\), proves that inversion negates the charge. Finally \(A_{c+2}=A_c-1\), so increasing a charge by two preserves flatness. These are KomorebiPaperIX.ChargedDworkClosure.B_mul, KomorebiPaperIX.ChargedDworkClosure.flat_inverse, and KomorebiPaperIX.ChargedDworkClosure.flat_charge_shift.

Packing \(g_j\) into degrees divisible by four gives \(K_{4,j}\). Its source property is precisely charge-one flatness. Inversion gives charge \(-1\), and the charge shift restores charge one for the reciprocal \(\mathcal P_{4,j}\). If \(\operatorname{dec}(F)(d)=d![t^d]F\), the exact coefficient identity is

At \(d=4n\), packing turns the right side into \(2^{-s}\Delta_1^sC_j(n)\). This extraction requires no negative degree and therefore holds at every \(n\), including zero. It proves the unit-step bound KomorebiPaperIX.DyadicFourAllRows.base_step_bound.

To incorporate \(v_2(u)\), expand a displacement using finite Newton coefficients. For any prime \(p\), \(u>0\), and \(1\le a\le u\),

as follows from \(a\binom ua=u\binom{u-1}{a-1}\) and \(v_p(a)<a\). Repeated displacement, retaining the remaining base-difference order at each induction step, gives a factor \(p^{k(1+v_p(u))}\) from \(k\) displacements. This induction is formalized in KomorebiPaperIX.StepAmplification.repeated_precision. Applying it with \(p=2\) proves (3.9); multiplication by \(j!\) proves (3.10). Zero step and zero order follow from their definitions. The final statements are KomorebiPaperIX.DyadicFourFinalStrengthening.normalized_step_bound and KomorebiPaperIX.DyadicFourFinalStrengthening.unnormalized_step_bound.

Back to statement · Read statement and proof side by side · Permalink · Source line 481 · Claim record · Lean coverage · Code · Worked examples

Proof of Corollary 3.12

Apply the same repeated-displacement theorem with the fixed cap \(mn\) to (3.6). The argument preserves this cap and improves the contribution from the order of the difference. Division by the fixed factorial gives the rational valuation statement, with the zero case included. These are KomorebiPaperIX.AllResidueStepAmplification.unnormalized_precision and KomorebiPaperIX.AllResidueStepAmplification.normalized_precision.

Back to statement · Read statement and proof side by side · Permalink · Source line 579 · Claim record · Lean coverage · Code · Worked examples

Proof of Corollary 3.13

Use Lemma 3.10 and the unit-step case of Theorem 3.11. At \(j=2,3\) the factorial contributes an additional power of two. The original degree versions are KomorebiPaperIX.DyadicFourFinalStrengthening.all_rows_period_degree and KomorebiPaperIX.DyadicFourFinalStrengthening.all_rows_half_period_degree. The next theorem sharpens these sufficient periods to a complete classification.

Back to statement · Read statement and proof side by side · Permalink · Source line 600 · Claim record · Lean coverage · Code · Worked examples

Proof of Lemma 3.14

Finite Newton reconstruction at an arbitrary row gives

The monotonicity of \(\lfloor\log_2k\rfloor\) therefore preserves the higher-coefficient bound after translation. In addition, \(\Delta_1f(n)-a_1\in2^{c+1}{\mathbb Z}_2\), so the first difference is nonzero of exact valuation \(c\).

Now expand the displacement:

For \(1\le k\le T\), the binomial denominator identity implies

Every term of the remaining sum consequently has valuation at least \(v_2(T)+c+1\). Its sum cannot cancel the leading term, which has exact valuation \(v_2(T)+c\). This proves nonvanishing and the claimed valuation using only finite sums. The general theorem is KomorebiPaperIX.NewtonDominance.exact_displacement.

Back to statement · Read statement and proof side by side · Permalink · Source line 626 · Claim record · Lean coverage · Code · Worked examples

Proof of Theorem 3.15

The first Newton coefficients, derived from (3.3), are

Their exact valuations are \(c_j\). Theorem 3.11 gives \(v_2(a_{j,k})\ge k\) for all orders. To obtain the stronger logarithmic envelope required by Lemma 3.14, only a finite initial segment needs improvement. The recurrence proves the following exact valuations:

For all subsequent \(k\), the elementary inequality \(c_j+1+\lfloor\log_2k\rfloor\le k\) completes the envelope. The entries follow by exact rational computation from the defining recurrence, and their valuations are proved in Lean. Together with the inequality for all subsequent orders, they establish the bound at every order. The uniform envelope is KomorebiPaperIX.DyadicFourPrefix.tail_precision.

Apply Lemma 3.14 to \(C_j\). Multiplication by the nonzero factorial \(j!\) adds \(v_2(j!)\) and preserves nonzeroness. Hence \(d_j=c_j+v_2(j!)\), giving the four valuation gains for the original coefficients. The declarations are KomorebiPaperIX.DyadicFourLeastPeriods.normalized_exact_displacement and KomorebiPaperIX.DyadicFourLeastPeriods.exact_displacement.

Back to statement · Read statement and proof side by side · Permalink · Source line 669 · Claim record · Lean coverage · Code · Worked examples

Proof of Corollary 3.16

By the exact displacement law, the congruence at any row is equivalent to \(v_2(T)+d_j\ge r\). This is exactly the displayed integer divisibility criterion. Its least positive solution is the indicated power of two, which also covers \(r=0\) and \(r\le d_j\). The all-period and least-element statements are KomorebiPaperIX.DyadicFourLeastPeriods.period_iff_dvd and KomorebiPaperIX.DyadicFourLeastPeriods.least_packet_period.

Back to statement · Read statement and proof side by side · Permalink · Source line 726 · Claim record · Lean coverage · Code · Worked examples

Proof of Theorem 3.18

The exponential generating series of the source is the finite sum

Multiplication by \(\cosh t\) telescopes. Since \(p\) is odd,

Taking its even part gives

Multiplication by the reciprocal \(\operatorname{sech}^2(pt)\) yields \(\operatorname{sech}t\). The EGF product rule now gives the reconstruction coefficient by coefficient. Replacing \(m\) by \(n-q\) produces the displayed lower triangular row. Its diagonal and weights follow from \(\gamma_0=1\) and the explicit factor \(p^{2(n-q)}\). The source-series identity is KomorebiPaperIX.OddPower.odd_source_even_egf; the reconstruction and row statement are KomorebiPaperIX.OddEuler.odd_euler_reconstruction and KomorebiPaperIX.OddEuler.row_action.

Back to statement · Read statement and proof side by side · Permalink · Source line 812 · Claim record · Lean coverage · Code · Worked examples

Proof of Corollary 3.19

Every omitted summand has \(m\ge M+1\), hence contains the integer factor \(p^{2m}\) divisible by \(p^{2M+2}\). All its other factors are integral. The finite sum of these omitted terms proves the assertion, with the empty-tail case giving exact equality. These are KomorebiPaperIX.OddEuler.odd_euler_supercongruence and KomorebiPaperIX.OddEuler.full_depth_exact.

Back to statement · Read statement and proof side by side · Permalink · Source line 847 · Claim record · Lean coverage · Code · Worked examples

Proof of Lemma 3.21

The ordinary kernel coefficients of \((\sinh z/z)^2\), in \(z^2\), are

Legendre's strict factorial bound \(v_2((2m+2)!)<2m+2\) makes them integral. Their constant coefficient is one. The coefficient recurrence for its reciprocal therefore proves integrality of every \(\beta_m\). For the source factor, lifting the exponent at the even power \(2n+2\) gives

Its denominator has the same valuation, since \(2n+1\) is odd. Thus \(A(n)\) is a nonzero unit.

Its exponential generating function is

The quotients by powers of \(t\) are well defined because the required initial coefficients vanish. The hyperbolic identity

then gives the exact formal-series product

Taking the factorial-scaled coefficient of \(t^{2n}\) produces the stated finite sum. Full depth leaves no omitted terms. The relevant declarations are KomorebiPaperIX.Dyadic.beta_integral, KomorebiPaperIX.Dyadic.source_valuation, KomorebiPaperIX.DyadicSeries.dyadic_reconstruction_series, and KomorebiPaperIX.DyadicReconstruction.dyadic_reconstruction.

Back to statement · Read statement and proof side by side · Permalink · Source line 909 · Claim record · Lean coverage · Code · Worked examples

Proof of Lemma 3.22

Let \(Q(z)=z\coth z\), the regular formal series with constant coefficient one. The elementary differential identity

and the Bernoulli expansion

give \(\beta_m=-2^{2m}(2m-1)B_{2m}/(2m)!\). Multiplication by \(2^{2m}(2m)!\) proves the identity for \(\kappa_m\). The Bernoulli denominator theorem gives \(v_2(B_{2m})=-1\) for \(m>0\): its denominator contains each prime \(q\) with \((q-1)\mid 2m\) exactly once, including \(2\)[DLMF24]. Since \(2m-1\) is odd, the valuation is exactly \(4m-1\). This also proves nonvanishing. In Lean, the hyperbolic identity is proved after clearing removable zeros. The library Bernoulli theorem then determines the valuation of \(\kappa_m\). The declarations are KomorebiPaperIX.DyadicSharpTower.kappa_bernoulli and KomorebiPaperIX.DyadicSharpTower.kappa_valuation.

Back to statement · Read statement and proof side by side · Permalink · Source line 959 · Claim record · Lean coverage · Code · Worked examples

Proof of Theorem 3.23

Rewrite the summand exactly as

For \(m>M\), its first factor is divisible by \(2^{4m-1}\), the binomial coefficient is integral, and \(A(n-m)\) is a unit. Hence every omitted summand is divisible by \(2^{4M+3}\). Summing the finite tail proves (3.14). If \(M\ge n\), the tail is empty and the statement includes the resulting zero error.

At \(n=M+1\) there is exactly one omitted summand. Here \(\binom{2n}{2n}=1\) and \(A(0)=1\), so the error is \(\kappa_{M+1}\). Lemma 3.22 gives its exact valuation \(4M+3\) and nonvanishing. The statements are KomorebiPaperIX.DyadicSharpTower.dyadic_supercongruence_sharp, KomorebiPaperIX.DyadicSharpTower.first_omitted_error, and KomorebiPaperIX.DyadicSharpTower.first_omitted_error_valuation.

Back to statement · Read statement and proof side by side · Permalink · Source line 994 · Claim record · Lean coverage · Code · Worked examples

Proof of Proposition 3.24

Use the same factorization of \(S_m(n)\), the nonzero binomial coefficient for \(m\le n\), the exact valuation of \(\kappa_m\), and the unit property of \(A(n-m)\). The tail conclusion follows by addition in \(2^L{\mathbb Z}_2\). These are KomorebiPaperIX.DyadicSharpTower.summand_valuation and KomorebiPaperIX.DyadicSharpTower.dyadic_supercongruence_row_weight.

Back to statement · Read statement and proof side by side · Permalink · Source line 1026 · Claim record · Lean coverage · Code · Worked examples

Proof of Theorem 3.25

For \(n>0\), the displacement law at row zero gives \(v_2(U_j(n)-j!)=v_2(n)+d_j\), so \(f_j(n)\in{\mathbb Z}_2\). The value at zero is zero. Applying the same law to the smaller of two unequal natural numbers shows

The natural numbers are dense in \({\mathbb Z}_2\), and the target is complete. The map therefore extends continuously. The distance identity extends on the dense product of natural-number points, making the extension an isometry. Density also proves uniqueness among all continuous maps with these prescribed values.

To prove surjectivity, use compactness. For an isometry \(g\) of a compact metric space into itself, the sequence of iterates \(g^n(x)\) has a convergent subsequence. Two sufficiently close iterates, with exponents \(a<b\), yield \(d(x,g^{b-a}(x))\) equally small after removing \(a\) isometric iterations. Since \(b-a>0\), the latter point is in the image of \(g\). Thus the image is dense. It is also compact and hence closed, so it is the whole space. Apply this to \(\Phi_j\) on \({\mathbb Z}_2\).

The general ingredients are KomorebiPaperIX.DensePadicIsometry.existsUnique_extensionEquiv and KomorebiPaperIX.CompactSelfIsometry.surjective. The packet specialization is KomorebiPaperIX.DyadicFourIsometry.existsUnique_isometry; uniqueness among continuous maps is KomorebiPaperIX.DyadicFourIsometry.unique_continuous.

Back to statement · Read statement and proof side by side · Permalink · Source line 1057 · Claim record · Lean coverage · Code · Worked examples

Proof of Corollary 3.26

The formula agrees with \(U_j\) on every natural number. Continuity and the distance equality follow from the corresponding properties of \(\Phi_j\). Its surjectivity gives precisely the displayed affine image, and multiplication by the nonzero scalar \(2^{d_j}\) preserves injectivity. The declarations are KomorebiPaperIX.DyadicFourIsometry.originalExtension_nat, KomorebiPaperIX.DyadicFourIsometry.originalExtension_dist, and KomorebiPaperIX.DyadicFourIsometry.originalExtension_range.

Back to statement · Read statement and proof side by side · Permalink · Source line 1102 · Claim record · Lean coverage · Code · Worked examples