syncPeriod_eq_lcm
plain-language theorem explainer
The synchronization period in RS-native units equals the least common multiple of 8 and 45. Researchers deriving time displays, coherence quanta, and phi-ladder scalings from the eight-tick octave cite this equality when aligning discrete ledger intervals. The proof is a one-line native evaluation of the constant definition.
Claim. The synchronization period equals $lcm(8,45)$.
background
The RSNativeUnits module defines a native measurement system with base units tick (τ₀, one ledger posting interval) and voxel (ℓ₀, causal spatial step), enforcing c=1 and organizing all scales on the phi-ladder φ^n. Derived quanta are coh = φ^{-5} (energy) and act = ħ (action). The synchronization period is the integer aligning the eight-tick octave with the 45-unit phase period, fixed at 360.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the equality between the defined synchronization period and lcm(8,45).
why it matters
This lemma anchors the synchronization period used in K-gate displays and time quanta, linking the eight-tick octave (T7) and D=3 (T8) to the phase period in the forcing chain. It supports the Recognition Composition Law and phi-ladder mass formula by fixing the common period for discrete time alignment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.