coprime_3
plain-language theorem explainer
The theorem proves that 8 and the triangular number T(9) share no common divisors other than 1. Researchers formalizing the selection of three spatial dimensions cite it to confirm that the synchronization period lcm(8,45) equals 360 with no partial alignment. The proof is a direct computational check via native_decide on the concrete integers.
Claim. $2^3$ and $T(3^2)$ are coprime, where $T(n) = n(n+1)/2$ is the $n$-th triangular number.
background
The SyncMinimization module encodes constraint (S) from the Dimensional Rigidity paper: the synchronization period for dimension D is lcm(2^D, T(D^2)). The upstream definition phasePeriod(D) := T(D * D) supplies the phase term T(D^2). For odd D the triangular number T(D^2) is odd, forcing gcd(2^D, T(D^2)) = 1 and therefore the full lcm value.
proof idea
One-line wrapper that applies native_decide to evaluate the concrete coprimality predicate on 8 and 45.
why it matters
The result is invoked directly by the gap45 definition in PerpetualComplexity, which builds the Gap45Frustration record with coprime field set to this theorem and sync_period set to 360. It supplies the D=3 case in the module argument that only odd dimensions yield full coprimality and that D=3 minimizes the period among them, consistent with the eight-tick octave generalized to 2^D.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.