T_25
plain-language theorem explainer
The theorem asserts that the 25th triangular number equals 325. Researchers verifying synchronization periods for odd dimensions D greater than or equal to 3 cite this value when comparing the five-dimensional case to the minimum achieved at D=3. The proof reduces to a direct evaluation of the triangular number definition via native_decide.
Claim. The 25th triangular number satisfies $T(25) = 325$, where $T(n) = n(n+1)/2$.
background
The triangular number function is defined by $T(n) = n(n+1)/2$. The Gap45 module uses this to compute synchronization periods via lcm(2^D, T(D^2)) for odd spatial dimensions D. The module documentation states that D=3 yields the minimal period among odd D >=3, with T(9)=45 giving lcm(8,45)=360, while D=5 requires T(25)=325 and produces lcm(32,325)=10400. Upstream, the Breath1024 module introduces T as the abbreviation for fundamental periods.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the triangular number definition directly at argument 25.
why it matters
This supplies the explicit value T(25)=325 required to compare synchronization costs across dimensions in the Dimensional Rigidity argument. It supports the module claim that D=3 uniquely minimizes the sync period lcm(2^D, T(D^2)) among odd D >=3. The result connects to the generalization of the eight-tick octave to 2^D and the selection of 45 as the minimal T(D^2) value.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.