triangular_formula
plain-language theorem explainer
The triangular number formula equates the nth triangular number to n(n+1)/2. Researchers deriving the 45-tick synchronization from the 8-tick cycle in Recognition Science cite this to compute cumulative phase accumulation over a closed cycle. The proof is a one-line reflexivity that matches the definition directly to the closed form.
Claim. The nth triangular number satisfies $T(n) = n(n+1)/2$.
background
The Gap45.PhysicalMotivation module supplies a physically grounded derivation of the number 45 in the dimension-forcing argument. It identifies 45 as the 9th triangular number arising from cumulative phase in the 8-tick ledger cycle: each tick k contributes phase proportional to k, so the total over a closed cycle of 9 steps is T(9). The sibling definition states that the nth triangular number is T(n) = 1 + 2 + ... + n. Upstream structures from LedgerFactorization and PhiForcingDerived calibrate the J-cost and ledger neutrality that make the phase accumulation constraint meaningful.
proof idea
This is a one-line wrapper that applies reflexivity to equate the definition of triangular to its closed-form expression.
why it matters
This declaration confirms the arithmetic identity required for the cumulative phase argument in the 45-tick synchronization. It directly supports the closure principle (8 ticks plus one step yields 9) that produces T(9) = 45, linking the eight-tick octave (T7) and D = 3 spatial dimensions from the forcing chain. The result fills the physical motivation gap noted in the module for the Recognition Science ledger model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.