vp_factorial_six_three
plain-language theorem explainer
The declaration states that the exponent of prime 3 in the factorization of 6! equals 2. Number theorists checking small cases of arithmetic functions or Möbius inversion setups would cite this explicit value. The proof is a one-line native decision that evaluates the factorization definition directly.
Claim. Let $v_p(n)$ denote the exponent of prime $p$ in the prime factorization of natural number $n$. Then $v_3(6!) = 2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. The upstream definition states that vp p n is the exponent of p in the prime factorization of n (implemented as n.factorization p). This supplies a concrete base case for p=3 and n=6! inside the arithmetic functions layer.
proof idea
The proof is a one-line term that invokes native_decide to compute vp 3 (Nat.factorial 6) from the factorization definition.
why it matters
This supplies a verified small-case evaluation inside the arithmetic functions module that supports Möbius footholds. No downstream theorems are recorded, so it functions as an isolated verification point rather than a link in a longer chain. It does not touch the Recognition Science forcing chain or constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.