T_1
plain-language theorem explainer
The first triangular number evaluates to one. Researchers computing synchronization periods lcm(2^D, T(D²)) for odd dimensions cite this base case when verifying T(9) = 45 for D = 3. The proof reduces directly to reflexivity on the triangular-number definition.
Claim. $T(1) = 1$ where $T(n) = n(n+1)/2$.
background
The Gap45 module formalizes constraint (S) from the Dimensional Rigidity paper: among odd spatial dimensions D ≥ 3, D = 3 uniquely minimizes the synchronization period lcm(2^D, T(D²)). T(n) is the nth triangular number, defined by T(n) = n(n+1)/2. This rests on the abbrev T := ℕ from Breath1024 and the local definition of T.
proof idea
The proof is a one-line wrapper that applies reflexivity to the definition of T at argument 1.
why it matters
This base case supports the explicit computation of T(9) = 45 that yields the minimal sync period 360 for D = 3. It anchors the eight-tick octave (T7) and D = 3 (T8) selection argument in the module. The declaration feeds no downstream theorems in the current graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.