pith. machine review for the scientific record. sign in
lemma proved wrapper high

minimal_sync_divides

show as:
view Lean formalization →

If a natural number t is divisible by both 8 and 45 then it is divisible by their least common multiple. Researchers tracking periodic alignments in the Gap45 framework cite this to confirm the minimal joint period before invoking the 360-beat form. The proof is a one-line wrapper that unfolds beats and applies the standard lcm divisibility property.

claimLet $t$ be a natural number. If $8$ divides $t$ and $45$ divides $t$, then the least common multiple of $8$ and $45$ divides $t$.

background

In the Gap45.Beat submodule, beats is defined as the least common multiple of 8 and 45; it supplies the minimal joint duration for 8-beat and 45-fold patterns. The module document states that experience is required exactly when the plan period is not a multiple of 8, capturing the policy that 8-beat alignment disables Gap45 gating. The upstream beats definition in Gap45 is identical and supplies the target for the present lemma.

proof idea

The proof is a one-line wrapper. It invokes Nat.lcm_dvd on the two divisibility hypotheses and then simplifies with the definition of beats.

why it matters in Recognition Science

This lemma supplies the core minimality fact that feeds minimal_sync_360_divides, which rewrites the conclusion with the explicit value 360. It thereby supports the Gap45 gating rule by confirming that any common multiple of 8 and 45 satisfies the alignment condition that disables experience gating. The result sits inside the eight-tick octave structure of the Recognition framework.

scope and limits

Lean usage

lemma minimal_sync_360_divides {t : Nat} (h8 : 8 ∣ t) (h45 : 45 ∣ t) : 360 ∣ t := by simpa [beats_eq_360] using minimal_sync_divides h8 h45

formal statement (Lean)

  39lemma minimal_sync_divides {t : Nat} (h8 : 8 ∣ t) (h45 : 45 ∣ t) : beats ∣ t := by

proof body

One-line wrapper that applies simpa.

  40  simpa [beats] using Nat.lcm_dvd h8 h45
  41

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.