MI-07: a counterexample to the triangle conjecture for the maximal symmetric modulus
Recorded by the registry's curators from GitHub; the authors did not submit it here.
George Stepaniants
Proves genuine complex matrix moduli, positive-integer CFC root-sequence limits at all witness matrices, the true spectral-norm topology bridge, an all-unitary trace obstruction, and the full original constant-one conjecture negation.
Claims
Files and sources
- Paper
- OpenProblemsInNLA @ e375a6f, MI-07/lean/ ↗
- Lean bundle
- submissions/bundles/openproblemsinnla-mi-07-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:34.152220
Declarations audited
| Declaration | Kind | Axioms | Unused hypotheses | Canonical |
|---|---|---|---|---|
| NLA.MI07.not_triangleConjecture | theorem · Prop | propext, Classical.choice, Quot.sound | none | matched |
| RegistryProblems.Problem_OP_00101 | definition | propext, Classical.choice, Quot.sound | none | no canonical statement |
NLA.MI07.not_triangleConjecture
Not NLA.MI07.TriangleConjecture
RegistryProblems.Problem_OP_00101
Prop
Build log
RegistryProblems: built against the registry's copy at 38ca23a44fc2b159a0c944d5c9af39a80eb601c2 rather than the pinned 545a5d18ad3917d52192c41ce172ec4b41945751. Statements are checked by content, not revision. ✔ [3148/3153] Built NLA.MI07.Definitions (6.4s) ✔ [3149/3153] Built NLA.MI07.FunctionalCalculus (3.7s) ℹ [3150/3153] Built NLA.MI07.Proof (9.0s) info: NLA/MI07/Proof.lean:325:0: 'NLA.MI07.modulus_eq_sqrt_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI07/Proof.lean:326:0: 'NLA.MI07.maximalModulus_eq_of_tendsto_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI07/Proof.lean:327:0: 'NLA.MI07.root_limit_iff_spectralNorm_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI07/Proof.lean:328:0: 'NLA.MI07.witness_moduli_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI07/Proof.lean:329:0: 'NLA.MI07.rpow_projection' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI07/Proof.lean:330:0: 'NLA.MI07.rpow_real_smul' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI07/Proof.lean:331:0: 'NLA.MI07.posDef_rpow_tendsto_one' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI07/Proof.lean:332:0: 'NLA.MI07.rootSequence_witnessA' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI07/Proof.lean:333:0: 'NLA.MI07.rootSequence_witnessB' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI07/Proof.lean:334:0: 'NLA.MI07.rootSequence_sum' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI07/Proof.lean:335:0: 'NLA.MI07.witness_root_limits_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI07/Proof.lean:336:0: 'NLA.MI07.trace_unitaryConjugate' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI07/Proof.lean:337:0: 'NLA.MI07.scalar_gap_positive' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI07/Proof.lean:338:0: 'NLA.MI07.no_unitary_domination' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI07/Proof.lean:339:0: 'NLA.MI07.counterexample_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI07/Proof.lean:340:0: 'NLA.MI07.not_triangleConjecture_proved' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3151/3153] Built Solution (4.1s) info: Solution.lean:91:0: 'NLA.MI07.modulus_eq_sqrt' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:92:0: 'NLA.MI07.maximalModulus_eq_of_tendsto' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:93:0: 'NLA.MI07.root_limit_iff_spectralNorm' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:94:0: 'NLA.MI07.witness_moduli' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:95:0: 'NLA.MI07.witness_root_limits' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:96:0: 'NLA.MI07.counterexample' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:97:0: 'NLA.MI07.not_triangleConjecture' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [3152/3153] Built RegistryRecord (4.2s) Build completed successfully (3153 jobs).