MI-19: a counterexample to the subset q-permanent inequality
Recorded by the registry's curators from GitHub; the authors did not submit it here.
George Stepaniants
Proves an actual complex Hermitian positive semidefinite Gram witness, evaluates its full and subset-preserving permutation sums, and refutes the complete original universal inequality by an exact strict gap.
Claims
Files and sources
- Paper
- OpenProblemsInNLA @ e375a6f, MI-19/lean/ ↗
- Lean bundle
- submissions/bundles/openproblemsinnla-mi-19-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:28.723787
Declarations audited
| Declaration | Kind | Axioms | Unused hypotheses | Canonical |
|---|---|---|---|---|
| NLA.MI19.not_subsetConjecture | theorem · Prop | propext, Classical.choice, Quot.sound | none | matched |
| RegistryProblems.Problem_OP_00103 | definition | propext, Classical.choice, Quot.sound | none | no canonical statement |
NLA.MI19.not_subsetConjecture
Not NLA.MI19.SubsetConjecture
RegistryProblems.Problem_OP_00103
Prop
Build log
RegistryProblems: built against the registry's copy at 38ca23a44fc2b159a0c944d5c9af39a80eb601c2 rather than the pinned 545a5d18ad3917d52192c41ce172ec4b41945751. Statements are checked by content, not revision. ✔ [3640/3644] Built NLA.MI19.Definitions (7.2s) ℹ [3641/3644] Built NLA.MI19.Proof (10s) info: NLA/MI19/Proof.lean:160:0: 'NLA.MI19.qPermanent_witness' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI19/Proof.lean:162:0: 'NLA.MI19.restrictedQPermanent_witness' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI19/Proof.lean:164:0: 'NLA.MI19.strict_scalar_gap' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI19/Proof.lean:166:0: 'NLA.MI19.counterexample_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI19/Proof.lean:168:0: 'NLA.MI19.not_subsetConjecture_proved' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3642/3644] Built Solution (4.0s) info: Solution.lean:31:0: 'NLA.MI19.counterexample' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:33:0: 'NLA.MI19.not_subsetConjecture' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [3643/3644] Built RegistryRecord (4.3s) Build completed successfully (3644 jobs).