Verified Qubit Decoherence and Stiefel Manifold Topology

This publication presents the machine-checked formal-verification proof artifacts in Lean 4 / Mathlib for both open quantum systems (qubit GKSL decoherence) and Stiefel manifold topology. The package includes: (1) formal proofs for the single-qubit GKSL dephasing and amplitude damping generators, verifying the textbook eigenvalue spectrum and the saturating bound T2 = 2T1 with zero sorry; (2) path-connectivity and simple-connectivity of the Stiefel manifold V_m(R^N) with isolated mathlib gaps declared as axioms; (3) compactness and the Poincaré inequality for the Stiefel Laplacian, bounding the SU(N) Yang-Mills mass gap via the Yettragrammaton coupling constant.