MI-13: the complete spectral-middle-factor rectangular commutator inequality
Recorded by the registry's curators from GitHub; the authors did not submit it here.
George Stepaniants
Full complex rectangular MI-13 inequality with coefficient two, actual Euclidean operator and Frobenius norms and the two largest actual singular values. All ranks, both dimension orderings and every m,n at least two are retained.
Claims
Files and sources
- Paper
- OpenProblemsInNLA @ e375a6f, MI-13/lean/ ↗
- Lean bundle
- submissions/bundles/openproblemsinnla-mi-13-lean.tar.gz
- Toolchain
- leanprover/lean4:v4.33.1
- Posted on GitHub
- 17 September 2026
Verification PASSED
- Attempt
- 1
- Toolchain
- leanprover/lean4:v4.33.1
- Auditor
- v1 · modal
- lake build
- succeeded
- Kernel replay
- succeeded
- Duration
- 0:02:54.773285
Declarations audited
| Declaration | Kind | Axioms | Unused hypotheses | Canonical |
|---|---|---|---|---|
| NLA.MI13.canonical_rectangular_bound | theorem · Prop | propext, Classical.choice, Quot.sound | none | matched |
| RegistryProblems.Problem_OP_00102 | definition | propext, Classical.choice, Quot.sound | none | no canonical statement |
NLA.MI13.canonical_rectangular_bound
∀ {m n : Nat}, instLENat.le 2 m → instLENat.le 2 n → ∀ (A C : NLA.MI13.Rect m n) (B : NLA.MI13.Rect n m), Real.instLE.le (instHPow.hPow (NLA.MI13.frobeniusNorm (instHSub.hSub (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul A B) C) (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul C B) A))) 2) (instHMul.hMul (instHMul.hMul (instHMul.hMul 2 (instHPow.hPow (NLA.MI13.spectralNorm B) 2)) (instHAdd.hAdd (instHPow.hPow (NLA.MI13.singularValue A 0) 2) (instHPow.hPow (NLA.MI13.singularValue A 1) 2))) (instHPow.hPow (NLA.MI13.frobeniusNorm C) 2))
RegistryProblems.Problem_OP_00102
Prop
Build log
.lean:76:0: 'NLA.MI13.two_coordinate_bound' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI13/ElementaryBounds.lean:78:0: 'NLA.MI13.off_corner_coefficient_bound' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI13/ElementaryBounds.lean:80:0: 'NLA.MI13.unit_circle_lift' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI13/ElementaryBounds.lean:82:0: 'NLA.MI13.frobenius_average_bound' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3740/3754] Built NLA.MI13.SVD (7.3s) info: NLA/MI13/SVD.lean:61:0: 'NLA.MI13.full_svd' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3741/3754] Built NLA.MI13.NormScaling (7.3s) info: NLA/MI13/NormScaling.lean:27:0: 'NLA.MI13.spectralNorm_smul' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3742/3754] Built NLA.MI13.UnitaryInvariance (8.9s) info: NLA/MI13/UnitaryInvariance.lean:75:0: 'NLA.MI13.unitary_singular_invariance' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI13/UnitaryInvariance.lean:77:0: 'NLA.MI13.unitary_norm_invariance' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3743/3754] Built NLA.MI13.CommutatorMaximum (9.1s) info: NLA/MI13/CommutatorMaximum.lean:80:0: 'NLA.MI13.commutator_spectral_maximum' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3744/3754] Built NLA.MI13.CommutatorEigenspaces (7.8s) info: NLA/MI13/CommutatorEigenspaces.lean:103:0: 'NLA.MI13.positive_eigenvector_pair' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI13/CommutatorEigenspaces.lean:105:0: 'NLA.MI13.eigenspace_functional_kernel' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3745/3754] Built NLA.MI13.TwoUnitaryAverage (7.7s) info: NLA/MI13/TwoUnitaryAverage.lean:85:0: 'NLA.MI13.two_unitary_average' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3746/3754] Built NLA.MI13.Padding (9.3s) info: NLA/MI13/Padding.lean:203:0: 'NLA.MI13.padding_product' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI13/Padding.lean:205:0: 'NLA.MI13.padding_norms' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI13/Padding.lean:207:0: 'NLA.MI13.padding_singular_values' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3747/3754] Built NLA.MI13.CancelledSVD (8.2s) info: NLA/MI13/CancelledSVD.lean:147:0: 'NLA.MI13.svd_corner_functional' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI13/CancelledSVD.lean:149:0: 'NLA.MI13.cancelled_svd_bound' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3748/3754] Built NLA.MI13.Sharpness (8.0s) info: NLA/MI13/Sharpness.lean:57:0: 'NLA.MI13.sharpness_example' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3749/3754] Built NLA.MI13.RefinedCommutator (7.2s) info: NLA/MI13/RefinedCommutator.lean:49:0: 'NLA.MI13.refined_commutator_bound' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3750/3754] Built NLA.MI13.MiddleBounds (5.1s) info: NLA/MI13/MiddleBounds.lean:96:0: 'NLA.MI13.unitary_middle_bound' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI13/MiddleBounds.lean:98:0: 'NLA.MI13.contraction_middle_bound' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI13/MiddleBounds.lean:100:0: 'NLA.MI13.square_middle_bound' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3751/3754] Built NLA.MI13.Complete (4.1s) info: NLA/MI13/Complete.lean:30:0: 'NLA.MI13.canonical_rectangular_bound' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3752/3754] Built Solution (4.0s) info: Solution.lean:18:0: 'NLA.MI13.frobenius_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:20:0: 'NLA.MI13.frobenius_linear_bounds' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:22:0: 'NLA.MI13.operator_norm_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:24:0: 'NLA.MI13.singular_values_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:26:0: 'NLA.MI13.singular_values_gram' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:28:0: 'NLA.MI13.ordered_gram_basis' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:30:0: 'NLA.MI13.positive_image_orthonormal' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:32:0: 'NLA.MI13.zero_singular_image' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:34:0: 'NLA.MI13.positive_image_extension' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:36:0: 'NLA.MI13.full_singular_vector_bases' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:38:0: 'NLA.MI13.full_svd' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:40:0: 'NLA.MI13.unitary_norm_invariance' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:42:0: 'NLA.MI13.unitary_singular_invariance' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:44:0: 'NLA.MI13.hilbert_schmidt_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:46:0: 'NLA.MI13.commutator_adjoint' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:48:0: 'NLA.MI13.commutator_conjugate_symmetry' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:50:0: 'NLA.MI13.commutator_spectral_maximum' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:52:0: 'NLA.MI13.positive_eigenvector_pair' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:54:0: 'NLA.MI13.eigenspace_functional_kernel' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:56:0: 'NLA.MI13.two_coordinate_bound' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:58:0: 'NLA.MI13.off_corner_coefficient_bound' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:60:0: 'NLA.MI13.svd_corner_functional' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:62:0: 'NLA.MI13.cancelled_svd_bound' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:64:0: 'NLA.MI13.refined_commutator_bound' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:66:0: 'NLA.MI13.half_certificate' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:68:0: 'NLA.MI13.unit_circle_lift' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:70:0: 'NLA.MI13.two_unitary_average' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:72:0: 'NLA.MI13.frobenius_average_bound' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:74:0: 'NLA.MI13.unitary_middle_bound' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:76:0: 'NLA.MI13.contraction_middle_bound' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:78:0: 'NLA.MI13.square_middle_bound' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:80:0: 'NLA.MI13.padding_product' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:82:0: 'NLA.MI13.padding_norms' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:84:0: 'NLA.MI13.padding_singular_values' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:86:0: 'NLA.MI13.canonical_rectangular_bound' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:88:0: 'NLA.MI13.sharpness_example' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [3753/3754] Built RegistryRecord (3.9s) Build completed successfully (3754 jobs).