T_16
The 16th triangular number equals 136. Researchers verifying parity of T(D²) for even dimensions in the sync-period minimization argument cite this value when checking that T(16) is even and shares factors with 2^4. The proof is a one-line native_decide evaluation of the closed-form expression.
claim$T(16) = 136$, where $T(n) = n(n+1)/2$ is the nth triangular number.
background
The triangular number function T(n) = n(n+1)/2 supplies the cumulative phase T(D²) for the parity matrix of the hypercube Q_D. This module formalizes constraint (S) from the Dimensional Rigidity paper: among odd spatial dimensions D ≥ 3, D = 3 uniquely minimizes the synchronization period lcm(2^D, T(D²)). For even D the value T(D²) is even, so gcd(2^D, T(D²)) > 1 and the periods partially align.
proof idea
The proof is a one-line term that applies native_decide to evaluate the arithmetic expression 16 * 17 / 2 and confirm equality with 136.
why it matters in Recognition Science
This supplies the even-dimensional case T(16) needed to contrast with the odd-D values (T(9) = 45, T(25) = 325) that appear in the uniqueness argument for D = 3. It supports the generalization of the eight-tick octave to period 2^D and the claim that only odd D yields full coprimality. No downstream uses are recorded, but the result closes a concrete check inside the sync-minimization scaffolding.
scope and limits
- Does not prove the general closed-form identity for arbitrary n.
- Does not compute any lcm or synchronization period.
- Does not address physical interpretations or forcing-chain steps.
- Does not establish minimality of D = 3.
formal statement (Lean)
48@[simp] theorem T_16 : T 16 = 136 := by native_decide
proof body
Term-mode proof.
49
50/-! ## Parity of T(D²) -/
51
52/-- T(D²) for a given dimension. -/