vp_lcm
The exponent of any natural number p in the least common multiple of two nonzero naturals a and b equals the larger of the separate exponents in a and in b. Researchers characterizing constants through prime factorizations in the Recognition Science primes layer cite this when handling lcm identities such as the 360 case. The proof is a direct term reduction that unfolds the local exponent definition and invokes the corresponding Mathlib lemma on lcm factorizations.
claimFor nonzero natural numbers $a$ and $b$ and any natural number $p$, the exponent of $p$ in the prime factorization of lcm$(a,b)$ equals the maximum of the exponents of $p$ in $a$ and in $b$.
background
The Factorization module defines the exponent function as the multiplicity returned by Mathlib's Nat.factorization at the given prime index. This supplies a thin, stable interface that downstream files use for algebraic identities involving multiplication, powers, and now lcm. The module's stated goal is to support later prime-based work such as squarefree detection and Möbius inversion without exposing raw Mathlib details.
proof idea
The term proof unfolds the exponent definition, rewrites the lcm via the Mathlib factorization_lcm lemma (which holds precisely under the nonzero hypotheses), and closes by reflexivity.
why it matters in Recognition Science
This result is applied in the lcm_eight_fortyfive_vp_characterization theorem to express 360 as lcm(8,45) through pointwise maximum exponents at each prime. It thereby supplies a required compatibility law for the prime-factorization tools that feed constant derivations in RSConstants and the broader Recognition Science number-theoretic layer.
scope and limits
- Does not require p to be prime.
- Does not apply if a or b equals zero.
- Does not address the gcd operation.
- Does not extend to integers outside the naturals.
formal statement (Lean)
96theorem vp_lcm {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) (p : ℕ) :
97 vp p (Nat.lcm a b) = max (vp p a) (vp p b) := by
proof body
Term-mode proof.
98 simp only [vp]
99 rw [Nat.factorization_lcm ha hb]
100 rfl
101
102/-! ### Prime power characterization -/
103
104/-- If `n = p^k` for prime `p` and `k ≥ 1`, then `vp p n = k`. -/