Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
Shivamshaiv wants to merge 2 commits into
base: main
Choose a base branch
from
Open

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
4a62a4c
Record bidisc Bohr bound with externally hosted proof package
Shivamshaiv Sep 5, 2026
0253406
Cite the published Zenodo proof archive
Shivamshaiv Sep 5, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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}$ |
Expand Down Expand Up @@ -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.

Expand Down
12 changes: 9 additions & 3 deletions constants/59a.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
$$

<a href="#Kne2025-lb-K2-0-3006">[Kne2025-lb-K2-0-3006]</a> <a href="#G2026-ub-K2-0-3174541">[G2026-ub-K2-0-3174541]</a>
<a href="#Kne2025-lb-K2-0-3006">[Kne2025-lb-K2-0-3006]</a> <a href="#P2026-ub-K2-0-302825279492">[P2026-ub-K2-0-302825279492]</a>

## Known upper bounds

Expand All @@ -55,6 +55,7 @@ $$
| $1/3$ | <a href="#BK1997">[BK1997]</a> | General upper bound $K_n\le 1/3$ (hence $K_2\le 1/3$). <a href="#BK1997-ub-1-3">[BK1997-ub-1-3]</a> |
| $0.3177$ | <a href="#BPWW2026">[BPWW2026]</a> | Explicit construction giving $K_2<0.3177$ (Theorem 6.4). <a href="#BPWW2026-ub-K2-0-3177">[BPWW2026-ub-K2-0-3177]</a> |
| $0.3174541$ | <a href="#G2026">[G2026]</a> | Degree-$(250,250)$ polynomial from a rational-inner Fejer averaging certificate. Exact integer verification gives $B\_{3174541/10000000}(p)>1$. <a href="#G2026-ub-K2-0-3174541">[G2026-ub-K2-0-3174541]</a> |
| $0.302825279492$ | <a href="#P2026">[P2026]</a> | 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`. <a href="#P2026-ub-K2-0-302825279492">[P2026-ub-K2-0-302825279492]</a> |

## Known lower bounds

Expand Down Expand Up @@ -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.”

- <a id="P2026"></a>**[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).
- <a id="P2026-ub-K2-0-302825279492"></a>**[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.