squarefree_prime
plain-language theorem explainer
A prime natural number is squarefree. Number theorists working inside the Recognition Science factorization setup cite this when they need the squarefree predicate to hold on primes before invoking the vp valuation. The proof is a one-line wrapper that converts the repo-local Prime predicate to Mathlib's Nat.Prime via an equivalence and applies the standard squarefree property of primes.
Claim. If $p$ is a prime natural number, then $p$ is squarefree.
background
The module links the standard Squarefree predicate on natural numbers to the repo-local valuation vp p n, defined as the exponent of p in the prime factorization of n. Squarefree n holds precisely when vp p n ≤ 1 for every prime p. The local Prime predicate is a transparent alias for Mathlib's Nat.Prime, and the upstream equivalence prime_iff states that Prime n ↔ Nat.Prime n.
proof idea
The proof applies the equivalence from prime_iff to obtain a Mathlib Nat.Prime instance, then invokes the Mathlib fact that every such prime is squarefree.
why it matters
The result supplies a basic primitive inside the squarefree development that feeds the vp-based factorization used throughout the Recognition number-theory layer. It supports clean statements about primes before they enter mass formulas or the phi-ladder constructions. No downstream uses are recorded yet, leaving the lemma as a foundational hook for later prime-distribution or squarefree-product arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.