syncPeriod_def
plain-language theorem explainer
Recognition Science papers rely on the identity that the synchronization period in D dimensions equals lcm(2^D, 45). This arithmetic fact supports derivations of the 360-unit period when D equals 3 and links to the eight-tick octave. The term-mode proof applies reflexivity directly to the definition supplied by the Gap45 module.
Claim. For every natural number $D$, the synchronization period satisfies $syncPeriod(D) = lcm(2^D, 45)$.
background
The module Papers.DraftV1 mirrors theorem statements from Draft_v1.tex and re-exports proved results under paper-oriented names. The synchronization period is introduced in Gap45.SyncMinimization as $syncPeriod(D) := lcm(2^D, phasePeriod D)$, with the base case fixed at 360 in Constants.RSNativeUnits. The upstream doc-comment states: 'The synchronization period for dimension D.'
proof idea
The proof is a one-line term-mode reflexivity application. It matches the definition of syncPeriod from Gap45.SyncMinimization exactly to the lcm expression. The inline comment records that 45 is odd so gcd(2^D, 45) = 1, confirming the lcm identity.
why it matters
This lemma supplies the explicit arithmetic form of the synchronization period used in the paper's proof of the synchronization selection principle. It connects to the T7 eight-tick octave by providing the period as lcm(2^D, 45) and closes the gap between the general Gap45 definition and the concrete 45-unit phase. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.