IV-06: four real interval-eigenvalue components in dimension three
Recorded by the registry's curators from GitHub; the authors did not submit it here.
George Stepaniants
Complete negative answer to the original universal at-most-dimension bound for connected components of the real eigenvalue union of an independent-entry interval matrix.
Claims
Files and sources
- Paper
- OpenProblemsInNLA @ e375a6f, IV-06/lean/ ↗
- Lean bundle
- submissions/bundles/openproblemsinnla-iv-06-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:01:37.791684
Declarations audited
| Declaration | Kind | Axioms | Unused hypotheses | Canonical |
|---|---|---|---|---|
| NLA.IV06.not_componentBoundConjecture | theorem · Prop | propext, Classical.choice, Quot.sound | none | matched |
| RegistryProblems.Problem_OP_00088 | definition | propext, Classical.choice, Quot.sound | none | no canonical statement |
NLA.IV06.not_componentBoundConjecture
Not NLA.IV06.ComponentBoundConjecture
RegistryProblems.Problem_OP_00088
Prop
Build log
RegistryProblems: built against the registry's copy at 38ca23a44fc2b159a0c944d5c9af39a80eb601c2 rather than the pinned 545a5d18ad3917d52192c41ce172ec4b41945751. Statements are checked by content, not revision. ✔ [2918/2922] Built NLA.IV06.Definitions (6.3s) ℹ [2919/2922] Built NLA.IV06.Proof (7.9s) info: NLA/IV06/Proof.lean:202:0: 'NLA.IV06.eigenvalue_determinant_semantics_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IV06/Proof.lean:203:0: 'NLA.IV06.family_and_determinant_semantics_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IV06/Proof.lean:204:0: 'NLA.IV06.witness_eigenpairs_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IV06/Proof.lean:205:0: 'NLA.IV06.numerical_separator_margin' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IV06/Proof.lean:206:0: 'NLA.IV06.witness_separators_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IV06/Proof.lean:207:0: 'NLA.IV06.connected_component_intervals_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IV06/Proof.lean:208:0: 'NLA.IV06.four_components_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IV06/Proof.lean:209:0: 'NLA.IV06.counterexample_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IV06/Proof.lean:210:0: 'NLA.IV06.not_componentBoundConjecture_proved' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [2920/2922] Built Solution (3.9s) info: Solution.lean:74:0: 'NLA.IV06.eigenvalue_determinant_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:76:0: 'NLA.IV06.family_and_determinant_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:78:0: 'NLA.IV06.witness_eigenpairs' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:80:0: 'NLA.IV06.witness_separators' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:82:0: 'NLA.IV06.connected_component_intervals' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:84:0: 'NLA.IV06.four_components' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:86:0: 'NLA.IV06.counterexample' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:88:0: 'NLA.IV06.not_componentBoundConjecture' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [2921/2922] Built RegistryRecord (3.7s) Build completed successfully (2922 jobs).