cumulative_phase
plain-language theorem explainer
cumulative_phase maps cycle length n to the nth triangular number T(n), encoding total phase from linear accumulation of tick contributions. Researchers closing the physical motivation gap for 45-tick synchronization in the Recognition framework cite it to equate T(9) with the closed 8-tick cycle. The definition is a direct one-line reference to the triangular function.
Claim. The cumulative phase over a closed cycle of length $n$ is the $n$th triangular number $T(n) = n(n+1)/2$.
background
The module supplies a physical derivation for the 45 appearing in the dimension-forcing argument by treating it as cumulative phase in the 8-tick ledger. The base time quantum is the tick, set to 1 in RS-native units. The 8-tick phase function returns $kπ/4$ for $k$ in Fin 8 and is periodic with period $2π$ (from EightTick.phase). Triangular numbers are defined by the sibling declaration as $T(n) = n(n+1)/2$, summing the first $n$ naturals to capture linear cost accumulation per step.
proof idea
One-line wrapper that applies the triangular definition.
why it matters
This definition supplies the object used by phase_45, whose doc-comment states that 45 equals T(9) and therefore equals the cumulative phase of a closed 8-tick cycle. It fills the physical-motivation gap identified in the module header for the 45-tick synchronization step. The construction rests on the eight-tick octave (T7) and the D=3 forcing (T8) from the unified chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.