coprime_9
plain-language theorem explainer
The declaration establishes that 512 and the 81st triangular number are coprime. Researchers verifying synchronization period minimization for odd dimensions would cite this instance when checking the D=9 case in the lcm construction. The proof succeeds by direct evaluation of the gcd via the native_decide tactic.
Claim. $gcd(2^9, T(81)) = 1$, where $T(n) = n(n+1)/2$ is the $n$th triangular number.
background
The SyncMinimization 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)). The function phasePeriod D returns the triangular number T(D*D). For odd D the value T(D^2) is odd, guaranteeing coprimality with the power of 2 and thereby the full uncomputability barrier in the sync period.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to compute gcd(512, T(81)) and confirm the result equals 1.
why it matters
This result supports the claim that odd dimensions yield coprime factors in lcm(2^D, T(D^2)), with D=3 producing the minimal sync period 360. It supplies a verification step for the D=9 case within the module's examination of odd dimensions and aligns with the generalization of the eight-tick octave to 2^D in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.