rotation_period
The declaration states that the synchronization period equals 360. A researcher deriving D=3 from ledger periodicity or SO(3) rotation would cite it when closing the eight-tick argument. The proof is a direct one-line wrapper that invokes the already-established equality for the least common multiple of the eight-tick cycle and the 45-phase.
claimThe synchronization period, defined as the least common multiple of the eight-tick cycle (equal to 8) and the gap-45 phase (equal to 45), equals 360.
background
The Dimension Forcing module derives spatial dimension D=3 from two independent arguments: topological linking (non-trivial knots exist only in D=3) and synchronization between the eight-tick ledger cycle and the 45-phase cumulative cost. The synchronization period is introduced as the least common multiple of these two quantities. Upstream results include the definition sync_period := Nat.lcm eight_tick gap_45 together with the direct verification that this lcm equals 360, and the parallel statement in PerpetualComplexity that the same period is 360.
proof idea
This is a one-line wrapper that applies the theorem sync_period_eq_360. The referenced equality itself unfolds the definition of sync_period and reduces the lcm computation to 360 by reflexivity.
why it matters in Recognition Science
The result closes the eight-tick synchronization step in the Dimension Forcing module, confirming that the period matches the 360-degree periodicity of SO(3) rotations. It thereby supports the T7-T8 forcing chain landmark that the eight-tick octave (period 2^3) forces D=3. The declaration supplies the numerical anchor needed for any downstream claim that links ledger conservation to spatial dimension.
scope and limits
- Does not derive the eight-tick value from the forcing chain.
- Does not prove topological linking properties.
- Does not address synchronization in dimensions other than D=3.
- Does not supply a physical model for the 45-phase accumulation.
formal statement (Lean)
343theorem rotation_period : sync_period = 360 := sync_period_eq_360
proof body
Term-mode proof.
344
345/-- The 2³ factor in 360 corresponds to D = 3. -/