IS-03: a seven-dimensional derivative-realizability counterexample
Recorded by the registry's curators from GitHub; the authors did not submit it here.
George Stepaniants
Complete negative answer to Johnson's original universal normalized-characteristic-polynomial derivative realizability conjecture, with genuine arbitrary-matrix trace certificates and the unchanged order-seven source witness.
Claims
LEAN VERIFIED
OP-00086 — Johnson's derivative-realizability conjecture
Files and sources
- Paper
- OpenProblemsInNLA @ e375a6f, IS-03/lean/ ↗
- Lean bundle
- submissions/bundles/openproblemsinnla-is-03-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:50.164448
Declarations audited
| Declaration | Kind | Axioms | Unused hypotheses | Canonical |
|---|---|---|---|---|
| NLA.IS03.not_derivativeRealizabilityConjecture | theorem · Prop | propext, Classical.choice, Quot.sound | none | matched |
| RegistryProblems.Problem_OP_00086 | definition | propext, Classical.choice, Quot.sound | none | no canonical statement |
NLA.IS03.not_derivativeRealizabilityConjecture
Not NLA.IS03.DerivativeRealizabilityConjecture
RegistryProblems.Problem_OP_00086
Prop
Build log
RegistryProblems: built against the registry's copy at 38ca23a44fc2b159a0c944d5c9af39a80eb601c2 rather than the pinned 545a5d18ad3917d52192c41ce172ec4b41945751. Statements are checked by content, not revision. ✔ [3096/3105] Built NLA.IS03.Definitions (6.4s) ℹ [3097/3105] Built NLA.IS03.Numerical (9.5s) info: NLA/IS03/Numerical.lean:24:0: 'NLA.IS03.numerical_negative_moment' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [3098/3105] Built NLA.IS03.Algebra (7.2s) ℹ [3099/3105] Built NLA.IS03.Newton (17s) info: NLA/IS03/Newton.lean:136:0: 'NLA.IS03.product_coeff_eq_elementary' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IS03/Newton.lean:137:0: 'NLA.IS03.powerMoments_newton' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IS03/Newton.lean:138:0: 'NLA.IS03.power_sums_of_derivative_product' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [3100/3105] Built NLA.IS03.Spectral (8.1s) ✔ [3101/3105] Built NLA.IS03.Witness (8.4s) ℹ [3102/3105] Built NLA.IS03.Proof (3.8s) info: NLA/IS03/Proof.lean:60:0: 'NLA.IS03.nonnegative_power_trace_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IS03/Proof.lean:61:0: 'NLA.IS03.witness_admissible_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IS03/Proof.lean:62:0: 'NLA.IS03.witness_polynomials_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IS03/Proof.lean:63:0: 'NLA.IS03.trace_moment_certificate_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IS03/Proof.lean:64:0: 'NLA.IS03.negative_moment_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IS03/Proof.lean:65:0: 'NLA.IS03.counterexample_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/IS03/Proof.lean:66:0: 'NLA.IS03.not_derivativeRealizabilityConjecture_proved' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3103/3105] Built Solution (3.7s) info: Solution.lean:64:0: 'NLA.IS03.nonnegative_power_trace' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:65:0: 'NLA.IS03.witness_admissible' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:66:0: 'NLA.IS03.witness_polynomials' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:67:0: 'NLA.IS03.trace_moment_certificate' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:68:0: 'NLA.IS03.negative_moment' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:69:0: 'NLA.IS03.counterexample' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:70:0: 'NLA.IS03.not_derivativeRealizabilityConjecture' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [3104/3105] Built RegistryRecord (3.5s) Build completed successfully (3105 jobs).