T_0
plain-language theorem explainer
The theorem states that the triangular number T evaluates to zero at argument zero. Researchers deriving dynamical times and acceleration ratios in the Gravity.ParameterizationBridge module cite this base case when unfolding T at the origin. The proof reduces directly to reflexivity on the defining equation of T.
Claim. The zeroth triangular number vanishes: $T(0) = 0$, where $T(n) := n(n+1)/2$.
background
The function T computes the nth triangular number via the formula T(n) = n(n + 1)/2. This declaration sits inside the SyncMinimization module, which formalizes why dimension D = 3 uniquely minimizes the synchronization period lcm(2^D, T(D²)) among odd D ≥ 3, as described in the module documentation. It depends on the definition of T in the same module and an alias T in Breath1024 for fundamental periods.
proof idea
The proof is a one-line wrapper that applies reflexivity to the definition of T.
why it matters
This base case supports the triangular number evaluations underlying the selection of D = 3 in the Dimensional Rigidity argument. It feeds into theorems in Gravity.ParameterizationBridge such as accel_mul_Tdyn_sq and time_ratio_sq_eq_accel_ratio_mul_r_ratio that relate accelerations and dynamical times. The result aligns with the eight-tick octave generalization to 2^D periods in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.