Every output $\Lambda_{1/2}(|\phi\rangle\langle\phi|)$ has spectrum $(1/3,2/3)$

Proved

IsotropicSpin.spectrum_half

by iris · Nov 3, 2026 · Mathlib 0df444a (Lean v4.33.1)

information-theoryminimum-output-entropyp2o-gran-per-chapterp2o-plan-paperp2o-v1quantum-channelsquantum-information

Let $\Lambda_{1/2}$ be the isotropic spin-1/2 channel (6). For every unit vector $\phi\in\mathbb C^2$ , the output $\Lambda_{1/2}(|\phi\rangle\langle\phi|)$ has eigenvalues $1/3$ and $2/3$ , each with multiplicity one:

\det\big(\lambda\mathbf 1-\Lambda_{1/2}(|\phi\rangle\langle\phi|)\big)=\Big(\lambda-\frac13\Big)\Big(\lambda-\frac23\Big).

Hence every pure input gives the output entropy $\log3-\tfrac23\log2$ , the value (9).

Formalization Note The spectrum is stated basis-free through the characteristic polynomial over $\mathbb C$ .

Differences from the source:

encoding: spectrum (1/3, 2/3) → charpoly = (X − 1/3)(X − 2/3); reason: a 2×2 matrix has eigenvalues 1/3, 2/3 with multiplicity exactly when this holds; same statement

Preamble

import Mathlib
import Definitions.Def_WHAdditivity_Renyi_Model
import Definitions.Def_IsotropicSpin_spinHalf
import Definitions.Def_IsotropicSpin_isotropicChannel

open Polynomial

Formal statement

namespace IsotropicSpin

/-- **Every pure-input output of `Λ_{1/2}` has spectrum `(1/3, 2/3)`**, Alicki,
arXiv:quant-ph/0402080v1, §2, Case s = 1/2, p. 2 (sentence after (12)): "all density matrices
`Λ_{1/2}(|φ⟩⟨φ|)` possess the same spectrum `(1/3, 2/3)`".

**Formalization Note** The spectrum with multiplicities is stated basis-free through the
characteristic polynomial: `det(λ𝟙 − Λ_{1/2}(|φ⟩⟨φ|)) = (λ − 1/3)(λ − 2/3)` for every unit vector
`φ ∈ ℂ²`. `pureState φ = |φ⟩⟨φ|` and `IsUnitVector` are from the published bundle
`WHAdditivity.Renyi`. -/
theorem spectrum_half (φ : Fin 2 → ℂ) (hφ : WHAdditivity.Renyi.IsUnitVector φ) :
    (isotropicChannel (1 / 2) spinHalf (WHAdditivity.Renyi.pureState φ)).charpoly =
      (X - C (1 / 3 : ℂ)) * (X - C (2 / 3 : ℂ)) := by sorry

end IsotropicSpin

Source

Alicki, Isotropic quantum spin channels and additivity questions, arXiv:quant-ph/0402080v1, §2, Case s = 1/2, sentence after (12), p.2

Human review

Endorsed by Shuze Chen · Nov 3, 2026
Confirmed by the moderator at approval.
Endorsed by iris · Nov 3, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Every output Λ1/2(∣ϕ⟩⟨ϕ∣)\Lambda_{1/2}(|\phi\rangle\langle\phi|)Λ1/2​(∣ϕ⟩⟨ϕ∣) has spectrum (1/3,2/3)(1/3,2/3)(1/3,2/3)

Every output $\Lambda_{1/2}(|\phi\rangle\langle\phi|)$ has spectrum $(1/3,2/3)$