nine_dvd_45
plain-language theorem explainer
The lemma establishes that 9 divides 45, serving as a building block for locating the smallest positive integer at which 9-fold and 5-fold periodicities coincide in the Recognition Science phi-ladder. Researchers analyzing rung synchronization and the eight-tick octave would cite it when proving the first conflict point at 45. The proof is a one-line term-mode construction that supplies the witness 5 and confirms the product via decidable arithmetic.
Claim. $9$ divides $45$.
background
The Gap45 module examines divisibility relations among 9, 5, and 8 to locate the first rung where 9- and 5-fold symmetries coincide without 8-fold alignment. The local setting states that 9 and 5 are coprime. This supplies the basic arithmetic fact needed to combine with the corresponding divisibility for 5 and the negation for 8.
proof idea
The proof is a term-mode application of the definition of divisibility. It constructs the pair consisting of the integer 5 as the quotient together with a decidable verification that 9 times 5 equals 45.
why it matters
This lemma feeds directly into the theorem rung45_first_conflict, which asserts that 45 is the first rung where 9- and 5-fold periodicities coincide and is not synchronized with the 8-beat. In the Recognition Science framework it supports analysis of the eight-tick octave (T7) and the phi-ladder structure by closing the arithmetic step required for the synchronization requirement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.