Dold Congruences and Formal Exponential Integrality

Abstract

Dold prime-power congruences imply integrality of a formal exponential.

Definition 1.1 (Prime-power congruences).

$$\forall c:\mathbb{N}\to \mathbb{Z},\mathrm{Dold}\left(c\right)⟺(\forall p:\mathbb{N},(Nat.Prime\left(p\right))⟹(\forall m:\mathbb{N},(m\ne 0)⟹((p:\mathbb{Z}{)}^{\mathrm{padicValNat}\left(p,m\right)+1}\mid (c\left(p\cdot m\right)-c\left(m\right)))))$$

Formalization. D5/S1/Recurrence/Algebraic/DoldExponentialIntegrality.Dold (✓ std3).

Citation. AINTLIB contributors (2026). AINTLIB rational local integrality and the Dieudonne-Dwork criterion. URL: https://github.com/CBirkbeck/AINTLIB/blob/1e63feb21e2dd9e54908d14c9c07058eff3ff1d4/projects/FltRegularBernoulli/BernoulliRegular/Reflection/ResidueSymbol/Furtwaengler/DieudonneDwork/DieudonneDworkCriterion.lean.

Commentary.

Dold(c) requires divisibility by p to the valuation of m plus one for every prime p and every nonzero natural m.

Definition 1.2 (The rational logarithmic input).

$$\forall c:\mathbb{N}\to \mathbb{Z},\mathrm{logInput}\left(c\right)=\mathrm{mk}\left((funn:\mathbb{N}\mapsto \frac{(c\left(n\right):\mathbb{Q})}{(n:\mathbb{Q})})\right)$$

Formalization. D5/S1/Recurrence/Algebraic/DoldExponentialIntegrality.logInput (✓ std3).

Source. Repository-derived.

Acknowledgement. AINTLIB contributors (2026). AINTLIB rational local integrality and the Dieudonne-Dwork criterion. URL: https://github.com/CBirkbeck/AINTLIB/blob/1e63feb21e2dd9e54908d14c9c07058eff3ff1d4/projects/FltRegularBernoulli/BernoulliRegular/Reflection/ResidueSymbol/Furtwaengler/DieudonneDwork/DieudonneDworkCriterion.lean.

Commentary.

The degree-n input coefficient is c(n)/n over the rationals; rational division makes the constant coefficient zero.

Theorem 1.3 (Scaling the input takes powers).

$$\forall f:\mathrm{PowerSeries}\left(\mathbb{Q}\right),(\mathrm{constantCoeff}\left(f\right)=0)⟹(\forall n:\mathbb{N},\mathrm{subst}\left(HSMul.hSMul\left(n,f\right),\exp \left(\mathbb{Q}\right)\right)=\mathrm{subst}{\left(f,\exp \left(\mathbb{Q}\right)\right)}^n)$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Algebraic/DoldExponentialIntegrality.expSeries_nsmul (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. AINTLIB contributors (2026). AINTLIB rational local integrality and the Dieudonne-Dwork criterion. URL: https://github.com/CBirkbeck/AINTLIB/blob/1e63feb21e2dd9e54908d14c9c07058eff3ff1d4/projects/FltRegularBernoulli/BernoulliRegular/Reflection/ResidueSymbol/Furtwaengler/DieudonneDwork/DieudonneDworkCriterion.lean.

Commentary.

Substitution into PowerSeries.exp_pow_eq_rescale_exp gives the natural-scaling identity.

Theorem 1.4 (Exponential of a sum).

$$\forall f:\mathrm{PowerSeries}\left(\mathbb{Q}\right),\forall g:\mathrm{PowerSeries}\left(\mathbb{Q}\right),(\mathrm{constantCoeff}\left(f\right)=0)⟹((\mathrm{constantCoeff}\left(g\right)=0)⟹(\mathrm{subst}\left(f+g,\exp \left(\mathbb{Q}\right)\right)=\mathrm{subst}\left(f,\exp \left(\mathbb{Q}\right)\right)\cdot \mathrm{subst}\left(g,\exp \left(\mathbb{Q}\right)\right)))$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Algebraic/DoldExponentialIntegrality.expSeries_add (✓ std3). ∎

Source. Repository-derived.

Commentary.

For two rational formal series with zero constant coefficients, substituting their sum into the exponential gives the product of the two substituted exponentials.

Theorem 1.5 (Dold congruences imply integrality).

$$\forall c:\mathbb{N}\to \mathbb{Z},(\mathrm{Dold}\left(c\right))⟹(\forall n:\mathbb{N},\exists z:\mathbb{Z},\mathrm{coeff}\left(n,\mathrm{subst}\left(\mathrm{logInput}\left(c\right),\exp \left(\mathbb{Q}\right)\right)\right)=(z:\mathbb{Q}))$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Algebraic/DoldExponentialIntegrality.integral_exp_of_dold (✓ std3). ∎

Citation. AINTLIB contributors (2026). AINTLIB rational local integrality and the Dieudonne-Dwork criterion. URL: https://github.com/CBirkbeck/AINTLIB/blob/1e63feb21e2dd9e54908d14c9c07058eff3ff1d4/projects/FltRegularBernoulli/BernoulliRegular/Reflection/ResidueSymbol/Furtwaengler/DieudonneDwork/DieudonneDworkCriterion.lean.

Commentary.

Apply the sufficient Dieudonne-Dwork criterion at each prime. The Dold congruences make the logarithmic difference locally integral; a rational coefficient integral at every prime has denominator one. The local-integrality induction is adapted from AINTLIB.

References

• Truth anchor: D5/S1/Recurrence/Algebraic/DoldExponentialIntegrality.Dold
• Truth anchor: D5/S1/Recurrence/Algebraic/DoldExponentialIntegrality.expSeries_add
• Truth anchor: D5/S1/Recurrence/Algebraic/DoldExponentialIntegrality.expSeries_nsmul
• Truth anchor: D5/S1/Recurrence/Algebraic/DoldExponentialIntegrality.integral_exp_of_dold
• Truth anchor: D5/S1/Recurrence/Algebraic/DoldExponentialIntegrality.logInput
• Dependency: D5/S1/Recurrence/Algebraic/HannaLogarithmicPowerClosure
• Dependency: D5/S1/Recurrence/Invariants/CubicFifteenSubstitutionParity
• Dependency: D5/S1/Recurrence/LinearRows/LinearExponentDyadicSupport
• Dependency: D5/S1/Recurrence/Residue/ParametricExponentialSquareCongruence