A polygon enclosure fails for sums of normal matrices

Dev D. Goyal

A polygon enclosure fails for sums of normal matrices

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

Problem and result

Problem: Kovačec's polygon enclosure conjecture for determinants of sums of normal matrices
Posed in: Kovačec, Universidade de Coimbra preprint 26-11 (April 2026), Conjecture 7; literal statement unverified
Status: Counterexample
Result: Normal 3×3 matrices with spectra (0, 1, i) and (−1−i, 1, −1+i) give det(A+B) = 2/3 + 2i/9, outside every bounded component closure of ℂ∖Γ, Γ the exterior boundary of the transposition graph, yet inside the permutation-value hull.

Abstract

A polygon enclosure fails for a specified pair of normal matrices and its complete transposition graph.

Details

Year: 2026
Discipline: Mathematics
Area: Matrix theory
Subject: Matrix theory
Result type: Standalone theorem and reproducible proof package
Formal proof: Standalone Lean package
Family: kovacec
Keywords: normal matrices, determinants of sums of normal matrices, Kovačec, Marcus–de Oliveira conjecture, permutation values, polygon enclosure

Statement and scope

Formal scope. Actual normal matrices, determinants, straight-segment exterior and component exclusion are formalized. Correspondence with an external source conjecture is conditional.

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 379 KB
PDF on GitHub: papers/mathematics/kovacec/manuscript/manuscript.pdf
LaTeX source: papers/mathematics/kovacec/manuscript/manuscript.tex
Bibliography: papers/mathematics/kovacec/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/mathematics/kovacec/

Lean project

papers/mathematics/kovacec/formalization/ 10 Lean files

Lakefile

papers/mathematics/kovacec/formalization/lakefile.toml

Toolchain

leanprover/lean4:v4.19.0

Library roots

Reproduce

The commands below are quoted from papers/mathematics/kovacec/README.md, which gives their context and working directory.

Formal proof and reproduction

cd formalization
bash build.sh

Formal proof and reproduction

cd manuscript
bash build.sh

README: papers/mathematics/kovacec/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 Professor Alexander Kovačec, I learned of his own June 2026 counterexample, documented in an unpublished preprint, and of another counterexample sent to him by Wenlin Zhang. Equivalence with this construction has not been established. Priority and novelty record.

Questions and answers

Is Kovačec's polygon enclosure conjecture false?

For the enclosure defined in this preprint, yes: spectra (0, 1, i) and (−1−i, 1, −1+i) give det(A+B) = 2/3 + 2i/9 outside every bounded component closure of the Jordan polygon. Correspondence with the literal Conjecture 7 of Kovačec's April 2026 report is unverified, and the example satisfies the Marcus–de Oliveira convex-hull inclusion.

Did anyone find a counterexample earlier?

Yes. Professor Kovačec found a counterexample to his own conjecture in June 2026, documented in an unpublished preprint, and Wenlin Zhang independently sent him another. Whether either is equivalent to this construction is not established, and no priority is claimed.

Is the proof formally verified?

Lean 4 checks the actual normal matrices, the determinant, the straight-segment exterior and its Jordan boundary, and exclusion from every bounded component closure. Identification with the external conjecture is not formalized.

Cite

Citation file papers/mathematics/kovacec/CITATION.bib. For the whole collection, use CITATION.cff or CITATION.bib.

@unpublished{goyal2026polygon,
  author = {Goyal, Dev D.},
  title = {A polygon enclosure fails for sums of normal matrices},
  year = {2026},
  note = {Manuscript, version 0.1.0}
}