vp_factorial_ten_five
plain-language theorem explainer
The exponent of prime 5 in the factorization of 10! equals 2. Number theorists verifying explicit p-adic valuations or small factorial computations would cite this for base-case checks. The proof is a term-mode native_decide that directly evaluates the factorization and extracts the exponent.
Claim. Let $v_p(n)$ denote the exponent of prime $p$ in the prime factorization of natural number $n$. Then $v_5(10!) = 2$.
background
The function vp(p, n) extracts the exponent of prime p in the prime factorization of n, implemented directly as n.factorization p. This module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and related tools for Dirichlet series and inversion; the local setting keeps statements minimal to stabilize basic interfaces before deeper algebra is added. Upstream results include the vp definition itself, structural axioms from UniversalForcingSelfReference.for, and an explicit log-derivative bound from CirclePhaseLift.and, though the latter two enter only via module imports.
proof idea
The proof is a one-line term-mode wrapper that applies native_decide to compute the prime factorization of 10! and confirm the exponent of 5 is exactly 2.
why it matters
This explicit base-case computation supports arithmetic-function work in the primes module, though it has no current dependents. It fills a verification gap for factorial valuations inside NumberTheory.Primes.ArithmeticFunctions and contributes to the number-theoretic layer required by Recognition Science forcing chains (T0-T8) and the Recognition Composition Law, without touching open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.