1. FormalConjectures
  2. Arxiv
  3. «2602.05192»
  4. FirstProof4
/- Copyright 2026 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ import FormalConjecturesUtil

First Proof, Theorem 4

Reference: arxiv/2602.05192v2 First Proof by Mohammed Abouzaid, Andrew J. Blumberg, Martin Hairer, Joe Kileel, Tamara G. Kolda, Paul D. Nelson, Daniel Spielman, Nikhil Srivastava, Rachel Ward, Shmuel Weinberger, Lauren Williams

open Polynomial Finset ENNRealopen scoped Natnamespace Arxiv.«2602.05192»variable {F : Type} [Field F]

Define $p \boxplus_n q(x)$ to be the polynomial $$ (p \boxplus_n q)(x) = \sum_{k=0}^n c_k x^{n-k} $$ where the coefficients $c_k$ are given by the formula: $$ c_k = \sum_{i+j=k} \frac{(n-i)! (n-j)!}{n! (n-k)!} a_i b_j $$ for $k = 0, 1, \dots, n$.

noncomputable def finiteAdditiveConvolution (n : ℕ) (p q : F[X]) : F[X] := let c := fun k => ∑ ij ∈ antidiagonal (k : ℕ), ((n - ij.1)! * (n - ij.2)! : F) / (n ! * (n - k)! : F) * p.coeff (n - ij.1) * q.coeff (n - ij.2) ∑ k ∈ range (n + 1), c k • X^(n - k)local notation p " (⊞_"n ")" q:65 => finiteAdditiveConvolution n p q@[category test, AMS 26] theorem finiteAdditiveConvolution_comm (n : ℕ) (p q : F[X]) : p (⊞_n) q = q (⊞_n) p := F:Typeinst✝:Field Fn:ℕp:F[X]q:F[X]⊢ p (⊞_n)q = q (⊞_n)p F:Typeinst✝:Field Fn:ℕp:F[X]q:F[X]⊢ ∑ a ∈ range (n + 1), (fun k ↦ ∑ ij ∈ HasAntidiagonal.antidiagonal k, ↑(n - ij.1)! * ↑(n - ij.2)! / (↑n ! * ↑(n - k)!) * p.coeff (n - ij.1) * q.coeff (n - ij.2)) a • X ^ (n - a) = ∑ a ∈ range (n + 1), (fun k ↦ ∑ ij ∈ HasAntidiagonal.antidiagonal k, ↑(n - ij.1)! * ↑(n - ij.2)! / (↑n ! * ↑(n - k)!) * q.coeff (n - ij.1) * p.coeff (n - ij.2)) a • X ^ (n - a) exact sum_congr rfl fun m hm => (congr_arg₂ _) (sum_equiv (.prodComm _ _) (F:Typeinst✝:Field Fn:ℕp:F[X]q:F[X]m:ℕhm:m ∈ range (n + 1)⊢ ∀ (i : ℕ × ℕ), i ∈ HasAntidiagonal.antidiagonal m ↔ (Equiv.prodComm ℕ ℕ) i ∈ HasAntidiagonal.antidiagonal m All goals completed! 🐙) fun _ _ => F:Typeinst✝:Field Fn:ℕp:F[X]q:F[X]m:ℕhm:m ∈ range (n + 1)x✝¹:ℕ × ℕx✝:x✝¹ ∈ HasAntidiagonal.antidiagonal m⊢ ↑(n - x✝¹.1)! * ↑(n - x✝¹.2)! / (↑n ! * ↑(n - m)!) * p.coeff (n - x✝¹.1) * q.coeff (n - x✝¹.2) = ↑(n - ((Equiv.prodComm ℕ ℕ) x✝¹).1)! * ↑(n - ((Equiv.prodComm ℕ ℕ) x✝¹).2)! / (↑n ! * ↑(n - m)!) * q.coeff (n - ((Equiv.prodComm ℕ ℕ) x✝¹).1) * p.coeff (n - ((Equiv.prodComm ℕ ℕ) x✝¹).2) All goals completed! 🐙) rfl@[category test, AMS 26] theorem finiteAdditiveConvolution_degree (n : ℕ) (p q : ℝ[X]) (hp : p.degree = n) (hq : q.degree = n): (p (⊞_n) q).degree = n := n:ℕp:ℝ[X]q:ℝ[X]hp:p.degree = ↑nhq:q.degree = ↑n⊢ (p (⊞_n)q).degree = ↑n All goals completed! 🐙n:ℕp:ℝ[X]q:ℝ[X]hn:0 < nhp_deg:p.degree = ↑nhq_deg:q.degree = ↑nhp_monic:p.Monichq_monic:q.Monichc0:∑ ij ∈ HasAntidiagonal.antidiagonal 0, ↑(n - ij.1)! * ↑(n - ij.2)! / (↑n ! * ↑(n - 0)!) * p.coeff (n - ij.1) * q.coeff (n - ij.2) = 1r:ℝ[X] := p (⊞_n)qk:ℕa✝:k ∈ range (n + 1)hk0:k ≠ 0this:n ≠ n - k⊢ ((∑ ij ∈ HasAntidiagonal.antidiagonal k, ↑(n - ij.1)! * ↑(n - ij.2)! / (↑n ! * ↑(n - k)!) * p.coeff (n - ij.1) * q.coeff (n - ij.2)) * if n = n - k then 1 else 0) = 0 All goals completed! 🐙 n:ℕp:ℝ[X]q:ℝ[X]hn:0 < nhp_deg:p.degree = ↑nhq_deg:q.degree = ↑nhp_monic:p.Monichq_monic:q.Monichc0:∑ ij ∈ HasAntidiagonal.antidiagonal 0, ↑(n - ij.1)! * ↑(n - ij.2)! / (↑n ! * ↑(n - 0)!) * p.coeff (n - ij.1) * q.coeff (n - ij.2) = 1r:ℝ[X] := p (⊞_n)q⊢ 0 ∉ range (n + 1) → ((∑ ij ∈ HasAntidiagonal.antidiagonal 0, ↑(n - ij.1)! * ↑(n - ij.2)! / (↑n ! * ↑(n - 0)!) * p.coeff (n - ij.1) * q.coeff (n - ij.2)) * if n = n - 0 then 1 else 0) = 0 -- 0 ∈ range (n+1) n:ℕp:ℝ[X]q:ℝ[X]hn:0 < nhp_deg:p.degree = ↑nhq_deg:q.degree = ↑nhp_monic:p.Monichq_monic:q.Monichc0:∑ ij ∈ HasAntidiagonal.antidiagonal 0, ↑(n - ij.1)! * ↑(n - ij.2)! / (↑n ! * ↑(n - 0)!) * p.coeff (n - ij.1) * q.coeff (n - ij.2) = 1r:ℝ[X] := p (⊞_n)qh:0 ∉ range (n + 1)⊢ ((∑ ij ∈ HasAntidiagonal.antidiagonal 0, ↑(n - ij.1)! * ↑(n - ij.2)! / (↑n ! * ↑(n - 0)!) * p.coeff (n - ij.1) * q.coeff (n - ij.2)) * if n = n - 0 then 1 else 0) = 0; exact absurd (Finset.mem_range.mpr (n:ℕp:ℝ[X]q:ℝ[X]hn:0 < nhp_deg:p.degree = ↑nhq_deg:q.degree = ↑nhp_monic:p.Monichq_monic:q.Monichc0:∑ ij ∈ HasAntidiagonal.antidiagonal 0, ↑(n - ij.1)! * ↑(n - ij.2)! / (↑n ! * ↑(n - 0)!) * p.coeff (n - ij.1) * q.coeff (n - ij.2) = 1r:ℝ[X] := p (⊞_n)qh:0 ∉ range (n + 1)⊢ 0 < n + 1 All goals completed! 🐙)) h n:ℕp:ℝ[X]q:ℝ[X]hn:0 < nhp_deg:p.degree = ↑nhq_deg:q.degree = ↑nhp_monic:p.Monichq_monic:q.Monichc0:∑ ij ∈ HasAntidiagonal.antidiagonal 0, ↑(n - ij.1)! * ↑(n - ij.2)! / (↑n ! * ↑(n - 0)!) * p.coeff (n - ij.1) * q.coeff (n - ij.2) = 1r:ℝ[X] := p (⊞_n)q⊢ r.natDegree ≤ n -- natDegree ≤ n: each term has degree ≤ n since n - k ≤ n n:ℕp:ℝ[X]q:ℝ[X]hn:0 < nhp_deg:p.degree = ↑nhq_deg:q.degree = ↑nhp_monic:p.Monichq_monic:q.Monichc0:∑ ij ∈ HasAntidiagonal.antidiagonal 0, ↑(n - ij.1)! * ↑(n - ij.2)! / (↑n ! * ↑(n - 0)!) * p.coeff (n - ij.1) * q.coeff (n - ij.2) = 1r:ℝ[X] := p (⊞_n)q⊢ (p (⊞_n)q).natDegree ≤ n n:ℕp:ℝ[X]q:ℝ[X]hn:0 < nhp_deg:p.degree = ↑nhq_deg:q.degree = ↑nhp_monic:p.Monichq_monic:q.Monichc0:∑ ij ∈ HasAntidiagonal.antidiagonal 0, ↑(n - ij.1)! * ↑(n - ij.2)! / (↑n ! * ↑(n - 0)!) * p.coeff (n - ij.1) * q.coeff (n - ij.2) = 1r:ℝ[X] := p (⊞_n)q⊢ (∑ x ∈ range (n + 1), (∑ ij ∈ HasAntidiagonal.antidiagonal x, ↑(n - ij.1)! * ↑(n - ij.2)! / (↑n ! * ↑(n - x)!) * p.coeff (n - ij.1) * q.coeff (n - ij.2)) • X ^ (n - x)).natDegree ≤ n n:ℕp:ℝ[X]q:ℝ[X]hn:0 < nhp_deg:p.degree = ↑nhq_deg:q.degree = ↑nhp_monic:p.Monichq_monic:q.Monichc0:∑ ij ∈ HasAntidiagonal.antidiagonal 0, ↑(n - ij.1)! * ↑(n - ij.2)! / (↑n ! * ↑(n - 0)!) * p.coeff (n - ij.1) * q.coeff (n - ij.2) = 1r:ℝ[X] := p (⊞_n)q⊢ fold max 0 (natDegree ∘ fun i ↦ (∑ ij ∈ HasAntidiagonal.antidiagonal i, ↑(n - ij.1)! * ↑(n - ij.2)! / (↑n ! * ↑(n - i)!) * p.coeff (n - ij.1) * q.coeff (n - ij.2)) • X ^ (n - i)) (range (n + 1)) ≤ n n:ℕp:ℝ[X]q:ℝ[X]hn:0 < nhp_deg:p.degree = ↑nhq_deg:q.degree = ↑nhp_monic:p.Monichq_monic:q.Monichc0:∑ ij ∈ HasAntidiagonal.antidiagonal 0, ↑(n - ij.1)! * ↑(n - ij.2)! / (↑n ! * ↑(n - 0)!) * p.coeff (n - ij.1) * q.coeff (n - ij.2) = 1r:ℝ[X] := p (⊞_n)q⊢ ∀ b ∈ range (n + 1), (natDegree ∘ fun i ↦ (∑ ij ∈ HasAntidiagonal.antidiagonal i, ↑(n - ij.1)! * ↑(n - ij.2)! / (↑n ! * ↑(n - i)!) * p.coeff (n - ij.1) * q.coeff (n - ij.2)) • X ^ (n - i)) b ≤ n n:ℕp:ℝ[X]q:ℝ[X]hn:0 < nhp_deg:p.degree = ↑nhq_deg:q.degree = ↑nhp_monic:p.Monichq_monic:q.Monichc0:∑ ij ∈ HasAntidiagonal.antidiagonal 0, ↑(n - ij.1)! * ↑(n - ij.2)! / (↑n ! * ↑(n - 0)!) * p.coeff (n - ij.1) * q.coeff (n - ij.2) = 1r:ℝ[X] := p (⊞_n)qk:ℕhk:k ∈ range (n + 1)⊢ (natDegree ∘ fun i ↦ (∑ ij ∈ HasAntidiagonal.antidiagonal i, ↑(n - ij.1)! * ↑(n - ij.2)! / (↑n ! * ↑(n - i)!) * p.coeff (n - ij.1) * q.coeff (n - ij.2)) • X ^ (n - i)) k ≤ n n:ℕp:ℝ[X]q:ℝ[X]hn:0 < nhp_deg:p.degree = ↑nhq_deg:q.degree = ↑nhp_monic:p.Monichq_monic:q.Monichc0:∑ ij ∈ HasAntidiagonal.antidiagonal 0, ↑(n - ij.1)! * ↑(n - ij.2)! / (↑n ! * ↑(n - 0)!) * p.coeff (n - ij.1) * q.coeff (n - ij.2) = 1r:ℝ[X] := p (⊞_n)qk:ℕhk:k ∈ range (n + 1)⊢ (X ^ (n - k)).natDegree ≤ n All goals completed! 🐙

For a monic polynomial $p(x)=\prod_{i\le n}(x- \lambda_i)$, define $$\Phi_n(p):=\sum_{i\le n}(\sum_{j\neq i} \frac1{\lambda_i-\lambda_j})^2$$ and $\Phi_n(p):=\infty$ if $p$ has a multiple root.

noncomputable def Φ (p : ℝ[X]) : ℝ≥0∞ := if p.roots.Nodup then let roots := p.roots.toFinset (∑ i ∈ roots, (∑ j ∈ roots.erase i, 1 / (i - j)) ^ 2).toNNReal else ⊤

A predicate that holds if $p(x)$ and $q(x)$ are monic real-rooted polynomials of degree $n$, then $$\frac{1}{\Phi_n(p\boxplus_n q)} \ge \frac{1}{\Phi_n(p)}+\frac{1}{\Phi_n(q)}?$$

def FourProp (p q : ℝ[X]) (n : ℕ) : Prop := p.degree = n → p.roots.card = n → q.degree = n → q.roots.card = n → p.Monic → q.Monic → 1 / Φ p + 1 / Φ q ≤ 1 / Φ (p (⊞_n) q)

Is it true that if $p(x)$ and $q(x)$ are monic real-rooted polynomials of degree $n$, then $$\frac{1}{\Phi_n(p\boxplus_n q)} \ge \frac{1}{\Phi_n(p)}+\frac{1}{\Phi_n(q)}?$$

arxiv/2602.05192v2 contains a proof.

@[category research solved, AMS 26, formal_proof using lean4 at "https://github.com/frenzymath/Archon-FirstProof-Results/blob/main/FirstProof/FirstProof4/Problem4.lean"] theorem four : answer(True) ↔ ∀ (p q : ℝ[X]) (n : ℕ), FourProp p q n := ⊢ True ↔ ∀ (p q : ℝ[X]) (n : ℕ), FourProp p q n All goals completed! 🐙

Is it true that if $p(x)$ and $q(x)$ are monic real-rooted polynomials of degree $2$, then $$\frac{1}{\Phi_2(p\boxplus_n q)} \ge \frac{1}{\Phi_2(p)}+\frac{1}{\Phi_2(q)}?$$

@[category research solved, AMS 26] theorem four_2 : answer(True) ↔ ∀ (p q : ℝ[X]), FourProp p q 2 := ⊢ True ↔ ∀ (p q : ℝ[X]), FourProp p q 2 All goals completed! 🐙

Is it true that if $p(x)$ and $q(x)$ are monic real-rooted polynomials of degree $3$, then $$\frac{1}{\Phi_3(p\boxplus_n q)} \ge \frac{1}{\Phi_3(p)}+\frac{1}{\Phi_3(q)}?$$

@[category research solved, AMS 26] theorem four_3 : answer(True ) ↔ ∀ (p q : ℝ[X]), FourProp p q 3 := ⊢ True ↔ ∀ (p q : ℝ[X]), FourProp p q 3 All goals completed! 🐙end Arxiv.«2602.05192»