T_1
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 in Recognition Science
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.
scope and limits
- Does not prove the closed-form sum for arbitrary n.
- Does not compute lcm values or compare periods across dimensions.
- Does not address even dimensions or the full coprimality argument.
formal statement (Lean)
41@[simp] theorem T_1 : T 1 = 1 := rfl