vp_lcm
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.