module module high

`IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions`

This module defines the Möbius function as an arithmetic function from natural numbers to integers, along with the bigOmega function. It supplies core algebraic definitions for prime-number work inside the Recognition framework. Number theorists citing arithmetic functions for inversion or factorization counts would reference it. The module consists entirely of definitions with no theorems or proofs.

claimThe Möbius function as an arithmetic function $μ:ℕ→ℤ$, together with the bigOmega function $Ω:ℕ→ℕ$.

background

The module lives in the NumberTheory.Primes namespace. It imports the Basic module, whose design reuses Mathlib’s Nat.Prime while remaining axiom-free and sorry-free, and the Squarefree module, which connects the squarefree predicate to the local valuation vp p n. The central object supplied is the Möbius function defined as an arithmetic function ℕ → ℤ.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds the parent Primes aggregator, which downstream code imports in preference to individual files. It completes the algebraic layer for arithmetic functions before any analytic number theory is added.

scope and limits

Does not prove any inversion formulas or multiplicative properties.
Does not extend into analytic number theory.
Contains no theorems, only definitions.
Depends on Mathlib and the two sibling prime modules for primitives.

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