no_smaller_multiple_8_45
plain-language theorem explainer
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.
Claim. There 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.