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