canonical
plain-language theorem explainer
The definition canonical supplies the Sync record whose beats field equals the least common multiple of 8 and 45. Algebraists building canonical cost systems or symmetry orbit counts cite this object to fix the joint period at 360. It is realized by a direct record constructor that substitutes the sibling lemmas beats, cycles_of_8 and cycles_of_45.
Claim. The canonical synchronization structure is the record whose beats component equals the least common multiple of 8 and 45, together with the identities that this value divided by 8 equals 45 and divided by 45 equals 8.
background
The Sync structure consists of a natural number beats together with proofs that this number is exactly 45 times 8 and 8 times 45. The local module Gap45.Beat implements the Gap45 gating rule under which experience is required exactly when the plan period is not a multiple of 8; 8-beat alignment therefore disables the gate.
proof idea
The definition is a one-line record constructor. It directly supplies the beats field from the sibling definition beats, the cycles8 field from the lemma cycles_of_8, and the cycles45 field from the lemma cycles_of_45.
why it matters
This definition supplies the concrete Sync instance required by canonicalCostAlgebra and canonicalRecognitionCostSystem in CostAlgebra as well as by orbitCount in SymmetryGroupPreference. It realizes the eight-tick octave together with the 45-fold cycle inside the Recognition framework, fixing the joint period at 360 beats. The construction closes the interface for any downstream algebra that must synchronize the two periodicities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.