triangular_1
plain-language theorem explainer
The lemma establishes that the first triangular number equals 1. Researchers deriving the 45-tick synchronization from the 8-tick cycle closure in Recognition Science cite this base case when summing cumulative phase contributions. The proof is a direct reflexivity reduction once the triangular definition is applied.
Claim. $T(1) = 1$
background
The PhysicalMotivation module defines the triangular number as $T(n) = n(n+1)/2$, which counts cumulative phase accumulation over a closed cycle of steps. The symbol $T$ stands for the type of natural numbers serving as fundamental periods, per the Breath1024 abbreviation. The module uses this to motivate the number 45 as $T(9)$ arising from the fence-post closure of an 8-tick cycle (8 sections plus one return step) in the ledger model for $D=3$.
proof idea
The proof is a one-line term-mode wrapper that applies reflexivity after the definition of triangular unfolds at argument 1.
why it matters
This base case anchors the computation of $T(9)=45$ that supplies the physical motivation for 45-tick synchronization in the dimension-forcing chain (T8). It supports sibling results such as triangular_9_is_45 that close the paper gap on cumulative phase. The lemma sits inside the eight-tick octave framework and the ledger neutrality constraint.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.