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

AbstractLet ρ₅ᴿ 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.Version 1.0.2 and supporting materialsThis version archives the revised 88-page manuscript and its 9-page Supplementary Index. The article expands the written canonical-height and complete-X arguments and documents a completed negative-diagonal finite-cover replay: 570 producer tasks passed and their final composition has effective open count zero, conditional on the retained upstream analytic and complete-X inputs. The index maps proof responsibilities S1–S8 to the archived proof objects and verifier entry points. The original v1.0.1 PDFs remain archived at https://doi.org/10.5281/zenodo.22727368.Exact certificates, verifier code and verification guides are available from the GitHub v1.0.2 release at https://github.com/hkjtsgmc79-boop/rho5-proof/releases/tag/v1.0.2. The unchanged large certificate assets remain at their original v1.0.0 locations. The paper revision and certificate asset versions need not coincide.Formalization scopeThe recorded first-phase Lean project cold rebuild passed 634 product modules, three additional example/audit modules and 47 named axiom checks. The B366 second-phase material described in the index is a source-only review snapshot, not a standalone cold-build package. The final sharp Lean equality remains conditional on XGlobalSafety and RootEndpointSafety. Neither a complete unconditional Lean proof nor formal verification of the Python/C++ acceptor implementations is claimed.