sync_implies_D3
plain-language theorem explainer
The declaration shows that the synchronization period is divisible by eight, isolating the 2^3 factor that forces spatial dimension D=3 under the gap-45 and eight-tick conditions of Recognition Science. Researchers deriving dimensional constraints from the RS forcing chain would cite it when closing the synchronization step. The proof is a one-line wrapper that rewrites the period via an upstream equality and exhibits the quotient 45.
Claim. $2^3$ divides the synchronization period.
background
The DimensionForcing module proves that spatial dimension D=3 is forced by the RS framework through four arguments, including the gap-45 / 8-tick synchronization. The synchronization period is defined as the least common multiple of the 8-tick cycle (arising from 2^D for ledger coverage) and the 45-tick cumulative phase (the ninth triangular number T(9)). This yields lcm(8,45)=360=2^3 * 3^2 * 5, which uniquely identifies D=3 via the 2^3 factor. The upstream result sync_period_eq_360 states: 'The sync period is 360 (proved in SyncMinimization).'
proof idea
The term proof rewrites the synchronization period using the equality from sync_period_eq_360, replacing it with the concrete value 360. It then applies the 'use' tactic with the integer 45 to witness the required divisibility, since 360 = 8 * 45, and closes with reflexivity.
why it matters
This theorem supplies the explicit 2^3 factor in the synchronization argument of the DimensionForcing module, completing the gap-45 step that isolates D=3. It directly supports the eight-tick octave (T7) and the forcing of D=3 (T8) in the RS chain. The result feeds the combined forcing section that follows in the same module and relies on the numerical value established by sync_period_eq_360.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.