sync_factorization
The declaration shows that the synchronization period, defined as the least common multiple of the eight-tick cycle and the gap-45 parameter, equals eight times forty-five. Researchers tracing the forcing chain from ledger coverage to spatial dimension would cite this identity to confirm the numerical link that isolates D equals 3. The proof unfolds the three definitions and closes by reflexivity after noting that the inputs are coprime.
claimLet the synchronization period be the least common multiple of the eight-tick period and the gap-45 parameter. Then this period equals $8 times 45$.
background
The DimensionForcing module proves that spatial dimension equals 3 by four routes, one of which is the synchronization condition between the eight-tick cycle and the gap-45 parameter. The eight-tick period is the ledger coverage length 2 to the power D at D equals 3. The gap-45 parameter is the triangular number T(9) equals 45, which accumulates linear phase cost over a closed cycle by the fence-post principle (eight sections require nine posts). Upstream definitions set the eight-tick period to the constant 8 and the gap parameter to the constant 45, with the synchronization period defined as their least common multiple.
proof idea
The proof unfolds the definitions of the synchronization period, the eight-tick period, and the gap-45 parameter. The least-common-multiple expression then reduces directly to the product because the greatest common divisor of 8 and 45 is 1. Reflexivity discharges the resulting equality.
why it matters in Recognition Science
This identity supplies the numerical step that lets the synchronization condition force D equals 3, since the factor 8 recovers 2 cubed while the full period 360 factors as 2 cubed times 3 squared times 5, matching the periodicity of SO(3). It feeds the degeneracy analysis that appears in Gap45Degeneracy. The result closes one link in the chain from the eight-tick octave (T7) to spatial dimension (T8) in the forcing sequence.
scope and limits
- Does not compute the numerical value of the synchronization period.
- Does not derive the gap-45 parameter from ledger axioms.
- Does not address the topological linking argument for D equals 3.
- Does not prove uniqueness of the synchronization period among possible cycles.
formal statement (Lean)
332theorem sync_factorization : sync_period = 8 * 45 := by
proof body
Term-mode proof.
333 unfold sync_period eight_tick gap_45
334 -- lcm(8, 45) = 8 * 45 / gcd(8, 45) = 360 / 1 = 360
335 -- But actually gcd(8, 45) = 1, so lcm = 8 * 45 = 360
336 rfl
337
338/-- 360 = 2³ × 3² × 5. -/