minimal_sync_360_divides
Any common multiple of 8 and 45 is necessarily a multiple of 360. Analysts of periodic pattern resolution in the Gap45 framework cite this lemma to bound minimal windows. The proof is a one-line wrapper that rewrites via the beats_eq_360 equality into the general divisibility result for the joint duration.
claimLet $t$ be a natural number. If $8$ divides $t$ and $45$ divides $t$, then $360$ divides $t$.
background
The Gap45 module encodes a gating rule: experience is required exactly when the plan period is not a multiple of 8. This captures the policy that 8-beat alignment disables Gap45 gating. The Beat submodule defines the minimal joint duration for 8-beat and 45-fold patterns as their least common multiple.
proof idea
This is a one-line wrapper. It applies simpa with the beats_eq_360 equality to instantiate the general minimal_sync_divides lemma at the target t.
why it matters in Recognition Science
The lemma supplies the 360-explicit form of the minimality condition. It is used to derive no_smaller_multiple_8_45, which shows no positive n less than 360 is divisible by both 8 and 45. It also feeds resolution_requires_full_period, which requires any resolving window to be a multiple of 360. This aligns with the eight-tick octave by fixing the minimal alignment period.
scope and limits
- Does not establish the least common multiple value from scratch.
- Does not apply outside natural numbers.
- Does not cover zero or negative divisors.
- Does not generalize to other pairs of periods.
Lean usage
theorem example (t : Nat) (h8 : 8 ∣ t) (h45 : 45 ∣ t) : 360 ∣ t := minimal_sync_360_divides h8 h45formal statement (Lean)
42lemma minimal_sync_360_divides {t : Nat} (h8 : 8 ∣ t) (h45 : 45 ∣ t) : 360 ∣ t := by
proof body
One-line wrapper that applies simpa.
43 simpa [beats_eq_360] using minimal_sync_divides (t:=t) h8 h45
44