T_9
plain-language theorem explainer
The theorem establishes that the ninth triangular number equals 45. Researchers formalizing dimensional rigidity would cite it to anchor the synchronization period calculation for three spatial dimensions. The proof is a direct one-line evaluation via native decision procedure on the triangular number definition.
Claim. $T(9) = 45$, where the triangular number function is given by $T(n) = n(n+1)/2$.
background
The triangular number function is defined by $T(n) = n(n+1)/2$. This module formalizes constraint (S) from the Dimensional Rigidity paper: among odd spatial dimensions $D$ at least 3, $D=3$ uniquely minimizes the synchronization period given by the least common multiple of $2^D$ and $T(D^2)$ because only odd $D$ yields full coprimality between the two arguments. For $D=3$ the relevant value is $T(9)=45$, which produces the minimal period 360. The upstream abbrev supplies the type of the period variable while the local definition supplies the explicit formula.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the closed-form expression for the ninth triangular number.
why it matters
This supplies the concrete value $T(9)=45$ required to show that three spatial dimensions minimize the synchronization period at 360, in contrast to 10400 for $D=5$ and 156800 for $D=7$. It directly supports the eight-tick octave (period $2^3$) and the selection of $D=3$ as the unique minimizer among odd dimensions, thereby closing one step in the argument that 45 is the selected rung on the phi-ladder for the lowest synchronization cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.