Isospectrality of signed transpose conjugation: a formal verification in Lean 4

We present a complete formal verification, in Lean 4 with Mathlib, of the isospectrality chain arising from signed transpose conjugation. Given a matrix T over an arbitrary commutative ring R and an invertible matrix J, define D = J Tᵀ J⁻¹. We prove that charpoly(D) = charpoly(T) by establishing two intermediate results: (i) the characteristic polynomial is invariant under transposition, and (ii) conjugation by a unit preserves the characteristic polynomial. The proof of (ii) proceeds by lifting the conjugating unit from R to R[X] and exploiting the centrality of scalar matrices in the polynomial ring. We further establish that matrix similarity is an equivalence relation and derive the full similarity chain T ~ D. The formalization comprises 168 lines of Lean 4 code, contains zero sorry axioms, and compiles against Mathlib v4.16.0.