coprime_eight_fortyfive
plain-language theorem explainer
The theorem asserts that 8 and 45 share no common prime factors. Number theorists working with Recognition Science constants cite this when verifying arithmetic-function inputs such as the Möbius function. The proof reduces to a single native_decide call that computes the gcd directly.
Claim. The positive integers 8 and 45 are coprime, i.e., $gcd(8,45)=1$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Statements remain minimal so that Dirichlet inversion can be added once interfaces stabilize. The coprimality fact supports vp-based characterizations of RS constants, including the prime spectrum of 8 (only 2-content with exponent 3).
proof idea
The proof is a one-line wrapper that applies native_decide to compute the gcd of 8 and 45.
why it matters
This result is the parent for the convenience wrapper in RSConstants.coprime_eight_fortyfive. It supplies a basic number-theoretic fact required for prime-factor characterizations of RS constants. In the Recognition framework such checks underpin the arithmetic functions used in the forcing chain and phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.