syncPeriod_eq_lcm
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the integers 8 and 45 from the forcing chain.
- Does not compute numerical lcm beyond native evaluation.
- Does not address SI conversions or external calibration.
formal statement (Lean)
207lemma syncPeriod_eq_lcm : syncPeriod = Nat.lcm 8 45 := by native_decide
proof body
Term-mode proof.
208
209/-! ## K-gate derived displays in RS-native units -/
210
211/-- Recognition time display: τ_rec = (2π)/(8 ln φ) · τ₀. -/