syncPeriod
plain-language theorem explainer
The declaration fixes the synchronization period at 360 for three spatial dimensions in RS-native units. Researchers proving dimensional rigidity or constraint (S) minimization would cite this constant when showing D=3 yields the shortest alignment period. The definition is a direct numerical assignment that matches lcm(8,45) without further computation.
Claim. The synchronization period is defined by the constant equation $S = 360$.
background
The RS-native unit system takes the tick (atomic time quantum) and voxel (causal spatial step with $c=1$) as base standards, with derived quantities coh $= φ^{-5}$ and action quantum $ħ = $ coh $· τ_0$. All scaling follows the φ-ladder, and synchronization periods align the eight-tick octave $2^D$ with a phase period of 45. Upstream, the general form is given by syncPeriod(D) $:=$ lcm$(2^D$, phasePeriod(D)) and equivalently lcm$(2^D$, 45) in the DraftV1 paper.
proof idea
Direct constant definition that assigns the integer 360. No tactics or lemmas are applied inside the body; the value is chosen to satisfy the lcm identity used by downstream results.
why it matters
This supplies the concrete value required by ConstraintS_Cert and constraint_S_minimization in Gap45.SyncMinimization, which formalize that D=3 uniquely minimizes the synchronization period among odd dimensions. It anchors the eight-tick octave and D=3 spatial dimensions from the forcing chain (T7-T8), enabling the paper's claim that 45 arises as the phase period that minimizes alignment cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.