sync_period
plain-language theorem explainer
The synchronization period is defined as the least common multiple of the eight-tick cycle and the gap-45 parameter. Dimension-forcing and cosmology researchers cite it when showing that this value equals 360 and isolates the 2 cubed factor required for three spatial dimensions. The definition is a direct one-line application of the lcm operation to the two fixed periods.
Claim. Define the synchronization period $s$ by $s = {lcm}(8,45)$, where 8 is the eight-tick period and 45 is the gap parameter.
background
In the Dimension Forcing module the eight-tick period is the constant 8, arising as 2^D for ledger coverage when D equals 3. The gap-45 parameter is the constant 45, obtained as the triangular number T(9) that accumulates linear phase cost over a closed eight-tick cycle. The module setting requires these two periods to synchronize, because only D equals 3 produces a common multiple whose prime factorization encodes the required 2 cubed factor while satisfying topological linking conditions.
proof idea
One-line definition that applies the Nat.lcm operation directly to the constants eight_tick and gap_45.
why it matters
This definition supplies the common period 360 that appears in rotation_period and in the structure RSCompatibleDimension, which requires 2^D to divide the synchronization period. It feeds the Gap45Frustration structure and the theorems sync_period_eq_360 and sync_exceeds_both in PerpetualComplexity. The construction closes the synchronization step of the dimension-forcing argument that links the eight-tick octave to D equals 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.