IE-18: a counterexample to the four-step Anderson identity
Recorded by the registry's curators from GitHub; the authors did not submit it here.
George Stepaniants
Derives the actual two residual-map executions and the maximum over the genuine Hermitian eigenvalue list, then refutes the complete original universal maximum identity by an admissible strict counterexample.
Claims
Files and sources
- Paper
- OpenProblemsInNLA @ e375a6f, IE-18/lean/ ↗
- Lean bundle
- submissions/bundles/openproblemsinnla-ie-18-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:01:46.708000
Declarations audited
| Declaration | Kind | Axioms | Unused hypotheses | Canonical |
|---|---|---|---|---|
| NLA.IE18.not_fourStepConjecture | theorem · Prop | propext, Classical.choice, Quot.sound | none | matched |
| RegistryProblems.Problem_OP_00082 | definition | propext, Classical.choice, Quot.sound | none | no canonical statement |
NLA.IE18.not_fourStepConjecture
Not NLA.IE18.FourStepConjecture
RegistryProblems.Problem_OP_00082
Prop
Build log
RegistryProblems: built against the registry's copy at 38ca23a44fc2b159a0c944d5c9af39a80eb601c2 rather than the pinned 545a5d18ad3917d52192c41ce172ec4b41945751. Statements are checked by content, not revision. ✔ [3683/3687] Built NLA.IE18.Definitions (7.3s) ℹ [3684/3687] Built NLA.IE18.Proof (8.8s) info: NLA/IE18/Proof.lean:257:0: 'NLA.IE18.strict_scalar_gap' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE18/Proof.lean:259:0: 'NLA.IE18.residual_certificate_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE18/Proof.lean:261:0: 'NLA.IE18.actual_pairMaximum' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE18/Proof.lean:263:0: 'NLA.IE18.counterexample_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IE18/Proof.lean:265:0: 'NLA.IE18.not_fourStepConjecture_proved' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3685/3687] Built Solution (4.3s) info: Solution.lean:44:0: 'NLA.IE18.residual_certificate' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:46:0: 'NLA.IE18.counterexample' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:48:0: 'NLA.IE18.not_fourStepConjecture' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [3686/3687] Built RegistryRecord (4.2s) Build completed successfully (3687 jobs).