What was already known
The alternating signs in a Pfaffian do not make positivity automatic. The paper derives coefficientwise positivity through interval decompositions and a twin-row cancellation, then obtains the nested-matching bound. Its broader bordered-matrix consequences have different formal coverage.
AI involvement
Johnson credits Claude Opus 5.5 and GPT-6 with generation of the original mathematical proofs and Lean formalization. He subsequently checked and revised the arguments, reviewed the formal statements and wrote the manuscript. The disclosure establishes a central AI proof role, without documenting task-only autonomy.
Importance
Supplies a general positive lower bound for convex distance kernels and identifies the unique universal matching product.
Limitations
The retained scope is the ordinary even-order Pfaffian and universal single-matching comparison. Lean proves a counterexample to every other matching bound, rather than the stronger infimum-zero assertion. Bordered Pfaffians and the complete Albouy–Moeckel corollary are outside the machine-checking scope.
Technical verification
Johnson explicitly reports checking the mathematical arguments. The released Lean development also documents sorry-free proofs of the diameter and rainbow bounds and the weaker comparison sufficient for uniqueness of the universal matching product, with standard-axiom guards and a paper correspondence. This rating excludes the stronger infimum-zero and bordered claims.
Independent checking
Explicit reported checking and revision of the mathematical proofs, with manuscript explanations
- Checker
- William Johnson
- Scope
- Let n≥2 be even, x₁<⋯<xₙ be real, and f:(0,∞)→(0,∞) be positive, nonincreasing and convex. For the skew matrix A with Aᵢⱼ=f(xⱼ−xᵢ) above the diagonal, Pf(A) is at least the positive product ∏ₖ₌₁^(n/2) f(xₙ₊₁₋ₖ−xₖ). This rainbow matching is the only single-matching product that is a universal lower bound over all such f and x.
- Basis
- Reported by the linked checker
Independent checking
Documented formal rainbow bound and failure of every other universal matching-product bound, with statement and standard-axiom guards
- Checker
- Johnson’s Lean 4 / Mathlib development
- Scope
- Let n≥2 be even, x₁<⋯<xₙ be real, and f:(0,∞)→(0,∞) be positive, nonincreasing and convex. For the skew matrix A with Aᵢⱼ=f(xⱼ−xᵢ) above the diagonal, Pf(A) is at least the positive product ∏ₖ₌₁^(n/2) f(xₙ₊₁₋ₖ−xₖ). This rainbow matching is the only single-matching product that is a universal lower bound over all such f and x.
- Basis
- Reported by the linked checker
Human understanding
William Johnson explains the interval decomposition, coefficient positivity, twin-row cancellation and nested-matching argument in his manuscript, after checking and revising the AI-generated proofs.
Correction and publication history
Added a reviewed, scoped central-AI contribution with checking and attribution limits.
Read this published revision