A pure-state matched-basis information inequality violation in dimension five

Dev D. Goyal

A pure-state matched-basis information inequality violation in dimension five

Dev D. Goyal · 2026 · Research preprint, not externally peer reviewed

Problem and result

Problem: Pure-state ECQC: matched-basis mutual-information inequality with mutually unbiased bases
Posed in: Attributed to Iqbal, Quantum Information Processing 25 (2026), Article 250, Conjecture 3.1; correspondence unverified
Status: Counterexample
Result: A normalized pure state in local dimension 5 with six fixed mutually unbiased bases, used identically by both parties, has five-setting classical information sum 5 log 5 versus quantum mutual information 2 log 5 (ratio 5/2).

Abstract

A dimension-five pure-state matched-basis information inequality violation, with a conventional all-prime companion.

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: pure-ecqc
Keywords: ECQC, mutual information, mutually unbiased bases, pure states, quantum information inequality, counterexample

Statement and scope

Formal scope. The dimension-five identical-local-basis theorem is formalized. The prime-family extension is conventional; arbitrary or independently optimized basis choices are outside the result.

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.pdf 346 KB
PDF on GitHub: papers/physics/pure-ecqc/manuscript/manuscript.pdf
LaTeX source: papers/physics/pure-ecqc/manuscript/manuscript.tex
Bibliography: papers/physics/pure-ecqc/manuscript/references.bib

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/physics/pure-ecqc/

Lean project

papers/physics/pure-ecqc/formalization/ 6 Lean files

Lakefile

papers/physics/pure-ecqc/formalization/lakefile.toml

Toolchain

leanprover/lean4:v4.19.0

Library roots

Reproduce

The commands below are quoted from papers/physics/pure-ecqc/README.md, which gives their context and working directory.

cd formalization
bash build.sh

cd manuscript
bash build.sh

README: papers/physics/pure-ecqc/README.md
Repository guide: verification/README.md
Unfinished proofs: UNFINISHED.md

Source and prior work

Prior work. The Omega Institute's public repository records the same dimension-five counterexample, with the same state and bases, first committed on 4 October 2026 (issue #12896), about 25 days before my first commit. No priority is claimed for it. Priority and novelty record.

Questions and answers

Is the pure-state ECQC inequality true?

Not in the displayed fixed-family, identical-basis formulation: the state 5^(−1/2) Σₓ |x⟩|2x⟩ with six specified mutually unbiased bases gives 5 log 5 against quantum mutual information 2 log 5, an excess of 3 log 5. It refutes Iqbal's published statement only if the definitions agree, and optimizing over other bases or local basis changes is outside the result.

Were there earlier ECQC counterexamples?

Yes. Wang, Wang and Chen (arXiv:2608.03828) gave earlier mixed-state ECQC counterexamples, so no priority for disproving ECQC is claimed; the original two-basis CQC question is separate.

Is the proof formally verified?

Lean 4 verifies the dimension-five state, the six bases, the Born tables, the reduced states and the entropies. The all-prime extension (p ≡ 1 mod 4, ratio p/2) has only a conventional proof.

Was this pure-state counterexample known before?

Yes. The Omega Institute's public repository records the same state and bases, with the same values 5 log 5 and 2 log 5, first committed on 4 October 2026 (issue #12896), about 25 days before this result was first committed here. No priority is claimed; the all-prime companion does not appear in that record.

Cite

Citation file papers/physics/pure-ecqc/CITATION.bib. For the whole collection, use CITATION.cff or CITATION.bib.

@unpublished{Goyal2026PureECQC,
  author = {Dev D. Goyal},
  title = {A pure-state matched-basis information inequality violation in dimension five},
  year = {2026},
  note = {Unpublished manuscript. Historical novelty remains provisional}
}