sync_period_eq_360
plain-language theorem explainer
The synchronization period defined as the least common multiple of the eight-tick cycle and gap-45 parameter equals 360. Researchers on dimension forcing cite this to confirm the numerical link between the 2^D ledger cycle and triangular phase accumulation at D=3. The proof is a one-line term wrapper that unfolds the three definitions and applies reflexivity.
Claim. Let the eight-tick period be 8 and the gap-45 parameter be 45. The synchronization period, defined as their least common multiple, equals 360.
background
The DimensionForcing module proves that spatial dimension D=3 is forced by the Recognition Science framework through four arguments, one of which is the gap-45 / 8-tick synchronization. The eight-tick period is the fundamental evolution period 2^D. The gap-45 parameter is the integration gap D^2(D+2) evaluated at D=3. The synchronization period is their least common multiple. Upstream, the tick definition supplies the fundamental time quantum, while the module's own sync_period definition encodes the lcm construction. The module document states that this synchronization condition lcm(8,45)=360 uniquely identifies D=3 because the 2^3 factor corresponds to the ledger coverage for three dimensions and matches the SO(3) periodicity of 360 degrees.
proof idea
The term proof unfolds sync_period, eight_tick, and gap_45 to expose the concrete Nat.lcm 8 45 expression, then applies reflexivity to verify the numerical identity.
why it matters
This equality feeds directly into D3_compatible (which assembles the RSCompatibleDimension record for dimension 3) and into sync_implies_D3 (which extracts the 2^3 divisor). It closes the gap-45 / 8-tick synchronization step in the Dimension Forcing module, supporting the claim that only D=3 produces the 360-period that aligns with the eight-tick octave (T7) and forces D=3 (T8). The downstream rotation_period theorem reuses the same equality to relate the period to SO(3) rotations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.