MI-03: the sharp constant for sums of complex contractions
Recorded by the registry's curators from GitHub; the authors did not submit it here.
George Stepaniants
Complete proof of the canonical odd-summand conjecture, via the stronger exact least admissible constant k/4 for every k≥2 in every positive dimension.
Claims
Files and sources
- Paper
- OpenProblemsInNLA @ e375a6f, MI-03/lean/ ↗
- Lean bundle
- submissions/bundles/openproblemsinnla-mi-03-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:02:03.940259
Declarations audited
| Declaration | Kind | Axioms | Unused hypotheses | Canonical |
|---|---|---|---|---|
| NLA.MI03.odd_contraction_conjecture | theorem · Prop | propext, Classical.choice, Quot.sound | none | matched |
| RegistryProblems.Problem_OP_00098 | definition | propext, Classical.choice, Quot.sound | none | no canonical statement |
NLA.MI03.odd_contraction_conjecture
NLA.MI03.OddContractionConjecture
RegistryProblems.Problem_OP_00098
Prop
Build log
RegistryProblems: built against the registry's copy at 38ca23a44fc2b159a0c944d5c9af39a80eb601c2 rather than the pinned 545a5d18ad3917d52192c41ce172ec4b41945751. Statements are checked by content, not revision. ✔ [3036/3045] Built NLA.MI03.Definitions (6.1s) ✔ [3037/3045] Built NLA.MI03.Modulus (4.0s) ✔ [3038/3045] Built NLA.MI03.Roots (7.8s) ✔ [3039/3045] Built NLA.MI03.UpperBound (8.8s) ✔ [3040/3045] Built NLA.MI03.Witness (4.9s) ✔ [3041/3045] Built NLA.MI03.Sharpness (5.3s) ℹ [3042/3045] Built NLA.MI03.Proof (4.5s) info: NLA/MI03/Proof.lean:52:0: 'NLA.MI03.modulus_semantics_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI03/Proof.lean:54:0: 'NLA.MI03.contraction_modulus_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI03/Proof.lean:56:0: 'NLA.MI03.positive_decomposition_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI03/Proof.lean:58:0: 'NLA.MI03.universal_upper_bound_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI03/Proof.lean:60:0: 'NLA.MI03.root_of_unity_data_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI03/Proof.lean:62:0: 'NLA.MI03.sharpness_witness_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI03/Proof.lean:64:0: 'NLA.MI03.sharp_constant_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI03/Proof.lean:66:0: 'NLA.MI03.odd_contraction_conjecture_proved' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3043/3045] Built Solution (4.1s) info: Solution.lean:74:0: 'NLA.MI03.modulus_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:76:0: 'NLA.MI03.contraction_modulus' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:78:0: 'NLA.MI03.positive_decomposition' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:80:0: 'NLA.MI03.universal_upper_bound' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:82:0: 'NLA.MI03.root_of_unity_data' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:84:0: 'NLA.MI03.sharpness_witness' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:86:0: 'NLA.MI03.sharp_constant' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:88:0: 'NLA.MI03.odd_contraction_conjecture' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [3044/3045] Built RegistryRecord (4.0s) Build completed successfully (3045 jobs).