Record K₂ < 0.302825279492 with an external proof archive (Markdown only)

[Shivamshaiv]

Bound update

This PR updates the recorded upper bound for the bidisc Bohr radius from
$K_2&lt;0.3174541$ to

$$ \boxed{K_2<\frac{302825279492}{10^{12}}=0.302825279492.} $$

It changes only README.md and constants/59a.md. The earlier upper-bound
rows and lower bound $0.3006$ are retained; the README table and Recent
progress entry are updated. The exact value of $K_2$ remains open.

External proof package

This replaces #154 and addresses the maintainer's packaging request.
All supporting code and formalization are hosted in
Shivamshaiv/bidisc-bohr-certificate,
with a versioned source release
and pinned source commit.

The Comments column records the SHA-256 of the explicitly attached
bidisc-bohr-certificate-v1.0.0.zip:

afc77b42cdd9de9b82e3d4c6a973dc32bf82b2c19960df58507b9a5cf333928b

The [P2026] reference now resolves to the external package and names the
final Lean theorem. The proof and algorithms are unchanged; LF line endings
restore the original frozen file hashes. This branch starts from current
main at 9d57db86c8564cb623ec9f9e41429a34efd819fb, including the corrected
Crouzeix entry and subsequent upstream changes.

The verified v1.0.0 package, checksum, validation report, and three run logs
are now publicly archived on Zenodo under version-specific DOI
10.5281/zenodo.22341928.
The Comments column and [P2026] citation include this permanent reference.
The archived ZIP is byte-for-byte identical to the attached GitHub release
asset, so the recorded SHA-256 is unchanged.

Mathematical certificate

Set $L=2500000000$, $T=3067398171$, $S=10^{15}$, and

$$ \begin{aligned} U(z,w)&=(1+z)(1-w), & V(z,w)&=1+zw,\\ P(z,w)&=LU(z,w)+iTV(z,w), & Q(z,w)&=LV(z,w)+iTU(z,w),\\ f(z,w)&=\frac{SQ(z,w)-P(z,w)}{SQ(z,w)+P(z,w)}. \end{aligned} $$

The exact identity

$$ \begin{aligned} &\lvert SQ+P\rvert^2-\lvert SQ-P\rvert^2\\ &\quad=2S(L^2+T^2)\left[(1-\lvert w\rvert^2)\lvert1+z\rvert^2 +(1-\lvert z\rvert^2)\lvert1-w\rvert^2\right] \end{aligned} $$

has a strictly positive right-hand side on the open bidisc. It proves
denominator nonvanishing and $\lvert f\rvert&lt;1$ there.

For the Taylor coefficients $c_{jk}$ of this explicit Schur function, two
independent exact computations of the $29\times29$ rectangle establish

$$ \sum_{j,k=0}^{28}\lvert c_{jk}\rvert \left(\frac{302825279492}{10^{12}}\right)^{j+k} >1+10^{-26}. $$

Continuity makes this finite sum exceed one at a strictly smaller positive
radius. Monotonicity then gives the strict supremal bound above. No estimate
of an uncomputed Taylor tail is needed.

Verification

The externally hosted package was checked again on 5 September 2026:

• Both independent Python verifiers pass and reproduce all six published
  certificate digests, including the 841 coefficients and integer norm floors.
• All eight frozen file checksums pass after extracting the release archive.
• A fresh lake build passes for both Lean files with Lean 4.19.0 and Mathlib
  c44e0c8ee63ca166450922a373c7409c5d26b00b.

The end-to-end theorem is

Optim.BohrRadius.bohrRadius_lt_302825279492_div_10pow12 :
  bohrRadius < (302825279492 : ℝ) / 10 ^ 12

Its printed axioms are [propext, Classical.choice, Lean.ofReduceBool, Quot.sound].
The finite native_decide computations introduce the explicit
Lean.ofReduceBool trust boundary. There are no sorry, admit, or custom
axiom declarations. This formalization covers the stated bound, not an
exact value or a separate structural-dominance theorem.

Submitted by Shivam Patel. The mathematical construction, proof
presentation, verification programs, Lean formalization, and this submission
were prepared with AI assistance. The original contribution's attribution and
disclosure are retained.

[Shivamshaiv]

The proof package is now also publicly archived on Zenodo:
DOI 10.5281/zenodo.22341928 (version 1.0.0).

The archive includes the exact release ZIP, SHA-256 checksum, validation report,
and both Python verification logs plus the successful pinned Lean build log.
The ZIP and its recorded checksum are unchanged. The Comments column and
[P2026] reference now cite the DOI. This PR still changes only README.md
and constants/59a.md; the proof code remains in the external repository.