sync_3_lt_11
plain-language theorem explainer
Among odd spatial dimensions D ≥ 3 the synchronization period lcm(2^D, T(D²)) is strictly smaller at D=3 than at D=11. Researchers formalizing dimensional selection in Recognition Science cite the result to justify why the 45-phase period is uniquely preferred. The proof is a direct native computation that evaluates the two concrete period values and confirms the inequality.
Claim. $lcm(2^3, T(9)) < lcm(2^{11}, T(121))$, where $T(n) = n(n+1)/2$ is the nth triangular number.
background
The module encodes constraint (S) from the Dimensional Rigidity paper: among odd D ≥ 3, D=3 uniquely minimizes the synchronization period lcm(2^D, T(D²)). The 8-tick period generalizes to 2^D while the parity matrix of the hypercube Q_D contributes D² entries whose cumulative phase is the triangular number T(D²). For odd D the triangular number is odd, guaranteeing coprimality with 2^D and therefore the full least-common-multiple cost.
proof idea
The proof is a one-line wrapper that applies native_decide to the concrete numerical values of the two synchronization periods.
why it matters
The declaration supplies the concrete comparison that realizes constraint (S) and thereby explains the selection of the 45-phase period as T(9) at the minimizing dimension. It sits inside the forcing chain at the step that fixes D=3 and the eight-tick octave, and it supplies the numerical grounding for later mass-ladder and Berry-threshold arguments that presuppose the minimal synchronization cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.