squarefree_prime_not_dvd_iff_vp_eq_zero
plain-language theorem explainer
For a nonzero squarefree natural number n and prime p, non-divisibility by p is equivalent to the p-adic valuation of n equaling zero. Number theorists working with factorization in the Recognition Science number theory layer cite this when converting between divisibility statements and exponent conditions. The proof is a term-mode construction that rewrites the statement via a companion lemma on valuation one and then cases on the zero-or-one dichotomy for squarefree inputs.
Claim. Let $n$ be a nonzero squarefree natural number and let $p$ be prime. Then $p$ does not divide $n$ if and only if the $p$-adic valuation $v_p(n)=0$.
background
The module links the standard Squarefree predicate (no square greater than 1 divides n) to the repo-local valuation vp p n, defined as the exponent of p in the prime factorization of n. This supplies the arithmetic substrate for later Recognition Science constructions that track prime factors along the phi-ladder. The local setting is pure natural-number arithmetic imported from Mathlib together with the module's own factorization utilities.
proof idea
The term proof first rewrites the target biconditional by invoking the sibling lemma squarefree_prime_dvd_iff_vp_eq_one. It then obtains the zero-or-one dichotomy from squarefree_vp_dichotomy. The forward direction cases on this dichotomy and eliminates the false branch; the reverse direction uses omega to derive a contradiction from the assumption that the valuation is simultaneously zero and one.
why it matters
The lemma completes the basic translation between divisibility and valuation zero for squarefree inputs, feeding the sibling results on products of coprime squarefree numbers and the squarefree-one case. It supplies the number-theoretic foundation required by the Recognition Science forcing chain when prime exponents appear in mass formulas or the eight-tick octave. No direct downstream uses are recorded, leaving open whether it will be invoked in later ledger or spectral-emergence arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.