SP-15: failure of a finite unitary-class bound for complete shifted singular values
Recorded by the registry's curators from GitHub; the authors did not submit it here.
George Stepaniants
The original finite-unitary-class assertion is false: for every M there are M+1 complex 9-by-9 matrices with every ordered singular value equal for every complex shift, and no unitarily similar pair.
Claims
Files and sources
- Paper
- OpenProblemsInNLA @ e375a6f, SP-15/lean/ ↗
- Lean bundle
- submissions/bundles/openproblemsinnla-sp-15-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:05:29.668885
Declarations audited
| Declaration | Kind | Axioms | Unused hypotheses | Canonical |
|---|---|---|---|---|
| NLA.SP15.canonical_finiteness_false | theorem · Prop | propext, Classical.choice, Quot.sound | none | matched |
| RegistryProblems.Problem_OP_00122 | definition | propext, Classical.choice, Quot.sound | none | no canonical statement |
NLA.SP15.canonical_finiteness_false
Not NLA.SP15.CanonicalFiniteness
RegistryProblems.Problem_OP_00122
Prop
Build log
o: NLA/SP15/JacobianCertificate.lean:66:0: 'NLA.SP15.jacobian_minor_nonsingular' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3762/3782] Built NLA.SP15.DerivativeRows.Row0 (10s) info: NLA/SP15/DerivativeRows/Row0.lean:53:0: 'NLA.SP15.coefficient_strict_derivative_row_0' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3763/3782] Built NLA.SP15.SquareRoots (9.9s) info: NLA/SP15/SquareRoots.lean:46:0: 'NLA.SP15.square_root_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3764/3782] Built NLA.SP15.CoefficientDerivative (9.1s) info: NLA/SP15/CoefficientDerivative.lean:40:0: 'NLA.SP15.coefficient_strict_derivative' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3765/3782] Built NLA.SP15.KernelFlag (9.8s) info: NLA/SP15/KernelFlag.lean:83:0: 'NLA.SP15.constructed_kernel_flag' depends on axioms: [propext, Classical.choice, Quot.sound] ⚠ [3766/3782] Built NLA.SP15.UnitaryBlocks (11s) warning: NLA/SP15/UnitaryBlocks.lean:23:29: Variable name `hy` is not explicitly referenced. Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning: [apply] _hy Note: This linter can be disabled with `set_option linter.unusedVariables false` info: NLA/SP15/UnitaryBlocks.lean:106:0: 'NLA.SP15.unitary_intertwiner_blocks' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3767/3782] Built NLA.SP15.SchurPositivity (9.1s) info: NLA/SP15/SchurPositivity.lean:31:0: 'NLA.SP15.schur_positive_blocks' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3768/3782] Built NLA.SP15.BlockGram (10s) info: NLA/SP15/BlockGram.lean:74:0: 'NLA.SP15.regularized_gram_blocks' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3769/3782] Built NLA.SP15.AugmentedDerivative (9.1s) info: NLA/SP15/AugmentedDerivative.lean:66:0: 'NLA.SP15.augmented_strict_derivative' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3770/3782] Built NLA.SP15.MiddleConjugacy (8.7s) info: NLA/SP15/MiddleConjugacy.lean:60:0: 'NLA.SP15.middle_block_conjugacy' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3771/3782] Built NLA.SP15.SchurAlgebra (9.9s) info: NLA/SP15/SchurAlgebra.lean:80:0: 'NLA.SP15.determinant_lower_commuting' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/SP15/SchurAlgebra.lean:82:0: 'NLA.SP15.final_schur_matrix' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3772/3782] Built NLA.SP15.AugmentedEquivalence (9.5s) info: NLA/SP15/AugmentedEquivalence.lean:59:0: 'NLA.SP15.augmented_derivative_equivalence' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3773/3782] Built NLA.SP15.UnitaryInjectivity (10s) info: NLA/SP15/UnitaryInjectivity.lean:22:0: 'NLA.SP15.constructed_unitary_injectivity' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3774/3782] Built NLA.SP15.ShiftedDeterminant (10s) info: NLA/SP15/ShiftedDeterminant.lean:112:0: 'NLA.SP15.shifted_gram_determinant' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3775/3782] Built NLA.SP15.LocalFiber (8.0s) info: NLA/SP15/LocalFiber.lean:80:0: 'NLA.SP15.local_augmented_inverse' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/SP15/LocalFiber.lean:82:0: 'NLA.SP15.local_coefficient_fiber' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3776/3782] Built NLA.SP15.GramPolynomial (8.8s) info: NLA/SP15/GramPolynomial.lean:57:0: 'NLA.SP15.equal_coefficients_gram_charpoly' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3777/3782] Built NLA.SP15.FiniteFiber (9.2s) info: NLA/SP15/FiniteFiber.lean:53:0: 'NLA.SP15.finite_fiber_selection' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3778/3782] Built NLA.SP15.ShiftedSpectrum (8.9s) info: NLA/SP15/ShiftedSpectrum.lean:26:0: 'NLA.SP15.equal_coefficients_shifted_singular_values' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3779/3782] Built NLA.SP15.Counterfamilies (4.3s) info: NLA/SP15/Counterfamilies.lean:41:0: 'NLA.SP15.arbitrary_finite_counterfamilies' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/SP15/Counterfamilies.lean:43:0: 'NLA.SP15.canonical_finiteness_false' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3780/3782] Built Solution (4.1s) info: Solution.lean:19:0: 'NLA.SP15.box_scalar_certificate' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:21:0: 'NLA.SP15.parameter_box_geometry' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:23:0: 'NLA.SP15.parameter_box_bounds' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:25:0: 'NLA.SP15.p_intervals_separate' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:27:0: 'NLA.SP15.parameter_matrices_positive' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:29:0: 'NLA.SP15.square_root_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:31:0: 'NLA.SP15.coefficient_determinant_identity' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:33:0: 'NLA.SP15.coefficient_base_value' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:35:0: 'NLA.SP15.coefficient_strict_derivative' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:37:0: 'NLA.SP15.jacobian_lu_certificate' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:39:0: 'NLA.SP15.jacobian_minor_nonsingular' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:41:0: 'NLA.SP15.augmented_strict_derivative' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:43:0: 'NLA.SP15.augmented_derivative_equivalence' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:45:0: 'NLA.SP15.local_augmented_inverse' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:47:0: 'NLA.SP15.local_coefficient_fiber' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:49:0: 'NLA.SP15.regularized_gram_blocks' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:51:0: 'NLA.SP15.schur_positive_blocks' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:53:0: 'NLA.SP15.shifted_gram_determinant' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:55:0: 'NLA.SP15.equal_coefficients_gram_charpoly' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:57:0: 'NLA.SP15.gram_charpoly_singular_values' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:59:0: 'NLA.SP15.equal_coefficients_shifted_singular_values' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:61:0: 'NLA.SP15.constructed_kernel_flag' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:63:0: 'NLA.SP15.unitary_intertwiner_blocks' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:65:0: 'NLA.SP15.middle_block_conjugacy' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:67:0: 'NLA.SP15.parameter_slice_rigidity' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:69:0: 'NLA.SP15.constructed_unitary_injectivity' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:71:0: 'NLA.SP15.finite_fiber_selection' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:73:0: 'NLA.SP15.arbitrary_finite_counterfamilies' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:75:0: 'NLA.SP15.canonical_finiteness_false' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [3781/3782] Built RegistryRecord (4.4s) Build completed successfully (3782 jobs).