Skip to content

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

Choose a tag to compare

View all tags
@github-actions github-actions released this 23 Aug 23:52
v1.1.0
05ff5d8

Release notes

v1.1.0 - 2026-08-24

Scholarly-completeness release. The mathematical proof and public Lean
endpoints are unchanged in substance. This version:

  • retitles the manuscript A Defect-Gram Proof of the Crouzeix Theorem;
  • adds a full introduction, contribution summary, related-work discussion,
    and paper organization;
  • adds 21 verified references to primary papers, publisher records, books,
    and versioned 2026 preprints;
  • clarifies independence from the contemporaneous proofs and from the sign
    condition discussed in Lorist--Schwenninger, Remark 2;
  • adds keywords, MSC classification, a sharpness section, formal-verification
    scope, author and AI contribution statements, acknowledgments, data/code
    availability, funding, and conflicts-of-interest declarations;
  • adds a preferred article citation to CITATION.cff and clarifies the
    Apache-2.0/CC BY 4.0 license split; and
  • refreshes the frozen source hash, PDF hash, line map, manifest, and release
    metadata after clean compilation and verification.

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