IE-19: negative resolution of the sharp inverse norm conjecture
Recorded by the registry's curators from GitHub; the authors did not submit it here.
George Stepaniants
Proves an admissible real symmetric order-three counterexample using actual matrix inverses and the maximum absolute row-sum norm, then refutes the complete original universal conjecture including its equality clause.
Claims
Files and sources
- Paper
- OpenProblemsInNLA @ e375a6f, IE-19/lean/ ↗
- Lean bundle
- submissions/bundles/openproblemsinnla-ie-19-lean.tar.gz
- Toolchain
- leanprover/lean4:v4.33.1
- Posted on GitHub
- 12 September 2026
Verification PASSED
- Attempt
- 1
- Toolchain
- leanprover/lean4:v4.33.1
- Auditor
- v1 · modal
- lake build
- succeeded
- Kernel replay
- succeeded
- Duration
- 0:02:39.818523
Declarations audited
| Declaration | Kind | Axioms | Unused hypotheses | Canonical |
|---|---|---|---|---|
| NLA.IE19.not_sharpConjecture | theorem · Prop | propext, Classical.choice, Quot.sound | none | matched |
| RegistryProblems.Problem_OP_00083 | definition | propext, Classical.choice, Quot.sound | none | no canonical statement |
NLA.IE19.not_sharpConjecture
Not NLA.IE19.SharpConjecture
RegistryProblems.Problem_OP_00083
Prop
Build log
RegistryProblems: built against the registry's copy at 38ca23a44fc2b159a0c944d5c9af39a80eb601c2 rather than the pinned 545a5d18ad3917d52192c41ce172ec4b41945751. Statements are checked by content, not revision. ✔ [3632/3636] Built NLA.IE19.Definitions (10s) ℹ [3633/3636] Built NLA.IE19.Proof (11s) info: NLA/IE19/Proof.lean:128:0: 'NLA.IE19.strict_scalar_gap' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE19/Proof.lean:130:0: 'NLA.IE19.counterexample_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE19/Proof.lean:132:0: 'NLA.IE19.not_lowerBoundConjecture_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE19/Proof.lean:134:0: 'NLA.IE19.not_sharpConjecture_proved' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3634/3636] Built Solution (7.0s) info: Solution.lean:29:0: 'NLA.IE19.counterexample' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:31:0: 'NLA.IE19.not_lowerBoundConjecture' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:33:0: 'NLA.IE19.not_sharpConjecture' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [3635/3636] Built RegistryRecord (7.7s) Build completed successfully (3636 jobs).