Caracterização matricial de uma identidade trigonométrica

In this article we present a derivation of the fundamental trigonometric identity cos2 x+sin2 x = 1 based on linear algebraic principles. By analyzing the orthogonality of planar rotationmatrices, the identity is obtained as a direct consequence of geometric invariance under rotations.In addition to the classical mathematical argument, the result is corroborated by a formal proofdeveloped and verified within the Lean 4 theorem prover using the Mathlib library, ensuring fulllogical rigor.