triangular_9_via_formula
plain-language theorem explainer
The declaration records that the ninth triangular number equals 45 by the closed-form sum. Workers on the 8-tick synchronization in the dimension-forcing chain cite it to supply the missing physical motivation for the cumulative phase. The proof is a direct reflexivity reduction on the arithmetic identity.
Claim. $T(9) = \frac{9 \times 10}{2} = 45$, where $T(n)$ is the nth triangular number.
background
The module supplies a physically grounded derivation of the number 45 in the dimension-forcing argument. It treats 45 as the cumulative phase accumulated over a closed 8-tick cycle. The cycle itself is not closed; the closure principle adds one extra step, yielding nine steps total.
Each tick k contributes a phase increment proportional to k. The total phase over the closed cycle is therefore the sum from k=1 to 9, which equals the triangular number T(9). This value is required for the ledger neutrality constraint and the cumulative phase constraint to hold simultaneously.
proof idea
The proof is a one-line term that applies reflexivity to the arithmetic identity 9 * 10 / 2 = 45.
why it matters
It closes the physical motivation gap for the 45-tick synchronization identified in the paper. The result supplies the concrete phase value needed to complete the eight-tick octave (T7) once D=3 is fixed (T8). No parent theorems or downstream uses appear in the current dependency graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.