T_49
plain-language theorem explainer
The 49th triangular number equals 1225. Researchers computing synchronization periods for seven-dimensional space cite this value when contrasting D=7 against the D=3 minimum. The proof reduces to a single native decision that evaluates the closed-form triangular expression directly.
Claim. $T(49) = 1225$, where $T(n) = n(n+1)/2$ is the $n$th triangular number.
background
The triangular number is defined by $T(n) = n(n+1)/2$. In this module it supplies the cumulative phase $T(D^2)$ arising from the parity matrix of the hypercube $Q_D$. The upstream abbrev T from Breath1024 simply tracks fundamental periods as natural numbers. The module formalizes constraint (S) from the Dimensional Rigidity paper: among odd dimensions $D >= 3$, only D=3 minimizes lcm(2^D, T(D^2)).
proof idea
The proof is a one-line wrapper that invokes the native_decide tactic to evaluate the arithmetic expression for T(49) and confirm equality to 1225.
why it matters
This supplies the explicit T(49) entry required for the D=7 row in the comparison that isolates D=3 as the unique minimizer of the synchronization period. It supports the selection of the 45-tick period at D=3 by exhibiting the contrasting larger value 1225. The result sits inside the eight-tick octave framework and the derivations that fix D=3 spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.