From 4a62a4caafca460e7f4233f5b0145d7de6e53cbf Mon Sep 17 00:00:00 2001 From: Shivam Patel Date: Sat, 5 Sep 2026 04:02:43 -0700 Subject: [PATCH 1/2] Record bidisc Bohr bound with externally hosted proof package --- README.md | 3 ++- constants/59a.md | 12 +++++++++--- 2 files changed, 11 insertions(+), 4 deletions(-) diff --git a/README.md b/README.md index c2c630fc..62594ce2 100644 --- a/README.md +++ b/README.md @@ -96,7 +96,7 @@ Bounds for which the level of available verification is currently at minimal lev | [57b](https://teorth.github.io/optimizationproblems/constants/57b.html) | Landau's constant | $\frac{1}{2}+10^{-335}$ | $\dfrac{\Gamma(1/3)\Gamma(5/6)}{\Gamma(1/6)}\approx 0.5433$ | | [57c](https://teorth.github.io/optimizationproblems/constants/57c.html) | Univalent Bloch constant | 0.5708858 | 1 | | [58](https://teorth.github.io/optimizationproblems/constants/58a.html) | Zaremba’s conjecture constant | 5 | $\infty$ | -| [59](https://teorth.github.io/optimizationproblems/constants/59a.html) | Bohr radius for the bidisc | 0.3006 | 0.3174541 | +| [59](https://teorth.github.io/optimizationproblems/constants/59a.html) | Bohr radius for the bidisc | 0.3006 | 0.302825279492 | | [60](https://teorth.github.io/optimizationproblems/constants/60a.html) | Favard-length decay exponent | $\frac{1}{6}$ | 1 | | [61](https://teorth.github.io/optimizationproblems/constants/61a.html) | Selberg congruence spectral-gap constant | 0 | $\frac{7}{64}$ | | [62a](https://teorth.github.io/optimizationproblems/constants/62a.html) | Lindelof (pointwise growth) exponent for the Riemann zeta function | 0 | $\frac{13}{84}$ | @@ -156,6 +156,7 @@ Bounds for which the level of available verification is currently at minimal lev - [2](https://teorth.github.io/optimizationproblems/constants/2a.html) **solved:** $C_2 = 2$ — Crouzeix's conjecture, by [S. Jin](https://www.preprints.org/manuscript/202607.1919), 27 Jul 2026; an independent proof by a different route followed in [E. Lorist and F. L. Schwenninger](https://arxiv.org/abs/2608.03841), 4 Aug 2026. - [3a](https://teorth.github.io/optimizationproblems/constants/3a.html) **improved lower bound (limit value):** $C_{3a} \geq 1.19519192*$ by [L. Kleinwaks](https://github.com/kleinwaks/masked-digit-sum-difference-bound), 14 Aug 2026. - [15a](https://teorth.github.io/optimizationproblems/constants/15a.html) **improved upper bound:** $C_{15a} \leq 2.371177$ by [E. Dupont, M. Eisenberger, B. Kozlovskii, A. Mehrabian, F. J. R. Ruiz, A. See, R. Zhou, J. Alman, V. Vassilevska Williams, M. Balog](https://arxiv.org/abs/2608.16884), 17 Aug 2026. +- [59](https://teorth.github.io/optimizationproblems/constants/59a.html) **improved upper bound:** $C\_{59}=K\_2<0.302825279492$ by [Shivam Patel](https://mathdb.com/p/392062/exact-value-of-the-bohr-radius-of-the-bidisc#s2), 26 Aug 2026. - [43](https://teorth.github.io/optimizationproblems/constants/43a.html) **improved lower bound (unverified):** $C_{43} \geq 0.860*$ (exact $43/50$; certificate-layer result conditional on the lemma set of [KHSHGW2026](https://arxiv.org/abs/2601.22365)) by [J. Savva](https://doi.org/10.5281/zenodo.22223485), 1 Sep 2026. - [88a](https://teorth.github.io/optimizationproblems/constants/88a.html) **improved upper bound:** $C_{88a} \leq 186$ via $\mathrm{DHL}[40,2]$, by [OpenAI](https://cdn.openai.com/pdf/51126fac-1b68-4128-9666-c908bcc16033/short_gaps.pdf), 30 Aug 2026, with a Lean 4 formalization conditional on three declared axioms. diff --git a/constants/59a.md b/constants/59a.md index 02547472..c0938fbf 100644 --- a/constants/59a.md +++ b/constants/59a.md @@ -43,10 +43,10 @@ The exact value of $K_d$ is unknown for every $d>1$; in particular, the exact va The best established range currently is $$ -0.3006\ \le\ K_2\ <\ 0.3174541. +0.3006\ \le\ K_2\ <\ 0.302825279492. $$ -[Kne2025-lb-K2-0-3006] [G2026-ub-K2-0-3174541] +[Kne2025-lb-K2-0-3006] [P2026-ub-K2-0-302825279492] ## Known upper bounds @@ -55,6 +55,7 @@ $$ | $1/3$ | [BK1997] | General upper bound $K_n\le 1/3$ (hence $K_2\le 1/3$). [BK1997-ub-1-3] | | $0.3177$ | [BPWW2026] | Explicit construction giving $K_2<0.3177$ (Theorem 6.4). [BPWW2026-ub-K2-0-3177] | | $0.3174541$ | [G2026] | Degree-$(250,250)$ polynomial from a rational-inner Fejer averaging certificate. Exact integer verification gives $B\_{3174541/10000000}(p)>1$. [G2026-ub-K2-0-3174541] | +| $0.302825279492$ | [P2026] | Set $U=(1+z)(1-w)$, $V=1+zw$, $P=LU+iTV$, $Q=LV+iTU$, and $f=(SQ-P)/(SQ+P)$, with $L=2500000000$, $T=3067398171$, and $S=10^{15}$. Two independent exact computations of the 841 coefficients with $0\le j,k\le N=28$ give a finite majorant greater than $1+10^{-26}$ at $r=302825279492/10^{12}$. [Proof package v1.0.0](https://github.com/Shivamshaiv/bidisc-bohr-certificate/releases/tag/v1.0.0); attached `bidisc-bohr-certificate-v1.0.0.zip` SHA-256: `afc77b42cdd9de9b82e3d4c6a973dc32bf82b2c19960df58507b9a5cf333928b`. [P2026-ub-K2-0-302825279492] | ## Known lower bounds @@ -124,6 +125,11 @@ $$ **loc:** pull request certificate and exact verifier **quote:** “The exact integer verifier proves $B\_{3174541/10000000}(p)>1+1/7307638490$ and the rational-inner Fejer averaging certificate proves $\lvert p\rvert\le 1$ on the bidisc.” +- **[P2026]** Patel, Shivam. *Complex phases and a certified upper bound for the bidisc Bohr radius.* Research note and reproducibility record, 26 August 2026. [MathDB solution](https://mathdb.com/p/392062/exact-value-of-the-bohr-radius-of-the-bidisc#s2). [Exact Python and Lean proof package, v1.0.0](https://github.com/Shivamshaiv/bidisc-bohr-certificate/releases/tag/v1.0.0), released 5 September 2026; [pinned source](https://github.com/Shivamshaiv/bidisc-bohr-certificate/tree/27464dce16c7fe41733befe32e672cff87139b6f/certificate). + - **[P2026-ub-K2-0-302825279492]** + **loc:** the analytic and finite coefficient certificates in the package README; `certificate/EndToEnd.lean`, theorem `Optim.BohrRadius.bohrRadius_lt_302825279492_div_10pow12` + **statement:** The explicit Schur witness and exact finite coefficient comparison prove $K\_2<302825279492/10^{12}=0.302825279492$. The exact value of $K\_2$ remains open. + ## Contribution notes -Prepared initially with assistance from ChatGPT 5.2 Pro and updated with assistance from ChatGPT 5.5 Pro. +Prepared initially with assistance from ChatGPT 5.2 Pro and updated with assistance from ChatGPT 5.5 Pro. The Patel update, independent exact verifiers, and Lean formalization were prepared with assistance from Codex. Shivam Patel reviewed the original references and submitted information. The external packaging and Markdown revision were prepared with Codex assistance. From 0253406b26a2e93870afd34f660709e0f6989d49 Mon Sep 17 00:00:00 2001 From: Shivam Patel Date: Sat, 5 Sep 2026 04:44:16 -0700 Subject: [PATCH 2/2] Cite the published Zenodo proof archive --- constants/59a.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/constants/59a.md b/constants/59a.md index c0938fbf..e5db960c 100644 --- a/constants/59a.md +++ b/constants/59a.md @@ -55,7 +55,7 @@ $$ | $1/3$ | [BK1997] | General upper bound $K_n\le 1/3$ (hence $K_2\le 1/3$). [BK1997-ub-1-3] | | $0.3177$ | [BPWW2026] | Explicit construction giving $K_2<0.3177$ (Theorem 6.4). [BPWW2026-ub-K2-0-3177] | | $0.3174541$ | [G2026] | Degree-$(250,250)$ polynomial from a rational-inner Fejer averaging certificate. Exact integer verification gives $B\_{3174541/10000000}(p)>1$. [G2026-ub-K2-0-3174541] | -| $0.302825279492$ | [P2026] | Set $U=(1+z)(1-w)$, $V=1+zw$, $P=LU+iTV$, $Q=LV+iTU$, and $f=(SQ-P)/(SQ+P)$, with $L=2500000000$, $T=3067398171$, and $S=10^{15}$. Two independent exact computations of the 841 coefficients with $0\le j,k\le N=28$ give a finite majorant greater than $1+10^{-26}$ at $r=302825279492/10^{12}$. [Proof package v1.0.0](https://github.com/Shivamshaiv/bidisc-bohr-certificate/releases/tag/v1.0.0); attached `bidisc-bohr-certificate-v1.0.0.zip` SHA-256: `afc77b42cdd9de9b82e3d4c6a973dc32bf82b2c19960df58507b9a5cf333928b`. [P2026-ub-K2-0-302825279492] | +| $0.302825279492$ | [P2026] | Set $U=(1+z)(1-w)$, $V=1+zw$, $P=LU+iTV$, $Q=LV+iTU$, and $f=(SQ-P)/(SQ+P)$, with $L=2500000000$, $T=3067398171$, and $S=10^{15}$. Two independent exact computations of the 841 coefficients with $0\le j,k\le N=28$ give a finite majorant greater than $1+10^{-26}$ at $r=302825279492/10^{12}$. [Proof package v1.0.0, DOI: 10.5281/zenodo.22341928](https://doi.org/10.5281/zenodo.22341928); archived `bidisc-bohr-certificate-v1.0.0.zip` SHA-256: `afc77b42cdd9de9b82e3d4c6a973dc32bf82b2c19960df58507b9a5cf333928b`. [P2026-ub-K2-0-302825279492] | ## Known lower bounds @@ -125,7 +125,7 @@ $$ **loc:** pull request certificate and exact verifier **quote:** “The exact integer verifier proves $B\_{3174541/10000000}(p)>1+1/7307638490$ and the rational-inner Fejer averaging certificate proves $\lvert p\rvert\le 1$ on the bidisc.” -- **[P2026]** Patel, Shivam. *Complex phases and a certified upper bound for the bidisc Bohr radius.* Research note and reproducibility record, 26 August 2026. [MathDB solution](https://mathdb.com/p/392062/exact-value-of-the-bohr-radius-of-the-bidisc#s2). [Exact Python and Lean proof package, v1.0.0](https://github.com/Shivamshaiv/bidisc-bohr-certificate/releases/tag/v1.0.0), released 5 September 2026; [pinned source](https://github.com/Shivamshaiv/bidisc-bohr-certificate/tree/27464dce16c7fe41733befe32e672cff87139b6f/certificate). +- **[P2026]** Patel, Shivam. *Complex phases and a certified upper bound for the bidisc Bohr radius.* Research note and reproducibility record, 26 August 2026. [MathDB solution](https://mathdb.com/p/392062/exact-value-of-the-bohr-radius-of-the-bidisc#s2). [Exact Python and Lean proof package, v1.0.0](https://doi.org/10.5281/zenodo.22341928), Zenodo, 5 September 2026, DOI: [10.5281/zenodo.22341928](https://doi.org/10.5281/zenodo.22341928); [GitHub release](https://github.com/Shivamshaiv/bidisc-bohr-certificate/releases/tag/v1.0.0); [pinned source](https://github.com/Shivamshaiv/bidisc-bohr-certificate/tree/27464dce16c7fe41733befe32e672cff87139b6f/certificate). - **[P2026-ub-K2-0-302825279492]** **loc:** the analytic and finite coefficient certificates in the package README; `certificate/EndToEnd.lean`, theorem `Optim.BohrRadius.bohrRadius_lt_302825279492_div_10pow12` **statement:** The explicit Schur witness and exact finite coefficient comparison prove $K\_2<302825279492/10^{12}=0.302825279492$. The exact value of $K\_2$ remains open.