Real zeros of $L(s,\chi)$ in $(0,1)$ are symmetric about $1/2$ (functional equation, Davenport §9)

Symmetry of the real zeros of a quadratic Dirichlet $L$-function. Let $q\ge1$, let $\chi$ be a non-principal Dirichlet character modulo $q$ which is quadratic (real-valued: every value of $\chi$ is $0$, $1$ or $-1$), and let $\beta$ be a real number with $0<\beta<1$. If

then also

Here $L(s,\chi)$ denotes the Dirichlet $L$-function of $\chi$, analytically continued to the whole complex plane.

This is the real-zero case of the reflection $\rho\mapsto 1-\bar\rho$ of the nontrivial zeros, which follows from the functional equation of the primitive character $\chi^*$ inducing $\chi$ (Davenport §9) together with the factorisation $L(s,\chi)=L(s,\chi^*)\prod_{p\mid q}(1-\chi^*(p)p^{-s})$, whose Euler factors do not vanish at real $s>0$. For quadratic $\chi$ one has $\overline{\chi}=\chi^{-1}=\chi$, so the functional equation relates $L(1-s,\chi^*)$ to $L(s,\chi^*)$ itself. Its role in the Siegel–Walfisz development is to show that an exceptional (Siegel) zero $\beta_1$ of a quadratic character, being the only zero in the region $\sigma\ge1-c/\log(q(|t|+2))$, must satisfy $\beta_1\ge 1/2$ (otherwise $1-\beta_1>1/2$ would be a second zero in the region).

Formalization Note. DirichletCharacter.LFunction χ is Mathlib's analytically continued $L$-function; χ.IsQuadratic means every value of $\chi$ lies in $\{0,1,-1\}$; the real numbers $\beta$ and $1-\beta$ are cast to $\mathbb{C}$.