coprime_5
plain-language theorem explainer
Nat.Coprime (2^5) (phasePeriod 5) asserts that 32 and T(25) share no common prime factors. A researcher verifying the uniqueness of D=3 in minimizing synchronization periods would reference this result to confirm coprimality at D=5. The proof relies on native_decide to evaluate the gcd computation directly.
Claim. $2^5$ and $T(25)$ are coprime, where $T(n) = n(n+1)/2$ and phasePeriod(5) evaluates to $T(25)$.
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^2)). phasePeriod(D) is defined as T(D*D), the triangular number of D squared, representing the cumulative phase from the parity matrix of the hypercube Q_D. This theorem checks the coprimality condition for D=5, where 2^5=32 and phasePeriod(5)=T(25)=325.
proof idea
The proof is a one-line wrapper that invokes native_decide to compute whether gcd(32, 325) equals 1.
why it matters
This result contributes to the argument that only odd D yield full coprimality between 2^D and T(D^2), supporting the selection of D=3 as the dimension minimizing the sync period to 360. It aligns with the eight-tick octave generalization to 2^D in the Recognition framework. No open questions are directly addressed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.