T_81
The declaration computes the 81st triangular number as 3321. Researchers extending the synchronization-period analysis to D=9 would cite this value when evaluating lcm(2^9, T(81)). The proof reduces the equality by direct arithmetic evaluation.
claimThe 81st triangular number equals 3321, where $T(n) = n(n+1)/2$.
background
The triangular number function is defined by $T(n) = n(n+1)/2$. The SyncMinimization module places these values inside the synchronization period $lcm(2^D, T(D^2))$ for odd spatial dimensions D. The upstream abbrev from Breath1024 supplies the natural-number type while the local definition supplies the closed-form arithmetic.
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 instance supplies T(81) for the D=9 case in the sequence of odd dimensions whose synchronization periods are compared in the module. It continues the pattern begun with T(9)=45 for D=3. No downstream theorems yet reference it, leaving its role in a full minimality proof open.
scope and limits
- Does not prove any minimality property for D=9.
- Does not compute the corresponding lcm or gcd values.
- Does not connect the result to physical forces or constants.
formal statement (Lean)
45@[simp] theorem T_81 : T 81 = 3321 := by native_decide