IE-23: nonuniqueness of induced-norm-minimizing right inverses
Recorded by the registry's curators from GitHub; the authors did not submit it here.
George Stepaniants
Complete negative answer to the original direct induced p-to-2 norm uniqueness conjecture, with two distinct global minimizers at the exact admissible p=4 witness.
Claims
Files and sources
- Paper
- OpenProblemsInNLA @ e375a6f, IE-23/lean/ ↗
- Lean bundle
- submissions/bundles/openproblemsinnla-ie-23-lean.tar.gz
- Toolchain
- leanprover/lean4:v4.33.1
- Posted on GitHub
- 22 September 2026
Verification PASSED
- Attempt
- 1
- Toolchain
- leanprover/lean4:v4.33.1
- Auditor
- v1 · modal
- lake build
- succeeded
- Kernel replay
- succeeded
- Duration
- 0:01:42.381402
Declarations audited
| Declaration | Kind | Axioms | Unused hypotheses | Canonical |
|---|---|---|---|---|
| NLA.IE23.not_rightInverseUniqueConjecture | theorem · Prop | propext, Classical.choice, Quot.sound | none | matched |
| RegistryProblems.Problem_OP_00084 | definition | propext, Classical.choice, Quot.sound | none | no canonical statement |
NLA.IE23.not_rightInverseUniqueConjecture
Not NLA.IE23.RightInverseUniqueConjecture
RegistryProblems.Problem_OP_00084
Prop
Build log
RegistryProblems: built against the registry's copy at 38ca23a44fc2b159a0c944d5c9af39a80eb601c2 rather than the pinned 545a5d18ad3917d52192c41ce172ec4b41945751. Statements are checked by content, not revision. ✔ [2389/2398] Built NLA.IE23.Definitions (5.4s) ✔ [2390/2398] Built NLA.IE23.Norms (3.3s) ✔ [2391/2398] Built NLA.IE23.FourthPower (7.7s) ✔ [2392/2398] Built NLA.IE23.Matrices (9.9s) ✔ [2393/2398] Built NLA.IE23.Actions (4.3s) ✔ [2394/2398] Built NLA.IE23.Minimizers (3.6s) ℹ [2395/2398] Built NLA.IE23.Proof (4.2s) info: NLA/IE23/Proof.lean:105:0: 'NLA.IE23.inducedNorm_semantics_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE23/Proof.lean:107:0: 'NLA.IE23.witness_matrix_identities_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE23/Proof.lean:109:0: 'NLA.IE23.fourth_power_norm_control_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE23/Proof.lean:111:0: 'NLA.IE23.witness_action_identities_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE23/Proof.lean:113:0: 'NLA.IE23.witness_attainment_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE23/Proof.lean:115:0: 'NLA.IE23.witness_norms_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE23/Proof.lean:117:0: 'NLA.IE23.witness_global_minimizers_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE23/Proof.lean:119:0: 'NLA.IE23.not_rightInverseUniqueConjecture_proved' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [2396/2398] Built Solution (3.9s) info: Solution.lean:95:0: 'NLA.IE23.inducedNorm_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:97:0: 'NLA.IE23.witness_matrix_identities' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:99:0: 'NLA.IE23.fourth_power_norm_control' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:101:0: 'NLA.IE23.witness_action_identities' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:103:0: 'NLA.IE23.witness_attainment' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:105:0: 'NLA.IE23.witness_norms' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:107:0: 'NLA.IE23.witness_global_minimizers' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:109:0: 'NLA.IE23.not_rightInverseUniqueConjecture' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [2397/2398] Built RegistryRecord (3.5s) Build completed successfully (2398 jobs).