mobius_prime_sq
The theorem shows that the Möbius function evaluates to zero at the square of any prime. Number theorists applying inclusion-exclusion or Dirichlet inversion would cite this elementary case. The term-mode proof converts the local Prime hypothesis to Nat.Prime via prime_iff then invokes the standard moebius_apply_prime_pow lemma at exponent 2.
claimIf $p$ is prime then $μ(p^2)=0$, where $μ$ is the Möbius function.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Here mobius is the abbrev that aliases ArithmeticFunction.moebius, yielding a map ℕ → ℤ. The Prime predicate is imported from the Basic submodule and related to the standard Nat.Prime notion by the prime_iff lemma. The local setting is a collection of small footholds for later Dirichlet algebra rather than a full development.
proof idea
The proof is a one-line term wrapper. It first obtains Nat.Prime p from the hypothesis hp by applying prime_iff, then feeds the result together with the literal exponent 2 into ArithmeticFunction.moebius_apply_prime_pow, using a decidable inequality to discharge the non-zero condition and obtain the zero value directly.
why it matters in Recognition Science
This supplies the prime-square case needed for the squarefree detection lemmas that appear as siblings in the same file. It supports the arithmetic-function layer that Recognition Science uses for inversion formulas, though it carries no direct link to the forcing chain, phi-ladder or physical constants. No downstream uses are recorded yet.
scope and limits
- Does not evaluate μ at prime powers with exponent other than 2.
- Does not address composite arguments or general squarefree detection.
- Does not connect the result to the Recognition forcing chain or constants.
formal statement (Lean)
35theorem mobius_prime_sq {p : ℕ} (hp : Prime p) : (mobius (p ^ 2)) = 0 := by
proof body
Term-mode proof.
36 have hp' : Nat.Prime p := (prime_iff p).1 hp
37 -- Use the prime-power formula with `k = 2`: `μ(p^2) = if 2 = 1 then -1 else 0 = 0`.
38 simpa [mobius] using
39 (ArithmeticFunction.moebius_apply_prime_pow (p := p) (k := 2) hp' (by decide : (2 : ℕ) ≠ 0))
40
41/-- If `n` is not squarefree, then `μ n = 0`. -/