MI-23: generalized geometric-mean log-majorization counterexample
Recorded by the registry's curators from GitHub; the authors did not submit it here.
George Stepaniants
Formalizes the complete negative answer to the corrected canonical conjecture using complex positive-definite matrices, genuine CFC real powers, full characteristic-root lists and exact log-majorization. Proved spectral and Euclidean norm bridges connect a small exact rational certificate to the original target.
Claims
Files and sources
- Paper
- OpenProblemsInNLA @ e375a6f, MI-23/lean/ ↗
- Lean bundle
- submissions/bundles/openproblemsinnla-mi-23-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:57.509227
Declarations audited
| Declaration | Kind | Axioms | Unused hypotheses | Canonical |
|---|---|---|---|---|
| NLA.MI23.not_generalizedGeometricMeanConjecture | theorem · Prop | propext, Classical.choice, Quot.sound | none | matched |
| RegistryProblems.Problem_OP_00106 | definition | propext, Classical.choice, Quot.sound | none | no canonical statement |
NLA.MI23.not_generalizedGeometricMeanConjecture
Not NLA.MI23.GeneralizedGeometricMeanConjecture
RegistryProblems.Problem_OP_00106
Prop
Build log
pectralNorm (8.6s) ✔ [3150/3156] Built NLA.MI23.Witness (11s) ✔ [3151/3156] Built NLA.MI23.NormBounds (5.3s) ✔ [3152/3156] Built NLA.MI23.Arithmetic (11s) ✔ [3153/3156] Built NLA.MI23.Proof (4.2s) ℹ [3154/3156] Built Solution (4.5s) info: Solution.lean:101:0: 'NLA.MI23.witness_GH_entry' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:103:0: 'NLA.MI23.witness_frobenius_AB' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:105:0: 'NLA.MI23.witness_exact_gap' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:107:0: 'NLA.MI23.scalar_gap_positive' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:109:0: 'NLA.MI23.squaredGap_positive' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:111:0: 'NLA.MI23.witness_strict_norm_gap' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:113:0: 'NLA.MI23.spectralPower_posDef' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:115:0: 'NLA.MI23.sandwich_posDef' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:117:0: 'NLA.MI23.positive_powers_and_means_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:119:0: 'NLA.MI23.ordered_eigenvalues_posDef' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:121:0: 'NLA.MI23.orderedEigenvalues_congr' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:123:0: 'NLA.MI23.positive_eigenvalues_of_charpoly_eq' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:125:0: 'NLA.MI23.spectralPower_add' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:127:0: 'NLA.MI23.spectralPower_nat' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:129:0: 'NLA.MI23.spectralPower_one' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:131:0: 'NLA.MI23.naturalPower_posDef' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:133:0: 'NLA.MI23.product_eigenvalue_semantics_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:135:0: 'NLA.MI23.entry_le_operatorNorm' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:137:0: 'NLA.MI23.operatorNorm_posSemidef_le_trace' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:139:0: 'NLA.MI23.trace_gram_eq_frobeniusSquared' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:141:0: 'NLA.MI23.operatorNorm_sq_le_frobeniusSquared' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:143:0: 'NLA.MI23.operator_norm_bounds_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:145:0: 'NLA.MI23.witness_data_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:147:0: 'NLA.MI23.witness_squared_gap_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:149:0: 'NLA.MI23.witness_largest_strict_gap' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:151:0: 'NLA.MI23.prefix_one_eq_largest' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:153:0: 'NLA.MI23.witness_not_logMajorized' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:155:0: 'NLA.MI23.counterexample_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:157:0: 'NLA.MI23.not_generalizedGeometricMeanConjecture_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:159:0: 'NLA.MI23.orderedEigenvalues_multiset' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:161:0: 'NLA.MI23.largestEigenvalue_spec' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:163:0: 'NLA.MI23.operatorNorm_eq_eigenvalueNorm' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:165:0: 'NLA.MI23.largestEigenvalue_posDef_eq_norm' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:167:0: 'NLA.MI23.squared_product_largest_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:169:0: 'NLA.MI23.witnessD_posDef' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:171:0: 'NLA.MI23.witnessPivots_posDef' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:173:0: 'NLA.MI23.witnessL_det' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:175:0: 'NLA.MI23.witnessL_isUnit' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:177:0: 'NLA.MI23.witnessT_ldl' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:179:0: 'NLA.MI23.witnessT_posDef' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:181:0: 'NLA.MI23.witnessA_posDef' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:183:0: 'NLA.MI23.witnessB_posDef' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:185:0: 'NLA.MI23.witnessG_posDef' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:187:0: 'NLA.MI23.witnessH_posDef' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:189:0: 'NLA.MI23.spectralPower_naturalPower' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:191:0: 'NLA.MI23.witnessA_half' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:193:0: 'NLA.MI23.witnessD_mul_inv' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:195:0: 'NLA.MI23.witnessD_inv_mul' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:197:0: 'NLA.MI23.witnessA_negative_half' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:199:0: 'NLA.MI23.witness_normalized_inner' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:201:0: 'NLA.MI23.witnessT_eighth_root' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:203:0: 'NLA.MI23.witnessT_seven_eighths' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:205:0: 'NLA.MI23.witness_mean_eighth' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:207:0: 'NLA.MI23.witness_mean_seven_eighths' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:209:0: 'NLA.MI23.witness_left_product' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:211:0: 'NLA.MI23.witness_right_product' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:213:0: 'NLA.MI23.positive_powers_and_means' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:215:0: 'NLA.MI23.product_eigenvalue_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:217:0: 'NLA.MI23.squared_product_largest' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:219:0: 'NLA.MI23.operator_norm_bounds' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:221:0: 'NLA.MI23.witness_data' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:223:0: 'NLA.MI23.witness_squared_gap' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:225:0: 'NLA.MI23.counterexample' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:227:0: 'NLA.MI23.not_generalizedGeometricMeanConjecture' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [3155/3156] Built RegistryRecord (4.2s) Build completed successfully (3156 jobs).