SP-05: a PSD minimizer for the positive definite Jordan–Kronecker product
Recorded by the registry's curators from GitHub; the authors did not submit it here.
George Stepaniants
The complete original symmetric/skew Rayleigh-minimum inequality for every real symmetric positive-definite pair and every n≥2, with actual attained sector minima. The stronger source result gives a real nonzero PSD eigenmatrix at the global Jordan minimum for every n≥1.
Claims
Files and sources
- Paper
- OpenProblemsInNLA @ e375a6f, SP-05/lean/ ↗
- Lean bundle
- submissions/bundles/openproblemsinnla-sp-05-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:02:08.983026
Declarations audited
| Declaration | Kind | Axioms | Unused hypotheses | Canonical |
|---|---|---|---|---|
| NLA.SP05.canonical_result | theorem · Prop | propext, Classical.choice, Quot.sound | none | matched |
| RegistryProblems.Problem_OP_00120 | definition | propext, Classical.choice, Quot.sound | none | no canonical statement |
NLA.SP05.canonical_result
∀ (n : Nat), instLENat.le 2 n → ∀ (A B : NLA.SP05.Mat n), Matrix.PosDef A → Matrix.PosDef B → Exists fun a => Exists fun b => And (IsLeast (NLA.SP05.sectorValues A B 1) a) (And (IsLeast (NLA.SP05.sectorValues A B (-1)) b) (Real.instLE.le a b))
RegistryProblems.Problem_OP_00120
Prop
Build log
RegistryProblems: built against the registry's copy at 38ca23a44fc2b159a0c944d5c9af39a80eb601c2 rather than the pinned 545a5d18ad3917d52192c41ce172ec4b41945751. Statements are checked by content, not revision. ✔ [3728/3742] Built NLA.SP05.Definitions (6.2s) ℹ [3729/3742] Built NLA.SP05.Certificates (10s) info: NLA/SP05/Certificates.lean:17:0: 'NLA.SP05.skew_norm_positive_certificate' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3730/3742] Built NLA.SP05.Complexification (11s) info: NLA/SP05/Complexification.lean:106:0: 'NLA.SP05.complexify_posSemidef' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/SP05/Complexification.lean:107:0: 'NLA.SP05.complexify_posDef' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/SP05/Complexification.lean:108:0: 'NLA.SP05.complexify_inv' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/SP05/Complexification.lean:109:0: 'NLA.SP05.complexify_sqrt' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/SP05/Complexification.lean:110:0: 'NLA.SP05.complexify_abs_I_smul' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [3731/3742] Built NLA.SP05.Basic (8.9s) ℹ [3732/3742] Built NLA.SP05.Sylvester (8.7s) info: NLA/SP05/Sylvester.lean:130:0: 'NLA.SP05.sylvester_posSemidef' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/SP05/Sylvester.lean:131:0: 'NLA.SP05.complex_jordan_injective' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/SP05/Sylvester.lean:132:0: 'NLA.SP05.complex_jordan_preimage_hermitian' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/SP05/Sylvester.lean:133:0: 'NLA.SP05.complex_jordan_solution_posSemidef' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [3733/3742] Built NLA.SP05.Sectors (9.1s) ℹ [3734/3742] Built NLA.SP05.Modulus (10s) info: NLA/SP05/Modulus.lean:147:0: 'NLA.SP05.complexMatrixAction_real' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/SP05/Modulus.lean:148:0: 'NLA.SP05.trace_product_posSemidef_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/SP05/Modulus.lean:149:0: 'NLA.SP05.hermitian_modulus_pairing_le' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/SP05/Modulus.lean:150:0: 'NLA.SP05.modulus_quadratic_improves' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [3735/3742] Built NLA.SP05.Spectral (5.7s) ✔ [3736/3742] Built NLA.SP05.Jordan (4.1s) ℹ [3737/3742] Built NLA.SP05.Cone (3.0s) info: NLA/SP05/Cone.lean:57:0: 'NLA.SP05.complex_jordan_columnVec' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/SP05/Cone.lean:58:0: 'NLA.SP05.actual_jordan_inverse_equation' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/SP05/Cone.lean:59:0: 'NLA.SP05.actual_jordan_inverse_cone' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3738/3742] Built NLA.SP05.Minimizer (3.8s) info: NLA/SP05/Minimizer.lean:31:0: 'NLA.SP05.global_positive_minimizer' depends on axioms: [propext, Classical.choice, Quot.sound] ⚠ [3739/3742] Built NLA.SP05.Proof (3.9s) warning: NLA/SP05/Proof.lean:41:5: Variable name `hA` 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] _hA Note: This linter can be disabled with `set_option linter.unusedVariables false` warning: NLA/SP05/Proof.lean:41:21: Variable name `hB` 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] _hB Note: This linter can be disabled with `set_option linter.unusedVariables false` info: NLA/SP05/Proof.lean:53:0: 'NLA.SP05.numerical_bound' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/SP05/Proof.lean:55:0: 'NLA.SP05.column_vectorization' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/SP05/Proof.lean:57:0: 'NLA.SP05.skew_witness' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/SP05/Proof.lean:59:0: 'NLA.SP05.positive_minimizer' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/SP05/Proof.lean:61:0: 'NLA.SP05.sector_minima' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/SP05/Proof.lean:63:0: 'NLA.SP05.canonical_result' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [3740/3742] Built Solution (3.7s) ✔ [3741/3742] Built RegistryRecord (3.8s) Build completed successfully (3742 jobs).