eight_not_dvd_45
plain-language theorem explainer
The lemma establishes that 8 does not divide 45. Researchers examining rung conflicts on the phi-ladder cite it to confirm that the first joint 9- and 5-fold periodicity at 45 lies outside the 8-tick octave. The proof is a one-line decision procedure that verifies the arithmetic non-divisibility directly.
Claim. $8$ does not divide $45$.
background
The Gap45 module works in the setting where 9 and 5 are coprime, using this fact to locate the smallest positive integer simultaneously divisible by both. The lemma supplies the complementary arithmetic fact that this integer is not divisible by 8. Upstream results supply the surrounding structures: collision-free classes, simplicial edge lengths, mechanism-design isomorphisms, mock-theta constructions, and circle-phase lifts, all of which presuppose decidable arithmetic facts of this kind.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the decidable proposition ¬(8 ∣ 45).
why it matters
The lemma is invoked inside rung45_first_conflict to record that 45 is the first rung at which 9- and 5-fold periodicities coincide yet remain unsynchronized with the 8-beat. It therefore supplies the number-theoretic prerequisite for the synchronization requirement stated in the downstream theorem. Within the Recognition framework this step closes the gap between the eight-tick octave (T7) and the first composite rung that mixes 9- and 5-fold symmetries.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.