Research proof index

The following result is technical and used to prove the saturation property of the Buchi congruence. Its main purpose is to "fill in" the states between the successive ss' m to produce a well-formed run in which the accepting states appear infinitely often. Note that ss needs to agree with ss' only at positions φ m: ∀ m, ss (φ m) = ss' m.

If M is finite-state, then M.PairAccLang acc s s' is regular for any pair of states s and s'. Note that we need to use the history NA construction to prove this result, because the NA needs to remember whether an accepting state has been visited.

If M is finite-state, then M.PairLang s s' is regular for any pair of states s and s'.

This lemma derives a form of the Ramsey theorem suitable for use in the next theorem.

Every zero $s$ of the Riemann zeta function in the upper half-plane lies in the critical strip: if $\zeta(s)=0$ and $\operatorname{Im}s>0$, then $0\le\operatorname{Re}s\le1.$

The Riemann zeta zero-counting function has a crude polynomial bound: there is a constant $A>0$ such that, for every $T\ge2$, $|N_\zeta(T)|\le A T^{3/2}.$