The exact asymmetric Merino–Welsh region for finite matroids

Dev D. Goyal

The exact asymmetric Merino–Welsh region for finite matroids

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

Problem and result

Problem: Asymmetric multiplicative Merino–Welsh inequality T_M(x,0)T_M(0,y) ≥ T_M(1,1)²
Status: Determined exactly
Result: T_M(x,0)T_M(0,y) ≥ T_M(1,1)² for every finite matroid without loops or coloops exactly when x > 1, y > 1, xy^k ≥ (√(x−1) + k√(y−1))² and yx^k ≥ (√(y−1) + k√(x−1))² for every integer k ≥ 2.

Abstract

The theorem characterizes all nonnegative pairs (x,y) for which T_M(x,0) T_M(0,y) ≥ T_M(1,1)² holds for every finite matroid without loops or coloops.

Details

Year: 2026
Discipline: Mathematics
Area: Matroid theory
Subject: Matroid theory
Result type: Exact asymmetric parameter region
Formal proof: Standalone Lean package
Family: asymmetric-tutte
Keywords: Merino–Welsh conjecture, Merino-Welsh, Tutte polynomial, matroids, forests and orientations, matroid inequalities

Statement and scope

Formal scope. The statement uses actual Mathlib matroids and the literal subset rank sum. It includes empty ground sets and finite ground sets in arbitrary ambient types.

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 329 KB
PDF on GitHub: papers/mathematics/asymmetric-tutte/manuscript.pdf
LaTeX source: papers/mathematics/asymmetric-tutte/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/mathematics/asymmetric-tutte/ 22 Lean files

Lakefile

papers/mathematics/asymmetric-tutte/lakefile.toml

Toolchain

leanprover/lean4:v4.32.1

Library roots

Reproduce

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

Reproduce the proof

lake exe cache get
lake build
lake env lean -DwarningAsError=true Audit.lean

README: papers/mathematics/asymmetric-tutte/README.md
Repository guide: verification/README.md
Unfinished proofs: UNFINISHED.md

Source and prior work

Prior work. Liu, 2026; Chen and Xie, 2026. The manuscript states the relation to the diagonal theorem.

Questions and answers

What does this paper prove about the Merino–Welsh inequality?

It characterizes all nonnegative pairs (x,y) for which T_M(x,0)T_M(0,y) ≥ T_M(1,1)² holds for every finite matroid without loops or coloops: exactly x > 1, y > 1 and two scalar conditions for every integer k ≥ 2. It does not classify negative parameters or equality cases, and the graph Merino–Welsh problem at (2,2) is unchanged.

How does this relate to earlier work?

The diagonal case x = y was settled by Liu, with threshold the largest real root of c³ = 9(c − 1), and Chen and Xie gave a direct inductive proof; the structural induction here follows Chen and Xie, and the obstruction from parallel thickenings of uniform matroids is due to Beke, Csáji, Csikvári and Pituk. The new part is the full asymmetric region.

Is the proof formally verified?

The equivalence is stated and proved in Lean 4 for actual Mathlib matroids with finite ground sets and the literal subset rank sum, using Liu's proof library as a dependency. The paper is an unrefereed preprint.

Cite

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

@misc{goyal2026asymmetrictutte,
  author = {Goyal, Dev D.},
  title = {The exact asymmetric Merino--Welsh region for finite matroids},
  year = {2026},
  howpublished = {Preprint},
  url = {https://github.com/dvgyl/math-and-theory/tree/main/papers/mathematics/asymmetric-tutte},
  note = {Fully autonomous agentic research generated by AI systems.}
}