Triangular Square Numbers and the Pell Equation

We establish a complete formal characterization of triangular square numbers via the Pell equation \(x^2 - 8y^2 = 1\). A triangular number \(T(n) = n(n+1)/2\) is a perfect square if and only if \((2n+1, 2m)\) satisfies this Pellian relation. We prove four foundational results: (1) the reduction from \(T(n) = m^2\) to the Pell form, (2) verification of the fundamental solution \((3, 1)\), (3) closure of the solution set under the standard recurrence, and (4) strict monotonicity ensuring infinitely many solutions. The entire argument is formalized in the Platonic proof kernel with zero axioms — all results are derived purely from natural number arithmetic.

Keywords: Triangular numbers, square numbers, Pell equation, number theory, formal verification

MSC 2020: 11D09, 11B37, 11Y50