vp_zero
plain-language theorem explainer
The exponent of any prime p in the number zero equals zero by the standard convention on empty factorizations. Researchers building arithmetic functions over the naturals in the Recognition Science layer cite this base case when stating uniform laws for multiplicative maps or Möbius inversion. The argument reduces immediately via a single simplification step on the definition of the exponent function.
Claim. $v_p(0) = 0$ for every natural number $p$, where $v_p(n)$ is the exponent of $p$ in the prime factorization of $n$.
background
The module supplies a thin wrapper around Mathlib's factorization to define the exponent of a prime p in a natural number n, together with the basic multiplicative and power laws needed for later squarefree and Möbius work. The local setting is therefore factorization and valuations treated as a stable interface rather than a full redevelopment of number theory. Upstream structures on J-cost, phi-forcing, and spectral emergence locate this arithmetic layer inside the broader Recognition Science derivation of physical constants from the forcing chain.
proof idea
The proof is a one-line wrapper that applies simplification directly to the definition of the exponent function, discharging the equality by reflexivity.
why it matters
The declaration closes the zero case for the exponent function, permitting uniform statements over all natural numbers without separate handling of the empty product. It anchors the algebraic interface in the primes module that later results on prime powers and factorization identities presuppose. In the Recognition framework it supplies the arithmetic base that interfaces with the eight-tick octave and the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.