A Lean formalization of smooth strongly convex interpolation in the real-valued setting

This technical note and reproducible Lean packet formalize the necessary and sufficient finite-data interpolation criterion of Adrien B. Taylor, Julien M. Hendrickx and François Glineur in Prove2Me's real-valued function class. The complete equivalence covers every finite Euclidean dimension and finite index type, including dimension zero and empty data, and every admissible curvature parameter and finite or infinite smoothness parameter. Sufficiency constructs actual conjugate optimizers using coercivity. Necessity proves subgradient existence, differentiability and the sharp quadratic upper estimate before deriving the interpolation inequality. The contribution is a formalization of established mathematics, not a new interpolation theorem. The archive preserves exact accepted source bytes, two platform definition modules, a complete-type and axiom audit, pinned Lean 4.33.1 and transitive Mathlib dependencies, acceptance and byte-comparison evidence, fresh staged-packet reproduction and rejecting integrity/axiom controls. Only propext, Classical.choice and Quot.sound are used. Pinned third-party binary caches remain trusted inputs; this is not bootstrap verification. Separate later curvature, conjugacy and semidefinite-programming platform milestones are not claimed as completed. Original mathematics: Taylor, Hendrickx and Glineur, arXiv:1502.05666v6, Theorem 4. Platform formulations: mikedeng1, with prior statement review by Shuze Chen; the shared subgradient interface cites N. Z. Shor. Lean and Mathlib contributors and an earlier accepted ordinary convex-interpolation component are credited. Alexander Richard Towell directed the work. Substantial OpenAI Codex assistance in formalization, verification, submission and packaging is disclosed. Platform acceptance and automated proof checking are not independent human peer review, endorsement by source authors, or an exhaustive novelty assessment. The proof was submitted and accepted publicly on Prove2Me on 20 October 2026. This archival edition is separately dated 20 October 2026. The owning development repository remains private; the public platform target and this focused packet supply accessible evidence. No legal priority claim is made.