T_121
The declaration computes the 121st triangular number as exactly 7381. Researchers verifying synchronization costs in odd-dimensional models would cite this specific value when checking arithmetic steps in period minimization. The proof is a one-line native decision that evaluates the closed-form expression directly.
claimLet $T(n) = n(n+1)/2$. Then $T(121) = 7381$.
background
The triangular number is defined by $T(n) = n(n+1)/2$. The Gap45 module uses this to formalize constraint (S) from the Dimensional Rigidity paper: among odd $D >= 3$, dimension 3 uniquely minimizes the synchronization period lcm($2^D$, $T(D^2)$). For $D=3$ this yields lcm(8,45)=360, the smallest such period. Upstream, the abbreviation T in Breath1024 stands for fundamental periods over the naturals.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the arithmetic identity directly.
why it matters in Recognition Science
This supplies a concrete triangular-number value that can be referenced in sync-period calculations within the Gap45 analysis. It supports the module's demonstration that D=3 minimizes the lcm against the eight-tick octave $2^D$. No downstream theorems currently cite it, leaving open whether it will be invoked in larger phi-ladder or forcing-chain arguments.
scope and limits
- Does not prove the general triangular-number formula.
- Does not establish minimality of any synchronization period.
- Applies only to the specific argument 121.
- Does not connect to J-cost, defect distance, or the phi-ladder.
formal statement (Lean)
46@[simp] theorem T_121 : T 121 = 7381 := by native_decide