triangular_4
plain-language theorem explainer
The lemma states that the fourth triangular number equals 10. Researchers deriving the 45-tick synchronization from the 8-tick cycle would cite this value when checking cumulative phase steps before the closure at n=9. The proof is a direct reflexivity reduction once the triangular definition is applied.
Claim. The fourth triangular number satisfies $T(4) = 10$.
background
The Gap45.PhysicalMotivation module defines the triangular number as $T(n) = n(n+1)/2$, the sum of the first n positive integers. This quantity supplies the cumulative phase in the 8-tick cycle: the cycle itself requires a ninth closure step to return to the initial phase state, so the total phase is $T(9) = 45$ and the synchronization condition follows from matching this accumulation to the ledger neutrality constraint.
proof idea
The proof is a one-line term that applies reflexivity after the definition of triangular unfolds to the arithmetic value 4*5/2 = 10.
why it matters
This supplies an intermediate checkpoint in the sequence of triangular numbers that physically motivates the 45-tick synchronization. It supports the closure principle for the 8-tick octave (T7) before the argument reaches T(9) = 45 and the dimension-forcing step (T8, D=3). The module fills the explicit gap noted in the paper for a physically grounded derivation of the 45 value.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.