The Moebius function lands on a carrier without negatives as a pair of Nat-valued halves whose sum is its absolute value and whose product is zero

Identifier: F:nat-moebius-as-a-graded-pair
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

The Moebius function takes values in {-1, 0, 1} and the natural numbers have no negatives, so mu is declared as two Nat-valued functions: moebiusPos n is 1 exactly when mu(n) = +1 and moebiusNeg n is 1 exactly when mu(n) = -1, each 0 unless n is squarefree. Two theorems make the pair behave as one signed quantity: their sum is the absolute value of mu(n), and their product is 0, so at most one half is nonzero. Both are proved by the three-way case split the definitions make -- not squarefree; squarefree with an even number of prime factors; squarefree with an odd number.

Formal statement

theorem Nat.moebius_pos_add_neg : ((x0 : AxNat) -> Eq.{1} AxNat (AxNat.add (AxNat.moebiusPos x0) (AxNat.moebiusNeg x0)) (AxNat.moebiusAbs x0))

Dependencies

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

1 direct dependencies 0 direct dependents

Evidence

eval-moebius-classical-values

Kind: instance-pin
Status: checked

Supports: the pair really encodes mu, with the sign convention the right way round

Checker command

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

Evidence notes

mu(1) = +1, mu(2) = -1, mu(3) = -1, mu(4) = 0, mu(5) = -1, mu(6) = +1, each read off both halves and off moebiusAbs, with every value reduced by the kernel. The parity-flipped definition has exactly the same type and would swap the n = 2 and n = 6 rows, so those two instances are what separate the readings. Magnitudes stay at or below 6 because every Nat numeral in this kernel is unary and both Squarefree and Nat.factorization are fuel-bounded searches.

kernel-Nat.moebius_pos_add_neg

Kind: kernel-term
Status: checked

Supports: the two halves carry exactly the absolute value of mu between them

Checker command

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

Evidence notes

Instantiated at n = 6 (squarefree, even omega), n = 2 (squarefree, odd omega) and n = 4 (not squarefree) -- all three branches of the proof's own case split, so no branch is confirmed only by the other two.

Provenance

{
  "date": "2026-09-04",
  "established_by": "axeyum lane `arithmetic-functions`, roadmap item W2-18: `nat_prelude/arith_functions_family.rs`. ADR-1619, following ADR-0603's graded-statement-family shape.",
  "source": "The Moebius function, standard since 1832. What is not standard is the encoding: a classical development gives mu a signed codomain and never faces this question.",
  "prior_art": [
    {
      "citation": "Mathlib, `ArithmeticFunction.moebius`, valued in the integers",
      "establishes": "the same function with a signed codomain; the graded-pair encoding here exists because the divisor aggregate this family is built on is Nat-valued and no Int-valued range-sum toolkit exists in the tree"
    }
  ]
}