T_25
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not prove the closed-form expression for T(n) at arbitrary n.
- Does not compute the least common multiple with 2^D.
- Does not establish minimality of the synchronization period.
- Does not reference the J-function or phi-ladder from the forcing chain.
formal statement (Lean)
43@[simp] theorem T_25 : T 25 = 325 := by native_decide