minimal_sync_360_divides
Any natural number t divisible by both 8 and 45 must be divisible by 360. Recognition Science modelers working on joint periodicities cite this to enforce the minimal synchronization interval between an 8-beat cycle and a 45-fold pattern. The proof is a one-line term wrapper that rewrites the joint period via beats_eq_360 and invokes the general lcm-divisibility result.
claimIf $8 mid t$ and $45 mid t$ for $t in mathbb{N}$, then $360 mid t$.
background
The module establishes that 9 and 5 are coprime, which fixes the least common multiple of 8 and 45 at 360. The identifier beats denotes the minimal joint duration for an 8-beat cycle and a 45-fold pattern. Upstream lemma beats_eq_360 states that this minimal duration equals 360, while minimal_sync_divides asserts that any common multiple of 8 and 45 is a multiple of beats.
proof idea
This is a one-line term proof. It applies simpa with the simp lemma beats_eq_360 to rewrite the target divisibility condition, then directly invokes minimal_sync_divides on the supplied hypotheses h8 and h45.
why it matters in Recognition Science
The lemma supplies the concrete 360-divisibility step required by no_smaller_multiple_8_45, which shows no positive integer smaller than 360 can satisfy both divisibility conditions simultaneously. It is invoked verbatim in resolution_requires_full_period to conclude that any window resolving both periodicities must be a multiple of 360. In the Recognition framework this anchors the eight-tick octave (period 2^3) together with the 45-fold structure arising from the coprime factors 9 and 5.
scope and limits
- Does not compute or prove the value of the least common multiple of 8 and 45.
- Does not apply outside the natural numbers.
- Does not guarantee that any common multiple exists.
- Does not rule out common multiples larger than 360.
Lean usage
theorem resolution_example (w : Nat) (h8 : 8 ∣ w) (h45 : 45 ∣ w) : 360 ∣ w := minimal_sync_360_divides h8 h45formal statement (Lean)
109lemma minimal_sync_360_divides {t : Nat} (h8 : 8 ∣ t) (h45 : 45 ∣ t) : 360 ∣ t := by
proof body
Term-mode proof.
110 simpa [beats_eq_360] using minimal_sync_divides (t:=t) h8 h45
111
112/-- No positive `n < 360` can be simultaneously divisible by 8 and 45. -/