MI-29: a counterexample to the modulus-order determinant comparison
Recorded by the registry's curators from GitHub; the authors did not submit it here.
George Stepaniants
Proves genuine continuous-functional-calculus bridges, positive-real determinant semantics, an admissible exact complex-matrix witness, and the negation of the full original conjecture with arbitrary nonnegative real exponents.
Claims
Files and sources
- Paper
- OpenProblemsInNLA @ e375a6f, MI-29/lean/ ↗
- Lean bundle
- submissions/bundles/openproblemsinnla-mi-29-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:40.355795
Declarations audited
| Declaration | Kind | Axioms | Unused hypotheses | Canonical |
|---|---|---|---|---|
| NLA.MI29.not_modulusDeterminantConjecture | theorem · Prop | propext, Classical.choice, Quot.sound | none | matched |
| RegistryProblems.Problem_OP_00109 | definition | propext, Classical.choice, Quot.sound | none | no canonical statement |
NLA.MI29.not_modulusDeterminantConjecture
Not NLA.MI29.ModulusDeterminantConjecture
RegistryProblems.Problem_OP_00109
Prop
Build log
RegistryProblems: built against the registry's copy at 38ca23a44fc2b159a0c944d5c9af39a80eb601c2 rather than the pinned 545a5d18ad3917d52192c41ce172ec4b41945751. Statements are checked by content, not revision. ✔ [3147/3151] Built NLA.MI29.Definitions (6.3s) ℹ [3148/3151] Built NLA.MI29.Proof (19s) info: NLA/MI29/Proof.lean:277:0: 'NLA.MI29.spectralPower_natCast_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI29/Proof.lean:278:0: 'NLA.MI29.modulus_power_eight_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI29/Proof.lean:279:0: 'NLA.MI29.comparison_positive_real_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI29/Proof.lean:280:0: 'NLA.MI29.scalar_gap_positive' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI29/Proof.lean:281:0: 'NLA.MI29.leftDet_exact' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI29/Proof.lean:282:0: 'NLA.MI29.rightDet_exact' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI29/Proof.lean:283:0: 'NLA.MI29.determinant_gap_exact' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI29/Proof.lean:284:0: 'NLA.MI29.witness_strict_violation' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI29/Proof.lean:285:0: 'NLA.MI29.counterexample_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI29/Proof.lean:286:0: 'NLA.MI29.not_modulusDeterminantConjecture_proved' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3149/3151] Built Solution (4.0s) info: Solution.lean:69:0: 'NLA.MI29.spectralPower_natCast' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:70:0: 'NLA.MI29.modulus_power_eight' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:71:0: 'NLA.MI29.comparison_positive_real' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:72:0: 'NLA.MI29.counterexample' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:73:0: 'NLA.MI29.not_modulusDeterminantConjecture' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [3150/3151] Built RegistryRecord (3.7s) Build completed successfully (3151 jobs).