Skip to content

A Defect-Gram Proof of the Crouzeix Theorem, v1.0.0

Choose a tag to compare

View all tags
@github-actions github-actions released this 23 Aug 17:16
v1.0.0
b9838fe

Release notes

v1.0.0 - 2026-08-24

Initial standalone release of:

  • the manuscript The Numerical-Range Inequality and the Rational Spectral-Set
    Formulation     and its compiled PDF;
  • the kernel-checked endpoint for the finite-dimensional scalar
    polynomial numerical-range inequality with constant 2;
  • the corresponding reduced-rational spectral-set endpoint;
  • direct Euclidean-operator-norm and attained-maximum wrappers;
  • the defect-Gram recurrence, strict scaled finite-Blaschke local bound,
    Schur-approximation completion, and convex outer-exhaustion assembly;
  • pinned Lean, Mathlib, supporting-package, and RMT4 revisions;
  • a source manifest, manuscript hashes, CI verification, and public axiom
    audit.

The kernel reports only propext, Classical.choice, and Quot.sound for
the public declarations. The manuscript is a non-peer-reviewed research
preprint. The completion stage in Lean is an alternative checked mechanism
with the same downstream endpoint consequence, rather than a line-by-line
transcription of the manuscript's confluent interpolation and
boundary-extension lemmas; see FORMALIZATION_MAP.md.

Assets 3
Loading