Exact extremizers for partial pivoting on orthogonal matrices
For a nonsingular real matrix $A$ let $\rho_{\mathrm{PP}}(A)$ be the growth factor of Gaussian elimination with partial pivoting in exact arithmetic: the largest entry modulus of the successive active Schur complements $S_1 = A, S_2, \dots, S_n$, divided by that of $A$. Let $L_n$ be the $n \times n$ unit lower triangular matrix whose entries below the diagonal are all $-1$, and let $Q_n$ be the orthogonal factor of its QR factorisation $L_n = Q_n R_n$ in which $R_n$ has positive diagonal. On $Q_n$, a tie in the choice of pivot is broken by taking the first available row; the supremum over the orthogonal group $O(n)$ below is taken over all real orthogonal $Q$ and all admissible pivot choices. Peca-Medlin showed $\rho_{\mathrm{PP}}(Q_n) = 2^{n-1}(1 + o(1))/\sqrt{3}$, and that for $n \ge 3$ the supremum is $c\,2^{n-1}(1 + o(1))$ for a constant $c \in [1/\sqrt{3}, 1)$.
Problem. Is $$\sup_{Q \in O(n)} \rho_{\mathrm{PP}}(Q) = \rho_{\mathrm{PP}}(Q_n)$$ for every $n \ge 2$?
Source: Peca-Medlin (2024), Sec. 3.2 and Appendix B; the tie conventions are OpenProblemsInNLA's.
Imported from github.com/ajt60gaibb/OpenProblemsInNLA.
Classification
- Primary
- NA — Numerical Analysis
- Keywords
- Gaussian elimination, growth factors, OpenProblemsInNLA, orthogonal matrices
References
@article{pecamedlin2024,
author = {Peca-Medlin, John},
title = {Growth factors of orthogonal matrices and local behavior of {G}aussian elimination with partial and complete pivoting},
journal = {SIAM J. Matrix Anal. Appl.},
volume = {45},
number = {3},
year = {2024},
pages = {1599--1620},
doi = {10.1137/23M1597733},
eprint = {2308.16146},
archivePrefix = {arXiv},
}
@misc{openproblemsinnla-ie05,
author = {Townsend, Alex},
title = {{IE-05}: Exact extremizers for partial pivoting on orthogonal matrices},
howpublished = {Open Problems in Numerical Linear Algebra, GitHub repository},
year = {2026},
url = {https://github.com/ajt60gaibb/OpenProblemsInNLA/blob/main/linear-systems-and-elimination/IE-05/README.md},
note = {Read at commit e375a6f, 2026-09-30},
}
Canonical Lean statement
A submission resolves this problem by proving the constant Problem_OP_00079.
namespace RegistryProblems.OP_00079
noncomputable section
open scoped BigOperators NNReal
abbrev Mat (n : ℕ) := Matrix (Fin n) (Fin n) ℝ
abbrev PivotPath (n : ℕ) := Fin n → Fin n
/-- Actual real column orthogonality, with no spectral or pivot assumptions. -/
def Orthogonal {n : ℕ} (A : Mat n) : Prop := A.transpose * A = 1
def prescribedLower (n : ℕ) : Mat n :=
fun i j => if i = j then 1 else if j < i then -1 else 0
/-- These are L2 Euclidean columns, not the coordinatewise supremum norm. -/
def euclideanColumns {n : ℕ} (A : Mat n) : Fin n → EuclideanSpace ℝ (Fin n) :=
fun j => WithLp.toLp 2 (fun i => A i j)
/-- Mathlib's normalized Gram--Schmidt, in the usual increasing `Fin n` order. -/
def normalizedQRQ {n : ℕ} (A : Mat n) : Mat n :=
fun i j => InnerProductSpace.gramSchmidtNormed ℝ (euclideanColumns A) j i
def candidateQ (n : ℕ) : Mat n := normalizedQRQ (prescribedLower n)
/-- Swap the current row positions; no column exchange occurs in partial pivoting. -/
def rowSwap {n : ℕ} (S : Mat n) (k p : Fin n) : Mat n :=
fun i j => S (Equiv.swap k p i) j
/-- The actual Schur update, padded by zero outside the new active trailing block.
Division is total in Lean; `AdmissiblePivot` separately requires a nonzero pivot. -/
def schurStep {n : ℕ} (S : Mat n) (k p : Fin n) : Mat n :=
let B := rowSwap S k p
fun i j => if k < i ∧ k < j then
B i j - (B i k / B k k) * B k j else 0
/-- Stage zero is the input; stages `0,...,n-1` are the active Schur complements. -/
def trajectory {n : ℕ} (A : Mat n) (path : PivotPath n) : ℕ → Mat n
| 0 => A
| k + 1 => if h : k < n then
schurStep (trajectory A path k) ⟨k, h⟩ (path ⟨k, h⟩) else 0
def AdmissiblePivot {n : ℕ} (S : Mat n) (k p : Fin n) : Prop :=
k ≤ p ∧ S p k ≠ 0 ∧ ∀ i, k ≤ i → |S i k| ≤ |S p k|
def AdmissiblePath {n : ℕ} (A : Mat n) (path : PivotPath n) : Prop :=
∀ k, AdmissiblePivot (trajectory A path k.val) k (path k)
/-- A deterministic ascending-row scan. Equal magnitudes never replace the current row. -/
def firstPivotIndex {n : ℕ} (S : Mat n) (k : Fin n) : Fin n :=
(List.finRange n).foldl
(fun p i => if k ≤ i ∧ |S p k| < |S i k| then i else p) k
def firstTrajectory {n : ℕ} (A : Mat n) : ℕ → Mat n
| 0 => A
| k + 1 => if h : k < n then
schurStep (firstTrajectory A k) ⟨k, h⟩
(firstPivotIndex (firstTrajectory A k) ⟨k, h⟩) else 0
def firstPath {n : ℕ} (A : Mat n) : PivotPath n :=
fun k => firstPivotIndex (firstTrajectory A k.val) k
/-- Finite maximum of absolute real entries, implemented as a supremum in `ℝ≥0`. -/
def entryMaxNN {n : ℕ} (A : Mat n) : ℝ≥0 :=
Finset.univ.sup (fun ij : Fin n × Fin n => ‖A ij.1 ij.2‖₊)
def entryMax {n : ℕ} (A : Mat n) : ℝ := entryMaxNN A
def activeMaxNN {n : ℕ} (S : Mat n) (k : ℕ) : ℝ≥0 :=
Finset.univ.sup (fun ij : Fin n × Fin n =>
if k ≤ ij.1.val ∧ k ≤ ij.2.val then ‖S ij.1 ij.2‖₊ else 0)
/-- All and only the `n` active stages enter the growth numerator. -/
def growth {n : ℕ} (A : Mat n) (path : PivotPath n) : ℝ :=
((Finset.univ.sup (fun k : Fin n =>
activeMaxNN (trajectory A path k.val) k.val) : ℝ≥0) : ℝ) / entryMax A
def firstGrowth {n : ℕ} (A : Mat n) : ℝ := growth A (firstPath A)
/-- Every orthogonal input and every admissible partial-pivoting path is included. -/
def orthogonalGrowthSet (n : ℕ) : Set ℝ :=
{r | ∃ A : Mat n, Orthogonal A ∧
∃ path : PivotPath n, AdmissiblePath A path ∧ r = growth A path}
/-- The actual conditionally complete real supremum. No boundedness is assumed here. -/
def orthogonalGrowthSup (n : ℕ) : ℝ := sSup (orthogonalGrowthSet n)
/-- OP-00079: Exact extremizers for partial pivoting on orthogonal matrices -/
def _root_.RegistryProblems.Problem_OP_00079 : Prop :=
∀ n : ℕ, 2 ≤ n → orthogonalGrowthSup n = firstGrowth (candidateQ n)
end
end RegistryProblems.OP_00079
Formalised by George Stepaniants (Apache-2.0); reviewed by clemens-admin.
Available to match against in: Lean v4.33.1 with Mathlib v4.33.1.
Resolving this problem in Lean
Add the problems package as a dependency, import this problem's module, and prove the constant. Any published revision works.
In lakefile.toml:
[[require]] name = "RegistryProblems" git = "https://github.com/cthalhammer/registry-problems" rev = "753bebc58e3fee845f4fffec7d24e7c8cc2a689a"
In your proof:
import RegistryProblems.OP_00079 theorem resolution : RegistryProblems.Problem_OP_00079 := by sorry
In preprint.toml, mapping the claim to the declaration that establishes it:
[[statements]] label = "Theorem 1" lean = "resolution" latex = "..." problem = "OP-00079" claim = "full"
To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:
theorem disproof : ¬ RegistryProblems.Problem_OP_00079 := by sorry
You can also write the statement out in full; the verifier checks it matches up to definitional equality. Partial results and reductions are not matched against this statement.
Resolution claims
Complete negative resolution of the original universal orthogonal GEPP QR-extremizer equality, by an exact order-eight counterexample and a strict gap to the genuine real supremum.
Let $L_8$ be the $8\times8$ unit lower triangular matrix with every entry below the diagonal equal to $-1$, and let $Q_8$ be its orthogonal factor in the QR factorization with positive diagonal in the triangular factor. Changing the $(8,2)$ entry of $L_8$ from $-1$ to $0$ and taking the orthogonal factor of the same QR convention gives an explicit $\widetilde …
Status history
| When | Change | By | Reason |
|---|---|---|---|
| 2026-10-05 | Needs verification → Lean verified | — | Verified here: OpenProblemsInNLA @ e375a6f, IE-05/lean/. |
Citing this problem
This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.
OP-00079, "Exact extremizers for partial pivoting on orthogonal matrices", clopen.solutions.