Exact Diamond Distance to Equilibrium for a Qubit Generalized-Amplitude-Damping Channel

This work establishes the exact, unhalved diamond-norm distance between a qubit generalized-amplitude-damping (GAD) channel Φₚ,ᵣ and its stationary-replacement channel Rₚ(X) = Tr(X) diag(1 − p, p). For stationary excited-state population 0 ≤ p ≤ 1 and coherence-amplitude factor 0 ≤ r ≤ 1, the closed-form result is ‖Φₚ,ᵣ − Rₚ‖⋄ = 2r[1 − p(1 − p)r²]/(2 − r). The result accounts for arbitrary finite-dimensional ancillas and arbitrary complex input matrices, rather than only unentangled states or density operators; a two-dimensional ancilla attains the optimum. The derivation includes the boundary cases r = 0 and r = 1 and the extreme stationary populations p = 0 and p = 1, without limiting arguments. The equality is supported by two explicit analytic certificates. A constructed three-Kraus completely positive, trace-preserving map Λₚ,ᵣ gives the factorization Φₚ,ᵣ − Rₚ = (δ/2)(id − Λₚ,ᵣ), where δ is the exact distance above. Trace-norm contractivity supplies a universal upper bound, while the normalized Schmidt state √(v/h)|00⟩ + √(u/h)|11⟩, with h = 2 − r, u = 1 − pr and v = 1 − (1 − p)r, saturates it through perfect discrimination of id from Λₚ,ᵣ. Independently, an explicit 4 × 4 semidefinite-programming dual witness satisfies Z ± J ⪰ 0 and Trₒᵤₜ(Z) = δI₂, reproducing the same upper bound without numerical optimization. A consolidated Lean 4 formalization of the physical four-Kraus channel and its finite-ancilla norm equality is accompanied by an author-reported successful kernel compilation, source hashes, and a replay protocol; the manuscript explicitly distinguishes this record from an independent rerun, which was not performed during assembly. The SDP certificate and the independent multi-qubit corollaries are analytic results, not separately claimed as kernel-checked. For independent channels, these corollaries bound the product-to-equilibrium distance between maxₖ δₖ and min{2, Σₖ δₖ}, and yield the asymptotic decay exponent minₖ γₖ when rₖ(t) = exp(−γₖt). The exact single-use discrimination error for equal prior probabilities is Pₑᵣᵣ = 1/2 − δ/4. Together, these results provide analytic and formally reproducible benchmarks for finite-temperature quantum noise and mixing, without asserting optimal multi-qubit discrimination strategies or experimental performance.