phasePeriod_even_10
plain-language theorem explainer
Researchers on dimensional rigidity cite this to confirm that even D yields an even T(D²), allowing partial alignment between the 2^D and triangular periods. It supplies one concrete data point in the argument that only odd dimensions achieve full coprimality and that D=3 therefore minimizes the synchronization period. The proof is a one-line native decision that evaluates the triangular number directly.
Claim. The triangular number $T(100)$ is even, i.e., $2$ divides $T(100)$ where $T(n) = n(n+1)/2$.
background
The SyncMinimization module formalizes constraint (S) from the Dimensional Rigidity paper: among odd spatial dimensions D ≥ 3, D=3 uniquely minimizes lcm(2^D, T(D²)). For even D the periods partially align because T(D²) is even; only odd D produces coprimality. The triangular number is defined locally by T(n) := n(n+1)/2 and the phase period by phasePeriod(D) := T(D*D). Upstream results supply the period concept via the T abbreviation in Breath1024 and the concrete phasePeriod definition in the same module.
proof idea
The proof is a one-line term that invokes native_decide on the predicate 2 ∣ phasePeriod 10.
why it matters
This instance illustrates the even-D case that reduces the uncomputability barrier via gcd(2^D, T(D²)) > 1. It feeds the parent claim that D=3 alone minimizes the sync period at 360 among odd dimensions. The module connects directly to the eight-tick octave generalized to 2^D and the selection of D=3 as the unique minimizer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.