rung45_first_conflict
plain-language theorem explainer
45 is the smallest positive integer divisible by both 9 and 5 but not by 8, with no smaller positive integer sharing both divisors. Researchers tracing symmetry alignments along the phi-ladder cite this result to locate the initial 9-5 conflict point. The proof assembles the four conjuncts directly from sibling divisibility lemmas without further reduction steps.
Claim. $9 | 45 ∧ 5 | 45 ∧ ¬(8 | 45) ∧ ∀ n ∈ ℕ, (0 < n → n < 45 → ¬(9 | n ∧ 5 | n))$
background
The Gap45 module treats 9 and 5 as coprime integers. Their least common multiple therefore supplies the first rung at which both periodicities coincide. The local setting isolates this coincidence outside the 8-beat structure, with the module comment noting that synchronization with the 8-fold symmetry requires exactly lcm(8,45) = 360 beats.
proof idea
The term-mode proof refines a four-tuple consisting of the lemmas that 9 divides 45, that 5 divides 45, that 8 does not divide 45, and the universal statement that no smaller positive n is divisible by both 9 and 5. The quantified conjunct is discharged by direct appeal to the lemma establishing the absence of smaller common multiples.
why it matters
The declaration pins the first coincidence of 9- and 5-fold symmetries at rung 45 outside the eight-tick octave (T7). It thereby supports the synchronization requirement that the minimal alignment time equals lcm(8,45) = 360 beats and feeds analyses that later force D = 3 spatial dimensions (T8). No downstream theorems are recorded, so the result remains a self-contained gap closure within the phi-ladder construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.