diff --git a/README.md b/README.md index 66d2de0..ab1f5b1 100644 --- a/README.md +++ b/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 diff --git a/certificates/59a/patel-2026/.gitignore b/certificates/59a/patel-2026/.gitignore new file mode 100644 index 0000000..e94a79f --- /dev/null +++ b/certificates/59a/patel-2026/.gitignore @@ -0,0 +1,3 @@ +/.lake/ +/*.olean +/*.ilean diff --git a/certificates/59a/patel-2026/EndToEnd.lean b/certificates/59a/patel-2026/EndToEnd.lean new file mode 100644 index 0000000..2bbc118 --- /dev/null +++ b/certificates/59a/patel-2026/EndToEnd.lean @@ -0,0 +1,1432 @@ +import FiniteCertificate +import Mathlib.Analysis.Analytic.Constructions +import Mathlib.Analysis.Analytic.Linear +import Mathlib.Analysis.Complex.AbsMax +import Mathlib.Analysis.Normed.Ring.InfiniteSum +import Mathlib.Analysis.SpecificLimits.Normed +import Mathlib.Tactic.FunProp + +/-! +# End-to-end certificate for the bidisc Bohr-radius upper bound + +This file closes the analytic and coefficient-identification gaps deliberately +left outside `FiniteCertificate.lean`. It proves that the Gaussian-integer +rectangle checked there is the Taylor rectangle of an explicit Schur function, +uses its certified norm floors to obtain a strict finite Bohr violation, and +deduces the strict upper bound `K₂ < 302825279492 / 10^12`. +-/ + +set_option maxRecDepth 10000 +set_option maxHeartbeats 8000000 + +open scoped BigOperators + +namespace Optim.BohrRadius + +/-- The open unit bidisc. -/ +def unitBidisc : Set (ℂ × ℂ) := + {p | ‖p.1‖ < 1 ∧ ‖p.2‖ < 1} + +/-- Analytic functions from the unit bidisc to the closed unit disc. -/ +def IsSchur (f : ℂ × ℂ → ℂ) : Prop := + AnalyticOn ℂ f unitBidisc ∧ + ∀ p ∈ unitBidisc, ‖f p‖ ≤ 1 + +/-- A family is the actual locally convergent Taylor germ of `f` at zero. -/ +def HasBidiscCoefficients (f : ℂ × ℂ → ℂ) + (coeff : ℕ → ℕ → ℂ) : Prop := + ∃ radius : ℝ, 0 < radius ∧ radius ≤ 1 ∧ + ∀ z w : ℂ, ‖z‖ < radius → ‖w‖ < radius → + HasSum (fun i : ℕ × ℕ => + coeff i.1 i.2 * z ^ i.1 * w ^ i.2) (f (z, w)) + +/-- Finite rectangular partial sums of the absolute Bohr series. -/ +noncomputable def finiteMajorant + (coeff : ℕ → ℕ → ℂ) (radius : ℝ) (N : ℕ) : ℝ := + ∑ j ∈ Finset.range (N + 1), + ∑ k ∈ Finset.range (N + 1), + ‖coeff j k‖ * radius ^ (j + k) + +def IsBohrAdmissible (radius : ℝ) : Prop := + ∀ (f : ℂ × ℂ → ℂ) (coeff : ℕ → ℕ → ℂ), + IsSchur f → HasBidiscCoefficients f coeff → + ∀ N : ℕ, finiteMajorant coeff radius N ≤ 1 + +/-- The bidisc Bohr radius, as the supremum of universally admissible radii. -/ +noncomputable def bohrRadius : ℝ := + sSup (insert 0 {radius : ℝ | 0 < radius ∧ IsBohrAdmissible radius}) + +theorem finiteMajorant_mono + (coeff : ℕ → ℕ → ℂ) (N : ℕ) + {r s : ℝ} (hr : 0 ≤ r) (hrs : r ≤ s) : + finiteMajorant coeff r N ≤ finiteMajorant coeff s N := by + unfold finiteMajorant + apply Finset.sum_le_sum + intro j hj + apply Finset.sum_le_sum + intro k hk + exact mul_le_mul_of_nonneg_left + (pow_le_pow_left₀ hr hrs (j + k)) (norm_nonneg (coeff j k)) + +theorem bohrRadius_le_of_finite_violation + {f : ℂ × ℂ → ℂ} {coeff : ℕ → ℕ → ℂ} + {radius : ℝ} {N : ℕ} + (hr : 0 ≤ radius) + (hf : IsSchur f) + (hcoeff : HasBidiscCoefficients f coeff) + (hviolation : 1 < finiteMajorant coeff radius N) : + bohrRadius ≤ radius := by + unfold bohrRadius + refine csSup_le ⟨0, Set.mem_insert _ _⟩ ?_ + intro s hs + rcases (Set.mem_insert_iff.mp hs) with hzero | hs + · simpa [hzero] using hr + · change 0 < s ∧ IsBohrAdmissible s at hs + by_contra hnot + have hrs : radius ≤ s := (lt_of_not_ge hnot).le + have hmono := finiteMajorant_mono coeff N hr hrs + have hadmissible := hs.2 f coeff hf hcoeff N + linarith + +theorem continuous_finiteMajorant (coeff : ℕ → ℕ → ℂ) (N : ℕ) : + Continuous (fun radius : ℝ => finiteMajorant coeff radius N) := by + unfold finiteMajorant + fun_prop + +/-- A strict finite violation gives a strict upper bound: continuity moves the +violation to a slightly smaller positive radius. -/ +theorem bohrRadius_lt_of_finite_violation + {f : ℂ × ℂ → ℂ} {coeff : ℕ → ℕ → ℂ} + {radius : ℝ} {N : ℕ} + (hr : 0 < radius) + (hf : IsSchur f) + (hcoeff : HasBidiscCoefficients f coeff) + (hviolation : 1 < finiteMajorant coeff radius N) : + bohrRadius < radius := by + have hopen : IsOpen {s : ℝ | 1 < finiteMajorant coeff s N} := + isOpen_lt continuous_const (continuous_finiteMajorant coeff N) + obtain ⟨ε, hε, hball⟩ := Metric.isOpen_iff.mp hopen radius hviolation + let δ : ℝ := min (radius / 2) (ε / 2) + have hδ : 0 < δ := lt_min (half_pos hr) (half_pos hε) + have hδr : δ < radius := lt_of_le_of_lt (min_le_left _ _) (half_lt_self hr) + have hδε : δ < ε := lt_of_le_of_lt (min_le_right _ _) (half_lt_self hε) + have hmem : radius - δ ∈ {s : ℝ | 1 < finiteMajorant coeff s N} := by + apply hball + rw [Metric.mem_ball, Real.dist_eq] + simp only [sub_sub_cancel_left, abs_neg, abs_of_pos hδ] + exact hδε + have hle := bohrRadius_le_of_finite_violation + (f := f) (coeff := coeff) (radius := radius - δ) (N := N) + (sub_nonneg.mpr hδr.le) hf hcoeff hmem + linarith + +end Optim.BohrRadius + +namespace Optim.BohrRadius + +/-- Taylor recurrence for a general bidegree-`(1,1)` rational function. -/ +noncomputable def recurrentCoefficient + (a c d e₀₀ e₁₀ e₀₁ e₁₁ : ℂ) : ℕ → ℕ → ℂ + | 0, 0 => e₀₀ + | j + 1, 0 => + a * recurrentCoefficient a c d e₀₀ e₁₀ e₀₁ e₁₁ j 0 + + if j = 0 then e₁₀ else 0 + | 0, k + 1 => + c * recurrentCoefficient a c d e₀₀ e₁₀ e₀₁ e₁₁ 0 k + + if k = 0 then e₀₁ else 0 + | j + 1, k + 1 => + a * recurrentCoefficient a c d e₀₀ e₁₀ e₀₁ e₁₁ j (k + 1) + + c * recurrentCoefficient a c d e₀₀ e₁₀ e₀₁ e₁₁ (j + 1) k - + d * recurrentCoefficient a c d e₀₀ e₁₀ e₀₁ e₁₁ j k + + if j = 0 ∧ k = 0 then e₁₁ else 0 +termination_by j k => j + k +decreasing_by all_goals omega + +theorem recurrentCoefficient_norm_le + {a c d e₀₀ e₁₀ e₀₁ e₁₁ : ℂ} + (ha : ‖a‖ ≤ 1) (hc : ‖c‖ ≤ 1) (hd : ‖d‖ ≤ 1) + (he₀₀ : ‖e₀₀‖ ≤ 1) (he₁₀ : ‖e₁₀‖ ≤ 1) + (he₀₁ : ‖e₀₁‖ ≤ 1) (he₁₁ : ‖e₁₁‖ ≤ 1) + (j k : ℕ) : + ‖recurrentCoefficient a c d e₀₀ e₁₀ e₀₁ e₁₁ j k‖ ≤ + (8 : ℝ) ^ (j + k) := by + have main : ∀ n : ℕ, ∀ j k : ℕ, j + k = n → + ‖recurrentCoefficient a c d e₀₀ e₁₀ e₀₁ e₁₁ j k‖ ≤ + (8 : ℝ) ^ (j + k) := by + intro n + induction n using Nat.strong_induction_on with + | h n ih => + intro j k hjk + cases j with + | zero => + cases k with + | zero => simpa [recurrentCoefficient] using he₀₀ + | succ k => + have hk := ih k (by omega) 0 k (by omega) + have hk' : + ‖recurrentCoefficient a c d e₀₀ e₁₀ e₀₁ e₁₁ 0 k‖ ≤ + (8 : ℝ) ^ k := by simpa using hk + have hs : ‖if k = 0 then e₀₁ else 0‖ ≤ 1 := by + split_ifs <;> simp_all + have hm : + ‖c * recurrentCoefficient a c d e₀₀ e₁₀ e₀₁ e₁₁ 0 k‖ ≤ + (8 : ℝ) ^ k := by + rw [norm_mul] + calc + ‖c‖ * ‖recurrentCoefficient a c d e₀₀ e₁₀ e₀₁ e₁₁ 0 k‖ + ≤ 1 * (8 : ℝ) ^ k := by gcongr + _ = (8 : ℝ) ^ k := one_mul _ + rw [recurrentCoefficient] + change + ‖c * recurrentCoefficient a c d e₀₀ e₁₀ e₀₁ e₁₁ 0 k + + (if k = 0 then e₀₁ else 0)‖ ≤ (8 : ℝ) ^ (0 + (k + 1)) + have htriangle := norm_add_le + (c * recurrentCoefficient a c d e₀₀ e₁₀ e₀₁ e₁₁ 0 k) + (if k = 0 then e₀₁ else 0) + have hp : 1 ≤ (8 : ℝ) ^ k := one_le_pow₀ (by norm_num) + simp only [zero_add, pow_succ] + nlinarith + | succ j => + cases k with + | zero => + have hj := ih j (by omega) j 0 (by omega) + have hj' : + ‖recurrentCoefficient a c d e₀₀ e₁₀ e₀₁ e₁₁ j 0‖ ≤ + (8 : ℝ) ^ j := by simpa using hj + have hs : ‖if j = 0 then e₁₀ else 0‖ ≤ 1 := by + split_ifs <;> simp_all + have hm : + ‖a * recurrentCoefficient a c d e₀₀ e₁₀ e₀₁ e₁₁ j 0‖ ≤ + (8 : ℝ) ^ j := by + rw [norm_mul] + calc + ‖a‖ * ‖recurrentCoefficient a c d e₀₀ e₁₀ e₀₁ e₁₁ j 0‖ + ≤ 1 * (8 : ℝ) ^ j := by gcongr + _ = (8 : ℝ) ^ j := one_mul _ + rw [recurrentCoefficient] + change + ‖a * recurrentCoefficient a c d e₀₀ e₁₀ e₀₁ e₁₁ j 0 + + (if j = 0 then e₁₀ else 0)‖ ≤ (8 : ℝ) ^ (j + 1 + 0) + have htriangle := norm_add_le + (a * recurrentCoefficient a c d e₀₀ e₁₀ e₀₁ e₁₁ j 0) + (if j = 0 then e₁₀ else 0) + have hp : 1 ≤ (8 : ℝ) ^ j := one_le_pow₀ (by norm_num) + simp only [add_zero, pow_succ] + nlinarith + | succ k => + have h₁ := ih (j + (k + 1)) (by omega) j (k + 1) rfl + have h₂ := ih ((j + 1) + k) (by omega) (j + 1) k rfl + have h₃ := ih (j + k) (by omega) j k rfl + have hs : ‖if j = 0 ∧ k = 0 then e₁₁ else 0‖ ≤ 1 := by + split_ifs <;> simp_all + have hm₁ : + ‖a * recurrentCoefficient a c d e₀₀ e₁₀ e₀₁ e₁₁ j (k + 1)‖ ≤ + (8 : ℝ) ^ (j + k + 1) := by + rw [norm_mul] + calc + ‖a‖ * ‖recurrentCoefficient a c d e₀₀ e₁₀ e₀₁ e₁₁ j (k + 1)‖ + ≤ 1 * (8 : ℝ) ^ (j + (k + 1)) := by gcongr + _ = (8 : ℝ) ^ (j + k + 1) := by simp [add_assoc] + have hm₂ : + ‖c * recurrentCoefficient a c d e₀₀ e₁₀ e₀₁ e₁₁ (j + 1) k‖ ≤ + (8 : ℝ) ^ (j + k + 1) := by + rw [norm_mul] + calc + ‖c‖ * ‖recurrentCoefficient a c d e₀₀ e₁₀ e₀₁ e₁₁ (j + 1) k‖ + ≤ 1 * (8 : ℝ) ^ ((j + 1) + k) := by gcongr + _ = (8 : ℝ) ^ (j + k + 1) := by + simp [add_assoc, add_left_comm, add_comm] + have hm₃ : + ‖d * recurrentCoefficient a c d e₀₀ e₁₀ e₀₁ e₁₁ j k‖ ≤ + (8 : ℝ) ^ (j + k) := by + rw [norm_mul] + calc + ‖d‖ * ‖recurrentCoefficient a c d e₀₀ e₁₀ e₀₁ e₁₁ j k‖ + ≤ 1 * (8 : ℝ) ^ (j + k) := by gcongr + _ = (8 : ℝ) ^ (j + k) := one_mul _ + rw [recurrentCoefficient] + change + ‖a * recurrentCoefficient a c d e₀₀ e₁₀ e₀₁ e₁₁ j (k + 1) + + c * recurrentCoefficient a c d e₀₀ e₁₀ e₀₁ e₁₁ (j + 1) k - + d * recurrentCoefficient a c d e₀₀ e₁₀ e₀₁ e₁₁ j k + + (if j = 0 ∧ k = 0 then e₁₁ else 0)‖ ≤ + (8 : ℝ) ^ ((j + 1) + (k + 1)) + have ht₁ := norm_add_le + (a * recurrentCoefficient a c d e₀₀ e₁₀ e₀₁ e₁₁ j (k + 1)) + (c * recurrentCoefficient a c d e₀₀ e₁₀ e₀₁ e₁₁ (j + 1) k) + have ht₂ := norm_sub_le + (a * recurrentCoefficient a c d e₀₀ e₁₀ e₀₁ e₁₁ j (k + 1) + + c * recurrentCoefficient a c d e₀₀ e₁₀ e₀₁ e₁₁ (j + 1) k) + (d * recurrentCoefficient a c d e₀₀ e₁₀ e₀₁ e₁₁ j k) + have ht₃ := norm_add_le + (a * recurrentCoefficient a c d e₀₀ e₁₀ e₀₁ e₁₁ j (k + 1) + + c * recurrentCoefficient a c d e₀₀ e₁₀ e₀₁ e₁₁ (j + 1) k - + d * recurrentCoefficient a c d e₀₀ e₁₀ e₀₁ e₁₁ j k) + (if j = 0 ∧ k = 0 then e₁₁ else 0) + have hp : 1 ≤ (8 : ℝ) ^ (j + k) := one_le_pow₀ (by norm_num) + have hp₁ : (8 : ℝ) ^ (j + k + 1) = + (8 : ℝ) ^ (j + k) * 8 := by rw [pow_succ] + have hp₂ : (8 : ℝ) ^ ((j + 1) + (k + 1)) = + (8 : ℝ) ^ (j + k) * 8 * 8 := by + rw [show (j + 1) + (k + 1) = (j + k + 1) + 1 by omega, + pow_succ, pow_succ] + nlinarith + exact main (j + k) j k rfl + +theorem recurrentCoefficient_summable + {a c d e₀₀ e₁₀ e₀₁ e₁₁ : ℂ} + (ha : ‖a‖ ≤ 1) (hc : ‖c‖ ≤ 1) (hd : ‖d‖ ≤ 1) + (he₀₀ : ‖e₀₀‖ ≤ 1) (he₁₀ : ‖e₁₀‖ ≤ 1) + (he₀₁ : ‖e₀₁‖ ≤ 1) (he₁₁ : ‖e₁₁‖ ≤ 1) + {z w : ℂ} (hz : ‖z‖ < (1 / 8 : ℝ)) (hw : ‖w‖ < (1 / 8 : ℝ)) : + Summable (fun i : ℕ × ℕ => + recurrentCoefficient a c d e₀₀ e₁₀ e₀₁ e₁₁ i.1 i.2 * + z ^ i.1 * w ^ i.2) := by + have hz₀ : 0 ≤ 8 * ‖z‖ := mul_nonneg (by norm_num) (norm_nonneg z) + have hw₀ : 0 ≤ 8 * ‖w‖ := mul_nonneg (by norm_num) (norm_nonneg w) + have hz₁ : 8 * ‖z‖ < 1 := by norm_num at hz ⊢; linarith + have hw₁ : 8 * ‖w‖ < 1 := by norm_num at hw ⊢; linarith + have hzg : Summable (fun j : ℕ => (8 * ‖z‖) ^ j) := + summable_geometric_of_lt_one hz₀ hz₁ + have hwg : Summable (fun k : ℕ => (8 * ‖w‖) ^ k) := + summable_geometric_of_lt_one hw₀ hw₁ + have hbound : Summable + (fun i : ℕ × ℕ => (8 * ‖z‖) ^ i.1 * (8 * ‖w‖) ^ i.2) := + hzg.mul_of_nonneg hwg + (fun _ => pow_nonneg hz₀ _) (fun _ => pow_nonneg hw₀ _) + refine Summable.of_norm_bounded _ hbound ?_ + intro i + rw [norm_mul, norm_mul, norm_pow, norm_pow] + calc + ‖recurrentCoefficient a c d e₀₀ e₁₀ e₀₁ e₁₁ i.1 i.2‖ * + ‖z‖ ^ i.1 * ‖w‖ ^ i.2 ≤ + (8 : ℝ) ^ (i.1 + i.2) * ‖z‖ ^ i.1 * ‖w‖ ^ i.2 := by + gcongr + exact recurrentCoefficient_norm_le ha hc hd he₀₀ he₁₀ he₀₁ he₁₁ _ _ + _ = (8 * ‖z‖) ^ i.1 * (8 * ‖w‖) ^ i.2 := by + rw [pow_add, mul_pow, mul_pow] + ring + +noncomputable def shiftFirstSeries (A : ℂ) (f : ℕ × ℕ → ℂ) + (i : ℕ × ℕ) : ℂ := + if i.1 = 0 then 0 else A * f (i.1 - 1, i.2) + +noncomputable def shiftSecondSeries (A : ℂ) (f : ℕ × ℕ → ℂ) + (i : ℕ × ℕ) : ℂ := + if i.2 = 0 then 0 else A * f (i.1, i.2 - 1) + +theorem hasSum_shiftFirstSeries + {f : ℕ × ℕ → ℂ} {s : ℂ} (hf : HasSum f s) (A : ℂ) : + HasSum (shiftFirstSeries A f) (A * s) := by + let emb : ℕ × ℕ → ℕ × ℕ := fun i => (i.1 + 1, i.2) + have hinj : Function.Injective emb := by + intro i j h + simpa [emb, Prod.ext_iff] using h + have hout : ∀ i : ℕ × ℕ, i ∉ Set.range emb → + shiftFirstSeries A f i = 0 := by + rintro ⟨j, k⟩ hnot + by_cases hj : j = 0 + · simp [shiftFirstSeries, hj] + · exfalso + apply hnot + refine ⟨(j - 1, k), ?_⟩ + simp [emb, Nat.sub_add_cancel (Nat.one_le_iff_ne_zero.mpr hj)] + apply (hinj.hasSum_iff hout).mp + refine (hf.mul_left A).congr_fun ?_ + intro i + simp [Function.comp_def, emb, shiftFirstSeries] + +theorem hasSum_shiftSecondSeries + {f : ℕ × ℕ → ℂ} {s : ℂ} (hf : HasSum f s) (A : ℂ) : + HasSum (shiftSecondSeries A f) (A * s) := by + let emb : ℕ × ℕ → ℕ × ℕ := fun i => (i.1, i.2 + 1) + have hinj : Function.Injective emb := by + intro i j h + simpa [emb, Prod.ext_iff] using h + have hout : ∀ i : ℕ × ℕ, i ∉ Set.range emb → + shiftSecondSeries A f i = 0 := by + rintro ⟨j, k⟩ hnot + by_cases hk : k = 0 + · simp [shiftSecondSeries, hk] + · exfalso + apply hnot + refine ⟨(j, k - 1), ?_⟩ + simp [emb, Nat.sub_add_cancel (Nat.one_le_iff_ne_zero.mpr hk)] + apply (hinj.hasSum_iff hout).mp + refine (hf.mul_left A).congr_fun ?_ + intro i + simp [Function.comp_def, emb, shiftSecondSeries] + +noncomputable def recurrentTerm + (a c d e₀₀ e₁₀ e₀₁ e₁₁ z w : ℂ) (i : ℕ × ℕ) : ℂ := + recurrentCoefficient a c d e₀₀ e₁₀ e₀₁ e₁₁ i.1 i.2 * + z ^ i.1 * w ^ i.2 + +noncomputable def recurrentSourceSeries + (e₀₀ e₁₀ e₀₁ e₁₁ z w : ℂ) (i : ℕ × ℕ) : ℂ := + (if i = (0, 0) then e₀₀ else 0) + + (if i = (1, 0) then e₁₀ * z else 0) + + (if i = (0, 1) then e₀₁ * w else 0) + + (if i = (1, 1) then e₁₁ * z * w else 0) + +theorem recurrent_shift_equation + (a c d e₀₀ e₁₀ e₀₁ e₁₁ z w : ℂ) (i : ℕ × ℕ) : + recurrentTerm a c d e₀₀ e₁₀ e₀₁ e₁₁ z w i - + shiftFirstSeries (a * z) + (recurrentTerm a c d e₀₀ e₁₀ e₀₁ e₁₁ z w) i - + shiftSecondSeries (c * w) + (recurrentTerm a c d e₀₀ e₁₀ e₀₁ e₁₁ z w) i + + shiftFirstSeries 1 + (shiftSecondSeries (d * z * w) + (recurrentTerm a c d e₀₀ e₁₀ e₀₁ e₁₁ z w)) i = + recurrentSourceSeries e₀₀ e₁₀ e₀₁ e₁₁ z w i := by + rcases i with ⟨j, k⟩ + cases j with + | zero => + cases k with + | zero => simp [recurrentTerm, recurrentCoefficient, + shiftFirstSeries, shiftSecondSeries, recurrentSourceSeries, + Prod.ext_iff] + | succ k => + simp [recurrentTerm, recurrentCoefficient, shiftFirstSeries, + shiftSecondSeries, recurrentSourceSeries, pow_succ, Prod.ext_iff] + split_ifs <;> simp_all <;> ring + | succ j => + cases k with + | zero => + simp [recurrentTerm, recurrentCoefficient, shiftFirstSeries, + shiftSecondSeries, recurrentSourceSeries, pow_succ, Prod.ext_iff] + split_ifs <;> simp_all <;> ring + | succ k => + simp [recurrentTerm, recurrentCoefficient, shiftFirstSeries, + shiftSecondSeries, recurrentSourceSeries, pow_succ, Prod.ext_iff] + split_ifs <;> simp_all <;> ring + +theorem recurrentSourceSeries_hasSum + (e₀₀ e₁₀ e₀₁ e₁₁ z w : ℂ) : + HasSum (recurrentSourceSeries e₀₀ e₁₀ e₀₁ e₁₁ z w) + (e₀₀ + e₁₀ * z + e₀₁ * w + e₁₁ * z * w) := by + have h₀₀ := hasSum_ite_eq ((0, 0) : ℕ × ℕ) e₀₀ + have h₁₀ := hasSum_ite_eq ((1, 0) : ℕ × ℕ) (e₁₀ * z) + have h₀₁ := hasSum_ite_eq ((0, 1) : ℕ × ℕ) (e₀₁ * w) + have h₁₁ := hasSum_ite_eq ((1, 1) : ℕ × ℕ) (e₁₁ * z * w) + exact ((h₀₀.add h₁₀).add h₀₁).add h₁₁ + +theorem recurrentCoefficient_generating_identity + {a c d e₀₀ e₁₀ e₀₁ e₁₁ : ℂ} + (ha : ‖a‖ ≤ 1) (hc : ‖c‖ ≤ 1) (hd : ‖d‖ ≤ 1) + (he₀₀ : ‖e₀₀‖ ≤ 1) (he₁₀ : ‖e₁₀‖ ≤ 1) + (he₀₁ : ‖e₀₁‖ ≤ 1) (he₁₁ : ‖e₁₁‖ ≤ 1) + {z w : ℂ} (hz : ‖z‖ < (1 / 8 : ℝ)) (hw : ‖w‖ < (1 / 8 : ℝ)) : + (1 - a * z - c * w + d * z * w) * + (∑' i : ℕ × ℕ, + recurrentTerm a c d e₀₀ e₁₀ e₀₁ e₁₁ z w i) = + e₀₀ + e₁₀ * z + e₀₁ * w + e₁₁ * z * w := by + let f := recurrentTerm a c d e₀₀ e₁₀ e₀₁ e₁₁ z w + have hs : Summable f := recurrentCoefficient_summable + ha hc hd he₀₀ he₁₀ he₀₁ he₁₁ hz hw + have hbase : HasSum f (∑' i : ℕ × ℕ, f i) := hs.hasSum + have hfirst := hasSum_shiftFirstSeries hbase (a * z) + have hsecond := hasSum_shiftSecondSeries hbase (c * w) + have hmixed : + HasSum (shiftFirstSeries 1 (shiftSecondSeries (d * z * w) f)) + ((d * z * w) * (∑' i : ℕ × ℕ, f i)) := by + simpa using hasSum_shiftFirstSeries + (hasSum_shiftSecondSeries hbase (d * z * w)) 1 + have hcombined := ((hbase.sub hfirst).sub hsecond).add hmixed + have hsource := recurrentSourceSeries_hasSum e₀₀ e₁₀ e₀₁ e₁₁ z w + have hpoint : ∀ i : ℕ × ℕ, + recurrentSourceSeries e₀₀ e₁₀ e₀₁ e₁₁ z w i = + f i - shiftFirstSeries (a * z) f i - + shiftSecondSeries (c * w) f i + + shiftFirstSeries 1 (shiftSecondSeries (d * z * w) f) i := by + intro i + exact (recurrent_shift_equation a c d e₀₀ e₁₀ e₀₁ e₁₁ z w i).symm + have hidentity := hcombined.unique + (hsource.congr_fun (fun i => (hpoint i).symm)) + change + (1 - a * z - c * w + d * z * w) * (∑' i : ℕ × ℕ, f i) = + e₀₀ + e₁₀ * z + e₀₁ * w + e₁₁ * z * w + linear_combination hidentity + +end Optim.BohrRadius + +namespace BidiscPhaseCertificate + +/-- The two bilinear forms used by the certified witness. -/ +def analyticU (z w : ℂ) : ℂ := (1 + z) * (1 - w) + +def analyticV (z w : ℂ) : ℂ := 1 + z * w + +def analyticP (l t : ℝ) (z w : ℂ) : ℂ := + (l : ℂ) * analyticU z w + Complex.I * (t : ℂ) * analyticV z w + +def analyticQ (l t : ℝ) (z w : ℂ) : ℂ := + (l : ℂ) * analyticV z w + Complex.I * (t : ℂ) * analyticU z w + +def analyticNumerator (l t s : ℝ) (z w : ℂ) : ℂ := + (s : ℂ) * analyticQ l t z w - analyticP l t z w + +def analyticDenominator (l t s : ℝ) (z w : ℂ) : ℂ := + (s : ℂ) * analyticQ l t z w + analyticP l t z w + +noncomputable def analyticWitness (l t s : ℝ) (z w : ℂ) : ℂ := + analyticNumerator l t s z w / analyticDenominator l t s z w + +/-- Exact global squared-norm identity underlying the Schur estimate. -/ +theorem analytic_normSq_gap (l t s : ℝ) (z w : ℂ) : + Complex.normSq (analyticDenominator l t s z w) - + Complex.normSq (analyticNumerator l t s z w) = + 2 * s * (l ^ 2 + t ^ 2) * + ((1 - Complex.normSq w) * Complex.normSq (1 + z) + + (1 - Complex.normSq z) * Complex.normSq (1 - w)) := by + simp [analyticDenominator, analyticNumerator, analyticP, analyticQ, + analyticU, analyticV, Complex.normSq_apply] + ring + +theorem analytic_normSq_gap_pos {l t s : ℝ} + (hs : 0 < s) (hlt : 0 < l ^ 2 + t ^ 2) + {z w : ℂ} (hz : ‖z‖ < 1) (hw : ‖w‖ < 1) : + 0 < Complex.normSq (analyticDenominator l t s z w) - + Complex.normSq (analyticNumerator l t s z w) := by + rw [analytic_normSq_gap] + have hz_sq : 0 < 1 - Complex.normSq z := by + rw [Complex.normSq_eq_norm_sq] + nlinarith [norm_nonneg z] + have hw_sq : 0 < 1 - Complex.normSq w := by + rw [Complex.normSq_eq_norm_sq] + nlinarith [norm_nonneg w] + have hz_add_ne : 1 + z ≠ 0 := by + intro hzero + have hzneg : z = -1 := by linear_combination hzero + rw [hzneg] at hz + norm_num at hz + have hfirst : + 0 < (1 - Complex.normSq w) * Complex.normSq (1 + z) := + mul_pos hw_sq (Complex.normSq_pos.mpr hz_add_ne) + have hsecond : + 0 ≤ (1 - Complex.normSq z) * Complex.normSq (1 - w) := + mul_nonneg hz_sq.le (Complex.normSq_nonneg _) + have hbracket : + 0 < (1 - Complex.normSq w) * Complex.normSq (1 + z) + + (1 - Complex.normSq z) * Complex.normSq (1 - w) := + add_pos_of_pos_of_nonneg hfirst hsecond + positivity + +theorem analyticDenominator_ne_zero {l t s : ℝ} + (hs : 0 < s) (hlt : 0 < l ^ 2 + t ^ 2) + {z w : ℂ} (hz : ‖z‖ < 1) (hw : ‖w‖ < 1) : + analyticDenominator l t s z w ≠ 0 := by + intro hzero + have hgap := analytic_normSq_gap_pos hs hlt hz hw + rw [hzero, Complex.normSq_zero] at hgap + nlinarith [Complex.normSq_nonneg (analyticNumerator l t s z w)] + +theorem analyticWitness_norm_lt_one {l t s : ℝ} + (hs : 0 < s) (hlt : 0 < l ^ 2 + t ^ 2) + {z w : ℂ} (hz : ‖z‖ < 1) (hw : ‖w‖ < 1) : + ‖analyticWitness l t s z w‖ < 1 := by + have hgap := analytic_normSq_gap_pos hs hlt hz hw + have hnorm : + ‖analyticNumerator l t s z w‖ < + ‖analyticDenominator l t s z w‖ := by + rw [Complex.normSq_eq_norm_sq, Complex.normSq_eq_norm_sq] at hgap + nlinarith [norm_nonneg (analyticNumerator l t s z w), + norm_nonneg (analyticDenominator l t s z w)] + have hden := analyticDenominator_ne_zero hs hlt hz hw + rw [analyticWitness, Complex.norm_div] + exact (div_lt_one (norm_pos_iff.mpr hden)).mpr hnorm + +theorem analyticWitness_analyticOn {l t s : ℝ} + (hs : 0 < s) (hlt : 0 < l ^ 2 + t ^ 2) : + AnalyticOn ℂ (fun p : ℂ × ℂ => analyticWitness l t s p.1 p.2) + Optim.BohrRadius.unitBidisc := by + intro p hp + change ‖p.1‖ < 1 ∧ ‖p.2‖ < 1 at hp + have hfirst : AnalyticAt ℂ (fun v : ℂ × ℂ => v.1) p := analyticAt_fst + have hsecond : AnalyticAt ℂ (fun v : ℂ × ℂ => v.2) p := analyticAt_snd + have hu : AnalyticAt ℂ + (fun v : ℂ × ℂ => analyticU v.1 v.2) p := by + unfold analyticU + exact ((analyticAt_const (v := (1 : ℂ))).fun_add hfirst).fun_mul + ((analyticAt_const (v := (1 : ℂ))).fun_sub hsecond) + have hv : AnalyticAt ℂ + (fun v : ℂ × ℂ => analyticV v.1 v.2) p := by + unfold analyticV + exact (analyticAt_const (v := (1 : ℂ))).fun_add (hfirst.fun_mul hsecond) + have hP : AnalyticAt ℂ + (fun v : ℂ × ℂ => analyticP l t v.1 v.2) p := by + unfold analyticP + exact ((analyticAt_const (v := (l : ℂ))).fun_mul hu).fun_add + ((analyticAt_const (v := Complex.I * (t : ℂ))).fun_mul hv) + have hQ : AnalyticAt ℂ + (fun v : ℂ × ℂ => analyticQ l t v.1 v.2) p := by + unfold analyticQ + exact ((analyticAt_const (v := (l : ℂ))).fun_mul hv).fun_add + ((analyticAt_const (v := Complex.I * (t : ℂ))).fun_mul hu) + have hn : AnalyticAt ℂ + (fun v : ℂ × ℂ => analyticNumerator l t s v.1 v.2) p := by + unfold analyticNumerator + exact ((analyticAt_const (v := (s : ℂ))).fun_mul hQ).fun_sub hP + have hd : AnalyticAt ℂ + (fun v : ℂ × ℂ => analyticDenominator l t s v.1 v.2) p := by + unfold analyticDenominator + exact ((analyticAt_const (v := (s : ℂ))).fun_mul hQ).fun_add hP + exact (hn.fun_div hd + (analyticDenominator_ne_zero hs hlt hp.1 hp.2)).analyticWithinAt + +/-- The concrete rational function used by the certificate. -/ +noncomputable def certifiedWitness (p : ℂ × ℂ) : ℂ := + analyticWitness (L : ℝ) (T : ℝ) (S : ℝ) p.1 p.2 + +theorem certifiedWitness_isSchur : + Optim.BohrRadius.IsSchur certifiedWitness := by + have hs : (0 : ℝ) < (S : ℝ) := by norm_num [S] + have hlt : (0 : ℝ) < (L : ℝ) ^ 2 + (T : ℝ) ^ 2 := by + norm_num [L, T] + refine ⟨analyticWitness_analyticOn hs hlt, ?_⟩ + intro p hp + exact (analyticWitness_norm_lt_one hs hlt hp.1 hp.2).le + +end BidiscPhaseCertificate + + + +namespace Optim.BohrRadius + +/-- A normalized complex bidegree-`(1,1)` rational function. -/ +noncomputable def complexBidegreeRational + (q₁₀ q₀₁ q₁₁ p₀₀ p₁₀ p₀₁ p₁₁ : ℂ) + (x : ℂ × ℂ) : ℂ := + (p₀₀ + p₁₀ * x.1 + p₀₁ * x.2 + p₁₁ * x.1 * x.2) / + (1 + q₁₀ * x.1 + q₀₁ * x.2 + q₁₁ * x.1 * x.2) + +/-- The recurrence is the actual Taylor germ of the normalized rational +function, not merely a formal or finite recurrence. -/ +theorem complexBidegreeRational_recurrent_hasBidiscCoefficients + {q₁₀ q₀₁ q₁₁ p₀₀ p₁₀ p₀₁ p₁₁ : ℂ} + (hq₁₀ : ‖q₁₀‖ ≤ 1) (hq₀₁ : ‖q₀₁‖ ≤ 1) (hq₁₁ : ‖q₁₁‖ ≤ 1) + (hp₀₀ : ‖p₀₀‖ ≤ 1) (hp₁₀ : ‖p₁₀‖ ≤ 1) + (hp₀₁ : ‖p₀₁‖ ≤ 1) (hp₁₁ : ‖p₁₁‖ ≤ 1) + (hden : ∀ z w : ℂ, ‖z‖ < (1 / 8 : ℝ) → ‖w‖ < (1 / 8 : ℝ) → + 1 + q₁₀ * z + q₀₁ * w + q₁₁ * z * w ≠ 0) : + HasBidiscCoefficients + (complexBidegreeRational q₁₀ q₀₁ q₁₁ p₀₀ p₁₀ p₀₁ p₁₁) + (recurrentCoefficient (-q₁₀) (-q₀₁) q₁₁ p₀₀ p₁₀ p₀₁ p₁₁) := by + refine ⟨(1 / 8 : ℝ), by norm_num, by norm_num, ?_⟩ + intro z w hz hw + have hmq₁₀ : ‖-q₁₀‖ ≤ 1 := by simpa using hq₁₀ + have hmq₀₁ : ‖-q₀₁‖ ≤ 1 := by simpa using hq₀₁ + have hs := recurrentCoefficient_summable + hmq₁₀ hmq₀₁ hq₁₁ hp₀₀ hp₁₀ hp₀₁ hp₁₁ hz hw + have hgen := recurrentCoefficient_generating_identity + hmq₁₀ hmq₀₁ hq₁₁ hp₀₀ hp₁₀ hp₀₁ hp₁₁ hz hw + have hvalue : + (∑' i : ℕ × ℕ, + recurrentTerm (-q₁₀) (-q₀₁) q₁₁ + p₀₀ p₁₀ p₀₁ p₁₁ z w i) = + complexBidegreeRational q₁₀ q₀₁ q₁₁ p₀₀ p₁₀ p₀₁ p₁₁ (z, w) := by + unfold complexBidegreeRational + apply (eq_div_iff (hden z w hz hw)).2 + linear_combination hgen + simp only [recurrentTerm] at hvalue + have hsum := hs.hasSum + rw [hvalue] at hsum + simpa using hsum + +noncomputable def complexBidegreeRecurrenceValue + (a c d p₀₀ p₁₀ p₀₁ p₁₁ : ℂ) + (v : ℕ → ℕ → ℂ) (j k : ℕ) : ℂ := + (if 0 < j then a * v (j - 1) k else 0) + + (if 0 < k then c * v j (k - 1) else 0) - + (if 0 < j ∧ 0 < k then d * v (j - 1) (k - 1) else 0) + + (if j = 0 ∧ k = 0 then p₀₀ + else if j = 1 ∧ k = 0 then p₁₀ + else if j = 0 ∧ k = 1 then p₀₁ + else if j = 1 ∧ k = 1 then p₁₁ + else 0) + +theorem recurrentCoefficient_eq_complexBidegreeRecurrenceValue + (a c d p₀₀ p₁₀ p₀₁ p₁₁ : ℂ) (j k : ℕ) : + recurrentCoefficient a c d p₀₀ p₁₀ p₀₁ p₁₁ j k = + complexBidegreeRecurrenceValue a c d p₀₀ p₁₀ p₀₁ p₁₁ + (recurrentCoefficient a c d p₀₀ p₁₀ p₀₁ p₁₁) j k := by + cases j with + | zero => + cases k with + | zero => simp [recurrentCoefficient, complexBidegreeRecurrenceValue] + | succ k => simp [recurrentCoefficient, complexBidegreeRecurrenceValue] + | succ j => + cases k with + | zero => simp [recurrentCoefficient, complexBidegreeRecurrenceValue] + | succ k => simp [recurrentCoefficient, complexBidegreeRecurrenceValue] + +theorem complexBidegreeRecurrence_unique_on_rectangle + (a c d p₀₀ p₁₀ p₀₁ p₁₁ : ℂ) (N : ℕ) + (v₁ v₂ : ℕ → ℕ → ℂ) + (h₁ : ∀ j k : ℕ, j < N → k < N → + v₁ j k = complexBidegreeRecurrenceValue a c d p₀₀ p₁₀ p₀₁ p₁₁ v₁ j k) + (h₂ : ∀ j k : ℕ, j < N → k < N → + v₂ j k = complexBidegreeRecurrenceValue a c d p₀₀ p₁₀ p₀₁ p₁₁ v₂ j k) : + ∀ j k : ℕ, j < N → k < N → v₁ j k = v₂ j k := by + intro j k hj hk + have hgeneral : ∀ n : ℕ, ∀ j k : ℕ, + j + k = n → j < N → k < N → v₁ j k = v₂ j k := by + intro n + induction n using Nat.strong_induction_on with + | h n ih => + intro j k hn hj hk + rw [h₁ j k hj hk, h₂ j k hj hk] + unfold complexBidegreeRecurrenceValue + have hfirst : + (if 0 < j then a * v₁ (j - 1) k else 0) = + (if 0 < j then a * v₂ (j - 1) k else 0) := by + split_ifs with hpos + · congr 1 + apply ih ((j - 1) + k) (by omega) (j - 1) k rfl (by omega) hk + · rfl + have hsecond : + (if 0 < k then c * v₁ j (k - 1) else 0) = + (if 0 < k then c * v₂ j (k - 1) else 0) := by + split_ifs with hpos + · congr 1 + apply ih (j + (k - 1)) (by omega) j (k - 1) rfl hj (by omega) + · rfl + have hmixed : + (if 0 < j ∧ 0 < k then d * v₁ (j - 1) (k - 1) else 0) = + (if 0 < j ∧ 0 < k then d * v₂ (j - 1) (k - 1) else 0) := by + split_ifs with hpos + · congr 1 + apply ih ((j - 1) + (k - 1)) (by omega) + (j - 1) (k - 1) rfl (by omega) (by omega) + · rfl + rw [hfirst, hsecond, hmixed] + exact hgeneral (j + k) j k rfl hj hk + +end Optim.BohrRadius + +namespace BidiscPhaseCertificate + +/-- Canonical embedding of the arithmetic certificate's Gaussian integers. -/ +noncomputable def gaussianCast (v : Gaussian) : ℂ := + (v.1 : ℂ) + (v.2 : ℂ) * Complex.I + +@[simp] theorem gaussianCast_zero : gaussianCast (0, 0) = 0 := by + simp [gaussianCast] + +@[simp] theorem gaussianCast_ofNat_zero : gaussianCast (0 : Gaussian) = 0 := by + change gaussianCast (0, 0) = 0 + exact gaussianCast_zero + +@[simp] theorem gaussianCast_gadd (a b : Gaussian) : + gaussianCast (gadd a b) = gaussianCast a + gaussianCast b := by + apply Complex.ext <;> simp [gaussianCast, gadd] + +@[simp] theorem gaussianCast_gneg (a : Gaussian) : + gaussianCast (gneg a) = -gaussianCast a := by + apply Complex.ext <;> simp [gaussianCast, gneg] + +@[simp] theorem gaussianCast_gmul (a b : Gaussian) : + gaussianCast (gmul a b) = gaussianCast a * gaussianCast b := by + apply Complex.ext <;> simp [gaussianCast, gmul] + +@[simp] theorem gaussianCast_gscale (n : Int) (a : Gaussian) : + gaussianCast (gscale n a) = (n : ℂ) * gaussianCast a := by + apply Complex.ext <;> simp [gaussianCast, gscale] + +theorem natAbs_sq_cast_real (z : Int) : + ((z.natAbs : ℕ) : ℝ) ^ 2 = (z : ℝ) ^ 2 := by + have hz : |(z : ℝ)| = (z.natAbs : ℝ) := by + calc + |(z : ℝ)| = ((|z| : Int) : ℝ) := Int.cast_abs.symm + _ = (z.natAbs : ℝ) := (Nat.cast_natAbs z).symm + rw [← hz, sq_abs] + +/-- Every checked integer square-root is a lower bound for the true complex +coefficient numerator norm. -/ +theorem lowerNorm_le_norm_gaussianCast + (j k : ℕ) + (hsq : (lowerNorm j k) ^ 2 ≤ normSquared (coefficientNumerator j k)) : + (lowerNorm j k : ℝ) ≤ ‖gaussianCast (coefficientNumerator j k)‖ := by + have hsq' : + (lowerNorm j k : ℝ) ^ 2 ≤ + ((coefficientNumerator j k).1.natAbs : ℝ) ^ 2 + + ((coefficientNumerator j k).2.natAbs : ℝ) ^ 2 := by + exact_mod_cast hsq + rw [natAbs_sq_cast_real, natAbs_sq_cast_real] at hsq' + have hnorm : + ‖gaussianCast (coefficientNumerator j k)‖ ^ 2 = + ((coefficientNumerator j k).1 : ℝ) ^ 2 + + ((coefficientNumerator j k).2 : ℝ) ^ 2 := by + rw [← Complex.normSq_eq_norm_sq] + simp [gaussianCast, Complex.normSq_apply] + ring + rw [← hnorm] at hsq' + have hlower : 0 ≤ (lowerNorm j k : ℝ) := by positivity + nlinarith [norm_nonneg (gaussianCast (coefficientNumerator j k))] + +end BidiscPhaseCertificate + +namespace BidiscPhaseCertificate + +noncomputable def q10 : ℂ := + gaussianCast (denominator.getD 1 (0, 0)) / (D : ℂ) +noncomputable def q01 : ℂ := + gaussianCast (denominator.getD 2 (0, 0)) / (D : ℂ) +noncomputable def q11 : ℂ := + gaussianCast (denominator.getD 3 (0, 0)) / (D : ℂ) +noncomputable def p00 : ℂ := + gaussianCast (numerator.getD 0 (0, 0)) / (D : ℂ) +noncomputable def p10 : ℂ := + gaussianCast (numerator.getD 1 (0, 0)) / (D : ℂ) +noncomputable def p01 : ℂ := + gaussianCast (numerator.getD 2 (0, 0)) / (D : ℂ) +noncomputable def p11 : ℂ := + gaussianCast (numerator.getD 3 (0, 0)) / (D : ℂ) + +noncomputable def certificateRational : ℂ × ℂ → ℂ := + Optim.BohrRadius.complexBidegreeRational + q10 q01 q11 p00 p10 p01 p11 + +/-- The all-orders Taylor family belonging to the normalized certified +rational function. -/ +noncomputable def certifiedTaylorCoefficient : ℕ → ℕ → ℂ := + Optim.BohrRadius.recurrentCoefficient + (-q10) (-q01) q11 p00 p10 p01 p11 + +/-- Closed scaled form represented by the checked Gaussian rectangle. -/ +noncomputable def closedCoefficient (j k : ℕ) : ℂ := + gaussianCast (coefficientNumerator j k) / (D : ℂ) ^ (j + k + 1) + +/-- The mapped coefficient arrays really are multiplication by the recorded +conjugate constant. -/ +theorem numerator_entry_mul_conjugate (i : Fin 4) : + numerator.getD i.val (0, 0) = + gmul (inputNumerator.getD i.val (0, 0)) conjugateConstant := by + fin_cases i <;> native_decide + +theorem denominator_entry_mul_conjugate (i : Fin 4) : + denominator.getD i.val (0, 0) = + gmul (inputDenominator.getD i.val (0, 0)) conjugateConstant := by + fin_cases i <;> native_decide + +theorem inputNumerator_entries : + inputNumerator.getD 0 (0, 0) = + (((S : Int) - 1) * (L : Int), ((S : Int) - 1) * (T : Int)) ∧ + inputNumerator.getD 1 (0, 0) = + (-(L : Int), (S : Int) * (T : Int)) ∧ + inputNumerator.getD 2 (0, 0) = + ((L : Int), -((S : Int) * (T : Int))) ∧ + inputNumerator.getD 3 (0, 0) = + (((S : Int) + 1) * (L : Int), -((S : Int) + 1) * (T : Int)) := by + native_decide + +theorem inputDenominator_entries : + inputDenominator.getD 0 (0, 0) = + (((S : Int) + 1) * (L : Int), ((S : Int) + 1) * (T : Int)) ∧ + inputDenominator.getD 1 (0, 0) = + ((L : Int), (S : Int) * (T : Int)) ∧ + inputDenominator.getD 2 (0, 0) = + (-(L : Int), -((S : Int) * (T : Int))) ∧ + inputDenominator.getD 3 (0, 0) = + (((S : Int) - 1) * (L : Int), -((S : Int) - 1) * (T : Int)) := by + native_decide + +theorem inputNumerator_polynomial (z w : ℂ) : + gaussianCast (inputNumerator.getD 0 (0, 0)) + + gaussianCast (inputNumerator.getD 1 (0, 0)) * z + + gaussianCast (inputNumerator.getD 2 (0, 0)) * w + + gaussianCast (inputNumerator.getD 3 (0, 0)) * z * w = + analyticNumerator (L : ℝ) (T : ℝ) (S : ℝ) z w := by + rw [inputNumerator_entries.1, inputNumerator_entries.2.1, + inputNumerator_entries.2.2.1, inputNumerator_entries.2.2.2] + simp [gaussianCast, analyticNumerator, + analyticP, analyticQ, analyticU, analyticV] + ring + +theorem inputDenominator_polynomial (z w : ℂ) : + gaussianCast (inputDenominator.getD 0 (0, 0)) + + gaussianCast (inputDenominator.getD 1 (0, 0)) * z + + gaussianCast (inputDenominator.getD 2 (0, 0)) * w + + gaussianCast (inputDenominator.getD 3 (0, 0)) * z * w = + analyticDenominator (L : ℝ) (T : ℝ) (S : ℝ) z w := by + rw [inputDenominator_entries.1, inputDenominator_entries.2.1, + inputDenominator_entries.2.2.1, inputDenominator_entries.2.2.2] + simp [gaussianCast, analyticDenominator, + analyticP, analyticQ, analyticU, analyticV] + ring + +theorem div_common_nonzero (N Q c d : ℂ) (hc : c ≠ 0) (hd : d ≠ 0) : + (N * c / d) / (Q * c / d) = N / Q := by + simp only [div_eq_mul_inv, mul_inv_rev, inv_inv] + calc + N * c * d⁻¹ * (d * (c⁻¹ * Q⁻¹)) = + N * (c * c⁻¹) * (d⁻¹ * d) * Q⁻¹ := by ring + _ = N * Q⁻¹ := by simp [hc, hd] + +/-- Multiplying numerator and denominator by the conjugate constant does not +change the rational witness. -/ +theorem certificateRational_eq_certifiedWitness : + certificateRational = certifiedWitness := by + funext x + rcases x with ⟨z, w⟩ + have hn0 := numerator_entry_mul_conjugate (⟨0, by omega⟩ : Fin 4) + have hn1 := numerator_entry_mul_conjugate (⟨1, by omega⟩ : Fin 4) + have hn2 := numerator_entry_mul_conjugate (⟨2, by omega⟩ : Fin 4) + have hn3 := numerator_entry_mul_conjugate (⟨3, by omega⟩ : Fin 4) + have hd0 := denominator_entry_mul_conjugate (⟨0, by omega⟩ : Fin 4) + have hd1 := denominator_entry_mul_conjugate (⟨1, by omega⟩ : Fin 4) + have hd2 := denominator_entry_mul_conjugate (⟨2, by omega⟩ : Fin 4) + have hd3 := denominator_entry_mul_conjugate (⟨3, by omega⟩ : Fin 4) + simp only [Fin.isValue] at hn0 hn1 hn2 hn3 hd0 hd1 hd2 hd3 + have hc : gaussianCast conjugateConstant ≠ 0 := by + intro hzero + have hre := congrArg Complex.re hzero + rw [show conjugateConstant = + gconj (inputDenominator.getD 0 (0, 0)) by rfl, + inputDenominator_entries.1] at hre + norm_num [gaussianCast, gconj, L, S] at hre + have hD : (D : ℂ) ≠ 0 := by + exact_mod_cast (show D ≠ 0 by native_decide) + unfold certificateRational Optim.BohrRadius.complexBidegreeRational + unfold q10 q01 q11 p00 p10 p01 p11 certifiedWitness analyticWitness + rw [hn0, hn1, hn2, hn3, hd1, hd2, hd3] + simp only [gaussianCast_gmul] + have hnpoly := inputNumerator_polynomial z w + have hdpoly := inputDenominator_polynomial z w + have hd0cast : + gaussianCast (inputDenominator.getD 0 (0, 0)) * + gaussianCast conjugateConstant = (D : ℂ) := by + rw [← gaussianCast_gmul, ← hd0, denominator_constant_correct] + simp [gaussianCast] + have hnscaled : + gaussianCast (inputNumerator.getD 0 (0, 0)) * + gaussianCast conjugateConstant / (D : ℂ) + + gaussianCast (inputNumerator.getD 1 (0, 0)) * + gaussianCast conjugateConstant / (D : ℂ) * z + + gaussianCast (inputNumerator.getD 2 (0, 0)) * + gaussianCast conjugateConstant / (D : ℂ) * w + + gaussianCast (inputNumerator.getD 3 (0, 0)) * + gaussianCast conjugateConstant / (D : ℂ) * z * w = + analyticNumerator (L : ℝ) (T : ℝ) (S : ℝ) z w * + gaussianCast conjugateConstant / (D : ℂ) := by + calc + _ = (gaussianCast (inputNumerator.getD 0 (0, 0)) + + gaussianCast (inputNumerator.getD 1 (0, 0)) * z + + gaussianCast (inputNumerator.getD 2 (0, 0)) * w + + gaussianCast (inputNumerator.getD 3 (0, 0)) * z * w) * + gaussianCast conjugateConstant / (D : ℂ) := by ring + _ = _ := by rw [hnpoly] + have hdscaled : + 1 + gaussianCast (inputDenominator.getD 1 (0, 0)) * + gaussianCast conjugateConstant / (D : ℂ) * z + + gaussianCast (inputDenominator.getD 2 (0, 0)) * + gaussianCast conjugateConstant / (D : ℂ) * w + + gaussianCast (inputDenominator.getD 3 (0, 0)) * + gaussianCast conjugateConstant / (D : ℂ) * z * w = + analyticDenominator (L : ℝ) (T : ℝ) (S : ℝ) z w * + gaussianCast conjugateConstant / (D : ℂ) := by + have hone : (1 : ℂ) = + gaussianCast (inputDenominator.getD 0 (0, 0)) * + gaussianCast conjugateConstant / (D : ℂ) := by + rw [hd0cast] + exact (div_self hD).symm + rw [hone] + calc + _ = (gaussianCast (inputDenominator.getD 0 (0, 0)) + + gaussianCast (inputDenominator.getD 1 (0, 0)) * z + + gaussianCast (inputDenominator.getD 2 (0, 0)) * w + + gaussianCast (inputDenominator.getD 3 (0, 0)) * z * w) * + gaussianCast conjugateConstant / (D : ℂ) := by ring + _ = _ := by rw [hdpoly] + rw [hnscaled, hdscaled] + exact div_common_nonzero _ _ _ _ hc hD + +end BidiscPhaseCertificate + +namespace BidiscPhaseCertificate + +/-! The certificate-specific normalized complex data. -/ + +noncomputable def q₁₀C : ℂ := + gaussianCast (denominator.getD 1 (0, 0)) / (D : ℂ) + +noncomputable def q₀₁C : ℂ := + gaussianCast (denominator.getD 2 (0, 0)) / (D : ℂ) + +noncomputable def q₁₁C : ℂ := + gaussianCast (denominator.getD 3 (0, 0)) / (D : ℂ) + +noncomputable def p₀₀C : ℂ := + gaussianCast (numerator.getD 0 (0, 0)) / (D : ℂ) + +noncomputable def p₁₀C : ℂ := + gaussianCast (numerator.getD 1 (0, 0)) / (D : ℂ) + +noncomputable def p₀₁C : ℂ := + gaussianCast (numerator.getD 2 (0, 0)) / (D : ℂ) + +noncomputable def p₁₁C : ℂ := + gaussianCast (numerator.getD 3 (0, 0)) / (D : ℂ) + +/-- The all-orders analytic coefficient family corresponding to the normalized +Gaussian numerator and denominator. -/ +noncomputable def actualCoefficient (j k : ℕ) : ℂ := + Optim.BohrRadius.recurrentCoefficient + (-q₁₀C) (-q₀₁C) q₁₁C p₀₀C p₁₀C p₀₁C p₁₁C j k + +/-- The finite coefficient obtained from the checked scaled Gaussian recurrence. -/ +noncomputable def scaledCertificateCoefficient (j k : ℕ) : ℂ := + gaussianCast (coefficientNumerator j k) / (D : ℂ) ^ (j + k + 1) + +theorem D_cast_ne_zero : (D : ℂ) ≠ 0 := by + exact_mod_cast input_parameters_positive.1.ne' + +/-- Algebraic normalization for a boundary row or column of the scaled recurrence. -/ +theorem normalize_scaled_axis + (d q v vprev p : ℂ) (n : ℕ) (hd : d ≠ 0) + (h : v = d ^ (n + 1) * p - q * vprev) : + v / d ^ (n + 2) = + -(q / d) * (vprev / d ^ (n + 1)) + p / d := by + rw [h] + field_simp [hd] + simp [pow_add, pow_succ] + ring + +/-- Algebraic normalization for an interior entry of the scaled recurrence. -/ +theorem normalize_scaled_interior + (d q₁₀ q₀₁ q₁₁ v vh vv vdiag p : ℂ) (n : ℕ) (hd : d ≠ 0) + (h : v = d ^ (n + 2) * p + + (-(d * q₁₁ * vdiag) - q₀₁ * vv - q₁₀ * vh)) : + v / d ^ (n + 3) = + -(q₁₀ / d) * (vh / d ^ (n + 2)) + + -(q₀₁ / d) * (vv / d ^ (n + 2)) - + (q₁₁ / d) * (vdiag / d ^ (n + 1)) + p / d := by + rw [h] + rw [add_div, sub_div, sub_div] + rw [neg_div] + rw [show d ^ (n + 2) * p / d ^ (n + 3) = p / d by + field_simp [hd] + simp [pow_add, pow_succ] + ring] + rw [show d * q₁₁ * vdiag / d ^ (n + 3) = + (q₁₁ / d) * (vdiag / d ^ (n + 1)) by + field_simp [hd] + simp [pow_add, pow_succ] + ring] + rw [show q₀₁ * vv / d ^ (n + 3) = + (q₀₁ / d) * (vv / d ^ (n + 2)) by + field_simp [hd] + simp [pow_add, pow_succ] + ring; simp] + rw [show q₁₀ * vh / d ^ (n + 3) = + (q₁₀ / d) * (vh / d ^ (n + 2)) by + field_simp [hd] + simp [pow_add, pow_succ] + ring; simp] + ring + +/-- The checked Gaussian recurrence, after normalization by +`D^(j+k+1)`, obeys the same complex Taylor recurrence. -/ +theorem scaledCertificateCoefficient_recurrence + (j k : ℕ) (hj : j < 29) (hk : k < 29) : + scaledCertificateCoefficient j k = + Optim.BohrRadius.complexBidegreeRecurrenceValue + (-q₁₀C) (-q₀₁C) q₁₁C p₀₀C p₁₀C p₀₁C p₁₁C + scaledCertificateCoefficient j k := by + have hraw := rectangle_recurrence (⟨j, hj⟩ : Fin 29) (⟨k, hk⟩ : Fin 29) + have hcast := congrArg gaussianCast hraw + cases j with + | zero => + cases k with + | zero => + simp [scaledCertificateCoefficient, + Optim.BohrRadius.complexBidegreeRecurrenceValue, + expected, p₀₀C] at hcast ⊢ + rw [hcast] + | succ k => + by_cases hk0 : k = 0 + · subst k + simp [scaledCertificateCoefficient, + Optim.BohrRadius.complexBidegreeRecurrenceValue, + expected, q₀₁C, p₀₁C, p₁₁C] at hcast ⊢ + have hcast' : + gaussianCast (coefficientNumerator 0 1) = + (D : ℂ) ^ (0 + 1) * gaussianCast (numerator.getD 2 (0, 0)) - + gaussianCast (denominator.getD 2 (0, 0)) * + gaussianCast (coefficientNumerator 0 0) := by + simpa [pow_succ] using hcast + simpa using normalize_scaled_axis (D : ℂ) + (gaussianCast (denominator.getD 2 (0, 0))) + (gaussianCast (coefficientNumerator 0 1)) + (gaussianCast (coefficientNumerator 0 0)) + (gaussianCast (numerator.getD 2 (0, 0))) 0 D_cast_ne_zero hcast' + · have hk2 : ¬ k + 1 < 2 := by omega + simp [scaledCertificateCoefficient, + Optim.BohrRadius.complexBidegreeRecurrenceValue, + expected, q₀₁C, p₀₁C, p₁₁C, hk0, hk2] at hcast ⊢ + have hcast' : + gaussianCast (coefficientNumerator 0 (k + 1)) = + (D : ℂ) ^ (k + 1) * 0 - + gaussianCast (denominator.getD 2 (0, 0)) * + gaussianCast (coefficientNumerator 0 k) := by + simpa using hcast + simpa [pow_add, pow_succ] using normalize_scaled_axis (D : ℂ) + (gaussianCast (denominator.getD 2 (0, 0))) + (gaussianCast (coefficientNumerator 0 (k + 1))) + (gaussianCast (coefficientNumerator 0 k)) 0 k D_cast_ne_zero hcast' + | succ j => + cases k with + | zero => + by_cases hj0 : j = 0 + · subst j + simp [scaledCertificateCoefficient, + Optim.BohrRadius.complexBidegreeRecurrenceValue, + expected, q₁₀C, p₁₀C, p₁₁C] at hcast ⊢ + have hcast' : + gaussianCast (coefficientNumerator 1 0) = + (D : ℂ) ^ (0 + 1) * gaussianCast (numerator.getD 1 (0, 0)) - + gaussianCast (denominator.getD 1 (0, 0)) * + gaussianCast (coefficientNumerator 0 0) := by + simpa [pow_succ] using hcast + simpa using normalize_scaled_axis (D : ℂ) + (gaussianCast (denominator.getD 1 (0, 0))) + (gaussianCast (coefficientNumerator 1 0)) + (gaussianCast (coefficientNumerator 0 0)) + (gaussianCast (numerator.getD 1 (0, 0))) 0 D_cast_ne_zero hcast' + · have hj2 : ¬ j + 1 < 2 := by omega + simp [scaledCertificateCoefficient, + Optim.BohrRadius.complexBidegreeRecurrenceValue, + expected, q₁₀C, p₁₀C, p₁₁C, hj0, hj2] at hcast ⊢ + have hcast' : + gaussianCast (coefficientNumerator (j + 1) 0) = + (D : ℂ) ^ (j + 1) * 0 - + gaussianCast (denominator.getD 1 (0, 0)) * + gaussianCast (coefficientNumerator j 0) := by + simpa using hcast + simpa [pow_add, pow_succ] using normalize_scaled_axis (D : ℂ) + (gaussianCast (denominator.getD 1 (0, 0))) + (gaussianCast (coefficientNumerator (j + 1) 0)) + (gaussianCast (coefficientNumerator j 0)) 0 j D_cast_ne_zero hcast' + | succ k => + by_cases hjk0 : j = 0 ∧ k = 0 + · rcases hjk0 with ⟨rfl, rfl⟩ + simp [scaledCertificateCoefficient, + Optim.BohrRadius.complexBidegreeRecurrenceValue, + expected, q₁₀C, q₀₁C, q₁₁C, p₁₁C] at hcast ⊢ + have hcast' : + gaussianCast (coefficientNumerator 1 1) = + (D : ℂ) ^ (0 + 2) * gaussianCast (numerator.getD 3 (0, 0)) + + (-((D : ℂ) * gaussianCast (denominator.getD 3 (0, 0)) * + gaussianCast (coefficientNumerator 0 0)) - + gaussianCast (denominator.getD 2 (0, 0)) * + gaussianCast (coefficientNumerator 1 0) - + gaussianCast (denominator.getD 1 (0, 0)) * + gaussianCast (coefficientNumerator 0 1)) := by + simpa [pow_succ, mul_assoc, sub_eq_add_neg, add_assoc] using hcast + simpa using normalize_scaled_interior (D : ℂ) + (gaussianCast (denominator.getD 1 (0, 0))) + (gaussianCast (denominator.getD 2 (0, 0))) + (gaussianCast (denominator.getD 3 (0, 0))) + (gaussianCast (coefficientNumerator 1 1)) + (gaussianCast (coefficientNumerator 0 1)) + (gaussianCast (coefficientNumerator 1 0)) + (gaussianCast (coefficientNumerator 0 0)) + (gaussianCast (numerator.getD 3 (0, 0))) 0 D_cast_ne_zero hcast' + · have hsource : ¬ (j + 1 < 2 ∧ k + 1 < 2) := by omega + simp [scaledCertificateCoefficient, + Optim.BohrRadius.complexBidegreeRecurrenceValue, + expected, q₁₀C, q₀₁C, q₁₁C, p₁₁C, + hjk0, hsource] at hcast ⊢ + have hcast' : + gaussianCast (coefficientNumerator (j + 1) (k + 1)) = + (D : ℂ) ^ (j + k + 2) * 0 + + (-((D : ℂ) * gaussianCast (denominator.getD 3 (0, 0)) * + gaussianCast (coefficientNumerator j k)) - + gaussianCast (denominator.getD 2 (0, 0)) * + gaussianCast (coefficientNumerator (j + 1) k) - + gaussianCast (denominator.getD 1 (0, 0)) * + gaussianCast (coefficientNumerator j (k + 1))) := by + simpa [mul_assoc, sub_eq_add_neg, add_assoc] using hcast + simpa [pow_add, pow_succ, add_assoc, add_left_comm, add_comm] using + normalize_scaled_interior (D : ℂ) + (gaussianCast (denominator.getD 1 (0, 0))) + (gaussianCast (denominator.getD 2 (0, 0))) + (gaussianCast (denominator.getD 3 (0, 0))) + (gaussianCast (coefficientNumerator (j + 1) (k + 1))) + (gaussianCast (coefficientNumerator j (k + 1))) + (gaussianCast (coefficientNumerator (j + 1) k)) + (gaussianCast (coefficientNumerator j k)) 0 (j + k) D_cast_ne_zero hcast' + +/-- The finite checked rectangle is exactly the corresponding rectangle of +the all-orders analytic Taylor family. -/ +theorem actualCoefficient_eq_scaledCertificateCoefficient + (j k : ℕ) (hj : j < 29) (hk : k < 29) : + actualCoefficient j k = scaledCertificateCoefficient j k := by + apply Optim.BohrRadius.complexBidegreeRecurrence_unique_on_rectangle + (-q₁₀C) (-q₀₁C) q₁₁C p₀₀C p₁₀C p₀₁C p₁₁C 29 + actualCoefficient scaledCertificateCoefficient + (fun m n _ _ => by + exact Optim.BohrRadius.recurrentCoefficient_eq_complexBidegreeRecurrenceValue + (-q₁₀C) (-q₀₁C) q₁₁C p₀₀C p₁₀C p₀₁C p₁₁C m n) + (fun m n hm hn => scaledCertificateCoefficient_recurrence m n hm hn) + j k hj hk + +end BidiscPhaseCertificate + +namespace BidiscPhaseCertificate + +/-- Exact upper norm-square checks for all seven normalized coefficients. -/ +theorem parameter_normSquares_le : + normSquared (denominator.getD 1 (0, 0)) ≤ D ^ 2 ∧ + normSquared (denominator.getD 2 (0, 0)) ≤ D ^ 2 ∧ + normSquared (denominator.getD 3 (0, 0)) ≤ D ^ 2 ∧ + normSquared (numerator.getD 0 (0, 0)) ≤ D ^ 2 ∧ + normSquared (numerator.getD 1 (0, 0)) ≤ D ^ 2 ∧ + normSquared (numerator.getD 2 (0, 0)) ≤ D ^ 2 ∧ + normSquared (numerator.getD 3 (0, 0)) ≤ D ^ 2 := by + native_decide + +theorem norm_gaussianCast_le_D (v : Gaussian) + (hsq : normSquared v ≤ D ^ 2) : + ‖gaussianCast v‖ ≤ (D : ℝ) := by + have hsq' : + ((v.1.natAbs : ℕ) : ℝ) ^ 2 + ((v.2.natAbs : ℕ) : ℝ) ^ 2 ≤ + (D : ℝ) ^ 2 := by + exact_mod_cast hsq + rw [natAbs_sq_cast_real, natAbs_sq_cast_real] at hsq' + have hnorm : ‖gaussianCast v‖ ^ 2 = (v.1 : ℝ) ^ 2 + (v.2 : ℝ) ^ 2 := by + rw [← Complex.normSq_eq_norm_sq] + simp [gaussianCast, Complex.normSq_apply] + ring + rw [← hnorm] at hsq' + have hDnonneg : (0 : ℝ) ≤ (D : ℝ) := by positivity + nlinarith [norm_nonneg (gaussianCast v)] + +theorem normalized_gaussian_norm_le_one (v : Gaussian) + (hsq : normSquared v ≤ D ^ 2) : + ‖gaussianCast v / (D : ℂ)‖ ≤ 1 := by + rw [norm_div] + have hDpos : (0 : ℝ) < ‖(D : ℂ)‖ := norm_pos_iff.mpr D_cast_ne_zero + apply (div_le_one hDpos).2 + simpa using norm_gaussianCast_le_D v hsq + +theorem q₁₀C_norm_le_one : ‖q₁₀C‖ ≤ 1 := by + exact normalized_gaussian_norm_le_one _ parameter_normSquares_le.1 + +theorem q₀₁C_norm_le_one : ‖q₀₁C‖ ≤ 1 := by + exact normalized_gaussian_norm_le_one _ parameter_normSquares_le.2.1 + +theorem q₁₁C_norm_le_one : ‖q₁₁C‖ ≤ 1 := by + exact normalized_gaussian_norm_le_one _ parameter_normSquares_le.2.2.1 + +theorem p₀₀C_norm_le_one : ‖p₀₀C‖ ≤ 1 := by + exact normalized_gaussian_norm_le_one _ parameter_normSquares_le.2.2.2.1 + +theorem p₁₀C_norm_le_one : ‖p₁₀C‖ ≤ 1 := by + exact normalized_gaussian_norm_le_one _ parameter_normSquares_le.2.2.2.2.1 + +theorem p₀₁C_norm_le_one : ‖p₀₁C‖ ≤ 1 := by + exact normalized_gaussian_norm_le_one _ parameter_normSquares_le.2.2.2.2.2.1 + +theorem p₁₁C_norm_le_one : ‖p₁₁C‖ ≤ 1 := by + exact normalized_gaussian_norm_le_one _ parameter_normSquares_le.2.2.2.2.2.2 + +theorem normalizedDenominator_ne_zero + (z w : ℂ) (hz : ‖z‖ < (1 / 8 : ℝ)) (hw : ‖w‖ < (1 / 8 : ℝ)) : + 1 + q₁₀C * z + q₀₁C * w + q₁₁C * z * w ≠ 0 := by + have h10 : ‖q₁₀C * z‖ < (1 / 8 : ℝ) := by + rw [norm_mul] + calc + ‖q₁₀C‖ * ‖z‖ ≤ 1 * ‖z‖ := + mul_le_mul_of_nonneg_right q₁₀C_norm_le_one (norm_nonneg z) + _ < 1 / 8 := by simpa using hz + have h01 : ‖q₀₁C * w‖ < (1 / 8 : ℝ) := by + rw [norm_mul] + calc + ‖q₀₁C‖ * ‖w‖ ≤ 1 * ‖w‖ := + mul_le_mul_of_nonneg_right q₀₁C_norm_le_one (norm_nonneg w) + _ < 1 / 8 := by simpa using hw + have h11 : ‖q₁₁C * z * w‖ < (1 / 64 : ℝ) := by + rw [norm_mul, norm_mul] + have hprod : ‖z‖ * ‖w‖ < (1 / 64 : ℝ) := by + by_cases hwzero : ‖w‖ = 0 + · simp [hwzero] + · have hwpos : 0 < ‖w‖ := lt_of_le_of_ne (norm_nonneg w) (Ne.symm hwzero) + calc + ‖z‖ * ‖w‖ < (1 / 8 : ℝ) * ‖w‖ := + mul_lt_mul_of_pos_right hz hwpos + _ < (1 / 8 : ℝ) * (1 / 8 : ℝ) := + mul_lt_mul_of_pos_left hw (by norm_num) + _ = 1 / 64 := by norm_num + calc + ‖q₁₁C‖ * ‖z‖ * ‖w‖ ≤ 1 * ‖z‖ * ‖w‖ := by + gcongr + exact q₁₁C_norm_le_one + _ = ‖z‖ * ‖w‖ := by ring + _ < 1 / 64 := hprod + have hsum : ‖q₁₀C * z + q₀₁C * w + q₁₁C * z * w‖ < 1 := by + calc + ‖q₁₀C * z + q₀₁C * w + q₁₁C * z * w‖ ≤ + ‖q₁₀C * z‖ + ‖q₀₁C * w‖ + ‖q₁₁C * z * w‖ := by + exact (norm_add_le _ _).trans (add_le_add_right (norm_add_le _ _) _) + _ < 1 := by linarith + intro hzero + have hone : (1 : ℂ) = -(q₁₀C * z + q₀₁C * w + q₁₁C * z * w) := by + linear_combination hzero + have heq : (1 : ℝ) = ‖q₁₀C * z + q₀₁C * w + q₁₁C * z * w‖ := by + calc + (1 : ℝ) = ‖(1 : ℂ)‖ := by norm_num + _ = ‖-(q₁₀C * z + q₀₁C * w + q₁₁C * z * w)‖ := by rw [hone] + _ = _ := norm_neg _ + linarith + +/-- The recurrence family is the genuine Taylor family of the same concrete +Schur witness used in the analytic proof. -/ +theorem actualCoefficient_hasBidiscCoefficients : + Optim.BohrRadius.HasBidiscCoefficients certifiedWitness actualCoefficient := by + have h := Optim.BohrRadius.complexBidegreeRational_recurrent_hasBidiscCoefficients + q₁₀C_norm_le_one q₀₁C_norm_le_one q₁₁C_norm_le_one + p₀₀C_norm_le_one p₁₀C_norm_le_one p₀₁C_norm_le_one p₁₁C_norm_le_one + normalizedDenominator_ne_zero + rw [← certificateRational_eq_certifiedWitness] + simpa [certificateRational, q10, q01, q11, p00, p10, p01, p11, + q₁₀C, q₀₁C, q₁₁C, p₀₀C, p₁₀C, p₀₁C, p₁₁C, + actualCoefficient] using h + +end BidiscPhaseCertificate + +namespace BidiscPhaseCertificate + +/-- The exact lower majorant obtained from the certified integer norm floors. -/ +noncomputable def certifiedLowerMajorant : ℝ := + ∑ j ∈ Finset.range 29, ∑ k ∈ Finset.range 29, + (lowerNorm j k : ℝ) / (D : ℝ) ^ (j + k + 1) * + ((R : ℝ) / (E : ℝ)) ^ (j + k) + +def commonDenominator : Nat := D * (E * D) ^ 56 + +/-- Universal denominator-clearing identity for one lower-majorant term. -/ +theorem homogeneous_lower_term + (v rn rd scale t N : ℕ) + (hrd : (rd : ℝ) ≠ 0) (hscale : (scale : ℝ) ≠ 0) + (ht : t ≤ N) : + (v : ℝ) / (scale : ℝ) ^ (t + 1) * + ((rn : ℝ) / (rd : ℝ)) ^ t * + ((scale : ℝ) * ((rd : ℝ) * (scale : ℝ)) ^ N) = + (v : ℝ) * (rn : ℝ) ^ t * + ((rd : ℝ) * (scale : ℝ)) ^ (N - t) := by + have hdecomp : + ((rd : ℝ) * (scale : ℝ)) ^ N = + ((rd : ℝ) * (scale : ℝ)) ^ (N - t) * + ((rd : ℝ) * (scale : ℝ)) ^ t := by + rw [← pow_add, Nat.sub_add_cancel ht] + rw [hdecomp, div_pow] + field_simp [hrd, hscale] + simp [mul_pow, pow_add, pow_succ] + ring + +theorem certifiedLowerMajorant_mul_commonDenominator : + certifiedLowerMajorant * (commonDenominator : ℝ) = + (weightedIntegerSum : ℝ) := by + unfold certifiedLowerMajorant commonDenominator weightedIntegerSum + push_cast + rw [Finset.sum_mul] + apply Finset.sum_congr rfl + intro j hj + rw [Finset.sum_mul] + apply Finset.sum_congr rfl + intro k hk + have hj' : j < 29 := Finset.mem_range.mp hj + have hk' : k < 29 := Finset.mem_range.mp hk + apply homogeneous_lower_term + · exact_mod_cast (show E ≠ 0 by native_decide) + · exact_mod_cast input_parameters_positive.1.ne' + · omega + +theorem weightedIntegerSum_gt_commonDenominator : + commonDenominator < weightedIntegerSum := by + have hmargin := strict_weighted_integer_margin + have hscale : 0 < 10 ^ 26 := by positivity + unfold commonDenominator + omega + +theorem certifiedLowerMajorant_exceeds_one : + 1 < certifiedLowerMajorant := by + have hcast : (commonDenominator : ℝ) < (weightedIntegerSum : ℝ) := by + exact_mod_cast weightedIntegerSum_gt_commonDenominator + have hcommonNat : 0 < commonDenominator := by + unfold commonDenominator + exact Nat.mul_pos input_parameters_positive.1 + (pow_pos (Nat.mul_pos (by native_decide) input_parameters_positive.1) _) + have hcommon : (0 : ℝ) < (commonDenominator : ℝ) := by exact_mod_cast hcommonNat + have hid := certifiedLowerMajorant_mul_commonDenominator + nlinarith + +/-- Every lower norm floor contributes no more than the corresponding true +Taylor coefficient norm. -/ +theorem certifiedLowerMajorant_le_finiteMajorant : + certifiedLowerMajorant ≤ + Optim.BohrRadius.finiteMajorant actualCoefficient + ((R : ℝ) / (E : ℝ)) 28 := by + unfold certifiedLowerMajorant Optim.BohrRadius.finiteMajorant + apply Finset.sum_le_sum + intro j hj + apply Finset.sum_le_sum + intro k hk + have hj29 : j < 29 := by + have := Finset.mem_range.mp hj + omega + have hk29 : k < 29 := by + have := Finset.mem_range.mp hk + omega + have hsq := (integer_square_roots_correct + (⟨j, hj29⟩ : Fin 29) (⟨k, hk29⟩ : Fin 29)).1 + have hfloor := lowerNorm_le_norm_gaussianCast j k hsq + have hcoefficient : + (lowerNorm j k : ℝ) / (D : ℝ) ^ (j + k + 1) ≤ + ‖actualCoefficient j k‖ := by + rw [actualCoefficient_eq_scaledCertificateCoefficient j k hj29 hk29, + scaledCertificateCoefficient, norm_div, norm_pow] + have hnormD : ‖(D : ℂ)‖ = (D : ℝ) := by simp + rw [hnormD] + exact div_le_div_of_nonneg_right hfloor (by positivity) + have hrnonneg : (0 : ℝ) ≤ (R : ℝ) / (E : ℝ) := by positivity + exact mul_le_mul_of_nonneg_right hcoefficient (pow_nonneg hrnonneg _) + +theorem actualCoefficient_finiteMajorant_exceeds_one : + 1 < Optim.BohrRadius.finiteMajorant actualCoefficient + ((R : ℝ) / (E : ℝ)) 28 := + lt_of_lt_of_le certifiedLowerMajorant_exceeds_one + certifiedLowerMajorant_le_finiteMajorant + +end BidiscPhaseCertificate + +namespace Optim.BohrRadius + +/-- End-to-end strict upper bound certified by Shivam Patel's 2026 Gaussian +phase witness. The theorem uses the genuine analytic Schur class, the actual +locally convergent Taylor family, and the supremal definition of the bidisc +Bohr radius. -/ +theorem bohrRadius_lt_patel2026 : + bohrRadius < + (BidiscPhaseCertificate.R : ℝ) / (BidiscPhaseCertificate.E : ℝ) := by + exact bohrRadius_lt_of_finite_violation + (by norm_num [BidiscPhaseCertificate.R, BidiscPhaseCertificate.E]) + BidiscPhaseCertificate.certifiedWitness_isSchur + BidiscPhaseCertificate.actualCoefficient_hasBidiscCoefficients + BidiscPhaseCertificate.actualCoefficient_finiteMajorant_exceeds_one + +/-- Decimal form of the new strict world-record upper bound. -/ +theorem bohrRadius_lt_302825279492_div_10pow12 : + bohrRadius < (302825279492 : ℝ) / 10 ^ 12 := by + convert bohrRadius_lt_patel2026 using 1 + norm_num [BidiscPhaseCertificate.R, BidiscPhaseCertificate.E] + +end Optim.BohrRadius + +#print axioms BidiscPhaseCertificate.certifiedWitness_isSchur +#print axioms BidiscPhaseCertificate.actualCoefficient_hasBidiscCoefficients +#print axioms BidiscPhaseCertificate.actualCoefficient_eq_scaledCertificateCoefficient +#print axioms BidiscPhaseCertificate.actualCoefficient_finiteMajorant_exceeds_one +#print axioms Optim.BohrRadius.bohrRadius_lt_302825279492_div_10pow12 diff --git a/certificates/59a/patel-2026/FiniteCertificate.lean b/certificates/59a/patel-2026/FiniteCertificate.lean new file mode 100644 index 0000000..02f0324 --- /dev/null +++ b/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 diff --git a/certificates/59a/patel-2026/README.md b/certificates/59a/patel-2026/README.md new file mode 100644 index 0000000..0ffdd24 --- /dev/null +++ b/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. diff --git a/certificates/59a/patel-2026/SHA256SUMS b/certificates/59a/patel-2026/SHA256SUMS new file mode 100644 index 0000000..ecb54f7 --- /dev/null +++ b/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 diff --git a/certificates/59a/patel-2026/lake-manifest.json b/certificates/59a/patel-2026/lake-manifest.json new file mode 100644 index 0000000..e42db16 --- /dev/null +++ b/certificates/59a/patel-2026/lake-manifest.json @@ -0,0 +1,95 @@ +{"version": "1.1.0", + "packagesDir": ".lake/packages", + "packages": + [{"url": "https://github.com/leanprover-community/mathlib4.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "c44e0c8ee63ca166450922a373c7409c5d26b00b", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "c44e0c8ee63ca166450922a373c7409c5d26b00b", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "77e08eddc486491d7b9e470926b3dbe50319451a", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "25078369972d295301f5a1e53c3e5850cf6d9d4c", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/import-graph", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "e6a9f0f5ee3ccf7443a0070f92b62f8db12ae82b", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "c4919189477c3221e6a204008998b0d724f49904", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "v0.0.57", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "5d50b08dedd7d69b3d9b3176e0d58a23af228884", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "fa4f7f15d97591a9cf3aa7724ba371c7fc6dda02", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "f5d04a9c4973d401c8c92500711518f7c656f034", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "02dbd02bc00ec4916e99b04b2245b30200e200d0", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}], + "name": "bidiscPhaseCertificate", + "lakeDir": ".lake"} diff --git a/certificates/59a/patel-2026/lakefile.toml b/certificates/59a/patel-2026/lakefile.toml new file mode 100644 index 0000000..e1ed302 --- /dev/null +++ b/certificates/59a/patel-2026/lakefile.toml @@ -0,0 +1,14 @@ +name = "bidiscPhaseCertificate" +version = "0.1.0" +defaultTargets = ["FiniteCertificate", "EndToEnd"] + +[[require]] +name = "mathlib" +git = "https://github.com/leanprover-community/mathlib4.git" +rev = "c44e0c8ee63ca166450922a373c7409c5d26b00b" + +[[lean_lib]] +name = "FiniteCertificate" + +[[lean_lib]] +name = "EndToEnd" diff --git a/certificates/59a/patel-2026/lean-toolchain b/certificates/59a/patel-2026/lean-toolchain new file mode 100644 index 0000000..7aca1d8 --- /dev/null +++ b/certificates/59a/patel-2026/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.19.0 diff --git a/certificates/59a/patel-2026/verify_gaussian_certificate.py b/certificates/59a/patel-2026/verify_gaussian_certificate.py new file mode 100644 index 0000000..b579ba2 --- /dev/null +++ b/certificates/59a/patel-2026/verify_gaussian_certificate.py @@ -0,0 +1,126 @@ +#!/usr/bin/env python3 +"""Exact recurrence certificate for K_2 < 302825279492 / 10^12.""" + +from decimal import Decimal, getcontext +from hashlib import sha256 +from math import isqrt + +L = 2_500_000_000 +T = 3_067_398_171 +S = 10**15 +R = 302_825_279_492 +E = 10**12 +N = 28 +MARGIN_POWER = 26 + +Gaussian = tuple[int, int] + + +def add(a: Gaussian, b: Gaussian) -> Gaussian: + return a[0] + b[0], a[1] + b[1] + + +def neg(a: Gaussian) -> Gaussian: + return -a[0], -a[1] + + +def mul(a: Gaussian, b: Gaussian) -> Gaussian: + return a[0] * b[0] - a[1] * b[1], a[0] * b[1] + a[1] * b[0] + + +def scale(n: int, a: Gaussian) -> Gaussian: + return n * a[0], n * a[1] + + +def digest_integer(value: int) -> str: + return sha256(str(value).encode("ascii")).hexdigest() + + +def digest_lines(lines: list[str]) -> str: + return sha256(("\n".join(lines) + "\n").encode("ascii")).hexdigest() + + +def main() -> None: + input_numerator = [ + ((S - 1) * L, (S - 1) * T), + (-L, S * T), + (L, -(S * T)), + ((S + 1) * L, -((S + 1) * T)), + ] + input_denominator = [ + ((S + 1) * L, (S + 1) * T), + (L, S * T), + (-L, -(S * T)), + ((S - 1) * L, -((S - 1) * T)), + ] + conjugate_constant = ( + input_denominator[0][0], + -input_denominator[0][1], + ) + numerator = [mul(v, conjugate_constant) for v in input_numerator] + denominator = [mul(v, conjugate_constant) for v in input_denominator] + d = (S + 1) ** 2 * (L**2 + T**2) + assert denominator[0] == (d, 0) + assert 0 < R < E and 1 < S + + values: list[list[Gaussian]] = [[(0, 0) for _ in range(N + 1)] for _ in range(N + 1)] + for j in range(N + 1): + for k in range(N + 1): + value = (0, 0) + if j < 2 and k < 2: + value = scale(d ** (j + k), numerator[j + 2 * k]) + if j: + value = add(value, neg(mul(denominator[1], values[j - 1][k]))) + if k: + value = add(value, neg(mul(denominator[2], values[j][k - 1]))) + if j and k: + value = add( + value, + neg(scale(d, mul(denominator[3], values[j - 1][k - 1]))), + ) + values[j][k] = value + + lower_norms = [ + [isqrt(values[j][k][0] ** 2 + values[j][k][1] ** 2) for k in range(N + 1)] + for j in range(N + 1) + ] + for j in range(N + 1): + for k in range(N + 1): + squared_norm = values[j][k][0] ** 2 + values[j][k][1] ** 2 + lower = lower_norms[j][k] + assert lower**2 <= squared_norm < (lower + 1) ** 2 + + base = E * d + a = sum( + lower_norms[j][k] * R ** (j + k) * base ** (2 * N - j - k) + for j in range(N + 1) + for k in range(N + 1) + ) + b = d * base ** (2 * N) + margin = 10**MARGIN_POWER + assert margin * a > (margin + 1) * b + slack = margin * (a - b) - b + coefficient_digest = digest_lines( + [f"{j},{k},{values[j][k][0]},{values[j][k][1]}" for j in range(N + 1) for k in range(N + 1)] + ) + floor_digest = digest_lines( + [f"{j},{k},{lower_norms[j][k]}" for j in range(N + 1) for k in range(N + 1)] + ) + + getcontext().prec = 60 + excess = Decimal(a - b) / Decimal(b) + print(f"D = {d}") + print(f"coefficients = {(N + 1) ** 2}") + print(f"r = {R}/{E}") + print(f"A/B - 1 = {excess}") + print(f"proved: 10^{MARGIN_POWER} A > (10^{MARGIN_POWER} + 1) B") + print(f"sha256(A) = {digest_integer(a)}") + print(f"sha256(B) = {digest_integer(b)}") + print(f"sha256(A-B) = {digest_integer(a - b)}") + print(f"sha256(slack) = {digest_integer(slack)}") + print(f"sha256(coefficients.csv) = {coefficient_digest}") + print(f"sha256(floors.csv) = {floor_digest}") + + +if __name__ == "__main__": + main() diff --git a/certificates/59a/patel-2026/verify_multinomial_certificate.py b/certificates/59a/patel-2026/verify_multinomial_certificate.py new file mode 100644 index 0000000..9c1220b --- /dev/null +++ b/certificates/59a/patel-2026/verify_multinomial_certificate.py @@ -0,0 +1,132 @@ +#!/usr/bin/env python3 +"""Independent multinomial certificate for K_2 < 302825279492 / 10^12.""" + +from decimal import Decimal, getcontext +from hashlib import sha256 +from math import comb, isqrt + +L = 2_500_000_000 +T = 3_067_398_171 +S = 10**15 +R = 302_825_279_492 +E = 10**12 +N = 28 + +Gaussian = tuple[int, int] + + +def gadd(x: Gaussian, y: Gaussian) -> Gaussian: + return x[0] + y[0], x[1] + y[1] + + +def gmul(x: Gaussian, y: Gaussian) -> Gaussian: + return x[0] * y[0] - x[1] * y[1], x[0] * y[1] + x[1] * y[0] + + +def gscale(n: int, x: Gaussian) -> Gaussian: + return n * x[0], n * x[1] + + +def gpow(x: Gaussian, n: int) -> Gaussian: + result = (1, 0) + base = x + while n: + if n & 1: + result = gmul(result, base) + base = gmul(base, base) + n //= 2 + return result + + +def digest_integer(value: int) -> str: + return sha256(str(value).encode("ascii")).hexdigest() + + +def digest_lines(lines: list[str]) -> str: + return sha256(("\n".join(lines) + "\n").encode("ascii")).hexdigest() + + +def main() -> None: + raw_p = [ + ((S - 1) * L, (S - 1) * T), + (-L, S * T), + (L, -S * T), + ((S + 1) * L, -(S + 1) * T), + ] + raw_q = [ + ((S + 1) * L, (S + 1) * T), + (L, S * T), + (-L, -S * T), + ((S - 1) * L, -(S - 1) * T), + ] + conjugate = raw_q[0][0], -raw_q[0][1] + p = [gmul(x, conjugate) for x in raw_p] + q = [gmul(x, conjugate) for x in raw_q] + d = (S + 1) ** 2 * (L**2 + T**2) + assert q[0] == (d, 0) + q10, q01, q11 = q[1], q[2], q[3] + + inverse_scaled: dict[tuple[int, int], Gaussian] = {} + for j in range(N + 1): + for k in range(N + 1): + total = (0, 0) + for m in range(min(j, k) + 1): + multinomial = comb(j + k - m, m) * comb(j + k - 2 * m, j - m) + scalar = (-1) ** (j + k - m) * multinomial * d**m + term = gmul(gpow(q10, j - m), gpow(q01, k - m)) + term = gmul(term, gpow(q11, m)) + total = gadd(total, gscale(scalar, term)) + inverse_scaled[j, k] = total + + def w(j: int, k: int) -> Gaussian: + return inverse_scaled.get((j, k), (0, 0)) + + coefficients: list[list[Gaussian]] = [[(0, 0) for _ in range(N + 1)] for _ in range(N + 1)] + for j in range(N + 1): + for k in range(N + 1): + value = gmul(p[0], w(j, k)) + value = gadd(value, gscale(d, gmul(p[1], w(j - 1, k)))) + value = gadd(value, gscale(d, gmul(p[2], w(j, k - 1)))) + value = gadd(value, gscale(d**2, gmul(p[3], w(j - 1, k - 1)))) + coefficients[j][k] = value + + lower = [ + [isqrt(coefficients[j][k][0] ** 2 + coefficients[j][k][1] ** 2) for k in range(N + 1)] + for j in range(N + 1) + ] + base = E * d + a = sum( + lower[j][k] * R ** (j + k) * base ** (2 * N - j - k) + for j in range(N + 1) + for k in range(N + 1) + ) + b = d * base ** (2 * N) + assert 10**26 * a > (10**26 + 1) * b + slack = 10**26 * (a - b) - b + coefficient_digest = digest_lines( + [ + f"{j},{k},{coefficients[j][k][0]},{coefficients[j][k][1]}" + for j in range(N + 1) + for k in range(N + 1) + ] + ) + floor_digest = digest_lines( + [f"{j},{k},{lower[j][k]}" for j in range(N + 1) for k in range(N + 1)] + ) + + getcontext().prec = 60 + print(f"D = {d}") + print(f"coefficients = {(N + 1) ** 2}") + print(f"r = {R}/{E}") + print(f"A/B - 1 = {Decimal(a - b) / Decimal(b)}") + print("proved independently by multinomial coefficient extraction") + print(f"sha256(A) = {digest_integer(a)}") + print(f"sha256(B) = {digest_integer(b)}") + print(f"sha256(A-B) = {digest_integer(a - b)}") + print(f"sha256(slack) = {digest_integer(slack)}") + print(f"sha256(coefficients.csv) = {coefficient_digest}") + print(f"sha256(floors.csv) = {floor_digest}") + + +if __name__ == "__main__": + main() diff --git a/constants/59a.md b/constants/59a.md index 0254747..60b286a 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}$. [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](https://github.com/teorth/optimizationproblems/tree/main/certificates/59a/patel-2026). + - **[P2026-ub-K2-0-302825279492]** + **loc:** Theorem 1 and the exact certificate in the linked proof package + **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 references and submitted information.