Certify K₂ < 0.302825279492 for the bidisc Bohr radius

[Shivamshaiv]

Summary

This PR updates the recorded upper bound for the bidisc Bohr radius
$C_{59}=K_2$ from $K_2&lt;0.3174541$ to the certified strict bound

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

The exact value of $K_2$ remains open; this PR claims only the strict
upper bound above.

What changes

• updates README.md and constants/59a.md;
• adds two independent exact Python verifiers;
• adds a complete pinned Lean package under
  certificates/59a/patel-2026/.

Mathematical certificate

Explicit Schur witness

Let

$$ L=2500000000,\qquad T=3067398171,\qquad S=10^{15}, $$

and define

$$ \begin{aligned} U(z,w)&=(1+z)(1-w),\\ V(z,w)&=1+zw,\\ P(z,w)&=L,U(z,w)+iT,V(z,w),\\ Q(z,w)&=L,V(z,w)+iT,U(z,w). \end{aligned} $$

The witness is the rational function

$$ f(z,w)=\frac{S Q(z,w)-P(z,w)} {S Q(z,w)+P(z,w)}. $$

For every $z,w\in\mathbb C$, direct algebra gives the exact identity

$$ \begin{aligned} &\left|S Q(z,w)+P(z,w)\right|^2 -\left|S Q(z,w)-P(z,w)\right|^2\\ &\qquad = 2S(L^2+T^2) \left[ (1-|w|^2)|1+z|^2 + (1-|z|^2)|1-w|^2 \right]. \end{aligned} $$

The right-hand side is strictly positive whenever $|z|&lt;1$ and $|w|&lt;1$.
Hence $SQ+P\neq0$ on the open bidisc, $f$ is analytic there, and

$$ |f(z,w)|<1. $$

Thus $f$ belongs to the bidisc Schur class.

Exact finite coefficient certificate

After multiplying the numerator and denominator by the Gaussian-integer
conjugate of the denominator's constant coefficient, the denominator has
real constant term

$$ \begin{aligned} D &=(S+1)^2(L^2+T^2)\\ &= 15,658,931,539,454,176,558,863,078,908,306,140,931,539,454,145,241. \end{aligned} $$

Write the normalized numerator and denominator as

$$ p(z,w)=\sum p_{jk}z^jw^k, \qquad q(z,w)=D+q_{10}z+q_{01}w+q_{11}zw. $$

If

$$ f(z,w)=\sum_{j,k\ge0}c_{jk}z^jw^k, $$

then the exact Gaussian-integer recurrence used in the certificate is

$$ c_{jk}=\frac{v_{jk}}{D^{j+k+1}}, $$

where coefficients with a negative index are zero and

$$ v_{jk}=p_{jk}D^{j+k}-q_{10}v_{j-1,k}-q_{01}v_{j,k-1}-Dq_{11}v_{j-1,k-1}. $$

For $0\le j,k\le N=28$, define the exact integer lower bounds

$$ n_{jk}=\left\lfloor\sqrt{(\operatorname{Re}v_{jk})^2+(\operatorname{Im}v_{jk})^2}\right\rfloor. $$

Set

$$ R=302825279492,\qquad E=10^{12}, $$

and form the integers

$$ A= \sum_{j,k=0}^{N} n_{jk}R^{j+k}(ED)^{2N-j-k}, \qquad B=D(ED)^{2N}. $$

Exact integer arithmetic proves

$$ 10^{26}A>(10^{26}+1)B. $$

Consequently,

$$ \begin{aligned} \sum_{j,k=0}^{28} |c_{jk}| \left(\frac RE\right)^{j+k} &\ge \frac AB\\ &>1+10^{-26}. \end{aligned} $$

This is a finite lower bound: no estimate of an uncomputed Taylor tail is
needed. The finite majorant is continuous in the radius, so it remains greater
than $1$ at some positive radius strictly smaller than $R/E$. Monotonicity then
gives

$$ K_2<\frac RE=0.302825279492. $$

Two independent standard-library Python programs verify all $29^2=841$ coefficients:

• verify_gaussian_certificate.py uses the triangular Gaussian-integer recurrence;
• verify_multinomial_certificate.py independently extracts the coefficients
  of $1/q$ using the multinomial formula.

They agree on all coefficients, all norm floors, the integers $A$ and $B$, and
the frozen SHA-256 digests recorded in the package.

Lean verification

The package contains two Lean files:

• FiniteCertificate.lean verifies the 841 Gaussian-integer recurrences,
  every integer-square-root floor, the homogenized weighted sum, and the exact
  inequality $10^{26}A&gt;(10^{26}+1)B$.
• EndToEnd.lean proves the global norm-square identity, denominator
  nonvanishing, analyticity, and the Schur bound; constructs the actual locally
  convergent Taylor family; identifies its checked $29\times29$ rectangle with
  the finite certificate; proves the finite Bohr violation; and derives the
  strict supremal upper bound.

The final formal theorem is

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

Both files compile without sorry, admit, or custom axioms. The final #print axioms output is

[propext, Classical.choice, Lean.ofReduceBool, Quot.sound]

Here Lean.ofReduceBool is the explicit trust boundary introduced by the
finite native_decide computations.

This is an end-to-end Lean formalization of the stated Bohr-radius upper bound.
It does not claim a Lean formalization of any broader structural-dominance
theorem, nor does it determine the exact value of $K_2$.

Reproduction

The Python verifiers require Python 3.9 or later and use only the standard library.

cd certificates/59a/patel-2026
python verify_gaussian_certificate.py
python verify_multinomial_certificate.py

The Lean project pins Lean 4.19.0 and Mathlib commit

c44e0c8ee63ca166450922a373c7409c5d26b00b

and can be checked with

cd certificates/59a/patel-2026
lake exe cache get
lake build

File hashes are frozen in certificates/59a/patel-2026/SHA256SUMS.

The corresponding mathematical write-up is recorded in Shivam Patel’s MathDB contribution.

Scope and disclosure

The exact value of $K_2$ remains open, and the separate structural-dominance
theorem is not claimed as Lean verified.

This contribution is submitted by Shivam Patel. The mathematical
construction, proof presentation, exact verification programs, Lean certificate,
and repository submission were prepared with AI assistance. Shivam Patel
supplied the contribution and reviewed the mathematical claim, references,
proof artifacts, and submitted information.