Math and TheoryGyires's permanent inequality for structured matrices
Problem and result
- Problem
- Gyires's permanent inequality for doubly stochastic matrices (Cheon–Wanless Conjecture 20)
- Posed in
- Gyires (1978); listed as Conjecture 20 in Cheon and Wanless (2005)
- Status
- Partially resolved
- Result
- Proves Gyires's permanent inequality for nonnegative circulants of orders 5, 6 and 7, permutation polynomials aI+bQ+cQ² and four-block matrices in all orders, one-exceptional-column/row matrices, and rank ≤ 2 through order 15.
Abstract
The preprint proves Gyires's permanent inequality for several structured matrix classes. These include nonnegative circulants of orders five through seven, all-order permutation polynomials A=aI+bQ+cQ², and all-order four-block doubly stochastic matrices. Here Q is any permutation matrix and a,b,c are nonnegative. The four-block result permits unequal block sizes and zero entries. Further results cover one exceptional column or row and every rank-at-most-two doubly stochastic matrix through order fifteen. The supporting sections prove structural, scalar, deletion, balancing, local polynomial, and counting results. Exact counterexamples identify the limits of auxiliary assertions. The principal order-five claims include equality and a sharp sorted-gap bound with coefficient 484. The principal order-five and order-six claims, the all-order permutation-polynomial and four-block theorems, and the exceptional-vector theorem have complete Lean proofs. The rank-two result has a complete Lean proof for orders 2 through 8. The general order-seven circulant result and rank-two orders 9 through 15 remain incomplete in Lean. The unrestricted conjecture remains outside these results.
Details
- Year
- 2026
- Discipline
- Mathematics
- Area
- Matrix theory
- Subject
- Matrix theory
- Result type
- Structured matrix inequalities and related polynomial bounds
- Formal proof
- Shared Lean library
- Family
gyires-circulant-five- Keywords
- Gyires conjecture, Gyires permanent inequality, doubly stochastic matrices, circulant matrices, permanents, rank-two matrices
Statement and scope
Formal scope. The selected Comparator statements cover order-five circulants, the all-order four-block theorem, and the exceptional-vector theorem for n ≥ 2. Separate Lean packages prove the general order-six and all-order permutation-polynomial theorems. General permanent comparisons and direct-sum closure are also proved in Lean. The rank-two theorem has a complete Lean proof for orders 2 through 8. The general order-seven circulant theorem and rank-two orders 9 through 15 remain incomplete in Lean.
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.pdf1.0 MB- PDF on GitHub
papers/mathematics/ gyires/ paper.pdf - LaTeX source
papers/mathematics/ gyires/ paper.tex - Bibliography
papers/mathematics/ gyires/ references.bib
Formal proof
The selected theorems of this result are proved in the shared Lean 4 library of the repository. Its Comparator configuration checks each one against the matching statement in the Challenge module and permits only the axioms propext, Quot.sound and Classical.choice.
- Proof module
lean/MathAndTheory/ Mathematics/ Gyires/ CirculantFive/ Main.lean - Family sources
lean/MathAndTheory/ Mathematics/ Gyires/ CirculantFive/ - Challenge
lean/Challenges/ Mathematics/ Gyires/ CirculantFive.lean - Solution interface
lean/Solutions/ Mathematics/ Gyires/ CirculantFive.lean - Comparator file
lean/comparator/ mathematics/ gyires.json - Statement guide
lean/docs/ mathematics/ gyires.md - Toolchain
leanprover/lean4:v4.35.0
Checked theorems
Namespace MathAndTheory.GyiresCirculant5
MathAndTheory.GyiresCirculant5. gyires_ratio MathAndTheory.GyiresCirculant5. gyires_ratio_eq_iff MathAndTheory.GyiresCirculant5. gyires_denominator_pos MathAndTheory.GyiresCirculant5. gyires_homogeneous MathAndTheory.GyiresCirculant5. gyires_homogeneous_eq_iff MathAndTheory.GyiresCirculant5. strong_inequality MathAndTheory.GyiresCirculant5. strong_inequality_eq_iff MathAndTheory.GyiresCirculant5. strong_margin MathAndTheory.GyiresCirculant5. strong_margin_attained MathAndTheory.GyiresCirculant5. strong_margin_sharp MathAndTheory.GyiresFourBlock. contractions MathAndTheory.GyiresFourBlock. margin MathAndTheory.GyiresFourBlock. gyires MathAndTheory.GyiresFourBlock. gyires_eq_iff MathAndTheory.GyiresExceptional. strong MathAndTheory.GyiresExceptional. gram_eq_iff MathAndTheory.GyiresExceptional. gyires MathAndTheory.GyiresExceptional. gyires_eq_iff
Reproduce
The commands below are quoted from papers/, which gives their context and working directory.
Reproduce the formal checks
lake build MathAndTheory Solutions
lake env lean Audit.lean
lake env lean -j1 ../papers/mathematics/gyires/verification/AxiomAudit.lean > ../papers/mathematics/gyires/verification/axiom-audit.log
python3 ../papers/mathematics/gyires/verification/check_axioms.py ../papers/mathematics/gyires/verification/axiom-audit.logReproduce the coefficient check
python3 papers/mathematics/gyires/verification/scan_sources.py
python3 papers/mathematics/gyires/verification/check_coefficients.py --output papers/mathematics/gyires/verification/coefficient-results.json- README
papers/mathematics/ gyires/ README.md - Verification guide
papers/mathematics/ gyires/ verification/ README.md - Repository guide
verification/README.md - Unfinished proofs
UNFINISHED.md
Source and prior work
Original problem. Gyires, 1978; Cheon and Wanless, 2005, Conjecture 20. Earlier formalization at the pinned Gyires repository.
Questions and answers
Is Gyires's permanent conjecture proved?
No. This preprint proves the inequality 4per(A)² ≥ c_n[per(AAᵀ) + per(AᵀA) + 2per(A²)], c_n = n!/nⁿ, only for structured classes: nonnegative circulants of orders five, six and seven, all-order permutation polynomials aI+bQ+cQ², all-order four-block matrices, matrices with one exceptional column or row, and rank-at-most-two doubly stochastic matrices through order fifteen. The unrestricted conjecture remains open.
Which parts are verified in Lean?
The order-five and order-six circulant theorems, the all-order permutation-polynomial, four-block and exceptional-vector theorems, and the rank-two theorem for orders 2 through 8 have complete Lean 4 proofs. The order-seven circulant theorem and rank-two orders 9 through 15 have conventional proofs with exact certificates but remain incomplete in Lean.
What was known before?
Chang proved the order-three case, and Ozols proved and formalized the full order-four case together with a stronger Gram-permanent bound. The literature comparison for the broader results is incomplete, so no priority claim is made.
Cite
Citation file papers/. For the whole collection, use CITATION.cff or CITATION.bib.
@misc{Goyal2026GyiresStructured,
author = {Dev D. Goyal},
title = {{Gyires}'s permanent inequality for structured matrices},
year = {2026},
month = oct,
howpublished = {Preprint},
version = {1.2.0},
url = {https://github.com/dvgyl/math-and-theory/tree/main/papers/mathematics/gyires},
note = {Preprint, 28 October 2026. Not peer reviewed. The principal order-five and order-six claims, the all-order permutation-polynomial and four-block theorems, the exceptional-vector theorem, and rank-two orders two through eight have complete Lean proofs. The general order-seven circulant result and rank-two orders nine through fifteen remain incomplete in Lean. See the collection's authorship disclosure for the autonomous research process.}
}