coprime_thirtyseven_360
plain-language theorem explainer
37 and 360 share no common prime factors. Modelers working with RS constants cite this fact to treat 37 as an independent prime marker next to the 360 anchor without repeated gcd checks. The proof is a one-line term that invokes native_decide to evaluate the coprimeness predicate directly.
Claim. $ gcd(37, 360) = 1 $
background
The RSConstants module assembles small, decidable arithmetic facts about integers that recur in the repository, including 8, 45, 360, 840 and the primes 11, 17, 37, 103, 137. These facts function as stable anchors that keep later bridge lemmas readable and eliminate repeated arithmetic proofs. The local setting is purely computational: each declaration is a verified integer relation with no additional hypotheses.
proof idea
The declaration is a term-mode proof consisting of a single native_decide tactic. This evaluates the Nat.Coprime predicate by computing the gcd inside the kernel and confirming the result equals 1.
why it matters
The theorem supplies one of the stable arithmetic anchors listed in the module documentation for RS constants. It prevents re-derivation of the same gcd fact in any bridge lemma that combines the prime marker 37 with the 360 constant. No downstream uses are recorded, but the fact aligns with the framework's reliance on small integers in eight-tick and phase-lift constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.