coprime_7
plain-language theorem explainer
The coprimality of 128 and the triangular number T(49) is asserted to confirm that the synchronization period for dimension 7 does not collapse. Researchers formalizing dimensional rigidity would cite it when comparing odd D values to isolate the D=3 minimum. The proof reduces to direct native computation of the gcd.
Claim. $gcd(2^7, T(49)) = 1$ where $T(n) = n(n+1)/2$ is the triangular number.
background
phasePeriod D computes the triangular number T(D²) with T(n) = n(n+1)/2. The module develops the synchronization period as lcm(2^D, phasePeriod D) and shows this quantity is minimized at D=3 among odd dimensions D ≥ 3 because T(D²) remains odd precisely when D is odd, yielding full coprimality with 2^D.
proof idea
A one-line wrapper applies the native_decide tactic to evaluate the coprimality predicate by direct computation of the gcd of 128 and 1225.
why it matters
The declaration supports the argument that only odd dimensions preserve coprime periods under the generalization of the eight-tick octave to 2^D, reinforcing why D=3 uniquely minimizes the synchronization period to 360. It supplies the D=7 case in the explicit comparison of odd dimensions given in the module documentation. No downstream theorems depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.