MI-06: a counterexample to arithmetic symmetric-modulus domination
Recorded by the registry's curators from GitHub; the authors did not submit it here.
George Stepaniants
Proves the genuine CFC square-root modulus identities, an exact rational three-dimensional witness, a nonzero common orthogonal vector for arbitrary complex constraints, all-unitary quadratic bounds, and the full negation of the original universal factor-sqrt(2) PSD domination conjecture.
Claims
Files and sources
- Paper
- OpenProblemsInNLA @ e375a6f, MI-06/lean/ ↗
- Lean bundle
- submissions/bundles/openproblemsinnla-mi-06-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:41.470154
Declarations audited
| Declaration | Kind | Axioms | Unused hypotheses | Canonical |
|---|---|---|---|---|
| NLA.MI06.not_dominationConjecture | theorem · Prop | propext, Classical.choice, Quot.sound | none | matched |
| RegistryProblems.Problem_OP_00100 | definition | propext, Classical.choice, Quot.sound | none | no canonical statement |
NLA.MI06.not_dominationConjecture
Not NLA.MI06.DominationConjecture
RegistryProblems.Problem_OP_00100
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.MI06.Definitions (6.8s) ℹ [3148/3151] Built NLA.MI06.Proof (19s) info: NLA/MI06/Proof.lean:435:0: 'NLA.MI06.modulus_eq_sqrt_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI06/Proof.lean:436:0: '_private.NLA.MI06.Proof.0.NLA.MI06.modulus_of_positive_square' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI06/Proof.lean:437:0: '_private.NLA.MI06.Proof.0.NLA.MI06.rankOne_posSemidef' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI06/Proof.lean:438:0: '_private.NLA.MI06.Proof.0.NLA.MI06.diagonal_table_posSemidef' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI06/Proof.lean:439:0: '_private.NLA.MI06.Proof.0.NLA.MI06.rightModulusA_posSemidef' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI06/Proof.lean:440:0: '_private.NLA.MI06.Proof.0.NLA.MI06.axialModulus_posSemidef' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI06/Proof.lean:441:0: '_private.NLA.MI06.Proof.0.NLA.MI06.leftModulusB_posSemidef' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI06/Proof.lean:442:0: '_private.NLA.MI06.Proof.0.NLA.MI06.rightModulusSum_posSemidef' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI06/Proof.lean:443:0: '_private.NLA.MI06.Proof.0.NLA.MI06.leftModulusSum_posSemidef' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI06/Proof.lean:444:0: '_private.NLA.MI06.Proof.0.NLA.MI06.missingA_posSemidef' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI06/Proof.lean:445:0: '_private.NLA.MI06.Proof.0.NLA.MI06.missingB_posSemidef' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI06/Proof.lean:446:0: '_private.NLA.MI06.Proof.0.NLA.MI06.modulus_witnessA' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI06/Proof.lean:447:0: '_private.NLA.MI06.Proof.0.NLA.MI06.modulus_witnessA_adjoint' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI06/Proof.lean:448:0: '_private.NLA.MI06.Proof.0.NLA.MI06.modulus_witnessB' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI06/Proof.lean:449:0: '_private.NLA.MI06.Proof.0.NLA.MI06.modulus_witnessB_adjoint' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI06/Proof.lean:450:0: '_private.NLA.MI06.Proof.0.NLA.MI06.modulus_sum' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI06/Proof.lean:451:0: '_private.NLA.MI06.Proof.0.NLA.MI06.modulus_sum_adjoint' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI06/Proof.lean:452:0: '_private.NLA.MI06.Proof.0.NLA.MI06.symmetricModulus_A' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI06/Proof.lean:453:0: '_private.NLA.MI06.Proof.0.NLA.MI06.symmetricModulus_B' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI06/Proof.lean:454:0: '_private.NLA.MI06.Proof.0.NLA.MI06.symmetricModulus_sum' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI06/Proof.lean:455:0: '_private.NLA.MI06.Proof.0.NLA.MI06.symmetricA_decomposition' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI06/Proof.lean:456:0: '_private.NLA.MI06.Proof.0.NLA.MI06.symmetricB_decomposition' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI06/Proof.lean:457:0: 'NLA.MI06.witness_moduli_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI06/Proof.lean:458:0: '_private.NLA.MI06.Proof.0.NLA.MI06.squaredLength_pos' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI06/Proof.lean:459:0: 'NLA.MI06.two_vector_orthogonal_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI06/Proof.lean:460:0: '_private.NLA.MI06.Proof.0.NLA.MI06.quadraticForm_add' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI06/Proof.lean:461:0: '_private.NLA.MI06.Proof.0.NLA.MI06.quadraticForm_sub' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI06/Proof.lean:462:0: '_private.NLA.MI06.Proof.0.NLA.MI06.quadraticForm_smul' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI06/Proof.lean:463:0: '_private.NLA.MI06.Proof.0.NLA.MI06.quadraticForm_one' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI06/Proof.lean:464:0: '_private.NLA.MI06.Proof.0.NLA.MI06.quadraticForm_rankOne_zero' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI06/Proof.lean:465:0: '_private.NLA.MI06.Proof.0.NLA.MI06.quadraticForm_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI06/Proof.lean:466:0: '_private.NLA.MI06.Proof.0.NLA.MI06.quadraticForm_mono' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI06/Proof.lean:467:0: '_private.NLA.MI06.Proof.0.NLA.MI06.unitaryConjugate_add' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI06/Proof.lean:468:0: '_private.NLA.MI06.Proof.0.NLA.MI06.unitaryConjugate_sub' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI06/Proof.lean:469:0: '_private.NLA.MI06.Proof.0.NLA.MI06.unitaryConjugate_smul' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI06/Proof.lean:470:0: '_private.NLA.MI06.Proof.0.NLA.MI06.unitaryConjugate_one' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI06/Proof.lean:471:0: '_private.NLA.MI06.Proof.0.NLA.MI06.unitaryConjugate_rankOne' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI06/Proof.lean:472:0: '_private.NLA.MI06.Proof.0.NLA.MI06.unitaryConjugate_posSemidef' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI06/Proof.lean:473:0: '_private.NLA.MI06.Proof.0.NLA.MI06.upper_bound_of_decomposition' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI06/Proof.lean:474:0: '_private.NLA.MI06.Proof.0.NLA.MI06.symmetricSum_lower_bound' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI06/Proof.lean:475:0: 'NLA.MI06.witness_quadratic_bounds_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI06/Proof.lean:476:0: '_private.NLA.MI06.Proof.0.NLA.MI06.scalar_squared_gap' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI06/Proof.lean:477:0: '_private.NLA.MI06.Proof.0.NLA.MI06.sqrt_two_lt_three_halves' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI06/Proof.lean:478:0: '_private.NLA.MI06.Proof.0.NLA.MI06.scalar_coefficient_gap' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI06/Proof.lean:479:0: 'NLA.MI06.counterexample_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI06/Proof.lean:480:0: 'NLA.MI06.not_dominationConjecture_proved' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3149/3151] Built Solution (4.1s) info: Solution.lean:81:0: 'NLA.MI06.modulus_eq_sqrt' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:82:0: 'NLA.MI06.witness_moduli' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:83:0: 'NLA.MI06.two_vector_orthogonal' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:84:0: 'NLA.MI06.witness_quadratic_bounds' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:85:0: 'NLA.MI06.counterexample' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:86:0: 'NLA.MI06.not_dominationConjecture' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [3150/3151] Built RegistryRecord (4.1s) Build completed successfully (3151 jobs).