Sync
plain-language theorem explainer
The Sync structure encodes a natural number beats together with the two cycle-count equalities that hold precisely when the period is the least common multiple of 8 and 45. Gap45 synchronization work cites this record when confirming 8-beat alignment that disables gating. The definition is a direct structure whose fields are satisfied by the upstream lcm value.
Claim. A synchronization record consists of a natural number $b$ satisfying $b/8=45$ and $b/45=8$.
background
The beats definition supplies the minimal joint duration for 8-beat and 45-fold patterns as Nat.lcm 8 45. The module implements the Gap45 gating rule: experience is required exactly when the plan period is not a multiple of 8, capturing the policy that 8-beat alignment disables gating.
proof idea
The declaration is the direct structure definition whose two equality fields are the cycle conditions. It depends on the upstream beats definition (lcm 8 45) that supplies the concrete value satisfying both equalities.
why it matters
Sync supplies the type for the canonical instance constructed in the same module and referenced by coprime_11 in SyncMinimization. It encodes the 8-beat alignment step (T7 eight-tick octave) that turns off Gap45 gating in the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.