syncPeriod_3
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not prove minimization over all odd dimensions greater than or equal to 3.
- Does not derive the definition of phasePeriod from the parity matrix.
- Does not address the coprimality argument for odd versus even D.
Lean usage
exact syncPeriod_3formal statement (Lean)
88@[simp] theorem syncPeriod_3 : syncPeriod 3 = 360 := by native_decide