even_D_not_coprime
plain-language theorem explainer
The theorem shows that even dimensions D in {2,4,6,8,10} make 2^D and the triangular number T(D squared) share a factor of two. Researchers formalizing the selection of spatial dimension three in Recognition Science cite this to demonstrate partial period alignment for even D. The argument proceeds by case exhaustion on the finite set of dimensions followed by direct computation of the coprimality predicate.
Claim. For every natural number $D$ belonging to the finite set $S = {2,4,6,8,10}$, the integers $2^D$ and $T(D^2)$ are not coprime, where the triangular number is given by $T(n) = n(n+1)/2$.
background
The SyncMinimization module encodes constraint (S) of the Dimensional Rigidity paper, which asserts that dimension three uniquely minimizes the synchronization period among odd spatial dimensions. The triangular number function T maps each natural number n to n(n+1)/2, and phasePeriod(D) is the specialization T(D squared). The module document notes that even D render T(D squared) even, producing a nontrivial gcd with 2^D. This fact is used to separate even from odd cases in the larger minimization argument. The phasePeriod definition in the same module provides the explicit formula appearing in the statement.
proof idea
The term proof introduces the variable D together with the hypothesis that it lies in the given Finset. It then invokes fin_cases on that hypothesis to generate five subgoals, one for each listed dimension. Each subgoal is discharged by native_decide, which evaluates the negated coprimality statement by direct calculation.
why it matters
The result populates the even_D_fails component of the ConstraintS_Cert structure that certifies constraint (S). It thereby contributes to the proof that only odd dimensions achieve coprimality between the octave period 2^D and the phase T(D²), confirming that D = 3 produces the minimal synchronization cost of 360. The argument aligns with the eight-tick octave and the selection of three spatial dimensions in the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.