no_smaller_multiple_9_5
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not address any n greater than or equal to 45.
- Does not claim 45 is the lcm of 9 and 5.
- Does not involve phi, mass formulas, or physical constants.
- Does not apply to non-positive integers or non-natural numbers.
formal statement (Lean)
55lemma no_smaller_multiple_9_5 (n : Nat) (hnpos : 0 < n) (hnlt : n < 45) :
56 ¬ (9 ∣ n ∧ 5 ∣ n) := by
proof body
Tactic-mode proof.
57 intro h
58 rcases h with ⟨h9, h5⟩
59 have hmul : 9 * 5 ∣ n := coprime_9_5.mul_dvd_of_dvd_of_dvd h9 h5
60 have h45 : 45 ∣ n := by simpa using hmul
61 rcases h45 with ⟨k, hk⟩
62 rcases (Nat.eq_zero_or_pos k) with rfl | hkpos
63 · simp only [mul_zero] at hk
64 omega
65 · have : 45 ≤ 45 * k := Nat.mul_le_mul_left 45 hkpos
66 have : 45 ≤ n := by simpa [hk] using this
67 exact (not_le_of_gt hnlt) this
68
69/-- Summary: 45 is the first rung where 9- and 5-fold periodicities coincide, and it is not
70 synchronized with the 8-beat (since 8 ∤ 45). -/