Strongly Polynomial Bounds in Linear Programming and Smale's 9th Problem

This preprint provides an exhaustive 9-page mathematical monograph on Smale's 9th Problem (Steve Smale, 2000), dedicated to the existence of a strongly polynomial-time algorithm for Linear Programming (LP). While the ellipsoid method (Khachiyan, 1979) and projective interior-point methods (Karmarkar, 1984) established that linear programming is solvable in weakly polynomial time (where complexity depends on the binary bit-length L), finding an algorithm whose arithmetic operations depend solely on the matrix dimensions m and n in the real RAM model remains one of the greatest open problems in optimization and theoretical computer science: ∃? Algorithme avec T(A, b, c) ≤ O((m + n)C) opérations arithmétiques dans ℝ This treatise develops a comprehensive, non-elliptical exposition of primal-dual complementary slackness, Éva Tardos' landmark theorem (1986) for matrices with bounded subdeterminants Δ, the Vavasis-Ye Layered Least- Squares (LLS) interior-point algorithm (1996) parameterized by χ̄(A), and tropical geometry curvature barriers (Allamigeon et al., 2018). Key Mathematical Results & Contributions Primal-Dual Duality Architecture: Exact algebraic derivation of the duality gap identity ⟨c, x⟩ − ⟨b, y⟩ = ⟨c − ATy, x⟩, establishing weak duality and complementary slackness equivalence. Éva Tardos' Landmark Theorem (1986): Step-by-step proof that LP is strongly polynomial with runtime O(poly(m, n, log Δ)) when subdeterminants satisfy Δ = maxB | det(AB)|, completely independent of the bit-lengths of b and c. Vavasis-Ye Layered Least-Squares (LLS) Method (1996): Detailed analysis of continuous path-following in ill-conditioned regimes, proving termination in O(n3.5 log(χ̄(A) + n)) iterations. Tropical Geometry Curvature Barriers: Structural study of log-barrier central path geometries showing exponential bendings for generic interior-point paths. 100% Machine-Checked Verification in Lean 4: Duality gap identity, weak duality theorem, complementary slackness equivalence, unimodular basis integer preservation, and logarithmic barrier contraction are machine-certified with 0 axioms, 0 linter warnings, and 0 sorry placeholders via the Lean 4 interactive theorem prover and Mathlib. Repository and Verification Artifacts The companion machine-checked code and formal verification artifacts are publicly hosted on GitHub:https://github.com/flouzzy/smale-problemsInteractive Portal: https://maths-proofs.edounze.com/#smale-09-linear-programming Primary MSC (2020): 90C05, 68Q25, 90C51, 68V20, 15A15, 52B12.Keywords: Smale's 9th Problem, Linear Programming, Strongly Polynomial Complexity, Weakly Polynomial, Tardos' Theorem, Interior-Point Methods, Central Path, Vavasis-Ye Algorithm, Duality Gap, Formal Verification, Lean 4, Mathlib.