mobius_twothousandthreehundredten
The Möbius function evaluates to -1 at 2310, confirming the integer is square-free with five distinct prime factors. Analytic number theorists working on Dirichlet inversion or inclusion-exclusion would reference this explicit value for calculations involving 2310. The proof is a direct computational check via native_decide on the arithmetic-function definition.
claim$μ(2310) = -1$, where $μ$ is the Möbius arithmetic function from $ℕ$ to $ℤ$.
background
The module supplies lightweight wrappers around Mathlib's arithmetic functions, beginning with the Möbius function $μ$ (implemented as the abbrev mobius for ArithmeticFunction.moebius). By definition $μ(n)$ returns 0 when $n$ is not square-free and otherwise equals $(-1)^k$ for $k$ the number of distinct prime factors. The local setting is a collection of small footholds for later Dirichlet algebra and inversion, kept deliberately lightweight.
proof idea
One-line wrapper that applies native_decide to evaluate the Möbius function at 2310.
why it matters in Recognition Science
This supplies a concrete numerical instance inside the arithmetic-functions module, verifying the expected sign for a product of five distinct primes. No downstream theorems currently cite it, but it supports explicit checks that can feed into broader prime-factorization or square-free properties. It stays within the module's stated scope of basic interfaces rather than touching Recognition Science forcing chains or constants.
scope and limits
- Does not prove the general formula for the Möbius function.
- Does not compute the function at any integer other than 2310.
- Does not link to Recognition Science forcing chains, phi-ladder, or physical constants.
- Does not establish new properties of highly composite numbers.
formal statement (Lean)
1384theorem mobius_twothousandthreehundredten : mobius 2310 = -1 := by native_decide
proof body
Term-mode proof.
1385
1386/-! ### Highly composite numbers -/
1387
1388/-- 12 is highly composite (has more divisors than any smaller positive integer). -/