no_smaller_multiple_8_45
No positive integer n smaller than 360 is divisible by both 8 and 45. Researchers establishing minimal alignment windows for dual periodicities cite this bound to show that any finite horizon below 360 must fail to verify simultaneous multiples. The proof assumes a common divisor pair, invokes minimal_sync_360_divides to force 360 to divide n, then contradicts n < 360 by case analysis on the quotient k.
claimThere is no positive integer $n$ with $n < 360$ such that $8$ divides $n$ and $45$ divides $n$.
background
The Gap45 module establishes coprimeness facts for 9 and 5 (hence for 45) and works with the periodicities 8 and 45. The upstream lemma minimal_sync_360_divides states that if 8 divides t and 45 divides t then 360 divides t; its doc-comment calls it a convenience form of minimality with 360 on the left. The sibling results include coprime_8_45, lcm_8_45_eq_360 and related divisibility lemmas that together fix the least common multiple at 360.
proof idea
Assume for contradiction that n is positive, n < 360, and both 8 and 45 divide n. Apply minimal_sync_360_divides to obtain 360 divides n, so n = 360 * k. Case on k = 0 (mul_zero yields n = 0, contradicting positivity via omega) or k > 0 (Nat.mul_le_mul_left gives 360 <= n, contradicting the strict upper bound).
why it matters in Recognition Science
The lemma is invoked verbatim by window_insufficient in RecognitionBarrier, whose doc-comment states that no window of length w < 360 can simultaneously be a multiple of 8 and 45 and that any finite-horizon procedure with horizon < 360 ticks will encounter a tick where it cannot verify alignment of both periods. It therefore supplies the concrete bound that the minimal window resolving both periodicities is exactly 360, closing a key step in the Gap45 analysis of recognition barriers and linking to the eight-tick octave periodicity.
scope and limits
- Does not prove that 360 is the least common multiple of 8 and 45.
- Does not apply to n = 0 or to negative integers.
- Does not address common multiples of any other pair of integers.
- Does not quantify the size of the smallest common multiple above 360.
Lean usage
theorem window_insufficient (w : ℕ) (hw_pos : 0 < w) (hw_lt : w < 360) : ¬ (8 ∣ w ∧ 45 ∣ w) := no_smaller_multiple_8_45 hw_pos hw_ltformal statement (Lean)
113lemma no_smaller_multiple_8_45 {n : Nat} (hnpos : 0 < n) (hnlt : n < 360) :
114 ¬ (8 ∣ n ∧ 45 ∣ n) := by
proof body
Tactic-mode proof.
115 intro h
116 rcases h with ⟨h8, h45⟩
117 have h360 : 360 ∣ n := minimal_sync_360_divides (t:=n) h8 h45
118 rcases h360 with ⟨k, hk⟩
119 rcases Nat.eq_zero_or_pos k with rfl | hkpos
120 · simp only [mul_zero] at hk
121 omega
122 · have : 360 ≤ 360 * k := Nat.mul_le_mul_left 360 hkpos
123 have : 360 ≤ n := by simpa [hk] using this
124 exact (not_le_of_gt hnlt) this
125
126end Beat
127
128-- (Moved to IndisputableMonolith/Gap45/TimeLag.lean)
129
130-- (Moved to IndisputableMonolith/Gap45/RecognitionBarrier.lean)
131
132-- (Moved to IndisputableMonolith/Gap45/GroupView.lean)
133
134-- (Moved to IndisputableMonolith/Gap45/AddGroupView.lean)
135
136end Gap45
137end IndisputableMonolith