SP-04: generic failure of the smallest-absolute-multiplier rule
Recorded by the registry's curators from GitHub; the authors did not submit it here.
George Stepaniants
Complete original generic selection rule refuted: a nonempty open family of real 3×3 data matrices has invertibility, distinct squared singular values, a finite full stationary set, a unique least-absolute-multiplier pair and a strictly closer feasible matrix in the actual Frobenius norm.
Claims
Files and sources
- Paper
- OpenProblemsInNLA @ e375a6f, SP-04/lean/ ↗
- Lean bundle
- submissions/bundles/openproblemsinnla-sp-04-lean.tar.gz
- Toolchain
- leanprover/lean4:v4.33.1
- Posted on GitHub
- 15 September 2026
Verification PASSED
- Attempt
- 1
- Toolchain
- leanprover/lean4:v4.33.1
- Auditor
- v1 · modal
- lake build
- succeeded
- Kernel replay
- succeeded
- Duration
- 0:03:09.616317
Declarations audited
| Declaration | Kind | Axioms | Unused hypotheses | Canonical |
|---|---|---|---|---|
| NLA.SP04.canonical_counterexample | theorem · Prop | propext, Classical.choice, Quot.sound | none | matched |
| RegistryProblems.Problem_OP_00119 | definition | propext, Classical.choice, Quot.sound | none | no canonical statement |
NLA.SP04.canonical_counterexample
Not NLA.SP04.AllGenericSelectionRules
RegistryProblems.Problem_OP_00119
Prop
Build log
RegistryProblems: built against the registry's copy at 38ca23a44fc2b159a0c944d5c9af39a80eb601c2 rather than the pinned 545a5d18ad3917d52192c41ce172ec4b41945751. Statements are checked by content, not revision. ✔ [3680/3697] Built NLA.SP04.Definitions (7.3s) ✔ [3681/3697] Built NLA.SP04.Generic (6.8s) ✔ [3682/3697] Built NLA.SP04.SpectralIntervals (8.8s) ✔ [3683/3697] Built NLA.SP04.Orthogonal (6.1s) ✔ [3684/3697] Built NLA.SP04.MatrixStationary (7.2s) ✔ [3685/3697] Built NLA.SP04.SVD (6.9s) ⚠ [3686/3697] Built NLA.SP04.Certificates (11s) warning: NLA/SP04/Certificates.lean:19:4: `Set.mem_setOf` has been deprecated: Use `Set.mem_ofPred` instead info: NLA/SP04/Certificates.lean:25:0: 'NLA.SP04.scalar_numerical_bounds' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [3687/3697] Built NLA.SP04.Spectrum (6.0s) ✔ [3688/3697] Built NLA.SP04.ScalarRoots (8.0s) ⚠ [3689/3697] Built NLA.SP04.ScalarPositive (11s) warning: NLA/SP04/ScalarPositive.lean:66:5: Variable name `hc` 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] _hc Note: This linter can be disabled with `set_option linter.unusedVariables false` ⚠ [3690/3697] Built NLA.SP04.Scalar (6.2s) warning: NLA/SP04/Scalar.lean:154:27: try 'simp' instead of 'simpa' Note: This linter can be disabled with `set_option linter.unnecessarySimpa false` info: NLA/SP04/Scalar.lean:201:0: 'NLA.SP04.scalar_least_unique' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/SP04/Scalar.lean:202:0: 'NLA.SP04.selected_parameter_exists' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/SP04/Scalar.lean:203:0: 'NLA.SP04.scalar_distance_improves' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3691/3697] Built NLA.SP04.Diagonal (4.4s) info: NLA/SP04/Diagonal.lean:50:0: 'NLA.SP04.selected_unique_least' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/SP04/Diagonal.lean:51:0: 'NLA.SP04.diagonal_counterexample_full' depends on axioms: [propext, Classical.choice, Quot.sound] ⚠ [3692/3697] Built NLA.SP04.Finiteness (28s) warning: NLA/SP04/Finiteness.lean:109:22: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` info: NLA/SP04/Finiteness.lean:188:0: 'NLA.SP04.stationaryEliminant_at_zero' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/SP04/Finiteness.lean:189:0: 'NLA.SP04.scalar_stationary_eliminant' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/SP04/Finiteness.lean:190:0: 'NLA.SP04.diagonal_stationary_finite' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3693/3697] Built NLA.SP04.Witness (4.7s) info: NLA/SP04/Witness.lean:97:0: 'NLA.SP04.uniqueLeastStationary_orthogonal_iff' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/SP04/Witness.lean:98:0: 'NLA.SP04.stationaryPairs_orthogonal_eq' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/SP04/Witness.lean:99:0: 'NLA.SP04.stationaryPairs_finite_orthogonal_iff' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/SP04/Witness.lean:100:0: 'NLA.SP04.selectionFails_of_admissible_svd' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3694/3697] Built NLA.SP04.Proof (4.4s) info: NLA/SP04/Proof.lean:92:0: 'NLA.SP04.numerical_bounds' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/SP04/Proof.lean:94:0: 'NLA.SP04.diagonal_stationary_iff' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/SP04/Proof.lean:96:0: 'NLA.SP04.diagonal_counterexample' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/SP04/Proof.lean:98:0: 'NLA.SP04.diagonal_finite' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/SP04/Proof.lean:100:0: 'NLA.SP04.orthogonal_transport' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/SP04/Proof.lean:102:0: 'NLA.SP04.spectral_family' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/SP04/Proof.lean:104:0: 'NLA.SP04.regular_svd' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/SP04/Proof.lean:106:0: 'NLA.SP04.open_family_counterexamples' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/SP04/Proof.lean:108:0: 'NLA.SP04.algebraic_avoidance' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/SP04/Proof.lean:110:0: 'NLA.SP04.generic_counterexamples' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/SP04/Proof.lean:112:0: 'NLA.SP04.canonical_counterexample' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [3695/3697] Built Solution (4.4s) ✔ [3696/3697] Built RegistryRecord (4.2s) Build completed successfully (3697 jobs).