triangular_4
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not prove the general triangular formula.
- Does not derive the synchronization constraint itself.
- Does not address the 45 value or higher triangular numbers.
formal statement (Lean)
99@[simp] lemma triangular_4 : triangular 4 = 10 := rfl
proof body
Term-mode proof.
100
101/-- T(5) = 15. -/