Alphabeta MathHow statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Classical Möbius inversion over positive divisors
Statement
Let be a commutative ring and let . Then
if and only if
All divisors in the sums are positive.
Facts & Assumptions
Given: A commutative ring and functions on the positive integers.
Lower-finite poset inversion says exactly when (Möbius inversion on a lower-finite poset, with the dual upper-finite form).
The divisibility poset of positive integers is lower-finite (The divisibility poset is lower-finite, and each divisor interval factorises as a product of finite chains of prime exponents).
A finite sum is invariant under bijective reindexing (Finite commutative-monoid sums are invariant under bijective reindexing, split over disjoint unions, and satisfy the finite Fubini rule).
Proof
Apply [L1] to the lower-finite divisibility poset from [L3] and substitute [L2]. This gives .
The map is a bijection of the positive divisors of with itself and is its own inverse. Reindexing the sum in step 1.1 by [L4] gives .
Since [L1] is an equivalence, steps 1.1 and 2.1 prove both directions and both standard indexings.
Depends on
- The number-theoretic Möbius function is the poset Möbius function of divisibility: $\mu(n)=\mu_{\mid}(1,n)$
- Möbius inversion on a lower-finite poset, with the dual upper-finite form
- The divisibility poset is lower-finite, and each divisor interval factorises as a product of finite chains of prime exponents
- Finite commutative-monoid sums are invariant under bijective reindexing, split over disjoint unions, and satisfy the finite Fubini rule
Used by
- Möbius inversion gives the closed formula for the number of monic irreducibles over F_q Corollary
- Möbius inversion gives Λ=μ*log Corollary
- The Dirichlet series of Euler's totient is zeta of s minus 1 divided by zeta of s on Re s greater than 2 Corollary
- The Dirichlet series of the Möbius function is the reciprocal of the zeta Dirichlet series on Re s greater than 1 Corollary
- Euler's totient as the convolution μ*id₁ Example
- Möbius inversion of ∑_d∣ nφ(d)=n gives φ(n)=∑_d∣ nμ(d)(n/d) Example
- False: classical Möbius inversion and inclusion-exclusion are unrelated inversion principles False statement
- The summatory totient function is 3 over pi squared times x squared plus O(x log x) Theorem
Dependency tree · two levels
24 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- P. J. Cameron, Notes on Number Theory, Theorem 7.9 (standard reference, not scraped)
- Stanford Pairing-Based Cryptography notes, Möbius inversion (standard reference, not scraped)