MI-26: a counterexample to concave unitary-orbit subadditivity
Recorded by the registry's curators from GitHub; the authors did not submit it here.
George Stepaniants
Proves the original function-class equivalence, genuine finite-spectrum CFC and half-line extension bridges, exact polynomial identities for two rational projections, their positive quadratic-form obstruction, and the full negation of the universal complex PSD unitary-orbit assertion.
Claims
Files and sources
- Paper
- OpenProblemsInNLA @ e375a6f, MI-26/lean/ ↗
- Lean bundle
- submissions/bundles/openproblemsinnla-mi-26-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:29.463687
Declarations audited
| Declaration | Kind | Axioms | Unused hypotheses | Canonical |
|---|---|---|---|---|
| NLA.MI26.not_subadditivityConjecture | theorem · Prop | propext, Classical.choice, Quot.sound | none | matched |
| RegistryProblems.Problem_OP_00107 | definition | propext, Classical.choice, Quot.sound | none | no canonical statement |
NLA.MI26.not_subadditivityConjecture
Not NLA.MI26.SubadditivityConjecture
RegistryProblems.Problem_OP_00107
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.MI26.Definitions (6.2s) ℹ [3148/3151] Built NLA.MI26.Proof (6.4s) info: NLA/MI26/Proof.lean:187:0: 'NLA.MI26.admissibleFunction_iff_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI26/Proof.lean:188:0: 'NLA.MI26.functionalCalculus_eq_spectral_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI26/Proof.lean:189:0: 'NLA.MI26.functionalCalculus_congr_nonneg_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI26/Proof.lean:190:0: 'NLA.MI26.quadratic_cfc_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI26/Proof.lean:191:0: 'NLA.MI26.witness_positive' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI26/Proof.lean:192:0: 'NLA.MI26.witness_data_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI26/Proof.lean:193:0: 'NLA.MI26.counterexample_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI26/Proof.lean:194:0: 'NLA.MI26.not_subadditivityConjecture_proved' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3149/3151] Built Solution (3.0s) info: Solution.lean:86:0: 'NLA.MI26.admissibleFunction_iff' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:87:0: 'NLA.MI26.functionalCalculus_eq_spectral' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:88:0: 'NLA.MI26.functionalCalculus_congr_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:89:0: 'NLA.MI26.quadratic_cfc' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:90:0: 'NLA.MI26.witness_data' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:91:0: 'NLA.MI26.counterexample' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:92:0: 'NLA.MI26.not_subadditivityConjecture' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [3150/3151] Built RegistryRecord (3.9s) Build completed successfully (3151 jobs).