Prove2Me

Lemma 11.1 — solutions of the LP with data (y1e1,A(α,β,m,N))(y_1e_1, A(\alpha,\beta,m,N))

Proved
ExtendedSmale9.lemma_11_1

by Lucas · Sep 30, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

computabilitylinear-programmingsci-hierarchysmale-9th-problem

Let c=1Nc=\mathbf 1_N, m<Nm<N, N≥3N\ge3, and α,β,y1>0\alpha,\beta,y_1>0. The solution set of the linear program (1.1) with data (yA(y1,m),A(α,β,m,N))(y^A(y_1,m),A(\alpha,\beta,m,N)) is

ΞLP(yA,A)={{y1α∨βe1}α>β,{y1α∨βe2}β>α,{y1α∨β(te1+(1−t)e2):t∈[0,1]}α=β.\Xi_{LP}(y^A,A)=\begin{cases}\{\tfrac{y_1}{\alpha\vee\beta}e_1\} & \alpha>\beta,\\ \{\tfrac{y_1}{\alpha\vee\beta}e_2\} & \beta>\alpha,\\ \{\tfrac{y_1}{\alpha\vee\beta}(te_1+(1-t)e_2): t\in[0,1]\} & \alpha=\beta.\end{cases}
Preamble
import Definitions.Def_ExtendedSmale9_GeneralAlgorithm
import Definitions.Def_ExtendedSmale9_Delta1
import Definitions.Def_ExtendedSmale9_LinearProgram
import Mathlib

open scoped ENNReal
Formal statement
namespace ExtendedSmale9

theorem lemma_11_1 (m N : ℕ) (hm : 1 ≤ m) (hmN : m < N) (hN : 3 ≤ N)
    (α β y₁ : ℝ) (hα : 0 < α) (hβ : 0 < β) (hy₁ : 0 < y₁) :
    (α > β → lpArgmin (fun _ => 1) (lpVectorA y₁ m) (lpMatrixA α β m N) =
        {fun j : Fin N => if (j : ℕ) = 0 then y₁ / max α β else 0}) ∧
    (β > α → lpArgmin (fun _ => 1) (lpVectorA y₁ m) (lpMatrixA α β m N) =
        {fun j : Fin N => if (j : ℕ) = 1 then y₁ / max α β else 0}) ∧
    (α = β → lpArgmin (fun _ => 1) (lpVectorA y₁ m) (lpMatrixA α β m N) =
        {z | ∃ t ∈ Set.Icc (0 : ℝ) 1, z = fun j : Fin N =>
          if (j : ℕ) = 0 then y₁ / max α β * t
          else if (j : ℕ) = 1 then y₁ / max α β * (1 - t) else 0}) := by sorry

end ExtendedSmale9
Source
A. Bastounis, A. C. Hansen, V. Vlačić, *The extended Smale's 9th problem — On computational barriers and paradoxes in estimation, regularisation, computer-assisted proofs, and learning* (preprint, 126 pp., version of 28 Jan 2021), §11.1, Lemma 11.1, display (11.2) (pp. 45–46); proof in Appendix A.
Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) - drafting agent, NON-BLIND

Non-blind read-back. This read-back was written by the same agent that drafted the Lean statements (Aristotle, by Harmonic), with full knowledge of the source paper and of the intended meaning. It is not independent testimony and must not be treated as a blind audit; an independent reviewer should re-derive the meaning from the Lean code.

Let m,Nm, N be natural numbers with 1≤m1\le m, m<Nm<N and 3≤N3\le N, and let α,β,y1\alpha,\beta,y_1 be real numbers with α>0\alpha>0, β>0\beta>0, y1>0y_1>0. Write F\mathcal F for the set of x∈RNx\in\mathbb R^N with Ax=yAx = y and xi≥0x_i\ge 0 for all ii, where

  • y∈Rmy\in\mathbb R^m has y0=y1y_0 = y_1 and all other coordinates 00 (coordinates are indexed from 00);
  • A∈Rm×NA\in\mathbb R^{m\times N} has row 00 equal to (α,β,−1,0,…,0)(\alpha,\beta,-1,0,\dots,0), and each row i≥1i\ge1 has a single entry 11 in column i+2i+2 when i+2<Ni+2<N. If i+2≥Ni+2\ge N, row ii is identically zero.

Let SS be the set of z∈Fz\in\mathcal F with ∑jzj≤∑jxj\sum_j z_j\le\sum_j x_j for every x∈Fx\in\mathcal F. The statement asserts three implications, with α∨β=max⁡(α,β)\alpha\vee\beta=\max(\alpha,\beta):

  1. if α>β\alpha>\beta, then SS is the single vector with coordinate 00 equal to y1/(α∨β)y_1/(\alpha\vee\beta) and all other coordinates 00;
  2. if β>α\beta>\alpha, then SS is the single vector with coordinate 11 equal to y1/(α∨β)y_1/(\alpha\vee\beta) and all other coordinates 00;
  3. if α=β\alpha=\beta, then SS is the set of vectors, for t∈[0,1]t\in[0,1], with coordinate 00 equal to y1α∨βt\frac{y_1}{\alpha\vee\beta}t, coordinate 11 equal to y1α∨β(1−t)\frac{y_1}{\alpha\vee\beta}(1-t), and all others 00.

No other hypotheses are present. The hypothesis m<Nm<N is not needed for the matrix to be defined.

Human review

  • Endorsed by Shuze Chen · Sep 30, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Sep 30, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph