sync_period
plain-language theorem explainer
The synchronization period is defined as the least common multiple of the eight-tick period and the 45-unit cumulative phase period. Researchers working on dimension forcing and perpetual complexity cite this to obtain the 360-unit cycle that reconciles the ledger closure with phase accumulation. The definition applies the lcm function directly to the two periods.
Claim. Let $T_8 = 8$ denote the eight-tick period arising from $2^D$ at $D=3$, and let $P_{45}=45$ be the cumulative phase over the closed cycle. The synchronization period is then $lcm(T_8, P_{45})$.
background
This definition sits in the module that supplies a physically grounded derivation of the number 45 to close the gap identified in the paper. The eight-tick period equals 8 because it is forced by $2^D$ when the spatial dimension equals 3. The phase period equals the ninth triangular number, obtained by summing the phase contributions 1 through 9 over the nine steps required to close an eight-tick cycle (the fence-post principle). Upstream results state that the eight-tick period is the fundamental time unit setting the infrared cutoff for recognition dynamics.
proof idea
The declaration is a direct definition that sets the synchronization period to the least common multiple of the eight-tick value and the phase value. It depends on the upstream definitions of those two periods and applies the standard lcm operation from the natural numbers library.
why it matters
This supplies the synchronization period that enters the Gap45Frustration structure, where the coprimality of 8 and 45 forces the sync period to be 360. Downstream theorems then equate this period to 360 and use it to establish that dimension 3 is RS-compatible, satisfying the eight-tick condition and the gap synchronization. It thereby closes the physical motivation for the 45 in the forcing chain from the eight-tick octave to D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.