T_121
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.