triangular_8
plain-language theorem explainer
The lemma computes the eighth triangular number as 36. Researchers modeling cumulative phase accumulation over closed 8-tick cycles cite this value when verifying the arithmetic step toward the 45-tick synchronization. The proof is a direct reflexivity reduction to the closed-form definition of triangular numbers.
Claim. $T(8) = 36$, where $T(n) = n(n+1)/2$ denotes the $n$th triangular number.
background
The triangular number function is defined as $T(n) = n(n+1)/2$, matching the upstream definitions in both PhysicalMotivation and SyncMinimization. The module addresses the physical motivation gap for the 45-tick synchronization by interpreting 45 as the cumulative phase $T(9)$ over a closed 8-tick cycle, where the extra step arises from the fence-post closure principle (8 ticks require 9 steps to return to the initial phase). Upstream, Breath1024.T supplies the abbreviation for fundamental periods as natural numbers, while the SyncMinimization.T definition supplies the same summation formula used here.
proof idea
One-line term proof that applies reflexivity directly to the triangular number definition.
why it matters
This anchors the arithmetic step in the cumulative phase argument that produces T(9) = 45, closing the physical motivation gap identified in the module documentation for the dimension-forcing chain. It supports the eight-tick octave (T7) and the forcing of D = 3 (T8) by supplying the concrete value needed for ledger neutrality and synchronization constraints. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.