A sum over the divisors of a positive n is unchanged by the substitution d -> n/d, because the map that fixes the non-divisors is a genuine involution

Identifier: F:nat-divisor-aggregate-reindex
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For every f : Nat -> Nat and every n > 0, the sum of f over the divisors of n equals the sum of d -> f (n/d) over the same divisors. The reindexing is NOT carried by the map d -> n/d itself, which is not injective on the range [0, n] that the sum walks -- at n = 6 it sends 4, 5 and 6 all to 1 -- but by the map that sends a divisor to its cofactor and FIXES every non-divisor. That map is an involution on all of Nat (a divisor's cofactor is again a divisor and returns; a non-divisor returns immediately), hence injective with no range bound at all, and it lands inside [0, n], which is exactly the pair of hypotheses the permutation law for sums consumes. Positivity is load-bearing in both halves: at n = 0 every d divides and the map collapses onto 0.

Formal statement

theorem Nat.sumDivisorsBy_reindex : ((x0 : ((x0 : AxNat) -> AxNat)) -> ((x1 : AxNat) -> ((x2 : AxNat.lt AxNat.zero x1) -> Eq.{1} AxNat (AxNat.sumDivisorsBy x0 x1) (AxNat.sumDivisorsBy (fun (x3 : AxNat) => x0 (AxNat.div x1 x3)) x1))))

Dependencies

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

3 direct dependencies 1 direct dependents

Evidence

kernel-Nat.sumDivisorsBy_reindex

Kind: kernel-term
Status: checked

Supports: the reindexed sum equals the original for every summand and every positive n

Checker command

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

Evidence notes

The instance test discharges the hypothesis at a literal -- positivity from `Nat.zero_lt_succ`, so no local context and no assumed premise -- and then reduces each side to 12. The equation is between two computed numbers, not between two stuck terms. A second instance at the summand `fun k => k+1` reduces to 16 on the left.

kernel-Nat.divisorFlip_involutive

Kind: kernel-term
Status: checked

Supports: the map that fixes the non-divisors is an involution, which is what makes it injective with no range bound

Checker command

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

Evidence notes

Instantiated at EVERY point of [0,6] -- the four divisors 1, 2, 3, 6 and the three non-divisors 0, 4, 5 -- with the positivity discharged and both sides reduced. The non-divisors are the half the naive `fun n k => n / k` gets wrong, and they are the reason `divisorFlip_injectiveOn` needs no bound.

eval-divisor-aggregate-small

Kind: instance-pin
Status: checked

Supports: the aggregate runs over ALL divisors including n itself and excluding 0, and it really applies its summand

Checker command

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

Evidence notes

The trusted gate cannot tell you a Definition is wrong: `Nat.sumDivisorsBy` has exactly the same type with the bound `n` in place of `succ n` (the proper-divisor reading) or with `0` counted as a divisor. Each wrong reading is named with the number it would produce -- numDivisors 6 is 4, and NOT the proper-divisor 3, and NOT the zero-counting 5. `dvdB` is exercised at both degenerate arguments: `dvdB 0 0` is true and `dvdB 0 6` is false, matching `Nat.dvd`'s own convention that 0 divides 0 alone.

shape-Nat.sumDivisorsBy

Kind: exhaustive-enumeration
Status: checked

Supports: nothing of this shape existed before, and the monomorphic Nat.sumDivisors that did exist is now provably an instance

Checker command

cargo run --release -q -p axeyum-lean-kernel --example shape_search -- --name Nat.sumDivisorsBy_reindex --kind theorem --expect 1

Evidence notes

Pre-state, measured at declarations=2857 with the positive control Nat.Finset.forallSubset_of_search FOUND 1 -- a declaration that landed the same day, so the index is not merely non-empty but current: --name-like returned ABSENT for dvdB, sumDivisorsBy, numDivisors, divisorFlip, moebius, mobius, dirichlet, IsMultiplicative and inclusionExclusion. Nat.sumDivisors was FOUND 1 as a definition of arity 1 -- present but monomorphic, which is the gap this closes.

Provenance

{
  "date": "2026-09-04",
  "established_by": "axeyum lane `arithmetic-functions`, roadmap item W2-18: `nat_prelude/arith_functions.rs` declares the polymorphic divisor aggregate `Nat.sumDivisorsBy`, the involution `Nat.divisorFlip`, and this reindexing. ADR-1619.",
  "source": "The classical d <-> n/d pairing of divisors. Standard, and in a classical development invisible, because there the divisor set is a Finset and the pairing is a bijection between finite sets rather than a self-map of an interval.",
  "prior_art": [
    {
      "citation": "Mathlib, `Nat.sum_div_divisors`",
      "establishes": "the same reindexing over `Nat.divisors`, a Finset built by filtering `Finset.range`; that route needs the Finset quotient, while this one permutes an interval and has an empty axiom footprint"
    }
  ]
}