IE-02: attained worst-case and ideal GMRES equality for every complex Jordan block
Recorded by the registry's curators from GitHub; the authors did not submit it here.
George Stepaniants
For every complex Jordan block in the original IE-02 range, ideal GMRES equals worst-case GMRES. All polynomial minima, sphere suprema and their attaining witnesses use the actual Euclidean matrix and vector norms.
Claims
Files and sources
- Paper
- OpenProblemsInNLA @ e375a6f, IE-02/lean/ ↗
- Lean bundle
- submissions/bundles/openproblemsinnla-ie-02-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:06:22.767778
Warnings
These never block publication — unused hypotheses have routine false positives — but they are the best mechanical signal of a mis-transcribed statement, so they are shown rather than hidden.
-
unused_hypothesis — The proof never uses: hlam, hk, hkn. This is often legitimate, but an unused hypothesis in a headline theorem is the commonest sign of a mis-transcribed statement.
NLA.IE02.canonical_jordan_minimax
Declarations audited
| Declaration | Kind | Axioms | Unused hypotheses | Canonical |
|---|---|---|---|---|
| NLA.IE02.canonical_jordan_minimax | theorem · Prop | propext, Classical.choice, Quot.sound | hlam, hk, hkn | matched |
| RegistryProblems.Problem_OP_00077 | definition | propext, Classical.choice, Quot.sound | none | no canonical statement |
NLA.IE02.canonical_jordan_minimax
∀ (n k : Nat) (lam : Complex), instLENat.le 2 n → Ne lam 0 → instLENat.le 1 k → instLTNat.lt k n → And (Eq (NLA.IE02.worstGMRES (NLA.IE02.jordan n lam) k) (NLA.IE02.idealGMRES (NLA.IE02.jordan n lam) k)) (And (∀ (x : NLA.IE02.H n), Set.instMembership.mem (NLA.IE02.unitSphere n) x → Exists fun p => And (NLA.IE02.Admissible k p) (And (Eq ((PiLp.instNorm 2 fun x => Complex).norm (LinearMap.instFunLike.coe (NLA.IE02.euclideanLin (NLA.IE02.polyEval p (NLA.IE02.jordan n lam))) x)) (NLA.IE02.gmresInner (NLA.IE02.jordan n lam) k x)) (∀ (q : NLA.IE02.Poly), NLA.IE02.Admissible k q → Real.instLE.le ((PiLp.instNorm 2 fun x => Complex).norm (LinearMap.instFunLike.coe (NLA.IE02.euclideanLin (NLA.IE02.polyEval p (NLA.IE02.jordan n lam))) x)) ((PiLp.instNorm 2 fun x => Complex).norm (LinearMap.instFunLike.coe (NLA.IE02.euclideanLin (NLA.IE02.polyEval q (NLA.IE02.jordan n lam))) x))))) (Exists fun p => Exists fun x => And (NLA.IE02.Admissible k p) (And (Set.instMembership.mem (NLA.IE02.unitSphere n) x) (And (Eq (NLA.IE02.operatorNorm (NLA.IE02.polyEval p (NLA.IE02.jordan n lam))) (NLA.IE02.idealGMRES (NLA.IE02.jordan n lam) k)) (And (Eq ((PiLp.instNorm 2 fun x => Complex).norm (LinearMap.instFunLike.coe (NLA.IE02.euclideanLin (NLA.IE02.polyEval p (NLA.IE02.jordan n lam))) x)) (NLA.IE02.operatorNorm (NLA.IE02.polyEval p (NLA.IE02.jordan n lam)))) (And (Eq (NLA.IE02.gmresInner (NLA.IE02.jordan n lam) k x) (NLA.IE02.worstGMRES (NLA.IE02.jordan n lam) k)) (And (∀ (q : NLA.IE02.Poly), NLA.IE02.Admissible k q → Real.instLE.le (NLA.IE02.operatorNorm (NLA.IE02.polyEval p (NLA.IE02.jordan n lam))) (NLA.IE02.operatorNorm (NLA.IE02.polyEval q (NLA.IE02.jordan n lam)))) (And (∀ (q : NLA.IE02.Poly), NLA.IE02.Admissible k q → Real.instLE.le ((PiLp.instNorm 2 fun x => Complex).norm (LinearMap.instFunLike.coe (NLA.IE02.euclideanLin (NLA.IE02.polyEval p (NLA.IE02.jordan n lam))) x)) ((PiLp.instNorm 2 fun x => Complex).norm (LinearMap.instFunLike.coe (NLA.IE02.euclideanLin (NLA.IE02.polyEval q (NLA.IE02.jordan n lam))) x))) (∀ (z : NLA.IE02.H n), Set.instMembership.mem (NLA.IE02.unitSphere n) z → Real.instLE.le (NLA.IE02.gmresInner (NLA.IE02.jordan n lam) k z) (NLA.IE02.gmresInner (NLA.IE02.jordan n lam) k x))))))))))
RegistryProblems.Problem_OP_00077
Prop
Build log
y.lean:54:0: 'NLA.IE02.gradient_compact_convex' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3719/3725] Built NLA.IE02.GradientSeparation (4.8s) info: NLA/IE02/GradientSeparation.lean:46:0: 'NLA.IE02.gradient_strict_separation' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3720/3725] Built NLA.IE02.MinimizerOrthogonality (4.6s) info: NLA/IE02/MinimizerOrthogonality.lean:41:0: 'NLA.IE02.minimizer_orthogonality' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3721/3725] Built NLA.IE02.AffineMinimax (5.9s) info: NLA/IE02/AffineMinimax.lean:138:0: 'NLA.IE02.affine_minimax_attained' depends on axioms: [propext, Classical.choice, Quot.sound] ⚠ [3722/3725] Built NLA.IE02.CanonicalJordan (4.5s) warning: NLA/IE02/CanonicalJordan.lean:75:18: Variable name `hlam` 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] _hlam Note: This linter can be disabled with `set_option linter.unusedVariables false` warning: NLA/IE02/CanonicalJordan.lean:75:35: Variable name `hk` 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] _hk Note: This linter can be disabled with `set_option linter.unusedVariables false` warning: NLA/IE02/CanonicalJordan.lean:75:48: Variable name `hkn` 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] _hkn Note: This linter can be disabled with `set_option linter.unusedVariables false` info: NLA/IE02/CanonicalJordan.lean:122:0: 'NLA.IE02.canonical_jordan_minimax' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3723/3725] Built Solution (4.4s) info: Solution.lean:13:0: 'NLA.IE02.coefficient_roundtrip' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:15:0: 'NLA.IE02.coefficient_inner_product' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:17:0: 'NLA.IE02.toeplitz_action' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:19:0: 'NLA.IE02.toeplitz_algebra' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:21:0: 'NLA.IE02.nilpotent_inverse' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:23:0: 'NLA.IE02.euclidean_norm_attainment' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:25:0: 'NLA.IE02.maximal_space_norm' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:27:0: 'NLA.IE02.schur_diagonal_bound' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:29:0: 'NLA.IE02.schur_scalar_endpoint' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:31:0: 'NLA.IE02.schur_dimension_one' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:33:0: 'NLA.IE02.schur_defect_identity' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:35:0: 'NLA.IE02.schur_strict_reduction' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:37:0: 'NLA.IE02.schur_active_block' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:39:0: 'NLA.IE02.schur_pair_step' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:41:0: 'NLA.IE02.finite_schur_boundary' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:43:0: 'NLA.IE02.scaled_maximal_factorization' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:45:0: 'NLA.IE02.reflection_algebra' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:47:0: 'NLA.IE02.reflection_product' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:49:0: 'NLA.IE02.reflection_evaluation' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:51:0: 'NLA.IE02.circle_polynomial_uniqueness' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:53:0: 'NLA.IE02.weighted_fold' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:55:0: 'NLA.IE02.common_circle_root_reduction' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:57:0: 'NLA.IE02.fourier_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:59:0: 'NLA.IE02.effective_factor_polynomial' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:61:0: 'NLA.IE02.reciprocal_root_pairing' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:63:0: 'NLA.IE02.reciprocal_inside_factor' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:65:0: 'NLA.IE02.strict_scalar_factorization' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:67:0: 'NLA.IE02.weighted_scalar_factorization' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:69:0: 'NLA.IE02.weighted_coefficient_preservation' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:71:0: 'NLA.IE02.maximal_complex_preservation' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:73:0: 'NLA.IE02.gradient_compact_convex' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:75:0: 'NLA.IE02.real_separator_complex_form' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:77:0: 'NLA.IE02.gradient_strict_separation' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:79:0: 'NLA.IE02.half_certificate' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:81:0: 'NLA.IE02.descent_step_bounds' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:83:0: 'NLA.IE02.descent_quadratic_expansion' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:85:0: 'NLA.IE02.descent_complement_gap' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:87:0: 'NLA.IE02.descent_empty_complement' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:89:0: 'NLA.IE02.descent_nonempty_complement' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:91:0: 'NLA.IE02.positive_gradient_descent' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:93:0: 'NLA.IE02.minimizer_orthogonality' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:95:0: 'NLA.IE02.affine_operator_minimum' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:97:0: 'NLA.IE02.affine_vector_minimum' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:99:0: 'NLA.IE02.affine_minimax_attained' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:101:0: 'NLA.IE02.jordan_reversal' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:103:0: 'NLA.IE02.jordan_direction_toeplitz' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:105:0: 'NLA.IE02.normalized_polynomial_residuals' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:107:0: 'NLA.IE02.jordan_polynomial_transport' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:109:0: 'NLA.IE02.gmres_extrema_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:111:0: 'NLA.IE02.canonical_jordan_minimax' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [3724/3725] Built RegistryRecord (4.6s) Build completed successfully (3725 jobs).