Sharp Bragg Zero-Free Disk

Abstract

A positive Bragg peak and its Bernstein variation bound determine a sharp zero-free disk.

Theorem 1.1 (The finite Bragg radius is zero-free and sharp).

$$\begin{gathered} \forall P:\mathbb{C}\to \mathbb{C},z_0\in \mathbb{C},T,\phi ,c\in \mathbb{R}, \\ T>0,\phi >0,c>0,\left|P\left(z_0\right)\right|\ge T\cdot c, \\ (\forall w\in \mathbb{C},\left|P\left(w\right)-P\left(z_0\right)\right|\le e\cdot T\cdot \left(\phi \cdot T+2\right)\cdot \left|w-z_0\right|) \\ \Rightarrow ((\forall w\in \mathbb{C},\left|w-z_0\right|<\frac{c}{e\cdot \left(\phi \cdot T+2\right)}\Rightarrow P\left(w\right)\ne 0)\wedge z_0\in B\left(z_0,\frac{c}{e\cdot \left(\phi \cdot T+2\right)}\right)\wedge P\left(z_0\right)\ne 0)\wedge \\ \exists Q:\mathbb{C}\to \mathbb{C},\exists w_{\ast }\in \mathbb{C},\left|Q\left(0\right)\right|=T\cdot c\wedge (\forall w\in \mathbb{C},\left|Q\left(w\right)-Q\left(0\right)\right|=e\cdot T\cdot \left(\phi \cdot T+2\right)\cdot \left|w\right|)\wedge \\ \left|w_{\ast }\right|=\frac{c}{e\cdot \left(\phi \cdot T+2\right)}\wedge Q\left(w_{\ast }\right)=0. \end{gathered}$$

Proof. Machine-checked in Lean as D5/S0/Asymptotics/Interference/BraggZeroFreeDisk.bragg_zero_free_disk (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let c denote the positive magnitude of the relevant Fourier-Bohr coefficient. The peak lower bound is T c, while the Bernstein estimate supplies Lipschitz constant L = e T (phi T + 2). Their quotient is the exact finite radius r = c/(e(phi T + 2)).

Inside the open disk, the maximum possible variation from the center is strictly smaller than T c. The reverse triangle inequality therefore prevents the function from vanishing there.

The linear profile Q(w) = T c - L w has the same central height and exact Lipschitz constant, and it vanishes at distance r. This boundary witness shows that the strict disk cannot be enlarged uniformly from only the two quantitative hypotheses.

The source’s c/(e phi T)(1+o(1)) is an asymptotic rewrite. This theorem retains the finite +2 term and explicitly assumes T, phi, and c positive, excluding totalized-division degeneracies.

References

• Truth anchor: D5/S0/Asymptotics/Interference/BraggZeroFreeDisk.bragg_zero_free_disk