Gyires' Permanent Inequality — n=4 Proof Available

Statement

A real matrix is doubly stochastic if its entries are nonnegative and every row and column sums to 1. Write Ω_n for the set of such n×n matrices and J_n for the matrix with every entry 1/n. Gyires' conjecture, as stated by Cheon and Wanless (2005, Conjecture 20), is

4 per(A)² / [per(AA*) + per(A*A) + 2 per(A²)] ≥ n! / nⁿ   for A ∈ Ω_n,

with equality only at A = J_n. For real A, A* = A^T. For n = 4 the right-hand side is 24/256 = 3/32, and since the denominator is positive the statement becomes:

Theorem (n = 4). For every real doubly stochastic 4×4 matrix A,

128 per(A)² ≥ 3 [per(AA^T) + per(A^TA) + 2 per(A²)],

with equality if and only if every entry of A is 1/4.

What is proved

Formalized for real 4×4 doubly stochastic matrices, using Mathlib's own Matrix.permanent, matrix product, transpose, and doublyStochastic ℝ (Fin 4):

• the polynomial inequality above (Gyires.gyires_4x4) and its equality case (Gyires.gyires_4x4_eq_iff), with strict inequality away from J₄;
• the Cheon–Wanless ratio form for n = 4 and its equality case (Gyires.gyires_4x4_ratio, Gyires.gyires_4x4_ratio_eq_iff);
• the stronger inequality 3 per(AA^T) ≤ 32 per(A)² on Ω₄ (Gyires.permanent_gram_le);
• 2 per(MN^T) ≤ per(MM^T) + per(NN^T) for real square M, N of every size (Gyires.permanent_gram_add_ge), using standard axioms only.

Not proved: Gyires' conjecture for n ≥ 5. The finite-certificate method used here does not extend to general n as it stands.

Proof outline

1. A stronger inequality suffices. With H(M) = 32 per(M)² − 3 per(MM^T), a sum-of-squares identity for permanents gives per(AA^T) + per(A^TA) ≥ 2 per(A²), and 128 per(A)² − 3[per(AA^T) + per(A^TA) + 2 per(A²)] = 2H(A) + 2H(A^T) + 3[per(AA^T) + per(A^TA) − 2 per(A²)]. So it is enough to show H ≥ 0 on Ω₄, with equality only at J₄.
2. Reduction to cones. Subtracting the smallest entry and repeatedly pulling out the center of the smallest face of the Birkhoff polytope containing the remainder writes A as a nonnegative combination of J and the centers of a chain of faces ending at a permutation matrix.
3. A finite certificate. On each such cone, H is a degree-8 polynomial in the coefficients. Using the 576 row and column permutations, 65,376 chains suffice, and for every one of them every coefficient is nonnegative, with strictly positive pure powers, which also gives the equality case.
4. Checked in Lean. A checker that regenerates the chains, symmetry reduction, and polynomials is proved sound in Lean; a successful run implies the real-matrix statement. Running that checker is the one step not checked by the kernel.

Verification and trust model

The formalization uses Lean 4.28.0 (commit 7e01a1b) with Mathlib v4.28.0 (commit 8f9d9cf). ./verify.sh deletes the project's build outputs, rebuilds all 41 project modules including every certificate piece, and checks Verification.lean with lake env lean --trust=0. That file restates the results with the doubly stochastic conditions written out entrywise. The audit checks the printed theorem types and the exact axiom set of 15 declarations.

Trust model. native_decide proves a closed Boolean fact by compiling and running code; the kernel accepts the result through the axiom Lean.ofReduceBool, and Lean.trustCompiler records that the compiler, interpreter, and runtime are trusted. It is used for exactly 36 Boolean checks (certificate pieces, multiplication tables, top-level face splits, and two small index facts). Every 4×4 inequality and equality theorem therefore depends on Lean.ofReduceBool and Lean.trustCompiler in addition to propext, Classical.choice, and Quot.sound. Of the 15 audited declarations, only Gyires.permanent_gram_add_ge, its restatement, and the denominator-positivity lemma use the standard axioms alone. Mathlib does not accept native_decide, and external Lean proof checkers cannot replay such proofs.

Independent cross-check. The finite part is re-implemented outside Lean: the certificate tree in Python and the coefficient test in C++ with 128-bit integers. It confirms all 65,376 cones, the tight coefficients, and the strict pure powers; as a negative control it rejects every cone when 32 is replaced by 31. An earlier, separate computational proof checked the same cone classes with another implementation.

Prior-art search

• Origin: Gyires (1978). The original article was not accessed. Cheon and Wanless (2005) state it as Conjecture 20, with equality precisely at J_n.
• Known cases: D. K. Chang, On two permanental conjectures, Linear Multilinear Algebra 26 (1990), 207–213 (DOI), proves n = 3 per the publisher's abstract (full text not accessed). Cheon and Wanless also report Chang's sufficient condition near J_n.
• Boundary of Ω₄: Yair Lavi's Conjecture 20 page lists the conjecture as open and announces strict inequality for every 4×4 doubly stochastic matrix with a zero entry; no proof was linked when checked on October 19, 2026. The boundary does not determine the interior.
• Later related work: this repository is cited by dvgyl/gyires-circulant-5 (October 2026), a Lean-verified proof of the inequality for doubly stochastic circulant matrices of order five. That repository describes the conjecture for all doubly stochastic 5×5 matrices as open.
• Nearby work not covering this statement: formally verified results for other dimension-four permanent conjectures (arXiv:2610.20681; Dittert's conjecture for n = 4, arXiv:2607.29191). Searches of public formal-mathematics collections found related permanent statements but no formalization of this one.

An AI-assisted literature review on October 16, 2026, with a bounded update on October 19, 2026, located no earlier unrestricted proof of the 4×4 case in the sources examined. Gyires' 1978 article, Chang's full text, and Minc's 1978 book were not read.

Provenance

Chris Ozols directed the work and its verification. AI assistants contributed the original computer-assisted proof, its audits, and the literature review. The Lean formalization of the inequality was produced by Harmonic's Aristotle. Anthropic's Claude independently rebuilt it and added the formalized equality case and ratio form, the cross-check, and the package. Nobody wrote the Lean proofs by hand. The original computer-assisted proof was written on October 15, 2026 (UTC, per file modification times), and the package was assembled on October 19, 2026.

Sources, verification, and records

Original problem

• Cheon and Wanless (2005), Conjecture 20 — DOI
• Cheon and Wanless (2005) — author's PDF
• Gyires (1978) — zbMATH 0398.15007

Proof and formalization

• GitHub repository
• Readable proof (PROOF.md)
• Main Lean theorem (RequestProject/Gyires.lean)
• Equality case (GyiresEquality/Equality.lean)
• Ratio form (GyiresEquality/Ratio.lean)
• Exact-statement check (Verification.lean)

Verification evidence

• Verification report and trust model
• Recorded verification (verification.json)
• Theorem types and axioms (kernel-check.log)
• Independent C++ cross-check
• Cross-check output (crosscheck.log)
• Reproduction guide (REPRODUCE.md)
• GitHub Actions verification runs

Prior art and provenance

• Prior-art review (PRIOR_ART.md)
• Provenance (PROVENANCE.md)
• Citation metadata (CITATION.cff)