T_4
plain-language theorem explainer
The fourth triangular number equals 10. Researchers computing synchronization periods for odd spatial dimensions would cite this value when verifying small cases ahead of the D=3 minimum. The proof is a direct native evaluation of the triangular-number definition.
Claim. $T(4) = 10$, where the triangular number is given by $T(n) = n(n+1)/2$.
background
The triangular number function is defined by $T(n) = n(n+1)/2$. In the Gap45 module this definition is used to evaluate the cumulative phase $T(D^2)$ that enters the synchronization period $lcm(2^D, T(D^2))$. The module formalizes the claim that, among odd dimensions $D >= 3$, only $D=3$ yields the globally minimal synchronization cost because $T(9)=45$ is coprime to $2^3=8$.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the arithmetic expression for $T(4)$.
why it matters
The result supplies a verified building block for the synchronization-period argument that selects D=3 and therefore the 45-tick phase in the eight-tick octave. It supports the broader claim that D=3 uniquely minimizes the uncomputability barrier among odd dimensions, consistent with the forcing-chain requirement that spatial dimension equal 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.