vp_def
plain-language theorem explainer
vp equates the local p-valuation on naturals to Mathlib's standard factorization exponent. Number theorists extending prime tools inside the Recognition framework cite this for stable notation across factorization lemmas. The proof is a direct reflexivity that confirms the wrapper matches the library definition with no further steps.
Claim. For natural numbers $p$ and $n$, the valuation $v_p(n)$ equals the exponent of $p$ in the prime factorization of $n$.
background
The module supplies a thin, stable wrapper around Mathlib's Nat.factorization so that downstream prime work (squarefree predicates, Möbius inversion, etc.) can use a repo-local name vp for the exponent of p in n. This keeps algebraic identities such as vp_mul and vp_pow uniform without repeated calls to the external library function. The local theoretical setting is purely number-theoretic and serves as infrastructure for the Recognition Science prime layer; upstream structures from forcing and spectral modules supply the broader context in which these valuations appear but are not invoked by this declaration.
proof idea
Term-mode proof consisting of a single reflexivity that matches the left-hand side to the right-hand side by the defining equation of vp.
why it matters
The declaration anchors the Factorization module by fixing the meaning of vp, which is presupposed by every subsequent lemma in the file (vp_mul, vp_pow, vp_prime_self, etc.). It thereby supplies the concrete link between Recognition Science's prime interface and the standard arithmetic factorization used in spectral emergence and ledger constructions. No open questions are closed here; the result is purely infrastructural.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.