syncPeriod_3_eq_360
plain-language theorem explainer
The equality establishes that the synchronization period evaluates to 360 at three dimensions in Recognition Science units. Researchers modeling the eight-tick octave or fixing spatial dimension D=3 would cite this when anchoring the phi-ladder constants. The proof reduces to a single native_decide tactic that computes the closed-form expression directly.
Claim. The synchronization period at three spatial dimensions satisfies $syncPeriod(3) = 360$.
background
In Recognition Science the synchronization period is the function $D mapsto 2^D times 45$, which equals lcm(8,45) at D=3. This definition appears in RSNativeUnits and is used throughout the forcing chain to realize the eight-tick octave (T7) and the emergence of D=3 (T8). The Papers.DraftV1 module re-exports such equalities from Draft_v1.tex so that paper statements can be audited against the certified library without introducing new axioms.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the equality from the definition of syncPeriod.
why it matters
This pins the minimal value of the synchronization period at the dimension forced by the unified forcing chain, directly supporting the synchronization_selection_principle that proves uniqueness of the minimum among D greater than or equal to 3. It aligns with the resource-functional minimization packaged in the same paper section and with the T7 eight-tick octave landmark.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.