module module high

`IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions`

Module defining the Möbius function as an arithmetic map from naturals to integers, plus related functions such as bigOmega. Number theorists in the monolith cite it when needing multiplicative arithmetic functions inside the primes namespace. The module assembles these definitions via direct imports from the Basic and Squarefree modules.

claimThe Möbius function $μ:ℕ→ℤ$, together with the total prime-factor counting function $Ω(n)$.

background

The upstream Basic module supplies axiom-free prime footholds that reuse Mathlib’s Nat.Prime while remaining sorry-free. The Squarefree module connects the standard squarefree predicate on naturals to the repo-local valuation vp p n (exponent of p in n.factorization). This ArithmeticFunctions module sits in the algebraic layer of the primes namespace and introduces the Möbius function as ℕ → ℤ.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

Feeds the parent Primes module, which acts as the namespace aggregator and states: 'Prefer importing this module (rather than individual files) from downstream code.' It supplies the Möbius function required for any later analytic number theory built on the algebraic layer.

scope and limits

Does not contain theorems or proofs.
Does not introduce axioms or sorrys.
Does not reference Recognition Science forcing chain or constants.
Limits scope to standard arithmetic functions on naturals.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.NumberTheory.Primes module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.NumberTheory.Primes.Basic module_import
IndisputableMonolith.NumberTheory.Primes.Squarefree module_import

declarations in this module (831)

abbrev mobius L24
theorem mobius_def L26
theorem mobius_prime L29
theorem mobius_prime_sq L35
theorem mobius_eq_zero_of_not_squarefree L42
theorem mobius_ne_zero_iff_squarefree L46
theorem mobius_eq_zero_iff_not_squarefree L50
theorem mobius_apply_of_squarefree L55
theorem mobius_ne_zero_iff_vp_le_one L60
abbrev bigOmega L73
theorem bigOmega_def L75
theorem bigOmega_apply L78
abbrev omega L82
theorem omega_def L84
theorem omega_apply L87
theorem bigOmega_eq_omega_of_squarefree L91
def totient L99
theorem totient_apply L101
theorem totient_one L104
theorem totient_prime L108
theorem totient_prime_pow L113
theorem totient_mul_of_coprime L119
theorem totient_divisor_sum L124
theorem totient_le L129
theorem totient_pos_iff L134
abbrev vonMangoldt L141
theorem vonMangoldt_def L143
theorem vonMangoldt_prime L146
theorem vonMangoldt_eq_zero_of_not_prime_pow L151
theorem vonMangoldt_prime_pow L156
theorem mobius_isMultiplicative L166
abbrev sigma L173
theorem sigma_def L175
theorem sigma_apply L178
theorem sigma_zero_apply L182
theorem sigma_one_apply L186
theorem sigma_isMultiplicative L190
theorem sigma_zero_prime L195
theorem sigma_one_prime L202
theorem sigma_prime L209
abbrev zeta L218
theorem zeta_def L220
theorem zeta_apply L223
theorem zeta_zero L227
theorem zeta_isMultiplicative L231
theorem moebius_mul_zeta L239
theorem zeta_mul_moebius L244
abbrev dirichletOne L249
theorem dirichletOne_def L251
theorem dirichletOne_one L254
theorem dirichletOne_ne_one L258
theorem omega_mul_of_coprime L264
theorem bigOmega_mul L270
theorem bigOmega_pow L276
def liouville L284
theorem liouville_zero L288
theorem liouville_eq L292
theorem liouville_one L296
theorem liouville_prime L300
theorem liouville_prime_pow L310
theorem liouville_mul L324
abbrev arithId L333
theorem arithId_def L335
theorem arithId_apply L338
theorem arithId_isMultiplicative L342
def primeCounting L349
theorem primeCounting_def L351
theorem primeCounting_zero L354
theorem primeCounting_one L358
theorem primeCounting_two L362
theorem primeCounting_three L366
theorem primeCounting_five L370
theorem primeCounting_ten L374
theorem primeCounting_seven L378
theorem primeCounting_eleven L382
theorem primeCounting_thirteen L386
theorem primeCounting_seventeen L390
theorem primeCounting_twenty L394
theorem primeCounting_hundred L398
theorem primeCounting_mono L402

… and 751 more