triangular_9_via_formula
plain-language theorem explainer
The arithmetic identity T(9) = 9*10/2 = 45 supplies the explicit cumulative phase count for the closed 8-tick cycle in the synchronization argument. Researchers closing the physical motivation gap in the dimension-forcing chain would cite this value to equate the 9-step closure with 45. The proof is a one-line reflexivity that reduces the closed-form expression immediately.
Claim. $T(9) = 9(n+1)/2 = 45$ where $T(n)$ denotes the nth triangular number.
background
The Gap45.PhysicalMotivation module supplies a physically grounded derivation of the 45-tick synchronization to address the paper gap on unmotivated 45. The 8-tick cycle (from 2^D with D=3) requires a closure step to return to the initial phase, yielding 9 steps total by the fence-post principle. Cumulative phase over the closed cycle is the triangular number T(n) = sum_{k=1 to n} k = n(n+1)/2.
proof idea
The proof is a one-line term that applies reflexivity to the arithmetic expression 9 * 10 / 2.
why it matters
This supplies the concrete numerical anchor for the 45-tick synchronization requirement in the physical motivation section, linking the 8-tick octave (T7) and D=3 (T8) to the cumulative phase constraint. It fills the explicit evaluation step in the closure principle and ledger neutrality argument. No downstream theorems are recorded, but the value supports the simultaneous satisfaction of phase and neutrality constraints.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.