coprime_eight_fortyfive
plain-language theorem explainer
8 and 45 are coprime. Researchers handling Recognition Science constants cite this fact when simplifying arithmetic steps that involve the factorization of 8 as 2 cubed and 45 as 3 squared times 5. The proof is a one-line wrapper that invokes native_decide to compute the gcd directly.
Claim. $8$ and $45$ are coprime, i.e., their greatest common divisor equals $1$.
background
The module assembles small, decidable arithmetic facts about integers that recur in the Recognition Science codebase, including 8, 45, 360, 840 and selected primes. These facts act as stable anchors that keep later bridge lemmas readable without repeated arithmetic proofs. Upstream structures such as the J-cost minimization convexity result and the phi-forcing derived ledger supply the broader context in which these constants appear.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the coprimality predicate on the concrete integers 8 and 45.
why it matters
This theorem supplies a reusable anchor for the RS constants 8 and 45 inside the NumberTheory.Primes hierarchy. It is referenced by the corresponding declaration in ArithmeticFunctions and supports downstream factorizations such as the wheel-840 and 360 characterizations. The fact aligns with the eight-tick octave (T7) and the phi-ladder rung assignments that treat 8 as 2^3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.