squarefree_vp_dichotomy
plain-language theorem explainer
The result guarantees that every prime exponent in the factorization of a nonzero squarefree natural number is either zero or one. Workers on factorization properties within the NumberTheory development cite this when they need the binary character of exponents under squarefreeness. Its proof is a one-line wrapper that obtains the upper bound of one from the squarefree characterization lemma and applies omega to reach the disjunction.
Claim. Let $n$ be a nonzero squarefree natural number and let $p$ be any natural number. Then the $p$-adic valuation $v_p(n)$ satisfies $v_p(n) = 0$ or $v_p(n) = 1$.
background
The Squarefree module links the standard Squarefree predicate to the valuation function that returns the exponent of $p$ in the prime factorization of $n$. An upstream lemma states that a nonzero natural number is squarefree precisely when this exponent is at most one for every $p$. The present result extracts the 0-or-1 dichotomy that follows once squarefreeness is given. The local setting is the development of prime factorization properties needed for later results on divisibility and coprimeness in the NumberTheory.Primes hierarchy.
proof idea
The proof is a one-line wrapper. It invokes the forward direction of the squarefree characterization lemma to obtain the inequality that the valuation is at most one, then applies the omega tactic to conclude that a natural number satisfying this bound must be 0 or 1.
why it matters
This result supports the theorem that for squarefree $n$ and prime $p$, $p$ does not divide $n$ if and only if the valuation is zero. It completes the basic properties of squarefree numbers under the valuation encoding, allowing clean statements without repeated appeals to the full factorization lemma. The result stays within number theory and does not engage the Recognition Science forcing chain or physical constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.