coprime_11
plain-language theorem explainer
The theorem shows that 2^11 and the triangular number T(121) share no common prime factors. Researchers checking the synchronization minimization argument across odd dimensions in Recognition Science cite this result to confirm period misalignment for D=11. The proof is a direct native_decide evaluation of the coprimality predicate on the explicit integers.
Claim. $2^{11}$ and $T(121)$ are coprime, where $T(n) = n(n+1)/2$ denotes the nth triangular number.
background
The SyncMinimization module encodes constraint (S) from the Dimensional Rigidity paper. It shows that 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 the squared dimension. The upstream Sync structure requires beats / 8 = 45 and beats / 45 = 8, fixing the minimal period at 360 for D=3. The period definition supplies phi-powered scaling while the for structure records meta-realization properties.
proof idea
The proof is a one-line term that invokes native_decide to evaluate the coprimality predicate directly on the concrete numbers 2^11 and phasePeriod 11.
why it matters
This result supports the module's demonstration that odd dimensions produce coprime synchronization periods, reinforcing why D=3 minimizes the lcm period among candidates. It aligns with the eight-tick octave (T7) in the forcing chain by verifying that 2^D stays distinct from T(D^2) when D is odd. No downstream theorems currently depend on this instance.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.