MI-22: Lemos–Soares singular-value log-majorization counterexample
Recorded by the registry's curators from GitHub; the authors did not submit it here.
George Stepaniants
Complete negative resolution of the canonical complex positive-definite weighted singular-value log-majorization statement, using an exact rational adaptation and proved genuine CFC, singular-value and Euclidean-norm semantics.
Claims
LEAN VERIFIED
OP-00105 — Lemos–Soares singular-value log-majorization
Files and sources
- Paper
- OpenProblemsInNLA @ e375a6f, MI-22/lean/ ↗
- Lean bundle
- submissions/bundles/openproblemsinnla-mi-22-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:50.909582
Declarations audited
| Declaration | Kind | Axioms | Unused hypotheses | Canonical |
|---|---|---|---|---|
| NLA.MI22.not_weightedLogMajorizationConjecture | theorem · Prop | propext, Classical.choice, Quot.sound | none | matched |
| RegistryProblems.Problem_OP_00105 | definition | propext, Classical.choice, Quot.sound | none | no canonical statement |
NLA.MI22.not_weightedLogMajorizationConjecture
Not NLA.MI22.WeightedLogMajorizationConjecture
RegistryProblems.Problem_OP_00105
Prop
Build log
RegistryProblems: built against the registry's copy at 38ca23a44fc2b159a0c944d5c9af39a80eb601c2 rather than the pinned 545a5d18ad3917d52192c41ce172ec4b41945751. Statements are checked by content, not revision. ✔ [3158/3167] Built NLA.MI22.Definitions (6.5s) ✔ [3159/3167] Built NLA.MI22.FunctionalCalculus (3.5s) ✔ [3160/3167] Built NLA.MI22.Norms (7.0s) ✔ [3161/3167] Built NLA.MI22.Witness (11s) ✔ [3162/3167] Built NLA.MI22.SingularValues (9.2s) ✔ [3163/3167] Built NLA.MI22.ExactData (11s) ℹ [3164/3167] Built NLA.MI22.Proof (4.5s) info: NLA/MI22/Proof.lean:128:0: 'NLA.MI22.singular_values_semantics_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI22/Proof.lean:129:0: 'NLA.MI22.spectral_power_semantics_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI22/Proof.lean:130:0: 'NLA.MI22.euclidean_norm_bounds_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI22/Proof.lean:131:0: 'NLA.MI22.witness_rational_data_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI22/Proof.lean:132:0: 'NLA.MI22.witness_principal_powers_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI22/Proof.lean:133:0: 'NLA.MI22.witness_operator_gap_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI22/Proof.lean:134:0: 'NLA.MI22.numerical_separation' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI22/Proof.lean:135:0: 'NLA.MI22.counterexample_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI22/Proof.lean:136:0: 'NLA.MI22.not_weightedLogMajorizationConjecture_proved' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3165/3167] Built Solution (4.5s) info: Solution.lean:93:0: 'NLA.MI22.singular_values_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:95:0: 'NLA.MI22.spectral_power_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:97:0: 'NLA.MI22.euclidean_norm_bounds' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:99:0: 'NLA.MI22.witness_rational_data' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:101:0: 'NLA.MI22.witness_principal_powers' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:103:0: 'NLA.MI22.witness_operator_gap' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:105:0: 'NLA.MI22.counterexample' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:107:0: 'NLA.MI22.not_weightedLogMajorizationConjecture' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [3166/3167] Built RegistryRecord (4.0s) Build completed successfully (3167 jobs).