vp_gcd
plain-language theorem explainer
vp_gcd states that for nonzero natural numbers a and b the exponent of any p in their gcd equals the minimum of the two individual exponents. Number theorists working inside the Recognition Science monolith would cite it when preserving valuation properties under gcd in prime factorization arguments. The proof is a direct term reduction that unfolds the local vp definition and applies Mathlib's factorization_gcd lemma.
Claim. For nonzero $a, b, p$ in the natural numbers, the exponent of $p$ in the prime factorization of $a$ and $b$ satisfies $v_p(a) = v_p(b)$ implies the exponent of $p$ in their gcd is the minimum of those two exponents.
background
The NumberTheory.Primes.Factorization module supplies a stable wrapper vp around Mathlib's Nat.factorization, where vp p n records the exponent of p in the factorization of n. The module's explicit goal is to export a small set of algebraic laws (multiplication, powering, and now gcd) for reuse in squarefree and Möbius constructions downstream.
proof idea
The term proof first simplifies the goal by the definition of vp, rewrites the gcd side via the Mathlib lemma Nat.factorization_gcd (which consumes the nonzero hypotheses ha and hb), and closes by reflexivity.
why it matters
vp_gcd completes the basic algebraic toolkit for vp alongside the sibling results vp_mul and vp_pow. It supplies the min property required for any later manipulation of gcds inside prime factorization work in the Recognition Science framework. No direct dependence on the T0-T8 forcing chain appears, but the lemma stabilizes the number-theoretic layer that supports spectral and complexity structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.