Heron–Rota–Welsh

The theorem

Let $M$ be a matroid on a finite ground set $E$, with rank function $r_M$. Its characteristic polynomial is

$$\chi_M(t)=\sum_{S\subseteq E}(-1)^{|S|}t^{r_M(E)-r_M(S)}.$$

Write $c_k(M)=|[t^k]\chi_M(t)|$. The Heron–Rota–Welsh theorem says that these unsigned coefficients are log-concave:

$$c_{k+1}(M)^2\geq c_k(M)c_{k+2}(M)\qquad(k\geq0).$$

The Lean statement uses coefficients in ascending degree. This reverses the indexing often used in the literature, without changing the inequality. It quantifies over every finite matroid whose ground set is the whole ambient finite type; there is no representability assumption. Loops are allowed, and coefficients beyond the polynomial’s degree are zero. Formal entry point.

Adiprasito, Huh, and Katz proved the theorem using the Hodge–Riemann relations for matroid Chow rings. Their 2018 paper treats arbitrary matroids; the earlier Huh–Katz paper establishes the result for realizable matroids through intersection theory.

The accepted formal proof follows an explicit route through weighted bilinear forms on the lattice of flats. It proves the Hodge-index inequality needed for the coefficient sequence. It does not formalize the complete Chow-ring construction, hard Lefschetz theorem, or full Hodge–Riemann package of the original paper.

1. Replace subsets by flats

A flat is a subset closed under matroid closure. Every subset has a unique closure, so the defining sum for $\chi_M$ can be grouped by flats. For a flat $F$, define

$$\omega(F)=\sum_{\operatorname{cl}(S)=F}(-1)^{|S|}.$$

For a loopless matroid, the proof identifies $\omega(F)$ with $\mu(\varnothing,F)$, the Möbius function of the flat lattice. Its cumulative sums are $1$ at the bottom flat and $0$ elsewhere, which characterizes this Möbius function. Consequently,

$$\chi_M(t)=\sum_F\mu(\varnothing,F)t^{r_M(E)-r_M(F)}.$$

The next ingredient is the sign rule $(-1)^{r_M(F)}\omega(F)\geq0$. Thus the nonnegative weight $w(F)=|\omega(F)|$ can replace signed Möbius weights whenever the rank is fixed. The proof establishes this sign rule using cancellation after adjoining a distinguished element to a flat, followed by induction on rank.

Sources: closure-fiber weights, Möbius identification, alternating signs.

2. Identify the reduced coefficients

For a nonempty loopless matroid of rank $r$, set $\overline\chi_M(t)=\chi_M(t)/(t-1)$ and

$$b_j(M)=\left|[t^{r-1-j}]\overline\chi_M(t)\right|\qquad(0\leq j<r).$$

Set $b_j(M)=0$ for $j\geq r$. This extension makes the consecutive-coefficient formulas below meaningful at every $j\geq0$; it also agrees with the avoiding-flat sum, since the top flat contains $e$ and no flat has rank greater than $r$.

Fix an element $e\in E$. The proof obtains two descriptions of the same number:

$$b_j(M)=\sum_{\substack{r_M(F)=j\\e\notin F}}w(F) =\sum_{\substack{r_M(F)=j+1\\e\in F}}w(F).$$

The first formula comes from the relation between the characteristic and reduced characteristic polynomials. The second uses closure with $e$: a flat avoiding $e$ is sent to $\operatorname{cl}(F\cup\{e\})$, increasing its rank by one. The relevant Möbius cancellation identity gives the equality of the weighted sums. This is a weighted identity, not an assertion that the two collections of flats have equal cardinality.

These formulas are the bridge from polynomial coefficients to the explicit bilinear form below. Reduced polynomial coefficient identity, avoiding-flat formula, containing-flat formula.

3. Build a form on adjacent ranks

Let $T$ be a flat, and let $s\geq1$. On real-valued functions on the flats, define

$$\begin{aligned} Q_{s,T}(x,y)={}&\sum_{\substack{F\leq T\\r_M(F)=s}}w(F)x_Fy_F +\sum_{\substack{G\leq T\\r_M(G)=s+1}}w(G)x_Gy_G\\ &-\sum_{\substack{F\leq T\\r_M(F)=s}}w(F) \sum_{F\lessdot G\leq T}(x_F-x_G)(y_F-y_G). \end{aligned}$$

Here $F\lessdot G$ means that $G$ covers $F$: no flat lies strictly between them. The last term is a weighted graph energy along cover relations. All ingredients are finite sums, ranks, containment, and the weights already defined.

Take $T=E$, and let $u_F$ indicate that $e\in F$, while $v_F$ indicates that $e\notin F$. The coefficient identities give

$$Q_{j+1,E}(u,u)=b_j,\qquad Q_{j+1,E}(u,v)=b_{j+1},\qquad Q_{j+1,E}(v,v)=b_{j+2}.$$

For example, an avoiding flat has exactly one cover containing $e$, namely its closure after adjoining $e$. Its contribution to the graph energy therefore cancels its contribution on the lower diagonal. This gives the last pairing identity. The mixed identity also uses the Möbius-weighted cancellation from the preceding step.

Sources: definition of the form, containing-vector pairing, avoiding-vector self-pairing.

4. Establish the Hodge-index inequality

The central theorem asserts that, whenever $Q_{s,T}(a,a)>0$,

$$Q_{s,T}(a,a)Q_{s,T}(x,x)\leq Q_{s,T}(a,x)^2.$$

This reverse Cauchy–Schwarz inequality expresses that the form has at most one positive direction. It is proved for every rank and every ceiling flat containing a chosen element. All-ranks theorem.

At rank one, call the rank-one flats points and the rank-two flats lines. Each pair of distinct points lies on a unique line, and a line’s weight is its number of points minus one. Expanding the form produces a square of the total point sum minus a sum of squares indexed by lines. On the hyperplane where the point sum is zero, the form is therefore nonpositive. Elementary bilinear algebra gives reverse Cauchy–Schwarz. Atomic nonpositivity.

The inductive step studies the deformation

$$B_t=tQ_{s,T}+Q_{s+1,T},\qquad t>0,$$

with reference vector $h_t(F)=t$ when $e\in F$ and $h_t(F)=1$ otherwise. Only flats of ranks $s,s+1,s+2$ contribute. For each flat in this three-rank window, the proof constructs a local form. At the lower rank the required inequality reduces to an atomic interval calculation; at the middle rank it is an explicit two-functional calculation; at the upper rank it follows from the induction hypothesis applied below that flat. Local forms.

5. Assemble the local inequalities

The passage from those local calculations to $B_t$ is the main assembly argument. The local forms obey exchange identities and decompose the global form. They also have positive norms at $h_t$.

From these norms, the proof constructs a positive diagonal form $D$ such that $K=D-B_t$ is a weighted graph Laplacian after rescaling coordinates by $h_t$. Its quadratic form is a sum of nonnegative edge energies. The cover graph on the three-rank window is connected, so its Laplacian equation is solvable for every forcing term of total mass zero. Connectivity, Laplacian solvability.

If $B_t(h_t,x)=0$, the resulting forcing term has zero total mass. A solution supplies a vector $z$ with $Kz=Dx$. Summing the local reverse Cauchy–Schwarz inequalities gives

$$B_t(z,z)\leq D(z-x,z-x).$$

Together with $Kz=Dx$, this implies $D(z,x)\leq D(x,x)$. Applying $K\geq0$ to $x-z$ then yields

$$B_t(x,x)\leq D(z,x)-D(x,x)\leq0.$$

Thus $B_t$ is nonpositive on its primitive hyperplane. The proof derives reverse Cauchy–Schwarz for $B_t$ and then sends $t$ to zero. In Lean, the last passage is an explicit small-parameter argument bounding the error terms of a quadratic polynomial, rather than an appeal to a spectral continuity theorem. This completes the rank induction for $Q_{s+1,T}$.

6. Recover log-concavity

Apply the all-ranks inequality to the containing and avoiding indicators from Step 3. When $b_j>0$, it gives immediately

$$b_jb_{j+2}\leq b_{j+1}^2.$$

If $b_j=0$, the same inequality follows from nonnegativity. The formal implementation packages the form, the two vectors, the pairing identities, and primitive nonpositivity as a finite Hodge witness, then applies a general coefficient reduction. Incidence witness, reduced log-concavity.

To return to $\chi_M$, adjoin one coloop: let $N=M\oplus U_{1,1}$. Direct-sum multiplicativity gives

$$\chi_N(t)=(t-1)\chi_M(t),\qquad \overline\chi_N(t)=\chi_M(t).$$

Reduced log-concavity for $N$ is therefore exactly the desired coefficient inequality for $M$, after reversing indices. The proof also handles the boundary cases: beyond rank the upper-degree coefficient vanishes; if $M$ has a loop, subsets cancel in pairs and the entire characteristic polynomial is zero. This coloop argument includes the empty ground set. Coloop identity, final reduction.

Formalization and provenance

The accepted overlay contains 14 Lean files, totaling 26,918 lines. That is the size of the preserved submission, including supporting developments and alternative constructions; it is not a measurement of a minimized dependency closure.

The acceptance record dates to September 5, 2026. Both the official and wide Comparator lanes passed submission #23. The recorded environment uses Lean 4.33.0 and mathlib commit 6f1ef4e5dd604a435bddba4747b13970cd65d2a1.

The submitted provenance describes a supervised Codexiom run lineage involving several models. It credits GPT-6 Astra at maximum reasoning effort with the decisive incidence construction and final proof, building on earlier coefficient reductions and exploration. It records human involvement in theorem selection, orchestration, recovery, model switching, and acceptance criteria, with no manually constructed Lean proof text. These are provenance claims in the submission record; the mathematical acceptance evidence is the checked theorem and the successful Comparator runs.

For historical background and the original Chow-ring proof, see Adiprasito–Huh–Katz, Hodge theory for combinatorial geometries, Annals of Mathematics 188 (2018), 381–452. The explanation above follows the accepted Lean declarations and makes no claim that this particular presentation is a new mathematical proof.