no_smaller_multiple_8_45
plain-language theorem explainer
No positive integer n below 360 is a common multiple of both 8 and 45. Gap45 recognition barrier arguments cite this to bound the minimal alignment window. The tactic proof assumes joint divisibility, applies minimal_sync_360_divides to force 360 to divide n, then splits on the quotient to reach a contradiction with the strict upper bound via mul_zero and inequality.
Claim. For any natural number $n$ with $0 < n < 360$, it is not the case that $8$ divides $n$ and $45$ divides $n$.
background
In Gap45.Beat the periods 8 and 45 appear as the eight-tick octave and the complementary cycle whose least common multiple is 360. The module doc states that experience is required exactly when the plan period is not a multiple of 8. The upstream lemma minimal_sync_360_divides asserts that simultaneous divisibility by 8 and 45 forces divisibility by 360, with the parent Gap45 version obtained by rewriting beats_eq_360.
proof idea
The proof introduces the joint-divisibility hypothesis, applies minimal_sync_360_divides to obtain 360 divides n, and decomposes n as 360 times k. Case analysis on k zero invokes mul_zero together with omega to contradict positivity. The positive-k case uses the inequality 360 times k at least 360 to contradict n less than 360.
why it matters
The lemma is invoked directly by window_insufficient in RecognitionBarrier, which concludes that any finite horizon shorter than 360 encounters a tick where alignment of both periods cannot be verified. It supplies the minimality step for the 360-tick window required by the Gap45 gating rule and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.