sync_strictly_increasing_odd
plain-language theorem explainer
The synchronization period increases strictly for successive odd dimensions starting at D=3. Researchers on dimensional selection in Recognition Science cite this result to confirm D=3 yields the unique minimum among odd integers. The proof is a direct term-mode verification that applies native_decide to each of the four lcm inequalities.
Claim. Let $syncPeriod(D) := lcm(2^D, T(D^2))$ where $T(n) = n(n+1)/2$ is the triangular number. Then $syncPeriod(3) < syncPeriod(5) < syncPeriod(7) < syncPeriod(9) < syncPeriod(11)$.
background
The module formalizes constraint (S) from the Dimensional Rigidity paper: among odd spatial dimensions D ≥ 3, D = 3 uniquely minimizes the synchronization period lcm(2^D, T(D²)). The synchronization period is defined locally as syncPeriod(D) = Nat.lcm (2^D) (phasePeriod D), where phasePeriod D equals the triangular number T(D²). Upstream results supply the base case syncPeriod = 360 in RSNativeUnits together with the Q₃ structures from SpectralEmergence that fix the eight-tick octave generalization to 2^D.
proof idea
The proof is a term-mode one-liner that applies native_decide to each conjunct, confirming the numerical ordering of the four lcm values for D = 3,5,7,9,11.
why it matters
This theorem supplies the D3_unique_minimizer component inside constraintS, the verified certificate for constraint (S). It directly supports the claim that D = 3 minimizes synchronization cost in the eight-tick octave (T7) and thereby selects the 45 rung on the phi-ladder. The result closes the strict-increase step required by the module's argument that only odd D preserves full coprimality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.