syncPeriod
plain-language theorem explainer
The declaration defines the synchronization period S(D) as lcm(2^D, 45) for the Draft_v1.tex formalization surface. Researchers verifying dimensional selection under constraint (S) cite it when checking why D=3 yields the minimal period among odd integers up to 11. The definition is a direct abbreviation that specializes the general phase-period form by fixing the second argument to 45.
Claim. The synchronization period is defined by $S(D) := lcm(2^D, 45)$.
background
In Recognition Science the synchronization period encodes the least common multiple required by the eight-tick octave (T7) and the phase period at dimension D. The module mirrors theorem statements from Draft_v1.tex, supplying paper-oriented names while routing heavy external mathematics through explicit hypothesis interfaces. Upstream, Gap45.SyncMinimization.syncPeriod supplies the general form lcm(2^D, phasePeriod D), and RSNativeUnits.syncPeriod specializes it at D=3 to the constant 360.
proof idea
This is a direct definition that applies Nat.lcm to the pair (2^D, 45). No lemmas or tactics are used; the body is a one-line abbreviation.
why it matters
The definition supplies the concrete S(D) required by constraint_S_minimization and D3_unique_minimizer in Gap45.SyncMinimization. It implements the synchronization period appearing in Draft_v1.tex and thereby supports the framework claim that D=3 uniquely minimizes the period among odd dimensions, fixing the value 360 that enters the alpha band and mass-ladder formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.