vp_factorial_twelve_three
plain-language theorem explainer
The theorem states that the exponent of the prime 3 in the prime factorization of 12! equals 5. Number theorists verifying explicit small-case valuations for arithmetic functions would cite this result. The proof is a one-line wrapper that invokes native_decide to compute the factorization directly from the definition of vp.
Claim. The 3-adic valuation of $12!$ satisfies $v_3(12!) = 5$.
background
The function vp p n extracts the exponent of prime p in the factorization of n, defined as n.factorization p. This sits inside the module supplying lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function to prepare for Dirichlet inversion once the interfaces stabilize. It depends directly on the vp definition from the Factorization module.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the equality by direct computation of the prime factorization of 12!.
why it matters
This supplies a concrete numerical check for the vp definition inside the number-theoretic scaffolding of Recognition Science. It supports downstream arithmetic function work even though no immediate uses are recorded. The result aligns with the module's focus on basic prime factorization tools that feed larger claims on arithmetic properties.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.