Math and TheoryThe three-state root-fidelity entropy bound
Problem and result
- Problem
- Fannes–de Melo–Roga–Życzkowski conjecture: root-fidelity matrix entropy bounds Holevo χ
- Posed in
- Fannes, de Melo, Roga and Życzkowski, 'Matrices of fidelities for ensembles of quantum states and the Holevo quantity', Quantum Inf. Comput. 12 (2012), 472–489, Conjecture 1, eq. (18)
- Status
- Proved
- Result
- For any three density matrices ρᵢ of finite dimension and probabilities pᵢ, the Holevo quantity S(Σ pᵢρᵢ) − Σ pᵢS(ρᵢ) is at most the entropy of the 3 × 3 matrix C_ij = √(pᵢpⱼ) ‖√ρᵢ √ρⱼ‖₁.
Abstract
The entropy of the weighted three-by-three root-fidelity matrix bounds the Holevo quantity of every three-state ensemble in arbitrary finite dimension. The result includes mixed and singular states and zero probabilities.
Details
- Year
- 2026
- Discipline
- Mathematical physics
- Area
- Quantum information
- Subject
- Quantum information
- Result type
- Standalone theorem and reproducible proof package
- Formal proof
- Standalone Lean package
- Family
fidelity-three-state- Keywords
- root fidelity, Holevo quantity, quantum ensembles, von Neumann entropy, fidelity matrix
Statement and scope
Formal scope. The unrestricted three-state ensemble theorem is formalized for actual positive semidefinite complex matrices of trace one, nonnegative weights summing to one, spectral entropy and nuclear-norm root fidelity. Credited QICLean foundations and prior-work adapters retain their attribution.
A Lean check establishes only the formal statement that is checked. It does not establish novelty, historical priority or a faithful transcription of an external source. Known gaps are listed in UNFINISHED.md; the authorship disclosure describes how the results were produced.
Manuscript
- PDF on this site
manuscript.pdf286 KB- PDF on GitHub
papers/physics/ fidelity-three-state/ manuscript.pdf - LaTeX source
papers/physics/ fidelity-three-state/ manuscript.tex
Formal proof
This result has a standalone Lean 4 package, separate from the shared library. Build it with the toolchain and instructions given in its README.
- Proof package
papers/3 Lean filesphysics/ fidelity-three-state/ - Lakefile
papers/physics/ fidelity-three-state/ lakefile.toml - Toolchain
leanprover/lean4:v4.35.0-rc3 - Library roots
Reproduce
The commands below are quoted from papers/, which gives their context and working directory.
Read and reproduce
python3 fetch_mathlib_cache.py
lake build FullCandidate
lake lean Audit.leanRead and reproduce
fidelity_output="$(mktemp -d)"
python3 verify.py --output "$fidelity_output/verification.json" --log-dir "$fidelity_output/logs"- README
papers/physics/ fidelity-three-state/ README.md - Repository guide
verification/README.md - Unfinished proofs
UNFINISHED.md
Source and prior work
Priority and subsequent correspondence. On 29 October 2026, through correspondence with Dr. Wojciech Roga, I learned that another group had contacted him several days earlier claiming a solution of the same conjecture using AI and Lean. The two proofs have not been compared, and neither mathematical equivalence nor priority has been conclusively established. Priority and novelty record.
Prior work. On 31 October 2026, a check of public records found a claimed Lean proof of the same conjecture in the Omega Institute's public repository, first committed on 19 October 2026 (issue #19184), about nine days before my first commit. The proofs have not been compared; no priority is claimed. Priority and novelty record.
Questions and answers
Is the Fannes–de Melo–Roga–Życzkowski fidelity conjecture proved?
This preprint proves the unrestricted three-state inequality stated as Conjecture 1, eq. (18): for three density matrices of any finite dimension and probabilities pᵢ, the Holevo quantity is at most the entropy of C_ij = √(pᵢpⱼ) ‖√ρᵢ √ρⱼ‖₁, including mixed and singular states and zero probabilities. It does not establish an analogous statement for an arbitrary number of states.
Has anyone else claimed a solution?
Yes. Wojciech Roga reported that another group had contacted him several days before 29 October 2026 claiming a solution of the same conjecture using AI and Lean; that claim has not been seen or compared, and neither equivalence nor priority is established. Zhang, Wu and Fei had earlier proved the bound under a compatibility condition on three polar unitaries.
Is the proof formally verified?
The theorem is formalized in Lean 4 for positive semidefinite complex trace-one matrices, nonnegative weights summing to one, spectral entropy and nuclear-norm root fidelity, building on credited QICLean foundations. The paper is an unrefereed preprint.
Did anyone prove this conjecture before this note?
A claimed Lean proof of the same three-state bound appears in the Omega Institute's public repository, first committed on 19 October 2026 (issue #19184), about nine days before this result was first committed here on 29 October 2026. The proofs have not been compared, and no priority is claimed.
Cite
Citation file papers/. For the whole collection, use CITATION.cff or CITATION.bib.
@unpublished{goyal2026threestatefidelity,
author = {Goyal, Dev D.},
title = {The three-state root-fidelity entropy bound},
year = {2026},
month = oct,
note = {Preprint. Fully autonomous agentic AI research. Dev D. Goyal is responsible for the public release.}
}