Strong Mason

The theorem

Let $M$ be a matroid on a finite ground set $E$ of cardinality $n$. Write

$$I_j=\#\{S\subseteq E: |S|=j\text{ and }S\text{ is independent in }M\}.$$

The strongest form of Mason’s conjecture, now a theorem, says that the sequence $I_j/\binom nj$, for $0\le j\le n$, is log-concave. Thus, whenever $1\le k<n$,

$$\left(\frac{I_k}{\binom nk}\right)^2 \ge \frac{I_{k-1}}{\binom n{k-1}} \frac{I_{k+1}}{\binom n{k+1}}.$$

The normalization matters: $I_k/\binom nk$ is the probability that a uniformly chosen $k$-element subset is independent. The theorem controls the shape of these probabilities, giving a stronger conclusion than ordinary log-concavity of the counts $I_k$.

The accepted Lean statement clears the binomial denominators:

$$\binom n{k-1}\binom n{k+1}I_k^2 \ge \binom nk^2 I_{k-1}I_{k+1} \qquad(k>0).$$

This formulation remains meaningful beyond the interior of the sequence. No representability, simplicity, looplessness, or connectedness assumption is imposed. The matroid may have loops, parallel elements, or rank zero. The exported result is branden_huh_strongest_mason.

Brändén and Huh prove this result as Theorem 4.14 of Lorentzian polynomials; Anari, Liu, Oveis Gharan, and Vinzant independently proved the strongest inequality. The formal development presented here takes a combinatorial-atlas route, closely related to the method explained by Chan and Pak. Its central objects are finite matrices of extension counts and a reverse Cauchy–Schwarz inequality.

The counting convention

The benchmark represents $E$ by a finite type and explicitly assumes that the matroid’s ground set is the entire type. Consequently, $n$ counts actual ground elements. Its independent-set count filters the finite collection of all $k$-element subsets by the predicate of matroid independence.

The atlas development uses a second, set-based cardinality expression. independentSetCount_eq_challenge proves exact equality between these definitions. This is a substantive interface check: the final theorem counts the subsets specified by the benchmark, with the same cardinality and independence predicate.

For the main argument, fix $0<k<n$. If $I_{k+1}=0$, the desired inequality is immediate. Otherwise, a positive count supplies an independent set $J$ of cardinality $k+1$. This witness will justify the positivity assumptions needed by the matrix induction. See strong_mason_finite.

1. Replace subsets by ordered continuations

For a finite prefix $S$, let $C(S,r)$ count ordered strings of $r$ distinct new elements whose union with $S$ is independent. The recursion is

$$C(S,0)=\begin{cases}1&S\text{ independent},\\0&\text{otherwise},\end{cases} \qquad C(S,r+1)=\sum_{x\in E\setminus S}C(S\cup\{x\},r).$$

Repetition is excluded at each insertion. Let $\mathcal E(S,r)$ be the collection of independent supersets of $S$ with cardinality $|S|+r$. Double counting a distinguished newly added element proves

$$C(S,r)=r!\,|\mathcal E(S,r)|, \qquad C(\varnothing,r)=r!I_r.$$

The factorial records the possible orders of the new elements. The recursive definition makes choosing the first letter an exact identity, which later becomes an identity between matrix entries. These facts are formalized in continuation and continuation_eq_factorial_mul_card_extensionLevel.

Matroid augmentation also proves that $C(S,r)>0$ whenever $S$ is independent and $|S|+r\le |J|$. Here $J$ need not contain $S$: augmentation supplies a sufficiently large independent extension of $S$.

2. Put the strongest normalization into the weights

Define a coefficient depending on the final cardinality:

$$c(j)=\begin{cases} \dfrac{n-k+1}{n-k}&j=k+1,\\ 1&j\ne k+1, \end{cases} \qquad W(S,r)=c(|S|+r)C(S,r).$$

The denominator is positive because $k<n$. Adding the first element increases the prefix size by one and decreases the remaining length by one. Their sum stays fixed, so the weighted counts satisfy the same first-letter recursion.

At the empty prefix, the three relevant values are

$$W(\varnothing,k-1)=(k-1)!I_{k-1},\quad W(\varnothing,k)=k!I_k,$$

$$W(\varnothing,k+1)=\frac{n-k+1}{n-k}(k+1)!I_{k+1}.$$

This single exceptional weight supplies the extra ground-set factor in the strongest Mason inequality. See masonCoeff and weightedContinuation.

3. Arrange the counts into an atlas of matrices

Introduce an extra letter $*$ which leaves a prefix unchanged. A ground letter $x$ inserts $x$, unless it is already present. For depth $m=r+1$, form a matrix $A(S,m)$ indexed by $E\cup\{*\}$: its $(i,j)$ entry is $W(T,r)$ if reading $i,j$ from $S$ validly produces $T$, and zero otherwise. Dependent extensions also give zero through the continuation count.

The matrices are symmetric and entrywise nonnegative. Reading one additional letter gives a child matrix. Commutativity of insertion and cyclic symmetry of three-letter insertion produce the inheritance identities used below. The construction is atlasMatrix.

For any such matrix, write $B_A(v,w)=v^{\mathsf T}Aw$ and $Q_A(v)=B_A(v,v)$. The formal predicate Hyperbolic means

$$Q_A(v)Q_A(w)\le B_A(v,w)^2 \quad\text{whenever }Q_A(v),Q_A(w)\ge0.$$

This reverse Cauchy–Schwarz property is the target of the matrix induction. It is defined explicitly and proved for the atlas matrices.

4. Establish hyperbolicity at depth one

Suppose $S$ is independent and $|S|\le k-1$. Its feasible one-element extensions split into parallel classes: two distinct feasible elements belong to the same class when adjoining both makes the prefix dependent. Matroid augmentation proves transitivity of this relation.

The depth-one matrix has star–star entry $1$, star–feasible entries $1$, zero entries within a parallel class, and a common coefficient $c$ between different classes. Here $c=1$ unless $|S|=k-1$, when $c=(n-k+1)/(n-k)$. Infeasible rows vanish.

For a vector $v$, let $b_q$ be the sum of its coordinates in parallel class $q$, and set $s=\sum_q b_q$. Expanding gives

$$Q_A(v)=(v_*+s)^2+(c-1)s^2-c\sum_qb_q^2.$$

On the hyperplane $B_A(v,e_*)=v_*+s=0$, ordinary Cauchy–Schwarz gives $s^2\le\ell\sum_qb_q^2$, where $\ell$ is the number of classes. If $c=1$, nonpositivity follows immediately. In the exceptional case,

$$\ell\le n-|S|=n-k+1, \qquad \ell(c-1)\le c,$$

which again proves $Q_A(v)\le0$ on that hyperplane. A quadratic-form lemma converts this into hyperbolicity. Dependent prefixes and empty feasible sets are handled separately. See atlasMatrix_one_hyperbolic.

5. Pass from children to parents

The linear-algebra engine considers a symmetric nonnegative parent $A$, a positive vector $h$, and hyperbolic children $B_i$ satisfying

$$(Av)_i=B_i(v,h),\qquad \sum_i h_iQ_{B_i}(v)=Q_A(v).$$

Child reverse Cauchy–Schwarz yields

$$Q_A(v)\le\sum_i h_i\frac{(Av)_i^2}{(Ah)_i}.$$

Positive diagonal normalization turns this into $Q_T(x)\le\|Tx\|^2$ for a symmetric nonnegative matrix $T$ having a positive fixed vector $p$. A maximum-ratio argument bounds its eigenvalues by $|\lambda|\le1$; the energy inequality gives $\lambda\le\lambda^2$. Thus every positive eigenvalue is $1$. A strictly positive hub column forces that eigenspace to be one-dimensional. The spectral theorem then makes $Q_T$ nonpositive on $p^\perp$, establishing hyperbolicity and transferring it back to $A$.

This argument is hyperbolic_of_local_quadratic_data.

For the atlas, apply it to

$$A_t=tA(S,m+1)+(1-t)A(S,m),\qquad0<t<1,$$

with ground-letter weights $t$ and star weight $1-t$. Remove infeasible coordinates, whose rows and columns are identically zero. The independent witness $J$ ensures positivity of the needed continuations, including the star hub. The insertion identities provide inheritance and the weighted quadratic identity exactly.

Finally, hyperbolicity passes to the endpoint as $t\to1$. Induction from depth one reaches $A(\varnothing,k)$. See hyperbolic_right_endpoint and atlasMatrix_hyperbolic_iter.

6. Evaluate the root and clear the factors

Let $u$ be one on ground coordinates and zero at the star, and let $e_*$ select the star. At the root $A=A(\varnothing,k)$, expanding finite sums gives

$$Q_A(e_*)=W(\varnothing,k-1),\quad B_A(u,e_*)=W(\varnothing,k),\quad Q_A(u)=W(\varnothing,k+1).$$

All these counts are nonnegative, so root hyperbolicity yields

$$(k!I_k)^2\ge (k-1)!I_{k-1}\frac{n-k+1}{n-k}(k+1)!I_{k+1}.$$

Canceling positive factorial and denominator factors gives

$$(k+1)(n-k+1)I_{k-1}I_{k+1}\le k(n-k)I_k^2.$$

The evaluation is normalized_inequality_of_root_hyperbolic. Binomial recurrences convert this into the benchmark’s exact statement. If $k\ge n$, both $\binom n{k+1}$ and $I_{k+1}$ vanish, so both sides are zero. The final adapter proves this boundary case explicitly: branden_huh_strongest_mason.

Scope and provenance

The accepted development formalizes this matroid inequality through combinatorial atlas matrices. It does not formalize the full theory of Lorentzian polynomials or tropical geometry. Mathlib supplies general infrastructure, including matroids, finite cardinalities, real symmetric spectral theory, and limits; the submitted modules assemble the missing argument.

Submission issue #15 passed both Axiom Proofs comparator lanes on September 1, 2026. The frozen submission is commit f0629e6b9c80a8aedef6a923892150735f56570a; its archived proof comprises 13 Lean source files and uses Lean 4.33.0. The verification record reports only the standard foundational dependencies propext, Classical.choice, and Quot.sound.

The recorded final worker used Codexiom with openai/gpt-5.6-sol-pro. It received a preloaded, audited AxiomMath atlas development, checked the dependency chain and counting conventions, completed the exact benchmark adapter, and removed warnings. Its recorded runtime and model cost therefore describe that final run, not the entire preceding development. Human involvement is recorded as theorem selection, orchestration, review requirements, and acceptance criteria. The accepted metadata and frozen proof blueprint preserve this distinction.

References

• Petter Brändén and June Huh, Lorentzian polynomials, Annals of Mathematics 192 (2020), 821–891. Theorem 4.14 gives the strongest Mason inequality.
• Nima Anari, Kuikui Liu, Shayan Oveis Gharan, and Cynthia Vinzant, Log-Concave Polynomials III: Mason’s Ultra-Log-Concavity Conjecture for Independent Sets of Matroids (2018), an independent proof through complete log-concavity.
• Swee Hong Chan and Igor Pak, Introduction to the combinatorial atlas (2022), especially the local-to-global framework and its application to Mason’s inequality.
• AxiomMath, frozen proof blueprint and audit record, and acceptance workflow.