IE-05: exact extremizers for partial pivoting on orthogonal matrices
Recorded by the registry's curators from GitHub; the authors did not submit it here.
George Stepaniants
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.
Claims
Files and sources
- Paper
- OpenProblemsInNLA @ e375a6f, IE-05/lean/ ↗
- Lean bundle
- submissions/bundles/openproblemsinnla-ie-05-lean.tar.gz
- Toolchain
- leanprover/lean4:v4.33.1
- Posted on GitHub
- 13 September 2026
Verification PASSED
- Attempt
- 1
- Toolchain
- leanprover/lean4:v4.33.1
- Auditor
- v1 · modal
- lake build
- succeeded
- Kernel replay
- succeeded
- Duration
- 0:02:22.389550
Declarations audited
| Declaration | Kind | Axioms | Unused hypotheses | Canonical |
|---|---|---|---|---|
| NLA.IE05.orthogonalExtremizerConjecture | theorem · Prop | propext, Classical.choice, Quot.sound | none | matched |
| RegistryProblems.Problem_OP_00079 | definition | propext, Classical.choice, Quot.sound | none | no canonical statement |
NLA.IE05.orthogonalExtremizerConjecture
Not NLA.IE05.OrthogonalExtremizerConjecture
RegistryProblems.Problem_OP_00079
Prop
Build log
' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/QR.lean:181:0: 'NLA.IE05._proved.euclideanColumns_normalizedQRQ' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/QR.lean:183:0: 'NLA.IE05._proved.normalizedQRQ_orthogonal' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/QR.lean:185:0: 'NLA.IE05._proved.gramSchmidt_inner_original' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/QR.lean:187:0: 'NLA.IE05._proved.normalizedQRQ_upper' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/QR.lean:189:0: 'NLA.IE05._proved.normalizedQRQ_diagonal_pos' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/QR.lean:191:0: 'NLA.IE05._proved.normalizedQRQ_positiveQR' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/QR.lean:193:0: 'NLA.IE05._proved.prescribedLower_det' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/QR.lean:195:0: 'NLA.IE05._proved.positiveQR_inner' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/QR.lean:197:0: 'NLA.IE05._proved.positiveQR_column' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/QR.lean:199:0: 'NLA.IE05._proved.gramSchmidt_eq_of_positiveQR' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/QR.lean:201:0: 'NLA.IE05._proved.normalizedQRQ_eq_of_positiveQR' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/QR.lean:203:0: 'NLA.IE05._proved.candidate_positiveQR' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3086/3093] Built NLA.IE05.GrowthBounds (7.3s) info: NLA/IE05/GrowthBounds.lean:41:0: 'NLA.IE05._proved.abs_div_sqrt_le' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/GrowthBounds.lean:43:0: 'NLA.IE05._proved.abs_div_sqrt_le_sqrt' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/GrowthBounds.lean:45:0: 'NLA.IE05._proved.entryMax_le_from_entries' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/GrowthBounds.lean:47:0: 'NLA.IE05._proved.growth_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3087/3093] Built NLA.IE05.IntegerQR (6.2s) info: NLA/IE05/IntegerQR.lean:67:0: 'NLA.IE05._proved.normalizedQRQ_of_gram_lu' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3088/3093] Built NLA.IE05.Witness (4.0s) info: NLA/IE05/Witness.lean:149:0: 'NLA.IE05._proved.castIntegerMatrix_mul' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/Witness.lean:151:0: 'NLA.IE05._proved.castIntegerMatrix_tailProduct' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/Witness.lean:153:0: 'NLA.IE05._proved.castIntegerMatrix_lower_bound' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/Witness.lean:155:0: 'NLA.IE05._proved.real_factor_certificates' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/Witness.lean:157:0: 'NLA.IE05._proved.normalizedInteger_orthogonal' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/Witness.lean:159:0: 'NLA.IE05._proved.normalizedInteger_path_trajectory' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/Witness.lean:161:0: 'NLA.IE05._proved.normalizedInteger_trajectory_entry' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/Witness.lean:163:0: 'NLA.IE05._proved.normalizedInteger_firstGrowth' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/Witness.lean:165:0: 'NLA.IE05._proved.integerLower_false_prescribed' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/Witness.lean:167:0: 'NLA.IE05._proved.canonical_integer_identification' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/Witness.lean:169:0: 'NLA.IE05._proved.witness_orthogonal_path' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3089/3093] Built NLA.IE05.Growth (4.8s) info: NLA/IE05/Growth.lean:143:0: 'NLA.IE05._proved.witness_entryMax_upper' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/Growth.lean:145:0: 'NLA.IE05._proved.witness_final_pivot' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/Growth.lean:147:0: 'NLA.IE05._proved.witness_peak_lower' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/Growth.lean:149:0: 'NLA.IE05._proved.witness_growth_lower' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/Growth.lean:151:0: 'NLA.IE05._proved.candidate_entryMax_lower' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/Growth.lean:153:0: 'NLA.IE05._proved.candidate_peak_upper' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/Growth.lean:155:0: 'NLA.IE05._proved.candidate_growth_upper' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/Growth.lean:157:0: 'NLA.IE05._proved.candidate_growth_sq_upper' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/Growth.lean:159:0: 'NLA.IE05._proved.bounded_growth_data' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/Growth.lean:161:0: 'NLA.IE05._proved.witness_strict_growth' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/Growth.lean:163:0: 'NLA.IE05._proved.supremum_strict_gap' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/Growth.lean:165:0: 'NLA.IE05._proved.orthogonalExtremizerConjecture' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3090/3093] Built NLA.IE05.Proof (4.3s) info: NLA/IE05/Proof.lean:142:0: 'NLA.IE05.entryMax_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/Proof.lean:144:0: 'NLA.IE05.schurStep_bound' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/Proof.lean:146:0: 'NLA.IE05.gepp_growth_bound' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/Proof.lean:148:0: 'NLA.IE05.firstPath_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/Proof.lean:150:0: 'NLA.IE05.orthogonalGrowthSet_bounded' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/Proof.lean:152:0: 'NLA.IE05.candidate_positiveQR' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/Proof.lean:154:0: 'NLA.IE05.scaledColumns_orthogonal' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/Proof.lean:156:0: 'NLA.IE05.scaledLU_trajectory' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/Proof.lean:158:0: 'NLA.IE05.integer_factor_certificates' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/Proof.lean:160:0: 'NLA.IE05.integer_entry_certificates' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/Proof.lean:162:0: 'NLA.IE05.canonical_integer_identification' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/Proof.lean:164:0: 'NLA.IE05.witness_orthogonal_path' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/Proof.lean:166:0: 'NLA.IE05.bounded_growth_data' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/Proof.lean:168:0: 'NLA.IE05.numerical_gap_positive' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/Proof.lean:170:0: 'NLA.IE05.witness_strict_growth' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/Proof.lean:172:0: 'NLA.IE05.supremum_strict_gap' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE05/Proof.lean:174:0: 'NLA.IE05.orthogonalExtremizerConjecture' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [3091/3093] Built Solution (4.1s) ✔ [3092/3093] Built RegistryRecord (3.0s) Build completed successfully (3093 jobs).