Papers With

← All papers
First page of Pfaffian Positivity for Convex Kernels and Optimal Matching Bounds

Pfaffian Positivity for Convex Kernels and Optimal Matching Bounds

William Johnson

math.CO Oct 17, 2026 · v1 math.DS
formalization mathlib combinatorics algebra
Read PDF arXiv abstract Code
TL;DR
Part of the Pfaffian positivity results is formalized in Lean 4 with Mathlib. The public repository maps the Lean theorems to the paper's results.
Abstract
We show that for all positive, nonincreasing, convex functions $f : (0, \infty) \to (0,\infty)$ and for any collection of $n$ points $x_i \in \mathbb{R}$ with $x_1 < x_2 < \ldots < x_n$ and $n$ even, the Pfaffian of the skew matrix defined by $f(x_j - x_i)$ above the diagonal is positive. More generally, we establish coefficientwise nonnegativity for Pfaffians arising from interval decompositions, which also yields quantitative lower bounds for singly and doubly bordered Pfaffians. Choosing $f(r) = r^{-2}$ proves the three nonvanishing assertions in the conjecture of Albouy and Moeckel. Further, we show that the rainbow bound (the product over the nested matching $\{1,n\}, \{2,n-1\}, \ldots \{n/2, n/2 + 1\}$) is the unique single-matching product that bounds $\mathrm{Pf}(A_f(x))$ below uniformly over $x$ and $f$ positive, nonincreasing, convex.
Problem

Pfaffians are alternating sums over perfect matchings, so their sign is not evident from the entries. The question is whether the Pfaffian of the skew matrix built from f(x_j - x_i) is positive for ordered points and positive, nonincreasing, convex f. A related target is the nonvanishing assertions of the Albouy–Moeckel conjecture.

Approach

The matrix is decomposed into indeterminates indexed by subintervals of [n] via Möbius inversion. A twin-rows lemma shows the Pfaffian of this interval matrix is a polynomial with nonnegative integer coefficients. Convexity and monotonicity of f give nonnegative specializations of these indeterminates. Alternating prefix sums of principal Pfaffians give an endpoint inequality, which is iterated to obtain the rainbow bound and also bounds for bordered Pfaffians; part of the work is machine-checked in Lean 4 with Mathlib.

Results

The Pfaffian is bounded below by the rainbow matching product, which implies the diameter bound f(x_n - x_1)^{n/2} > 0. Taking f(r) = r^{-2} proves the three nonvanishing assertions of the Albouy–Moeckel conjecture. The rainbow product is the unique single-matching product that bounds the Pfaffian below uniformly over x and f.