SP-06: a real Jordan-curve symbol with a nonreal finite Toeplitz spectrum

Recorded by the registry's curators from GitHub; the authors did not submit it here.

George Stepaniants

Complete negative resolution of the original finite-Toeplitz-spectrum implication, independently reviewed and verified by the actual Linux sandbox, Comparator, permitted-axiom audit and default kernel.

Claims

LEAN VERIFIED OP-00121 — A real-valued symbol on a Jordan curve and real Toeplitz spectra

Disproof · statement matched the canonical formalisation

Files and sources

Paper: OpenProblemsInNLA @ e375a6f, SP-06/lean/ ↗
Lean bundle: submissions/bundles/openproblemsinnla-sp-06-lean.tar.gz
Toolchain: leanprover/lean4:v4.33.1
Posted on GitHub: 13 September 2026

Verification PASSED

Attempt: 1
Toolchain: leanprover/lean4:v4.33.1
Auditor: v1 · modal
lake build: succeeded
Kernel replay: succeeded
Duration: 0:01:32.880804

Declarations audited

Declaration	Kind	Axioms	Unused hypotheses	Canonical
NLA.SP06.not_targetImplication	theorem · Prop	propext, Classical.choice, Quot.sound	none	matched
RegistryProblems.Problem_OP_00121	definition	propext, Classical.choice, Quot.sound	none	no canonical statement

NLA.SP06.not_targetImplication

Not NLA.SP06.targetImplication

RegistryProblems.Problem_OP_00121

Prop

Build log

RegistryProblems: built against the registry's copy at 38ca23a44fc2b159a0c944d5c9af39a80eb601c2 rather than the pinned 545a5d18ad3917d52192c41ce172ec4b41945751. Statements are checked by content, not revision.
✔ [2335/2341] Built NLA.SP06.Definitions (5.0s)
✔ [2336/2341] Built NLA.SP06.Numeric (8.1s)
✔ [2337/2341] Built NLA.SP06.Curve (4.7s)
✔ [2338/2341] Built NLA.SP06.Proof (3.5s)
✔ [2339/2341] Built Solution (3.5s)
✔ [2340/2341] Built RegistryRecord (3.5s)
Build completed successfully (2341 jobs).