clopen.solutions
Submission v1

IE-17: both LSMR backward errors can increase

Recorded by the registry's curators from GitHub; the authors did not submit it here.

George Stepaniants

Complete exact counterexample to both canonical monotonicity claims: attained matrix-only spectral minimum and the literal Moore–Penrose approximation along actual exact LSMR iterates.

Claims

LEAN VERIFIED OP-00081 — Monotonic optimal backward error along LSMR
Disproof · statement matched the canonical formalisation

Files and sources

Paper
OpenProblemsInNLA @ e375a6f, IE-17/lean/ ↗
Lean bundle
submissions/bundles/openproblemsinnla-ie-17-lean.tar.gz
Toolchain
leanprover/lean4:v4.33.1
Posted on GitHub
15 September 2026

Verification PASSED

Attempt
1
Toolchain
leanprover/lean4:v4.33.1
Auditor
v1 · modal
lake build
succeeded
Kernel replay
succeeded
Duration
0:02:16.163682

Declarations audited

DeclarationKindAxiomsUnused hypothesesCanonical
RegistryProblems.Problem_OP_00081 definition propext, Classical.choice, Quot.sound none no canonical statement
RegistryRecord.resolution theorem · Prop propext, Classical.choice, Quot.sound none matched

RegistryProblems.Problem_OP_00081

Prop

RegistryRecord.resolution

Not RegistryProblems.Problem_OP_00081

Build log

RegistryProblems: built against the registry's copy at 38ca23a44fc2b159a0c944d5c9af39a80eb601c2 rather than the pinned 545a5d18ad3917d52192c41ce172ec4b41945751. Statements are checked by content, not revision.
✔ [3643/3655] Built NLA.IE17.Definitions (7.8s)
✔ [3644/3655] Built NLA.IE17.NumericData (11s)
✔ [3645/3655] Built NLA.IE17.Norms (12s)
✔ [3646/3655] Built NLA.IE17.Geometry (8.2s)
✔ [3647/3655] Built NLA.IE17.Certificates (16s)
✔ [3648/3655] Built NLA.IE17.BackwardError (9.3s)
✔ [3649/3655] Built NLA.IE17.LSMR (19s)
ℹ [3650/3655] Built NLA.IE17.Optimal (9.0s)
info: NLA/IE17/Optimal.lean:63:0: 'NLA.IE17.optimal_error_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3651/3655] Built NLA.IE17.Approximation (10s)
info: NLA/IE17/Approximation.lean:166:0: 'NLA.IE17.penrose_projection_unique' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/IE17/Approximation.lean:167:0: 'NLA.IE17.penroseAt_correct' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/IE17/Approximation.lean:168:0: 'NLA.IE17.approximation_error_values' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3652/3655] Built NLA.IE17.Proof (4.5s)
info: NLA/IE17/Proof.lean:115:0: 'NLA.IE17.spectralNorm_semantics' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/IE17/Proof.lean:116:0: 'NLA.IE17.witness_full_column_rank' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/IE17/Proof.lean:117:0: 'NLA.IE17.exact_lsmr_run' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/IE17/Proof.lean:118:0: 'NLA.IE17.optimal_errors' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/IE17/Proof.lean:119:0: 'NLA.IE17.approximation_values' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/IE17/Proof.lean:120:0: 'NLA.IE17.terminal_errors_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/IE17/Proof.lean:121:0: 'NLA.IE17.both_errors_increase' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/IE17/Proof.lean:122:0: 'NLA.IE17.canonical_counterexamples' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3653/3655] Built Solution (4.2s)
✔ [3654/3655] Built RegistryRecord (4.5s)
Build completed successfully (3655 jobs).