The exact maximum growth factor for complete pivoting on real 5 × 5 matrices

Abstract Let ρ₅ᴿ be the largest element growth possible in exact Gaussian elimination with complete pivoting on real 5 × 5 matrices, with every legal choice at a pivot tie allowed. We prove ρ₅ᴿ = α = 4.132517078632472854223346853277…, where α is the algebraic lower bound identified by Chen, Edelman, and Urschel, specified by their degree-61 polynomial and a rational isolating interval. Our contribution is the global upper bound. An exact inverse-elimination representation retains all initial and intermediate entry bounds of the same matrix. A constructive contraction preserves the final-pivot height while reducing the problem to two saturated tail geometries. On the negative-diagonal geometry, three feasible paths eliminate six variables and give an attained fibre maximum over seventeen shared parameters. Rational certificates control the remaining domains, while a constrained algebraic maximum argument and feasible transports resolve regions meeting the sharp value. The proof combines these analytic reductions with exact verification of a finite, complete cover. We provide a partial Lean formalization together with publicly available exact certificates and verification code. Files and supporting materials This record contains the 56-page manuscript and its 7-page supplementary index. Both PDFs are archived unchanged from the fixed GitHub release v1.0.1. The supplementary index maps proof responsibilities S1–S8 to the original proof objects and verifier entry points. Source code, exact certificates, verification guides and file manifests are available at GitHub release v1.0.1. The original certificate assets remain frozen under v1.0.0 and are linked from that release. Formalization scope The recorded first-phase Lean project cold rebuild passed 634 product modules, three additional example/audit modules and 47 named axiom checks, using an explicit dependency-order driver with pinned third-party caches reused and supplemented. The final sharp Lean equality remains conditional on XGlobalSafety and RootEndpointSafety. This is a partial Lean formalization accompanying the computer-assisted proof; neither a complete unconditional Lean proof nor formal verification of the Python/C++ acceptor implementations is claimed. The frozen PDFs retain the publication-status wording at the time of their GitHub release; this Zenodo record supplies their archival deposit.