The Dirichlet convolution of two arithmetic functions is commutative, and its proof is the divisor reindexing plus the cofactor law

Identifier: F:nat-dirichlet-convolution-commutes
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

Define the Dirichlet convolution of f and g at n as the sum over the divisors d of n of f(d) times g(n/d). For every n > 0 this is symmetric in f and g. The proof introduces no new argument: reindex the sum by d -> n/d, use n/(n/d) = d at every divisor to rewrite the second factor, and commute the product. The middle step needs a pointwise congruence for the divisor aggregate bounded BY DIVISIBILITY rather than by an index bound, because n/(n/d) = d is false off the divisor set, and the unconditional congruence for a range sum cannot state that hypothesis.

Formal statement

theorem Nat.dirichlet_comm : ((x0 : ((x0 : AxNat) -> AxNat)) -> ((x1 : ((x1 : AxNat) -> AxNat)) -> ((x2 : AxNat) -> ((x3 : AxNat.lt AxNat.zero x2) -> Eq.{1} AxNat (AxNat.dirichlet x0 x1 x2) (AxNat.dirichlet x1 x0 x2)))))

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

3 direct dependencies 0 direct dependents

Evidence

kernel-Nat.dirichlet_comm

Kind: kernel-term
Status: checked

Supports: the convolution is symmetric in its two arguments at every positive n

Checker command

cargo test --release -p axeyum-lean-kernel --lib nat_prelude::arith_functions -- --test-threads=4

Evidence notes

Instantiated with the positivity DISCHARGED at a literal and at a pair (id, succ) whose convolution summands differ TERM BY TERM: at n = 6, d = 2 the left side contributes 2*4 = 8 and the right 3*3 = 9. Both totals reduce to 36. So the theorem is not confirmed by an accidental symmetry of the summand.

eval-dirichlet-small

Kind: instance-pin
Status: checked

Supports: the definition is the convolution and not the pointwise product over divisors

Checker command

cargo test --release -p axeyum-lean-kernel --lib nat_prelude::arith_functions -- --test-threads=4

Evidence notes

`Nat.dirichlet` has exactly the same type with `g d` in place of `g (n/d)`. At f = id, g = succ, n = 6 the convolution is 36 and the pointwise product is 62, and the test asserts both the positive and the negative.

kernel-Nat.isMultiplicative_totient

Kind: kernel-term
Status: checked

Supports: the multiplicativity predicate the family is stated over is inhabited by a function already proved multiplicative

Checker command

cargo test --release -p axeyum-lean-kernel --lib nat_prelude::arith_functions -- --test-threads=4

Evidence notes

Coprimality is spelled Eq (gcd a b) 1 and not Nat.Coprime, because shape_search --name Nat.Coprime returns ABSENT at declarations=2857 and Eq (gcd a b) 1 is what the existing Nat.totient_mul_of_coprime already uses. The instance test discharges the coprimality at a literal pair by Eq.refl (Nat.gcd computes at numerals) and reduces phi(2*3) to 2.

Provenance

{
  "date": "2026-09-04",
  "established_by": "axeyum lane `arithmetic-functions`, roadmap item W2-18: `nat_prelude/arith_functions_family.rs`. ADR-1619.",
  "source": "Standard; commutativity of Dirichlet convolution is the first structural fact about the ring of arithmetic functions.",
  "prior_art": [
    {
      "citation": "Mathlib, `ArithmeticFunction.mul_comm`",
      "establishes": "the same statement inside a full commutative-ring instance on arithmetic functions valued in a commutative semiring; this route has no ring structure and states the identity directly over Nat-valued functions"
    }
  ]
}