gcd_eight_fortyfive_eq_one
plain-language theorem explainer
The declaration states that the greatest common divisor of 8 and 45 equals 1. Researchers assembling Recognition Science constants cite this fact to anchor coprimality arguments in bridge lemmas. The proof is a one-line wrapper that delegates verification to native_decide for direct arithmetic computation.
Claim. $ gcd(8,45)=1 $
background
The module collects small decidable arithmetic facts about integers such as 8, 45, 360, and 840 that recur throughout the Recognition Science development. These facts function as stable anchors that keep later bridge lemmas readable without repeated arithmetic re-proofs. No upstream lemmas are invoked because the claim reduces to a direct computation.
proof idea
The proof is a one-line wrapper that invokes native_decide to confirm the equality by exhaustive computation.
why it matters
This result supplies the base equality for the downstream theorem coprime_eight_fortyfive_vp, which shows that the p-adic valuation of the gcd vanishes for every prime p. It anchors the factorization facts inside the RSConstants module and supports the use of 8 and 45 as coprime components in the eight-tick octave construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.