coprime_9_5
plain-language theorem explainer
The lemma asserts that 9 and 5 are coprime natural numbers. It is cited inside Gap45 when showing that 45 is the least common multiple of 9 and 5. The proof is a one-line decision procedure that computes the gcd directly.
Claim. The natural numbers 9 and 5 are coprime: $9$ and $5$ share no common positive divisors other than $1$, or equivalently $gcd(9,5)=1$.
background
Gap45 assembles elementary divisibility facts among the integers 8, 9, 5 and 45 that appear in the phi-ladder analysis at rung 45. These facts control the size of the smallest common multiple and the location of the first conflict. The upstream result and supplies an explicit log-derivative bound M on a disk that yields an angular Lipschitz constant, but the present lemma is independent of that bound and rests on direct computation.
proof idea
The proof is a term proof consisting of a single decide tactic. The tactic evaluates the Nat.Coprime predicate by computing gcd(9,5) and confirming the result equals 1.
why it matters
no_smaller_multiple_9_5 invokes this lemma to conclude that no positive integer n less than 45 is divisible by both 9 and 5. The fact therefore contributes to the gap analysis at rung 45, consistent with the self-similar fixed point phi, the eight-tick octave of period 2^3, and the forcing chain steps T5 through T8 that fix D=3. It closes a small but necessary step in the mass-formula ladder construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.