sync_period_is_360
plain-language theorem explainer
The synchronization period equals 360, confirming that the least common multiple of the eight-tick cycle and the 45-tick cumulative phase closes after exactly 360 steps. Dimension-forcing arguments cite this result to close the physical motivation gap for the 45 parameter at D=3. The proof is a one-line simplification of the definitions followed by native decision on the arithmetic equality.
Claim. The synchronization period, defined as the least common multiple of the eight-tick period and the 45-tick phase closure, equals 360.
background
In the Gap45.PhysicalMotivation module the eight-tick period is defined as 8, arising from the 2^D cycle with D=3. The 45-tick phase equals the ninth triangular number T(9)=45, obtained via the closure principle: an 8-tick cycle requires 9 steps to return to the initial phase state, so the cumulative phase sum equals 1+2+...+9=45. The synchronization period is then defined as Nat.lcm eight_tick gap_45. This module supplies the physical motivation for the 45 parameter that the paper identified as missing from the dimension-forcing argument.
proof idea
The term proof applies simp using the definitions of sync_period, eight_tick and phase_45, then invokes native_decide to confirm the numerical equality lcm(8,45)=360.
why it matters
This theorem supplies the arithmetic verification required by the synchronization requirement in the Gap45 module documentation, thereby supporting the eight-tick octave (T7) and the forcing of D=3 (T8) in the unified chain. It directly addresses the paper's noted gap on physical motivation for the 45-tick closure. No downstream uses appear in the current graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.