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

Release notes

v1.2.0 - 2026-08-24

ArXiv-readiness and provenance release. The mathematical proof and public
Lean endpoints are unchanged. This version:

• keeps GPT-5.6 Sol's substantive research contribution in a detailed
  disclosure while reserving the author byline for the accountable human
  author;
• shortens the affiliation in the title block to ByteDance, Beijing, China;
• cites and contrasts the author's earlier boundary-kernel/Fourier-recurrence
  proof, including its archived Zenodo DOI;
• states precisely that the manuscript proof is independent of the two
  contemporaneous theorem announcements, while the Lean development reuses
  a pinned supporting package only for documented lower-level infrastructure;
• records that the recursive dependency audit excludes the supporting
  package's constant-2 endpoints and alternative positive-real-completion
  and ordered-Gramian route;
• gives the version-specific Lorist--Schwenninger v2 link; and
• refreshes the frozen source hash, PDF hash, line map, manifest, and release
  metadata after clean compilation and verification.

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.

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

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.

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

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.