no_smaller_multiple_9_5
plain-language theorem explainer
No positive integer n less than 45 is divisible by both 9 and 5. Researchers tracing the minimal rung where 9-fold and 5-fold symmetries coincide in the Recognition Science phi-ladder would cite this result. The proof assumes simultaneous divisibility, applies the coprimeness of 9 and 5 to conclude 45 divides n, and obtains a contradiction with n < 45 via ordering and the mul_zero theorem.
Claim. Let $n$ be a positive integer with $n < 45$. Then it is not the case that both 9 divides $n$ and 5 divides $n$.
background
The Gap45 module examines synchronization of 9-fold and 5-fold periodicities, with the module documentation stating that 9 and 5 are coprime. This coprimeness ensures their least common multiple equals 45, as handled by sibling lemmas such as lcm_9_5_eq_45. The local setting focuses on the first coincidence at rung 45 and its lack of synchronization with the 8-beat, since 8 does not divide 45.
proof idea
The tactic proof introduces the assumption that 9 divides n and 5 divides n. It applies coprime_9_5.mul_dvd_of_dvd_of_dvd to obtain 45 divides n. It then cases on the multiplier k via Nat.eq_zero_or_pos, rules out k = 0 using mul_zero, and for positive k invokes Nat.mul_le_mul_left to show n >= 45, contradicting the hypothesis n < 45 via not_le_of_gt.
why it matters
This lemma is invoked directly by rung45_first_conflict, which asserts that 45 is the first rung where 9- and 5-fold periodicities coincide and is not synchronized with the 8-beat. In the Recognition Science framework it supports the eight-tick octave (T7) and the synchronization requirement for aligning 8-beat and 45-fold symmetries on the phi-ladder. It closes a combinatorial gap before mass formulas or Berry thresholds are applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.