The Sharp Numerical-Range Spectral-Set Inequality — Candidate Proof and Complete Lean 4 Formalization (v0.1.0)

Status

This is the first archival release of Qinyu Luo's candidate proof of the finite-dimensional scalar Crouzeix conjecture, its complete Lean 4 formalization, and the accompanying three-route numerical cross-checks.

The manuscript is a candidate proof and has not been peer reviewed. The Lean kernel checks the precise formal theorem described below; this does not replace expert review of the correspondence between the manuscript and its formal encoding.

Formal verification

The principal checked declaration is:

CrouzeixFormalization.luoCrouzeixEndpoint

It proves, for every positive finite dimension and every complex matrix, the sharp constant-2 scalar polynomial inequality over the numerical range, together with the reduced-rational consequence when the reduced denominator has no zero on the numerical range. The 2 × 2 nilpotent Jordan example formally attains the ratio 2.

The release is pinned to:

• Lean 4.28.0
• Mathlib 8f9d9cff6bd728b17a24e163c9402775d9e6a365
• jinshanmu/CrouzeixConjecture at f9d5c8d39bece41ceedf6346ef50ad1fb393260e
• RMT4 at 69a9efe77e912647d651aa7368856955b24dca2f

A clean Ubuntu build completed all 3,456 build tasks. The project contains no sorry, admit, custom axioms, unsafe, or native_decide. The audited endpoint depends only on the standard Lean/Mathlib axioms propext, Classical.choice, and Quot.sound.

Numerical cross-checks

The recorded three-route run evaluates ten exact and near-extremal examples. All ten cases passed at the documented tolerance. These finite-precision computations are falsification tests, not proofs.

Provenance

The frozen manuscript source has SHA-256:

9ea8adcda6fd3c57161457c69edea68794ac1560a85cfd8e1e2280c9e015b7d9

The Luo endpoint does not invoke Jin's constant-2 endpoint. It does reuse documented lower-level declarations from the pinned Jin package. The vendored RMT4 source retains its upstream attribution and license.

Licensing

Original software and formalization source are released under Apache License 2.0. The manuscript in paper/ is released under Creative Commons Attribution 4.0 International. Vendored and external dependencies retain their respective upstream terms; see NOTICE, THIRD_PARTY_NOTICES.md, and the directory-level license files.

Reproduction

See the root README.md, Lean/README.md, and Lean/FORMALIZATION_MAP.md. File integrity can be checked using MANIFEST.sha256.