triangular
plain-language theorem explainer
The function computing the nth triangular number T(n) equals n(n+1)/2. Researchers deriving the 45-tick synchronization from the eight-tick cycle cite this to express cumulative phase accumulation over the closure count of nine steps. The definition is introduced as a direct algebraic formula with no reduction steps.
Claim. The nth triangular number is given by $T(n) = n(n+1)/2$.
background
The module supplies a physically grounded derivation of the number 45 in the dimension-forcing argument. The key insight is that 45 equals the 9th triangular number T(9) = 9*10/2. This arises because the 8-tick cycle (from 2^D with D=3) requires a closure step, yielding nine steps total for a complete cycle. Cumulative phase then sums the linear contributions from each step k, producing the triangular number T(9).
proof idea
This is a direct definition implementing the standard triangular number formula T(n) = n(n+1)/2.
why it matters
This definition supplies the triangular number used in closure_number_eq_9 and cumulative_phase to motivate the 45-tick synchronization. It feeds the dimension_forcing theorem that equates 2^3 = 8 with lcm(8,45)=360, thereby forcing D=3. The parent result is the dimension_sum theorem, which equates the sum of fundamental representation dimensions to the D-th triangular number for the cube face-pairs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.