The minimal Lebesgue constants for Lagrange interpolation of degrees four and five on [−1, 1]: algebraic numbers of degrees 73 and 358

Exact minimal Lebesgue constants for polynomial interpolation on [−1, 1] were previously known only for degrees two and three. Rack and Vajda (Studia Univ. Babeş-Bolyai Math. 60, 2015) left degree four open after settling degree three. This paper settles degrees four and five. For degree four, the minimal Lebesgue constant Λ₄* = 1.55949020987555526480… is the largest real root of an explicit irreducible integer polynomial of degree 73. It is therefore an algebraic number of degree exactly 73. The unique extremal node system containing ±1 is {−1, −t*, 0, t*, 1}, where t* = 0.62091130468991204068… is the unique root in (0.61, 0.67) of a second irreducible polynomial of degree 73. Every extremal system in [−1, 1] is an affine image c + sξ of this system. The admissible pairs (s, c) form an explicit quadrilateral in the (s, c)-plane, described by a constant ρ that has a closed form in t* and Λ₄*. For degree five, Λ₅* = 1.67221036502263078954… is the unique root in [1.67221036502263, 1.67221036502264] of an explicit irreducible integer polynomial of degree 358. It is therefore an algebraic number of degree exactly 358. The extremal nodes containing ±1 are {−1, −b*, −a*, a*, b*, 1}, with a* = 0.26890704477197294321… and b* = 0.73412666718917528233…, both algebraic of degree 716. All extremal systems again form an explicit two-parameter affine family. The proofs combine three ingredients: the Kilgore–de Boor–Pinkus characterisation of the optimal nodes by equioscillation; elimination by resultants, with exact factorisation and certified real-root isolation; for degree five, a Krawczyk interval certificate that encloses the optimal nodes in a box of width 2·10⁻⁶⁰ and decides which factor carries the optimal system at each step of the elimination. Irreducibility is proved by reduction modulo a prime. The algebra of the Lebesgue functions, the location of the central maximum, and sign certificates for both degree-73 polynomials and the degree-358 polynomial are verified in Lean 4 with Mathlib: 20 theorems, standard axioms only, no sorry. Every step not verified in Lean is a cited theorem, a named textbook fact, or a stated computation with independent cross-checks. Running the method on degree three reproduces the known cubic polynomial for Λ₃*. The ancillary files contain the Lean sources, the polynomials and the scripts.