syncPeriod_3
plain-language theorem explainer
The synchronization period for three spatial dimensions equals 360 in native units. Cosmology models of perpetual complexity cite this to fix the minimal synchronization cost at D=3. The proof is a direct native decision on the lcm expression for input 3.
Claim. The synchronization period for three spatial dimensions equals 360, where the period is the least common multiple of $2^D$ and the triangular number $T(D^2)$.
background
This module formalizes constraint (S) from the Dimensional Rigidity paper: among odd spatial dimensions D ≥ 3, D = 3 uniquely minimizes the synchronization period given by the least common multiple of 2 to the D and the triangular number T of D squared. The synchronization period is defined as the least common multiple of 2^D and phasePeriod D, with phasePeriod D yielding the triangular number T(D²). Upstream results fix the constant value at 360 in RSNativeUnits while the general form in DraftV1 specializes to the least common multiple of 2^D and 45 for the D=3 case.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the least common multiple expression for input 3.
why it matters
This supplies the value 360 invoked by sync_period_eq_360 and sync_exceeds_both in PerpetualComplexity. It realizes the minimal sync period claim for D=3 from the module documentation, linking to the eight-tick octave at T7 in the forcing chain. It provides the computational anchor for synchronization cost in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.