Strong Mason conjecture for matroid independent sets

strong_mason_conjecture — a formalization challenge from the lean-eval benchmark.

Notes

For a finite Mathlib Matroid, independentSetCount M k is exactly the number of independent k-element subsets of its ground set. The theorem is the division-free form of ultra-log-concavity of these counts: if the ground set has cardinality n and 0 < k < n, then I_k^2 k(n-k) >= I_{k-1} I_{k+1} (k+1)(n-k+1). Using M.E.ncard, rather than the cardinality of the ambient type, is essential because Mathlib matroids carry an explicit ground set.

Formal statement

/-- **The strong Mason conjecture** (Branden-Huh; independently
Anari-Liu-Oveis Gharan-Vinzant). If `I k` counts the independent sets of
size `k` in a finite matroid on `n` elements, then

`I k ^ 2 * k * (n - k) >= I (k - 1) * I (k + 1) * (k + 1) * (n - k + 1)`.

Equivalently, `I k / n.choose k` is a log-concave sequence. -/
theorem strong_mason_conjecture {α : Type*} (M : Matroid α) [M.Finite]
    (k : ℕ) (hk : 0 < k) (hkn : k < M.E.ncard) :
    independentSetCount M (k - 1) * independentSetCount M (k + 1) *
          (k + 1) * (M.E.ncard - k + 1) ≤
      independentSetCount M k ^ 2 * k * (M.E.ncard - k) := by
  sorry

Informal solution sketch

Branden and Huh associate to a matroid its homogenized multivariate Tutte polynomial and prove that this polynomial is Lorentzian. Lorentzian polynomials remain Lorentzian under the relevant specializations and directional derivatives, and their coefficients satisfy normalized log-concavity. Applying this to the independent-set generating polynomial gives (I_k / choose n k)^2 >= (I_{k-1} / choose n (k-1)) (I_{k+1} / choose n (k+1)). Clearing the positive binomial denominators for 0 < k < n yields exactly the natural-number inequality in the Lean statement. Anari, Liu, Oveis Gharan, and Vinzant independently proved the same strongest form using complete log-concavity and high-dimensional random walks.

Source

P. Branden and J. Huh, 'Lorentzian polynomials', Ann. of Math. 192 (2020), 821-891, Theorem 4.14, https://doi.org/10.4007/annals.2020.192.3.4; independently N. Anari, K. Liu, S. Oveis Gharan, and C. Vinzant, 'Log-concave polynomials III: Mason's ultra-log-concavity conjecture for independent sets of matroids', https://arxiv.org/abs/1811.01600.

How to submit

Challenge.lean and Solution.lean are part of the trusted benchmark and must not be modified. Write your proof in Submission.lean (plus any local modules under Submission/). Mathlib may be used freely; anything not in Mathlib has to be inlined into the submission.

Comparator configuration

• Solution module: Solution
• Theorems checked: strong_mason_conjecture
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Kim Morrison.