clopen.solutions
Submission v1

MI-21: a counterexample to the weighted geometric-mean norm conjecture

Recorded by the registry's curators from GitHub; the authors did not submit it here.

George Stepaniants

Proves admissibility of the genuine Euclidean operator norm, exact CFC geometric-mean identities at positive definite complex matrices, a strict counterexample for every positive outer parameter, and the full original universal conjecture's negation.

Claims

LEAN VERIFIED OP-00104 — Freewan–Hayajneh inequality for sums of weighted geometric means
Disproof · statement matched the canonical formalisation

Files and sources

Paper
OpenProblemsInNLA @ e375a6f, MI-21/lean/ ↗
Lean bundle
submissions/bundles/openproblemsinnla-mi-21-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:33.433089

Declarations audited

DeclarationKindAxiomsUnused hypothesesCanonical
NLA.MI21.not_geometricMeanNormConjecture theorem · Prop propext, Classical.choice, Quot.sound none matched
RegistryProblems.Problem_OP_00104 definition propext, Classical.choice, Quot.sound none no canonical statement

NLA.MI21.not_geometricMeanNormConjecture

Not NLA.MI21.GeometricMeanNormConjecture

RegistryProblems.Problem_OP_00104

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.MI21.Definitions (6.3s)
ℹ [3148/3151] Built NLA.MI21.Proof (12s)
info: NLA/MI21/Proof.lean:376:0: 'NLA.MI21.operatorNorm_isUnitaryInvariant_proved' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/MI21/Proof.lean:377:0: 'NLA.MI21.geometricMean_eq_of_riccati' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/MI21/Proof.lean:378:0: 'NLA.MI21.mean_squared_of_scaled_riccati' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/MI21/Proof.lean:379:0: 'NLA.MI21.witness_left_matrix' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/MI21/Proof.lean:380:0: 'NLA.MI21.real_eigenvalue_le_operatorNorm' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/MI21/Proof.lean:381:0: 'NLA.MI21.witness_eigenvalue_gt_one' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/MI21/Proof.lean:382:0: 'NLA.MI21.counterexample_proved' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/MI21/Proof.lean:383:0: 'NLA.MI21.not_geometricMeanNormConjecture_proved' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3149/3151] Built Solution (3.9s)
info: Solution.lean:50:0: 'NLA.MI21.operatorNorm_isUnitaryInvariant' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:51:0: 'NLA.MI21.counterexample' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:52:0: 'NLA.MI21.not_geometricMeanNormConjecture' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3150/3151] Built RegistryRecord (3.0s)
Build completed successfully (3151 jobs).