TR-15: odd-order Hankel H-eigenvalue inheritance counterexample
Recorded by the registry's curators from GitHub; the authors did not submit it here.
George Stepaniants
Formalizes the full negative answer to the canonical inheritance conjecture with actual ordered tensor contractions, real nonzero H-eigenpairs, universal lower positivity, an explicit upper negative pair and unconditional lower-pair existence from the intermediate value theorem.
Claims
Files and sources
- Paper
- OpenProblemsInNLA @ e375a6f, TR-15/lean/ ↗
- Lean bundle
- submissions/bundles/openproblemsinnla-tr-15-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:01:24.058327
Declarations audited
| Declaration | Kind | Axioms | Unused hypotheses | Canonical |
|---|---|---|---|---|
| NLA.TR15.not_inheritanceConjecture | theorem · Prop | propext, Classical.choice, Quot.sound | none | matched |
| RegistryProblems.Problem_OP_00124 | definition | propext, Classical.choice, Quot.sound | none | no canonical statement |
NLA.TR15.not_inheritanceConjecture
Not NLA.TR15.InheritanceConjecture
RegistryProblems.Problem_OP_00124
Prop
Build log
RegistryProblems: built against the registry's copy at 38ca23a44fc2b159a0c944d5c9af39a80eb601c2 rather than the pinned 545a5d18ad3917d52192c41ce172ec4b41945751. Statements are checked by content, not revision. ✔ [2521/2564] Built NLA.TR15.Definitions (5.5s) ℹ [2919/2922] Built NLA.TR15.Proof (8.1s) info: NLA/TR15/Proof.lean:171:0: 'NLA.TR15.lower_contractions_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/TR15/Proof.lean:172:0: 'NLA.TR15.upper_contraction_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/TR15/Proof.lean:173:0: 'NLA.TR15.lower_eigenvalues_pos_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/TR15/Proof.lean:174:0: 'NLA.TR15.lower_eigenpair_exists_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/TR15/Proof.lean:175:0: 'NLA.TR15.negative_eigenvalue_certificate' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/TR15/Proof.lean:176:0: 'NLA.TR15.upper_negative_eigenpair_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/TR15/Proof.lean:177:0: 'NLA.TR15.counterexample_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/TR15/Proof.lean:178:0: 'NLA.TR15.not_inheritanceConjecture_proved' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [2920/2922] Built Solution (3.8s) info: Solution.lean:61:0: 'NLA.TR15.lower_contractions' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:62:0: 'NLA.TR15.upper_contraction' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:63:0: 'NLA.TR15.lower_eigenvalues_pos' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:64:0: 'NLA.TR15.lower_eigenpair_exists' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:65:0: 'NLA.TR15.upper_negative_eigenpair' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:66:0: 'NLA.TR15.counterexample' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:67:0: 'NLA.TR15.not_inheritanceConjecture' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [2921/2922] Built RegistryRecord (3.8s) Build completed successfully (2922 jobs).