Certify K₂ < 0.302825279492 for the bidisc Bohr radius

README.md

@@ -95,7 +95,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}$ |
@@ -153,6 +153,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 [Jin](https://www.preprints.org/manuscript/202607.1919) (July 2026); a second proof followed shortly after in [E. Lorist and F. L. Schwenninger](https://arxiv.org/abs/2608.03841), 4 Aug 2026, which acknowledges Jin.
 - [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.
 
 ## Maintainers
 

certificates/59a/patel-2026/.gitignore

@@ -0,0 +1,3 @@
+/.lake/
+/*.olean
+/*.ilean

certificates/59a/patel-2026/FiniteCertificate.lean

@@ -0,0 +1,172 @@
+import Mathlib.Data.Nat.Sqrt
+import Mathlib.Tactic
+
+/-!
+Exact finite ARITHMETIC certificate for the rational data at radius
+302825279492 / 10^12. This file does not formalize the analytic Schur proof
+or the deduction about the bidisc Bohr radius. Those are separate claims.
+
+The computational proofs use native_decide. The axiom audit at the end
+records that native-computation trust boundary.
+-/
+
+set_option maxRecDepth 10000
+set_option maxHeartbeats 4000000
+
+namespace BidiscPhaseCertificate
+
+abbrev Gaussian := Int × Int
+
+def gadd (a b : Gaussian) : Gaussian := (a.1 + b.1, a.2 + b.2)
+def gneg (a : Gaussian) : Gaussian := (-a.1, -a.2)
+def gmul (a b : Gaussian) : Gaussian :=
+  (a.1 * b.1 - a.2 * b.2, a.1 * b.2 + a.2 * b.1)
+def gscale (n : Int) (a : Gaussian) : Gaussian := (n * a.1, n * a.2)
+def gconj (a : Gaussian) : Gaussian := (a.1, -a.2)
+
+def L : Nat := 2500000000
+def T : Nat := 3067398171
+def S : Nat := 1000000000000000
+def R : Nat := 302825279492
+def E : Nat := 1000000000000
+def side : Nat := 29
+def maxDegree : Nat := 56
+
+/-- Coefficients of SQ-P, ordered as 1,z,w,zw. -/
+def inputNumerator : Array Gaussian := Id.run do
+  let l : Int := L
+  let t : Int := T
+  let s : Int := S
+  return #[((s - 1) * l, (s - 1) * t),
+    (-l, s * t), (l, -(s * t)),
+    ((s + 1) * l, -((s + 1) * t))]
+
+/-- Coefficients of SQ+P, ordered as 1,z,w,zw. -/
+def inputDenominator : Array Gaussian := Id.run do
+  let l : Int := L
+  let t : Int := T
+  let s : Int := S
+  return #[((s + 1) * l, (s + 1) * t),
+    (l, s * t), (-l, -(s * t)),
+    ((s - 1) * l, -((s - 1) * t))]
+
+def conjugateConstant : Gaussian :=
+  gconj (inputDenominator.getD 0 (0, 0))
+
+def numerator : Array Gaussian :=
+  inputNumerator.map (fun v => gmul v conjugateConstant)
+
+def denominator : Array Gaussian :=
+  inputDenominator.map (fun v => gmul v conjugateConstant)
+
+def D : Nat := (S + 1) ^ 2 * (L ^ 2 + T ^ 2)
+
+theorem denominator_constant_correct :
+    denominator.getD 0 (0, 0) = ((D : Int), 0) := by
+  native_decide
+
+theorem input_parameters_positive :
+    0 < D ∧ 0 < R ∧ R < E ∧ 1 < S := by
+  native_decide
+
+def rectangle : Array Gaussian := Id.run do
+  let q10 := denominator.getD 1 (0, 0)
+  let q01 := denominator.getD 2 (0, 0)
+  let q11 := denominator.getD 3 (0, 0)
+  let d : Int := D
+  let mut values := Array.replicate (side * side) ((0, 0) : Gaussian)
+  for j in [:side] do
+    for k in [:side] do
+      let first := if 0 < j then
+        gmul q10 (values.getD ((j - 1) * side + k) (0, 0)) else (0, 0)
+      let second := if 0 < k then
+        gmul q01 (values.getD (j * side + (k - 1)) (0, 0)) else (0, 0)
+      let mixed := if 0 < j ∧ 0 < k then
+        gscale d (gmul q11
+          (values.getD ((j - 1) * side + (k - 1)) (0, 0))) else (0, 0)
+      let source := if j < 2 ∧ k < 2 then
+        gscale (d ^ (j + k)) (numerator.getD (j + 2 * k) (0, 0)) else (0, 0)
+      values := values.set! (j * side + k)
+        (gadd source (gneg (gadd first (gadd second mixed))))
+  return values
+
+def coefficientNumerator (j k : Nat) : Gaussian :=
+  rectangle.getD (j * side + k) (0, 0)
+
+def expected (j k : Nat) : Gaussian :=
+  let first := if 0 < j then
+    gmul (denominator.getD 1 (0, 0)) (coefficientNumerator (j - 1) k) else (0, 0)
+  let second := if 0 < k then
+    gmul (denominator.getD 2 (0, 0)) (coefficientNumerator j (k - 1)) else (0, 0)
+  let mixed := if 0 < j ∧ 0 < k then
+    gscale (D : Int) (gmul (denominator.getD 3 (0, 0))
+      (coefficientNumerator (j - 1) (k - 1))) else (0, 0)
+  let source := if j < 2 ∧ k < 2 then
+    gscale ((D : Int) ^ (j + k)) (numerator.getD (j + 2 * k) (0, 0)) else (0, 0)
+  gadd source (gneg (gadd first (gadd second mixed)))
+
+theorem rectangle_recurrence :
+    ∀ j k : Fin 29,
+      coefficientNumerator j.val k.val = expected j.val k.val := by
+  native_decide
+
+def normSquared (v : Gaussian) : Nat := v.1.natAbs ^ 2 + v.2.natAbs ^ 2
+
+def lowerRectangle : Array Nat :=
+  rectangle.map (fun v => Nat.sqrt (normSquared v))
+
+def lowerNorm (j k : Nat) : Nat := lowerRectangle.getD (j * side + k) 0
+
+theorem integer_square_roots_correct :
+    ∀ j k : Fin 29,
+      (lowerNorm j.val k.val) ^ 2 ≤ normSquared (coefficientNumerator j.val k.val) ∧
+      normSquared (coefficientNumerator j.val k.val) <
+        (lowerNorm j.val k.val + 1) ^ 2 := by
+  native_decide
+
+def diagonals : Array Nat := Id.run do
+  let mut values := Array.replicate 57 0
+  for j in [:side] do
+    for k in [:side] do
+      values := values.set! (j + k)
+        (values.getD (j + k) 0 + lowerNorm j k)
+  return values
+
+def homogeneous : Nat × Nat := Id.run do
+  let base := E * D
+  let mut denominatorPower := 1
+  let mut value := diagonals.getD 56 0
+  for t in [:56] do
+    denominatorPower := denominatorPower * base
+    value := value * R + diagonals.getD (55 - t) 0 * denominatorPower
+  return (value, D * denominatorPower)
+
+open scoped BigOperators
+
+def weightedIntegerSum : Nat :=
+  ∑ j ∈ Finset.range 29, ∑ k ∈ Finset.range 29,
+    lowerNorm j k * R ^ (j + k) * (E * D) ^ (56 - (j + k))
+
+theorem weighted_sum_eq_homogeneous :
+    weightedIntegerSum = homogeneous.1 := by
+  native_decide
+
+theorem homogeneous_denominator_correct :
+    homogeneous.2 = D * (E * D) ^ 56 := by
+  native_decide
+
+/-- This is only the finite integer comparison, not an analytic Bohr theorem. -/
+theorem strict_integer_margin :
+    10 ^ 26 * homogeneous.1 > (10 ^ 26 + 1) * homogeneous.2 := by
+  native_decide
+
+theorem strict_weighted_integer_margin :
+    10 ^ 26 * weightedIntegerSum > (10 ^ 26 + 1) * (D * (E * D) ^ 56) := by
+  rw [weighted_sum_eq_homogeneous, ← homogeneous_denominator_correct]
+  exact strict_integer_margin
+
+end BidiscPhaseCertificate
+
+#print axioms BidiscPhaseCertificate.rectangle_recurrence
+#print axioms BidiscPhaseCertificate.integer_square_roots_correct
+#print axioms BidiscPhaseCertificate.strict_weighted_integer_margin

certificates/59a/patel-2026/README.md

@@ -0,0 +1,158 @@
+# Certified upper bound for the bidisc Bohr radius
+
+This directory is the reproducibility package for Shivam Patel's bound
+
+$$
+K_2 < \frac{302825279492}{10^{12}} = 0.302825279492.
+$$
+
+It proves an upper bound only. It does not determine the exact value of
+$K_2$.
+
+## Analytic certificate
+
+Set
+
+$$
+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)&=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}
+$$
+
+Direct expansion gives, for all complex $z,w$,
+
+$$
+\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}
+$$
+
+The right-hand side is strictly positive on the open bidisc. Consequently
+$SQ+P$ has no zero there, $f$ is holomorphic there, and $\lvert f\rvert<1$.
+
+## Finite coefficient certificate
+
+Multiply the numerator and denominator of $f$ by the Gaussian-integer
+conjugate of the denominator's constant coefficient. The new denominator has
+constant coefficient
+
+$$
+D=(S+1)^2(L^2+T^2)
+=15658931539454176558863078908306140931539454145241.
+$$
+
+Write the resulting numerator and denominator as
+$p=\sum p_{jk}z^jw^k$ and
+$q=D+q_{10}z+q_{01}w+q_{11}zw$. The Taylor coefficients of $f=p/q$ are
+$c_{jk}=v_{jk}/D^{j+k+1}$, where coefficients with negative indices vanish
+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\le28$, let
+
+$$
+n_{jk}=\left\lfloor
+\sqrt{(\operatorname{Re}v_{jk})^2+(\operatorname{Im}v_{jk})^2}
+\right\rfloor.
+$$
+
+With $R=302825279492$, $E=10^{12}$, and $N=28$, exact integer arithmetic
+checks
+
+$$
+A=\sum_{j,k=0}^{N}n_{jk}R^{j+k}(ED)^{2N-j-k},
+\qquad B=D(ED)^{2N},
+$$
+
+and
+
+$$
+10^{26}A>(10^{26}+1)B.
+$$
+
+Thus
+
+$$
+\sum_{j,k=0}^{28}\lvert c_{jk}\rvert(R/E)^{j+k}
+\ge \frac AB>1+10^{-26}.
+$$
+
+The left side is a continuous polynomial in the radius. It is therefore
+greater than one at some smaller positive radius. Radial monotonicity then
+excludes every larger radius from the admissible set, so its supremum is
+strictly below $R/E$.
+
+## Verification
+
+The two Python programs use independent coefficient algorithms. The first
+uses the triangular recurrence above; the second extracts coefficients of
+$1/q$ by a multinomial formula. They require Python 3.9 or later and only its
+standard library.
+
+```text
+python verify_gaussian_certificate.py
+python verify_multinomial_certificate.py
+```
+
+Both programs produce the same frozen certificate digests:
+
+```text
+sha256(A)                = f048ac2e8f00f62a2d3958a55f985b2271d9cc8e688cd0869f4df44e0b3f3c67
+sha256(B)                = 4bb5937ea8c3cfa784ec421a546a25d979bc67b8689854da1e2227c3b5c69e31
+sha256(A-B)              = 41125e30d4d1f11a7351daeb219a4e2f1ff85bd7e3d15382f76b67da2aee28b8
+sha256(strict slack)     = 0f0d7efd492c6b1ce53b3ce35a76de04dbfce9901bcb34ed38a8fe133ed2116e
+sha256(841 coefficients)= 3951d7ad8a9ce423db03a9ff0a036dac2b636c4e1b32551361b10de13559ca4c
+sha256(841 norm floors) = cef41ae7e5e6d82a2aa3f8e699e6fc415af0325596c52f9182579cfa8940de62
+```
+
+`FiniteCertificate.lean` verifies the 841 Gaussian-integer recurrences, every
+integer-square-root floor, the homogenized weighted sum, and the strict
+integer margin. `EndToEnd.lean` then proves the global norm-square identity,
+denominator nonvanishing, joint 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
+majorant is greater than one; and applies continuity and the supremal
+definition of the bidisc Bohr radius.
+
+The final formal statement is
+
+```text
+Optim.BohrRadius.bohrRadius_lt_302825279492_div_10pow12 :
+  bohrRadius < (302825279492 : ℝ) / 10 ^ 12
+```
+
+From this directory, run:
+
+```text
+lake exe cache get
+lake build
+```
+
+The Lean project pins Lean 4.19.0 and Mathlib commit
+`c44e0c8ee63ca166450922a373c7409c5d26b00b`. Both files compile without
+`sorry`, `admit`, or custom axioms. `#print axioms` reports
+`propext`, `Classical.choice`, `Lean.ofReduceBool`, and `Quot.sound` for the
+final theorem; `Lean.ofReduceBool` is the explicit trust boundary introduced
+by the finite `native_decide` checks.
+
+## AI assistance disclosure
+
+The mathematical construction, proof presentation, verification programs,
+Lean certificate, and repository submission were prepared with AI assistance.
+Shivam Patel supplied the contribution and reviewed the mathematical claim,
+references, and submitted information.

certificates/59a/patel-2026/SHA256SUMS

@@ -0,0 +1,8 @@
+aedfc3eb0f9e1a4720f3e2eff510d84755c7c1f5831eb26fb185ff9401b79571  FiniteCertificate.lean
+8f4cf0293df278100631a7df55d00fb8b90dbb750f2d7693cd0fc7c9611441ef  EndToEnd.lean
+9d4bc504ee57a92203792ff6f5acfb9ef23fd9ad2cbc1ebc78b600cd50ac6e24  verify_gaussian_certificate.py
+5fce9fe84e7074b4df8ee875a5c2f5a7be3d6a0caf25297d91f515bb1224d99c  verify_multinomial_certificate.py
+da8290a79bf0f7c93336768b6aba54d151587b8cf9321023c715d39f07f9caf3  README.md
+f304859f5a9f47e9b6ae92b811730d3cb45e5a024407753d1b44bd2f23703a1b  lakefile.toml
+370b7c5f900a7d004411ad51684dbe7bf8a131bf60853694793a13621c462ad1  lake-manifest.json
+55e97be96000b5e9e290c9e74482e5e317861499a5540353ce845471bded8cea  lean-toolchain