gcd_mul_lcm
plain-language theorem explainer
The declaration establishes the arithmetic identity that the product of the gcd and lcm of any two natural numbers equals their product. Researchers deriving lcm values from coprimality conditions in periodic pattern analysis or prime synchronization within the Recognition Science primes framework would cite this result. The proof consists of a direct one-line application of the corresponding theorem from Mathlib.
Claim. For any natural numbers $a$ and $b$, $d(a,b) · l(a,b) = a · b$, where $d$ denotes the greatest common divisor and $l$ the least common multiple.
background
This lemma sits in the GCD/LCM utilities module, which centralizes small algebraic identities for reuse across the primes framework. The module exposes stable wrappers around Mathlib results to support prime-friendly calculations in the broader Recognition Science setting.
proof idea
The proof is a one-line wrapper that applies the Mathlib theorem Nat.gcd_mul_lcm directly via the exact tactic.
why it matters
This result supports downstream calculations such as lcm(8,45)=360 in Gap45 and the cicada safety interval for primes in Resonance, where it enables deriving lcm from coprimality. It fills a basic arithmetic step in the primes framework, aiding periodicities tied to the eight-tick octave. No open questions are directly touched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.