vp_factorial_five_two
plain-language theorem explainer
The declaration establishes that the exponent of 2 in the prime factorization of 5! equals 3. Number theorists verifying small factorial valuations or building arithmetic function tables in the Recognition Science setting would cite this for direct computation checks. The proof is a one-line native decision that evaluates the factorization definition without expansion.
Claim. $v_2(5!) = 3$, where $v_2(n)$ is the exponent of 2 in the prime factorization of $n$.
background
The function vp, imported from the Factorization module, is defined as the exponent of prime p in the factorization of n via n.factorization p. This supplies the standard p-adic valuation used throughout the arithmetic functions file. The module supplies lightweight wrappers around Mathlib's arithmetic library, beginning with the Möbius function and related squarefree checks, to support Dirichlet inversion once interfaces stabilize.
proof idea
The proof is a one-line term that applies native_decide to compute vp 2 (Nat.factorial 5) directly from the upstream vp definition.
why it matters
This supplies a concrete small-case check of the valuation function that underpins prime factorization arguments in the NumberTheory section. No downstream theorems currently depend on it, but it anchors exact arithmetic facts needed for later Möbius and bigOmega applications. It fits the framework's pattern of verifying basic number-theoretic identities before layering Recognition Science structures such as the phi-ladder or RCL.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.