MSC-2010-class: 11A25, 11N56 (Primary); 11M26 (Secondary)

Remainder in the Modified Mertens Formula

and Ramanujan Inequality111 This work was supported by the grant of Russian
Foundation of Fundamental Research
(project # $14-01-00684.$)

by Gennadiy Kalyabin222 Samara, Russia<EMAIL_ADDRESS>
Abstract: A highly strong upper estimate in the modified asymptotic

formula for sums of the primes’ reciprocals is proved to be necessary

(as well as sufficient) in order the Ramanujan inequality holds true.

Some other criteria in similar terms are also obtained.

Keywords: Mertens formula, Gronwall numbers, Ramanujan

inequality, Riemann Hypothesis

Bibliography: 9 items

1\. Notations, brief history and main results

As usually, let $\mathbb{N}$ be a set of all positive integers,
$\mathbb{N}_{0}:=\mathbb{N}\cup\\{0\\}$, $p$ run the set
$\mathbb{P}:=\\{p_{1},p_{2},\dots\\},\ p_{j}<p_{j+1},$ of all primes,
${\varepsilon}$ is an arbitrary positive number, $C_{y}$ stand for positive
constants which may depend only on a parameter $y$; symbols $\triangleright$
and $\Box$ denote the proof’s beginning and end; $\log x$ and $\gamma$ stand
(resp.) for the natural logarithm of a positive $x$ and the Euler-Masceroni
constant:

$\gamma:=\lim_{n\to\infty}\left(\sum_{k=1}^{n}\frac{1}{k}-\log n\right)=0.577\
215\ 664\ \dots$ $None$

In 1874 F. Mertens [1] proved his famous asymptotic formula

$S(x):=\sum_{p\leq x}\log\frac{p}{p-1}=\log\log x+\gamma+R(x)\hbox{ with
}R(x)=O\left(\frac{1}{\log x}\right).$ $None$

The best known unconditional, (i. e. without assumption of the Riemann
Hypothesis (RH) ), estimate for this remainder at the moment (2021) seems to
be $R(x)=O(\exp(-c(\log x)^{3/5}(\log\log x)^{-1/5})$.

In 1984 assuming  RH G. Robin [2, Th. 3] has come to the fundamentally
stronger estimate: $|R(x)|<\log x/(8\pi\sqrt{x}),\ x>X_{0}$.

We will present an integer $N>1$ as its canonical factorization in primes

$N:=p_{1}^{\alpha_{1}}p_{2}^{\alpha_{2}}\dots
p_{k}^{\alpha_{k}};\qquad\alpha_{j}\in\mathbb{N}_{0},\ \alpha_{k}>0,$ $None$

where the number $k:=k(N)$ and exponents $\alpha_{j}:=\alpha_{j}(N),\ 1\leq
j\leq k,$ are uniquely defined by $N$.

The greatest prime factor $p_{k}:=p_{k(N)}$ of $N$ will be denoted by
$\hbox{\bf gpf}(N)$.

Let $\sigma(N)$ stand for the arithmetic multiplicative function sum of all
divisors of $N\in\mathbb{N}$. The properties of this function are well
described in a very informative paper [3], which contains a lot of valuable
historical remarks, as well as many definions, notations and facts widely used
in this paper. In particular, in Sect. 5 the classical formula for $\sigma(N)$
is adduced, $N$ being defined in (1.3), namely:

$\sigma(N):=\prod_{j=1}^{k}(1+p_{j}+\dots+p_{j}^{\alpha_{j}})=\prod_{j=1}^{k}\frac{p_{j}^{\alpha_{j}+1}-1}{p_{j}-1}$
$None$

T. Gronwall in 1913, basing on (1.2) established the sharp upper order of
$\sigma(n)$, namely he proved [4] that:

$\limsup_{N\to\infty}G(N)=e^{\gamma}=1.781\ 072\dots;\hbox{ where
}G(N):=\frac{\sigma(N)}{N\log\log N},$ $None$

which we will call Gronwall numbers.

S. Ramanujan has noticed (in 1915, the first publication in 1997 [5]) that:

if RH holds true, then in addition to (1.6) for all $N$ sufficiently large the
following strict (Ramanujan) inequality (RI) takes place:

$G(N)<e^{\gamma},\qquad\forall N>n_{0}.$ $None$

Almost 70 years later G. Robin [2, Th 1] proved a paramount assertion, which
in a sense complements the Ramanujan’s result, namely:

if (1.6) holds true for all integers $N>5040$, then RH is valid.

We will call (1.6) with $n_{0}=5040$ the Ramanujan-Robin inequality (RRI), in
which the statement of RH is exhaustively encoded in terms of $\sigma(N)$.

Robin has also shown that in fact RI (with uncertain $n_{0}$) and RRI are
equivalent, because if RH holds false, then there are infinitely many $N$’s
such that $G(N)>\gamma$.

In this paper we do not strive to prove any of these conjectures but rather to
reveal the direct interrelation between them and the remainder in the modified
Mertens formula:

$S(x)=\log\log\theta(x)+\gamma+Q(x),$ $None$

which differs from (1.2) by replacing $x$ in $\log\log$ by the first Chebyshev
function $\theta(x):=\sum\\{\log p:p\leq x\\}$ (cf [6, 3.1]).

Theorem. RRI is equivalent to each of the following three conditions:

$\forall\varepsilon>0\ \forall x>1:\ Q(x)<C_{\varepsilon}x^{-0.5+\varepsilon}\
$ $None$ $\ \forall\varepsilon>0\ \forall x>1:\
Q(x)>-C_{\varepsilon}x^{-0.5+\varepsilon},$ $None$ $\quad
A_{0}:=\limsup_{x\to+\infty}\ Q(x)\sqrt{x}\log x<+\infty.$ $None$

In addition, (1.10) necessarily implies that $A_{0}\leq 2\sqrt{2}$; for this
reason the situation $2\sqrt{2}<A_{0}<+\infty$ is logically impossible.

The proof of the Theorem is set forth in Sect. 3; in Section 2 all needed
auxillaries and the main Lemma are adduced; in Sect. 4 some corollaries and
directions of further research are given.

2\. Some known facts and main lemma

Further the well-known assertions are brought together concerning the
asymptotic behavior of primes [6, Ch. 5] in their weak form sufficient for our
purposes:

Proposition 1. (i) For all $x>1$ one has $|\theta(x)-x|<C_{0}x/\log x;$

(ii) $\ p_{k+1}-p_{k}<C_{1}p_{k}/\log p_{k}$;

(iii) RH is equivalent to each of the two relationships:

$\forall{\varepsilon}>0\exists C_{{\varepsilon}}\forall
x>1:|\theta(x)-x|<C_{{\varepsilon}}x^{0.5+{\varepsilon}};\ \
|\theta(x)-x|<\frac{\sqrt{x}\log^{2}x}{8\pi},\ x>X_{0}.$ $None$

For the sequel we will need the (perhaps also well-known) ascertion, which
follows from Proposition 1(i):

Proposition 2.  Let $\lambda>1$; then for all
$x>X_{\lambda}:=\exp(\max(1,2/(\lambda-1)))$ one has:

$Y=Y(x,\lambda):=\sum_{p>x}\frac{1}{p^{\,\lambda}}=\frac{1+\delta(x,\lambda)}{(\lambda-1)x^{\lambda-1}\log
x};\quad|\delta(x,\lambda)|<\frac{C_{1}}{(\lambda-1)\log x}.$ $None$

$\triangleright$ In fact, using the integration by parts one obtains

$Y=\int_{x^{+}}^{\infty}\frac{d\theta(t)}{t^{\lambda}\log
t}=\frac{\theta(t)}{t^{\lambda}\log t}\
\Bigg{|}_{x^{+}}^{\infty}-\int_{x}^{\infty}\theta(t)\left(\frac{1}{t^{\lambda}\log
t}\right)^{\prime}dt$ $=-\frac{\theta(x^{+})}{x^{\lambda}\log
x}+\int_{x}^{\infty}\frac{\theta(t)(\lambda\log
t+1)}{t^{\lambda+1}\log^{2}t}\,dt$ $None$

Analogously, replacing here $\theta(t)$ by $t$ one obtains the identity:

$J=J(x,\lambda):=\int_{x}^{\infty}\frac{dt}{t^{\lambda}\log
t}=-\frac{x}{x^{\lambda}\log x}+\int_{x}^{\infty}\frac{t\ (\lambda\log
t+1)}{t^{\lambda+1}\log^{2}t}\,dt$ $=-\frac{1}{x^{\lambda-1}\log x}+\lambda
J+\frac{{\beta}J}{\log x};\hbox{ where }0<{\beta}={\beta}(x,\lambda)<1\hbox{
for }x>X_{\lambda},$ $None$

whence it follows that for all $x>X_{\lambda}$ (explanations below):

$J(x,\lambda)=\frac{1}{(\lambda-1)x^{\lambda-1}\log
x\left(1-\frac{{\beta}}{(\lambda-1)\log x}\right)}$ $\Rightarrow\quad
0<J(x,\lambda)-\frac{1}{(\lambda-1)x^{\lambda-1}\log
x}<\frac{2}{(\lambda-1)^{2}x^{\lambda-1}\log^{2}x}.$ $None$

Here we have taken into accout that since $x>X_{\lambda}$ then by virtue of
the $X_{\lambda}$-definition the number $t:=1/(\lambda-1)\log x$ belongs to
the interval $(0,1/2)$ and hence the inequality $1/(1-t)<1+2t$ holds.

On the other hand, substracting (2.4) from (2.3) and using Proposition 1(i)
leads to:

$|Y-J|\leq\frac{|\theta(x^{+})-x|}{x^{\lambda}\log
x}+\int_{x}^{\infty}\frac{|\theta(t)-t|(\lambda\log
t+1)}{t^{\lambda+1}\log^{2}t}\,dt$ $\leq\frac{C_{0}}{\log
x}\left(\frac{2}{x^{\lambda-1}\log
x}+J\right)<\frac{4C_{0}}{(\lambda-1)x^{\lambda-1}\log^{2}x},\quad\forall
x>X_{\lambda}.$ $None$

Joining (2.6) with (2.5) one comes to (2.2) $\Box$.

The main role in the proof of the Theorem plays the following unconditional
assertion, binding Mertens function $S(x)$ and Gronwall numbers $G(N)$, which
is the most important and complicated part of the paper.

Lemma. For any $k\in\mathbb{N}$ there are a real number $\delta_{k},\
(\\{\delta_{k}\\}\to 0$ as $k\to\infty),$ and an integer $N_{k}^{*}$ such that
$\hbox{\bf gpf}(N_{k}^{*})=p_{k}$ and

$\log
G(N_{k}^{*})>S(p_{k})-\log\log\theta(p_{k})-\frac{2\sqrt{2}+\delta_{k}}{\sqrt{p_{k}}\log
p_{k}}.$ $None$

$\triangleright$ 1) First we describe the special construction of
$\\{N_{k}^{*}\\}_{k=1}^{\infty}$ providing (2.7).

We’ll suppose that $k$ is large enough; put $r=r_{k}:=[\sqrt{\log 2p_{k}}],$
and define:

$\ \ q_{1}:=p_{k},\quad q_{m}:=\max\\{p_{j}:p_{j}^{m}\leq{2p_{k}}\\},\ 2\leq
m\leq r.$ $None$

In other words, $q_{m}=q_{m,k}$ is the greatest prime $\leq(2p_{k})^{1/m}$;
hence $q_{m-1}<q_{m}$ for all $m,1<m\leq r.$ From Proposition 3 one may easily
deduce that the quantity $q_{m,k}=(2p_{k})^{1/m}(1-\delta_{k,m});\
0\leq\delta_{k}:=\max_{1<m\leq r}\delta_{k,m}\to 0,\ k\to\infty$.

Let $\nu=\nu_{r}:=\max\\{j:p_{j}\leq q_{r}\\},\ H:=q_{r}^{r+1}$; define the
exponents $\\{\alpha_{j}\\}_{j=1}^{k}$

$\alpha_{j}:=\left[\frac{\log H}{\log p_{j}}\right]-1,\ \ \hbox{if
}j<\nu;\quad\alpha_{j}:=\max\\{m\leq r:q_{m}\geq p_{j}\\},\ \hbox{if
}j\geq\nu;$ $None$

It is clear that: 1) $\alpha_{\nu}=\alpha_{\nu+1}=r,\ p_{\nu}=q_{r},$ 2)
$\alpha_{j}\geq\alpha_{j+1},\ 1\leq j<k$,
3) the equality $\alpha_{j}=m<r$ is equivalent to $q_{m+1}<p_{j}\leq q_{m}.$

Let $T(x):=\exp(\theta(x))$ stand for a product of all primes $p\leq x.$

Now we are able to determine the numbers $N_{k}^{*},$ for which the
relationship (2.7) is guaranteed:

$N_{k}^{*}:=\prod_{m=1}^{r}T(q_{m})\cdot\prod_{j=1}^{\nu-1}p_{j}^{\alpha_{j}-r}=\prod_{j=1}^{k}p_{j}^{\alpha_{j}}.$
$None$

2) Let’s study the quantity $\eta=\eta_{k}:=\log
N_{k}^{*}=E_{k}+F_{k};E_{k}:=\sum_{m=1}^{r}\theta(q_{m}),\\\
F_{k}:=\sum_{j=1}^{\nu-1}(\alpha_{j}-r)\log p_{j}.$ Having taken into account
the definition (2.8) of $q_{m}$ and the relationships:
$\max\\{|1-\theta(q_{m,k})(2p_{k})^{-1/m}|:1<m\leq r\\}\to 0,\ k\to\infty,$
$\nu<p_{\nu}=q_{r}<(2p_{k})^{1/r},\log H=(r+1)\log q_{r},$ one has:

$\ E_{k}:=\theta(p_{k})+C_{k}\sqrt{p_{k}}+O(p_{k}^{1/3}\sqrt{\log 2p_{k}}),\
C_{k}\to\sqrt{2},\ k\to\infty;$ $\qquad 0<F_{k}<\nu\log H<q_{r}(r+1)\log
q_{r}=O(p_{k}^{{\varepsilon}})\
\Rightarrow\eta_{k}-\theta(p_{k})\approx\sqrt{2p_{k}}.$ $None$

3) From (1.4) and (1.2) it follows that

$\log G(N_{k})=\log\frac{\sigma(N_{k})}{N_{k}}-\log\log\log
N_{k}=\sum_{j=1}^{k}\log\
\frac{p_{j}^{\alpha_{j}+1}-1}{p_{j}^{\alpha_{j}}(p_{j}-1)}-\log\log\eta_{k}$
$=\sum_{j=1}^{k}\log\
\frac{p_{j}}{p_{j}-1}-\sum_{j=1}^{k}\log\frac{p_{j}^{\alpha_{j}+1}}{p_{j}^{\alpha_{j}+1}-1}-\log\log\eta_{k}=S_{k}-U_{k}-V_{k}.$
$None$

Now with certain $t_{k}$ in between of $\theta(p_{k})$ and $\eta_{k}$, one
has:

$V_{k}-\log\log\theta(p_{k})=\frac{\eta_{k}-\theta(p_{k})}{t_{k}\log
t_{k}}\approx\frac{\sqrt{2}}{\sqrt{p_{k}}\log p_{k}},\quad k\to\infty.$ $None$

4) To make sure that the quantity $U_{k}$ is also
$\approx\sqrt{2}/\sqrt{p_{k}}\log p_{k}$ as $k\to\infty$, we present it as a
sum:

$U_{k}=\sum_{m=1}^{r}U_{k,m};\qquad U_{k,m}:=\sum_{q_{m+1}<p_{j}\leq
q_{m}}\log\frac{p_{j}^{m+1}}{p_{j}^{m+1}-1},\ m<r;$ $\quad
U_{k,r}:=\sum_{j=1}^{\nu-1}\log\frac{p_{j}^{\alpha_{j}+1}}{p_{j}^{\alpha_{j}+1}-1}.$
$None$

All summands $U_{k,m}$ here are positive. Using the elementary inequality:
$-t^{2}<\log(1-t)+t<0,\ 0<t<1/4$, easily deduced from the Taylor formula, one
may assert that for $m<r,\ k>k_{0}$ and some $\delta_{j,m}\in(0,1)$:

$U_{k,m}=\sum_{q_{m+1}<p_{j}\leq
q_{m}}-\log\left(1-\frac{1}{p_{j}^{m+1}}\right)=\sum_{q_{m+1}<p_{j}\leq
q_{m}}\left(\frac{1}{p_{j}^{m+1}}+\frac{\delta_{j,m}}{p_{j}^{2m+2}}\right),$
$None$

5) Recollecting now the definition (2.2) of the quantity $Y(x,\lambda)$ in
Proposition 2, we may rewrite the latter equality as follows:

$U_{k,m}=Y(q_{m+1},m+1)-Y(q_{m},m+1)+W_{k,m};$ $\quad
0<W_{k,m}<Y(q_{m+1},2m+2),\ 1\leq m<r.$ $None$

Applying the relationship (2.2) with $\lambda=m+1,\ 2m+2,\ x=q_{m+1},q_{m},$
and having taken into account that $q_{m+1}\approx(2p_{k})^{1/(m+1)}$, by
virtue of defining formula (2.8), one comes to the estimates

$U_{k,m}<\frac{1}{mq^{m}_{m+1}\log q_{m+1}}\left(1+\frac{C_{1}}{\log
q_{m+1}}\right)<{C_{2}}\ p_{k}^{-m/(m+1)};\quad m<r.$ $None$

Further, for $m=r$ due to the fact that $\alpha_{j}\log p_{j}>(r+1)\log
q_{r}-\log p_{\nu}$ for $j<\nu$ (cf. the left part of definition (2.9)) and
$\nu<p_{\nu}=q_{r}$, one obtains:

$U_{k,r}<{2}\sum_{j=1}^{\nu-1}\frac{1}{p_{j}^{\alpha_{j}+1}}<\frac{2\nu
p_{\nu}}{q_{r}^{r+1}}<\frac{2}{q_{r}^{r-1}}<\frac{3}{(2p_{k})^{1-1/r}}=O(p_{k}^{-1+{\varepsilon}}).$
$None$

From these two estimates it follows that for $k$ large enough:

$\sum_{m=2}^{r}U_{k,m}<C_{2}p_{k}^{-2/3}(\log p_{k})^{1/2}.$ $None$

6) At last, if $m=1$, then again by virtue of Proposition 2, one has

$U_{k,1}=Y(q_{2},2)+O(p_{k}^{-1})=\frac{1+O(1/\log
x)}{\sqrt{2p_{k}}\log\sqrt{2p_{k}}}=\frac{\sqrt{2}+O(1/\log
p_{k})}{\sqrt{p_{k}}\log p_{k}}.$ $None$

whence in junction with (2.13) and (2.19) it follows that
$U_{k}\approx\sqrt{2}/\sqrt{p_{k}}\log p_{k}$, and joining this with (2.11),
(2.12), one comes to the limit relationship:

$\log
G(N_{k}^{*})-(S(p_{k})-\log\log\theta(p_{k}))\approx\frac{2\sqrt{2}}{\sqrt{p_{k}}\log
p_{k}},\quad k\to\infty,$ $None$

which in turn implies (2.7) $\ \Box$.

Now we have got all the tools needed to move forward.

3\. Proof of the Theorem

Sufficiency.  $\triangleright$ Due to Nicolas result (cf [7], [2], Sect. 4)
the negation of RH implies $Q(x)=\Omega_{\pm}(x^{-b})$ for some $b\in(0,0.5)$,
i. e. according to the meaning of the symbol $\Omega_{\pm}$, for some
$\delta>0$ and any $X>0$ there are $y>z>X$ such that $Q(y)>\delta y^{-b},\
Q(z)<-\delta z^{-b}$, but each of these two inequalities contradicts (resp.)
to (1.8), (1.9). Besides, obviously (1.10) $\Rightarrow$ (1.8).

Thus it is proved that each of (1.8), (1.9) and (1.10) implies RH $\Box$.

Necessity.  $\triangleright$ Let us suppose that (1.10) is false, or more
precisely, that $B_{0}>2\sqrt{2}$; then taking into account the relationships
(1.2), (1.7) and (1.10), one may conclude that for any fixed
$\varepsilon_{1}\in(0,B_{0}-2\sqrt{2})$ the set

$K_{\varepsilon_{1}}:=\left\\{k:Q(p_{k})>\frac{2\sqrt{2}+\varepsilon_{1}}{\sqrt{p_{k}}\log
p_{k}}\right\\}\quad\hbox{is {\it infinite.} }$ $None$

But then by virtue of Lemma and the equality
$Q(x)=S(x)-\log\log\theta(x)-\gamma,$ (cf (1.7), (2.1)) one obtains for all
sufficiently large $k\in{K}_{\varepsilon_{1}}$

$\log
G(N_{k}^{*})>\gamma+Q(p_{k})-\frac{2\sqrt{2}+\delta_{k}}{\sqrt{p_{k}}\log
p_{k}}>\gamma+\frac{\varepsilon_{1}-\delta_{k}}{\sqrt{p_{k}}\log
p_{k}}>\gamma,$ $None$

because $\delta_{k}\to 0,\ k\to\infty,$ whereas $\varepsilon_{1}>0,$ and
consequently RH holds false.

Further, assuming RH one deduces from (1.2), (1.7) and Proposition 1(iii),
that there is $t,(t-x)(t-\theta(x))<0$ for which

$|R(x)-Q(x)|=\frac{|\theta(x)-x|}{t\log t}<\frac{1+o(1)}{8\pi\sqrt{x}\log x},$
$None$

and joining this with Robin’s estimate $|R(x)|<\log x/(8\pi\sqrt{x})$,
mentioned in Sect. 1, one obtains $|Q(x)|<(1+o(1))\log x/(8\pi\sqrt{x})$,
which in turn implies (1.9) $\Box$.

This completes the Theorem’s proof.

4\. Conclusive Remarks.

1) The assertions in Theorem may be presented in a discrete form, when $x$ in
(1.2) runs only the sequence of primes $\\{p_{j}\\}_{j=1}^{\infty}$.

2) One may also replace in (1.2) $\log(p/p-1)$ by primes reciprocals $1/p$.

Corollary. The Ramanujan inequality (1.6) (and thus RH) is equavalent to each
of the following three unilateral estimates for all suficiently large $k$:

$\qquad\qquad\quad\sum_{j=1}^{k}\frac{1}{p_{j}}<\log\log\theta(p_{k})+B_{1}+p_{k}^{-0.5+\varepsilon},\quad\forall\
{\varepsilon}>0;$ $None$
$\qquad\qquad\quad\sum_{j=1}^{k}\frac{1}{p_{j}}>\log\log\theta(p_{k})+B_{1}-p_{k}^{-0.5+\varepsilon},\quad\forall\
{\varepsilon}>0;$ $None$
$\qquad\qquad\quad\sum_{j=1}^{k}\frac{1}{p_{j}}<\log\log\theta(p_{k})+B_{1}+\frac{A_{0}}{\sqrt{p_{k}}\log
p_{k}},\quad A_{0}<\infty,$ $None$

where $B_{1}$ stands for the Meissel-Mertens constant:

$\qquad
B_{1}:=\lim_{k\to\infty}\left(\sum_{j=1}^{k}\frac{1}{p_{j}}-\log\log\theta(p_{k})\right)=\gamma-\sum_{p}\left(\log\frac{p}{p-1}-\frac{1}{p}\
\right)$ $=\gamma-\sum_{p}\sum_{k=2}^{\infty}\frac{1}{kp^{k}}=0.261\ 497\dots$
$None$

For the proof one should use the Theorem and notice that (cf. (1.2))

$\sum_{j=1}^{k}\left(\frac{1}{p_{j}}+\log\left(1-\frac{1}{p_{j}}\right)\right)=B_{1}-\gamma+O\left(\frac{1}{p_{k}}\right).$
$None$

3) Quite recently the author established (combining the method by Ingham [8,
Sect. V. 10] with the properties of the so called locally G-maximal numbers,
studied in [9, Sect 2]), that if in (1.10) $A_{0}<+\infty$, and thus RH is
true, then necessarily

$1.5-{\varepsilon}\ <\ Q(x)\sqrt{x}\log x\ <\ 2.5+{\varepsilon},\ \forall\
x>X_{{\varepsilon}}$ $None$

whence one may deduce the relationship:

$\max\\{\log G(N):{\bf gpf}(N)=p_{k}\\}=\gamma-\frac{a_{k}}{\sqrt{p_{k}}\log
p_{k}};$
$2\sqrt{2}-2.5-{\varepsilon}<a_{k}<2\sqrt{2}-1.5+{\varepsilon},\quad\forall\
k>K_{{\varepsilon}},$ $None$

which quantitatively refines the initial Ramanujan inequality (1.6).

These results will be presented in the next author’s papers.

LIST OF REFERENCES

[1] Mertens F. $\ddot{U}ber$ einige asymptotische Gesetze der Zahlentheorie.

J. Reine Angew. Math., 77, 1874, pp. 289 – 338.

[2] Robin G. Grandes valeurs de la fonction somme des diviseurs et hypothèse

de Riemann. J. Math. Pures Appl. V. 63 (1984), pp. 187 – 213.

[3] Caveney G., Nicolas J.-L., Sondow J. Robin’s theorem, primes,

and a new elementary reformulation of Riemann Hypothesis.

INTEGERS 11 (2011), #A33, pp 1 – 10.

[4] Gronwall T.H. Some asymptotic expressions in the theory of numbers.

Trans. Amer. Math. Soc. V. 14 (1913), pp. 113 – 122.

[5] Ramanujan S. Highly composite numbers, annotated and with a foreword

by J.-L. Nicolas and G. Robin, Ramanujan J. V. 1, 1997, pp. 119 – 153.

[6] Narkiewicz W. The Development of Prime Number Theory.

Springer-Verlag Berlin Heidelberg New York, 2000.

[7] Nicolas J.-L. Petites valeurs de la fonction d’Euler.

Journal of Number Theory, vol. 17, no. 3, 1983, p. 375 – 388.

[8] Ingham A. E. Distribution of Prime Numbers.

Cambridge at the University Press, 1932.

[9] Kalyabin G. A. One-Step $G$-Unimprovable Numbers.

https://arxiv.org/abs/1810.12585, 2018.


Mark A. Siebert & Anthony J. Remijan Clues to PPN Chemical Evolution: The
Unique Molecular Environment of V510 Pup

17 2021 10.1017/xxxxx

Proceedings IAU Symposium

# IAU384_Siebert_Proceeding

Mark Siebert  Mark A. Siebert1 & Anthony J. Remijan2<EMAIL_ADDRESS>1Department of Astronomy, University of Virginia, Charlottesville, VA 22904,
USA
email:
2National Radio Astronomy Observatory, Charlottesville, VA 22903, USA

(November 2023)

# Clues to PPN Chemical Evolution: The Unique Molecular Environment of V510
Pup

Mark Siebert  Mark A. Siebert1 & Anthony J. Remijan2<EMAIL_ADDRESS>1Department of Astronomy, University of Virginia, Charlottesville, VA 22904,
USA
email:
2National Radio Astronomy Observatory, Charlottesville, VA 22903, USA

(November 2023)

###### Abstract

V510 Pup (IRAS 08005-2356) is a binary post-AGB system with a fast molecular
outflow that has been noted for its puzzling mixture of carbon- and oxygen-
rich features in the optical and infrared. To explore this chemical dichotomy
and relate it to the kinematics of the source, we present an ACA spectral line
survey detailing fourteen newly detected molecules in this pre-planetary
nebula. The simultaneous presence of CN/C2H/HC3N and SO/SO2 support the
previous conclusion of mixed chemistry, and their line profiles indicate that
the C- and O-rich material trace distinct velocity structures in the outflow.
This evidence suggests that V510 Pup could harbor a dense O-rich central waist
from an earlier stage of evolution, which persisted after a fast C-rich
molecular outflow formed. By studying the gas phase composition of this unique
source, we aim to reveal new insights into the interplay between dynamics and
chemistry in rapidly evolving post-AGB systems.

###### keywords:

Stellar evolution, circumstellar matter, astrochemistry, post-AGB stars

††editors: C. Sterken, J. Hearnshaw & D. Valls-Gabaud, eds.

##  1 Introduction

The nebulae surrounding evolved stars undergoing mass loss represent important
sites of recycling for metal-rich gas and dust in our Galaxy. As
low–intermediate mass stars leave the Asymptotic Giant Branch (AGB), their
circumstellar envelopes undergo dramatic changes: transitioning from slow,
spherical winds to complex bipolar/multipolar outflows seen in planetary
nebulae (PNe) (Sahai et. al, 2011). These dynamics are often met with a
chemical transition as well, with molecules and dust being increasingly
affected by conditions including high-velocity shocks, internal UV radiation,
and AGB dredge up events (Pardo et al., 2007; Weiss et al., 2009). The
mechanisms for the physical and chemical changes during the transitional pre-
planetary nebula (PPN) phase are still not fully understood, but recent work
has shown that binary and common envelope interactions are key to this
evolution (e.g. Sahai et. al, 2018).

One puzzling class of object that is critical to understanding the chemical
output of evolved stars are PPNe showing signs of mixed chemistry. Stellar
outflows are designated as either carbon- or oxygen-rich depending on the C/O
ratio of the central star, which typically determines the molecular and dust
grain composition throughout the wind (Höfner et al., 2018). However, it
appears that this dichotomy is not universal, especially as stars evolve off
the AGB. Evidence of this includes the widespread IR observations of fullerene
and PAH features toward O-rich PNe (Gielen et al., 2011), as well as the
existence of “silicate carbon stars” which have C-rich photospheres but are
surrounded by O-rich circumstellar dust, and often show OH masers (Ohnaka et
al., 2013).

V510 Pup (IRAS 08005-2356) is post-AGB star surrounded by a young high-
velocity outflow that shows clear evidence of mixed chemistry. It exhibits OH
maser emission typical of O-rich evolved stars (Zijlstra et. al, 2001), but
also shows optical absorption lines from C2 and CN (Bakker et al., 1997). The
extreme dynamics of V510 Pup were characterized recently by Sahai & Patel
(2015), where broad (${\sim}$200 km/s) line profiles were observed in CO and
SiO using the Submillimeter Array (SMA). Analysis of the velocity gradient
across the nebula showed that radiation pressure alone is insufficient to
drive the outflow. Optical observations later discovered that V510 Pup is part
of a radial-velocity binary, and that its H$\alpha$ line profile modulates
with the seven-year orbital period, confirming that the high-velocity bipolar
outflow originates from accretion onto a close binary companion (Manick et
al., 2021). This makes it the only extreme PPN whose jet origin is directly
observed.

V510 Pup is at a critical point in its evolution to offer new insights into
chemical transitions and binary interaction in exotic PPNe, but it lacks key
constraints on its gas phase chemical inventory. To address this, a detailed
spectroscopic study of this source is needed to determine the molecular
abundances and their relationship to kinematic structures within the wind. We
used interferometric observations from the Atacama Compact Array (ACA) to
perform these measurements, and reveal the unique dynamics of C- and O-rich
material in this source.

##  2 Observations

We utilize archival data from a Cycle 6 ACA filler program which observed 16
evolved stars transitioning between the AGB and PNe phases (Project code
2018.A.00047.S). These data include spectral line observations of V510 Pup
covering the entirety of Bands 3 and 6 (85–115 GHz, and 211–274 GHz) at
$1{\sim}3$ km/s velocity resolution. Calibrated visibilities were produced
using the standard pipeline of the Common Astronomy Software Application
(CASA; McMullin et al., 2007), and each spectral window was then continuum-
subtracted, then imaged and deconvolved using the tclean CASA task with briggs
weighting. The resulting rms sensitivity ranges between 5 and 13 mJy/beam
among the 56 spectral windows. Some spectral windows overlap in their
frequency coverage, so these data were combined in the visibility plane to
improve sensitivity. The ACA beam size is $10.1"$–$11.5"$ and $4.3"$–$5.3"$ at
Bands 3 and 6, respectively. This is notably larger than the ${\sim}2"$
nebular extent of V510 Pup observed by Sahai & Patel (2015), meaning a spatial
analysis was not possible with these data, and our study is purely
spectroscopic.

##  3 Results & Analysis

###  3.1 Detected species and line profiles

We detect emission from a total of 16 molecules and isotopologues toward V510
Pup, 13 of which have not yet been observed in this source. A list of all
detected species is shown in Table 1, including the number of lines observed
of each, and whether they are typically found in C- or O-rich sources, using
Ziurys (2006) as reference. All these molecules are common in evolved stars
environments, including “parent” molecules originating from the stellar
atmosphere (e.g. SO, HCN, CS), as well as species produced through
photochemistry like HCO+, HNC, HC3N, and C2H (Woods et. al, 2003). The
remarkable result seen in Table 1 is the presence of characteristic O-rich
molecules (SO, SO2) paired with C-rich species (HNC, CN, C2H, and HC3N). This
is the first AGB-related source with simultaneous detections of all these
molecules, lending support to previous classifications of mixed chemistry.

Table 1: Summary of detected molecules and isotopologues

Molecule | No. of transitions | Range in Eup (K) a | Velocity Component(s)b | Chemistryc
---|---|---|---|---
^12CO | 2 | 10 – 30 | CV, MV, HV | Both
^13CO | 2 | 10 – 30 | CV, MV, HV | Both
SiO | 3 | 6 – 45 | CV, MV, HV | Both
^29SiO | 2 | 31 – 45 | CV, MV, HV | Both
^30SiO | 2 | 31 – 45 | CV, MV, HV | Both
HCN | 1 | 26 | CV, MV | Both
H^13CN | 1 | 25 | CV, MV | Both
CS | 1 | 35 | CV(?), MV | C-rich
C^34S | 1 | 28 | MV | C-rich
HCO+ | 1 | 26 | CV, MV | Both
SO | 5 | 44 – 56 | CV | O-rich
SO2 | 9 | 24 – 94 | CV | O-rich
HNC | 1 | 26 | MV | C-rich
CN | 1 | 16 | MV | C-rich
C2H | 1 | 25 | MV | C-rich
HC3N | 7 | 131 – 203 | MV | C-rich

Notes: aUpper state energies obtained from Cologne Database of Molecular
Spectroscopy (CDMS) Müller et al. 2005. bLSR velocity ranges of the CV, MV,
and HV components are defined in Section 3.1 and shown in Fig. 1. cDenotes
whether a particular molecule is typically associated with a carbon- or
oxygen-rich surface chemistry in circumstellar envelopes, using the list from
Ziurys (2006).

The peculiar chemistry of V510 Pup can be further explored using the kinematic
information provided by molecular line profiles. Figure 1 shows a sample of
these spectra. The full extent of the extreme outflow can be seen in the broad
CO and SiO line profiles which span the range between $-150$ and $200$ km/s.
Following Sahai & Patel (2015), we decompose this into three main velocity
components: a central component (CV) centered on the system velocity
($V_{\mathrm{sys}}=48$ km/s), a intermediate component (MV) at
$V_{\mathrm{sys}}\pm 50$ km/s, and high-velocity wings (HV) at
$V_{\mathrm{sys}}\pm 110$ km/s, all shown in Fig. 1. With the improved
sensitivity on the ^13CO $J=2-1$ line now available, we note that the CV
component has a narrow feature (width $<10$ km/s) appearing on top of the
broad line profile, similar to how this transition was appears toward the
similar extreme PPN HD 101584 (Olofsson et al., 2019). This narrow CV
component is also observed isolated from the MV and HV components in the
emission profiles of SO, SO2, and HCN. Table 1 also lists which velocity
components are detected for each molecule. We find that all molecules which
are primarily associated with carbon-rich outflows appear solely in the MV
component, while oxygen-rich species are located in the narrow CV region. This
can be seen in the middle and right panels of Fig. 1.

Figure 1: Emission line profiles of various molecules measured by the ACA
toward V510 Pup. The central velocity (CV), medium-velocity (MV), and high-
velocity (HV) components are defined in the left panel. Species that are
typically associated with O- and C-rich evolved stellar outflows are shown in
the middle and right panels, respectively. Spectra were extracted from an
aperture with diameter 10” centered on the position of the post-AGB star. Some
transitions are scaled for comparison.

Figure 2 shows the measured brightnesses of SO ($6_{5}$–$5_{4}$) and HC3N
(24–23) relative to ^13CO compared with more well-studied PPNe for which these
transitions have been observed previously (Olofsson et al., 2019; Pardo et
al., 2004). From this, we see that the CV component of V510 Pup is chemically
similar to O-rich sources like HD 101584, while the MV component is like the
prototypical C-rich PPN CRL 618. Furthermore, this comparison provides
evidence that the narrow CV is not depleted in its molecular chemistry as is
the case for the Red Rectangle and other “disk-prominent” post-AGBs (Gallardo
Cava et al., 2022).

Figure 2: Comparison of integrated molecular line brightness (relative to
^13CO) for SO (red) and HC3N (blue) among a sample of nearby PPNe. For V510
Pup, the O-rich central and C-rich medium velocity components are labeled CV
and MV, respectively. Hatched regions denote upper limits, while solid regions
indicate detected transitions. Data for sources other than V510 Pup adapted
from Olofsson et al. (2019), Gallardo Cava et al. (2022), and Pardo et al.
(2004).

###  3.2 LTE modeling

To obtain estimates on the abundances of detected molecules, we model the
observed transitions assuming local thermodynamic equilibrium (LTE). This
assumption is necessary since we lack spatial data and constraints on the
physical conditions of the velocity components to perform a full radiative
transfer analysis. To simulate line profiles and fit the transitions, we use
the publicly available package molsim (Lee, 2021). For each velocity
component, we perform a least-squares minimization of the column density,
rotational temperature, and line width of a given molecule. For species where
only one transition was available, we fix the rotational temperature to that
obtained for SO (CV) or HC3N (MV). We employ the same procedure for ^13CO,
simultaneously fitting the overlapping CV, MV, and HV components. Then,
assuming a ^13CO/H2 ratio of $3.9\times 10^{-5}$ (Sahai & Patel, 2015), we use
the relative column densities to calculate final abundances. While this
eliminates the need to adopt an explicit angular source size, it does assume
that this size is equal to that of ^13CO emission (whether in the CV or MV
component).

Figure 3: Examples of LTE emission line fits for SO (left panels) and HC3N
(right panels). ACA spectrum shown in black, while colored lines represent
fitted molsim simulation. For SO, a narrow (magenta dashed) and wide (green
dashed) gaussian were needed to reproduce the shape of the CV component. For
HC3N, one component was used, centered on the red-shifted side of the MV
region. Table 2: Measurements on physical conditions of optically thin species
in the outflow of V510 Pup

Molecule | Component | Trot (K) |  $f_{\mathrm{H2}}$ (err.)
---|---|---|---
SO | CV | $43\pm 13$ |  $4.5\times 10^{-6}$ $(1.0)$
SO2 | CV | $57\pm 18$ |  $4.8\times 10^{-6}$ $(0.9)$
HC3N | MV | $63\pm 16$ |  $1.6\times 10^{-6}$ $(0.6)$
CS | MV | 63a |  $5.1\times 10^{-6}$ $(0.5)$
CN | MV | 63a |  $1.3\times 10^{-5}$ $(0.1)$
C2H | MV | 63a |  $2.8\times 10^{-6}$ $(0.3)$

Notes: aRotational temperature of HC3N adopted for abundance calculation.

The results of this analysis are shown in Figure 3 and Table 2. We find that
the CV component exhibits excitation temperatures between 40–60 K, while the
MV component (measured by HC3N) is about 63 K. These values are in line with
the temperatures found in the slowly expanding equatorial waist and the
bipolar outflow of HD 101584 (Olofsson et al., 2019). The abundances of
molecules observed in the MV component are close (within a factor of five) to
their measured abundances in C-rich AGB stars (Agúndez et al., 2017; Massalkhi
et al., 2019), indicating that this component does derive from acetylene-rich
stellar material.

##  4 Conclusions

Using archival ACA observations, we analyzed the millimeter spectrum of V510
Pup to provide some of the first constraints on its molecular inventory. The
new sensitivity and velocity information offered by our spectra indicate that
not only does V510 Pup exhibit mixed chemistry in its outflow, but the carbon-
and oxygen-rich material is separated into reservoirs of gas that are
morphologically unique. The line profiles of the newly characterized CV
component appear remarkably similar to the “disk-prominent” subclass of post-
AGB stars (Gallardo Cava et al., 2022), as well as the central region of the
similar PPN HD 101584 (Olofsson et al., 2019). These equatorial density
enhancements (EDEs) are common in PPNe and PNe, and recent works suggest that
they can form during the AGB phase through binary-shaping (Sahai et. al, 2022;
Decin et al., 2020). Thus, one possible explanation for the observed chemistry
(summarized in Fig. 4) is that V510 Pup harbors a slowly expanding waist from
an earlier stage of evolution when its surface chemistry was O-rich, then as
its fast bipolar outflow formed it also underwent a transition to ejecting
C-rich material. This scenario has been proposed to explain mixed dust
features in silicate carbon stars (Ohnaka et al., 2013), but the observations
presented here provide some of the first kinematic evidence for it. To confirm
this, future observations of V510 Pup at higher resolution will be critical,
as spatially resolving the chemically distinct CV, MV, and HV components will
allow one to determine their physical conditions and dynamical histories.

This paper makes use of the following ALMA data: ADS/JAO.ALMA#2018.A.00047.S.
ALMA is a partnership of ESO (representing its member states), NSF (USA) and
NINS (Japan), together with NRC (Canada), MOST and ASIAA (Taiwan), and KASI
(Republic of Korea), in cooperation with the Republic of Chile. The Joint ALMA
Observatory is operated by ESO, AUI/NRAO and NAOJ. The National Radio
Astronomy Observatory is a facility of the National Science Foundation
operated under cooperative agreement by Associated Universities, Inc. Support
for this work and travel was provided to M. A. S. by the NSF through the Grote
Reber Fellowship Program administered by Associated Universities,
Inc./National Radio Astronomy Observatory.

Figure 4: Diagram of the circumstellar environment of V510 Pup as suggested by
our ACA analysis of its millimeter spectrum. Includes major morphological
structures and their velocities, as well as the observed chemistry in each
region. Proposed components include a carbon-rich bipolar outflow (red and
blue), and a slowly expanding oxygen-rich equatorial waist surrounding the
central binary (brown).

## References

  * Agúndez et al. (2017) Agúndez, M., Cernicharo, J., Quintana-Lacaci, G., et al. 2017, A&A, 601, A4
  * Bakker et al. (1997) Bakker, E. J., van Dishoeck, E. F., Waters, L. B. F. M., et al. 1997, A&A, 323, 469
  * Decin et al. (2020) Decin, L., Montargès, M., Richards, A. M. S., et al. 2020, Science, 369, 1497
  * Gallardo Cava et al. (2022) Gallardo Cava, I., Bujarrabal, V., Alcolea, J., et al. 2022, A&A, 659, A134
  * Fu et al. (2012) Fu, R. R., Moullet, A., Patel, N. A., et al. 2012, ApJ, 746, 42
  * Gielen et al. (2011) Gielen, C., Cami, J., Bouwman, J., et al. 2011, A&A, 536, A54
  * Höfner et al. (2018) Höfner, S., & Olofsson, H. 2018, A&A Revs, 26, 1
  * Lee (2021) Lee, K. 2021, Zenodo, 10.5281/zenodo.4560750
  * Manick et al. (2021) Manick, R., Miszalski, B., Kamath, D., et al. 2021, MNRAS, 508, 2226
  * Massalkhi et al. (2019) Massalkhi, S., Agúndez, M., Cernicharo, J. 2019, A&A, 628, A62
  * McMullin et al. (2007) McMullin, J. P., Waters, B., Schiebel, D., et al. 2007, Astronomical Society of the Pacific Conference Series, 376, 127
  * Ohnaka et al. (2013) Ohnaka, K., Boboltz, D. A., Mulitz-Schimel, G., et al. 2013, A&A, 559, A120
  * Olofsson et al. (2019) Olofsson, H., Khouri, T., Maercker, M., et al. 2019, A&A, 623, A153
  * Pardo et al. (2004) Pardo, J. R., Cernicharo, J., Goicoechea, J. R., et al. 2004, ApJ, 615, 495
  * Pardo et al. (2007) Pardo, J. R., Cernicharo, J., Goicoechea, J. R., et al. 2007, ApJ, 661, 250
  * Sahai et. al (2011) Sahai, R., Claussen, M. J., Schnee, S., et al. 2011, ApJL, 739, L3
  * Sahai & Patel (2015) Sahai, R., & Patel, N. A., 2015, ApJL, 810, L8
  * Sahai et. al (2018) Sahai, R., Sánchez Contreras, C., Mangan, A. S. et al. 2018, ApJ, 860, 2
  * Sahai et. al (2022) Sahai, R., Huang, P. S., Scibelli, S., et al. 2022, ApJ, 929, 59
  * Weiss et al. (2009) Weiss, A., & Ferguson, J. W. 2009, A&A, 508, 1343
  * Woods et. al (2003) Woods, P M., Millar, T. J., Herbst, E., et al. 2002, A&A, 402, 189
  * Zijlstra et. al (2001) Zijlstra, A. A., Chapman, J. M., te Lintel Hekkert, P., et al. 2001, MNRAS, 322, 280
  * Ziurys (2006) Ziurys, L. M. 2007, PNAS, 103, 12274


# Electro-magnetic field fluctuation and its correlation with the participant
plane in Au+Au and isobaric collisions at $\sqrt{s_{NN}}=200$ GeV

Sk Noor Alam<EMAIL_ADDRESS>Aligarh Muslim University, Aligarh,
Uttar Pradesh-202002, India  Victor Roy<EMAIL_ADDRESS>National Institute
Of Science Education and Research, Jatni, Odisha-752050, India  Shakeel Ahmad
Aligarh Muslim University, Aligarh, UP-202002,India  Subhasis Chattopadhyay
Variable Energy Cyclotron Centre, HBNI, Kolkata, WB-700064,India

###### Abstract

Intense transient electric (E) and magnetic (B) fields are produced in the
high energy heavy-ion collisions. The electromagnetic fields produced in such
high-energy heavy-ion collisions are proposed to give rise to a multitude of
exciting phenomenon including the Chiral Magnetic Effect. We use a Monte Carlo
(MC) Glauber model to calculate the electric and magnetic fields, more
specifically their scalar product $\bf{E}\cdot\bf{B}$, as a function of space-
time on an event-by-event basis for the Au+Au collisions at
$\sqrt{s_{NN}}=200$ GeV for different centrality classes. We also calculate
the same for the isobars Ruthenium and Zirconium at $\sqrt{s_{NN}}=200$ GeV.
In the QED sector $\bf{E}\cdot\bf{B}$ acts as a source of Chiral Separation
Effect, Chiral Magnetic Wave, etc., which are associated phenomena to the
Chiral Magnetic Effect. We also study the relationships between the
electromagnetic symmetry plane angle defined by $\bf{E}\cdot\bf{B}$
($\psi_{E.B}$) and the participant plane angle $\psi_{P}$ defined from the
participating nucleons for the second-fifth order harmonics.

##  I Introduction

The initial state fluctuations in high-energy heavy-ion collisions play an
essential role in understanding several bulk observables. We can attribute the
two primary sources of these initial state fluctuations to the event-by-event
(e-by-e) geometry fluctuations of the nucleon’s position inside the nuclei due
to the nuclear wave function and the fluctuation in impact strong fluctuating
transient electro-magentic (EM) fields in the overlap zone of the colliding
nucleus. The EM field generated in high-energy heavy-ion collision experiments
such as Relativistic Heavy Ion Collider (RHIC) and the Lager Hadron Collider
(LHC) is known to be the strongest magnetic field in the universe (e.g., B
$\sim 10^{18}-10^{19}$ Gauss for $\sqrt{s_{NN}}=200$ GeV) Ref1 ; Ref2 ; Ref3 ;
Ref4 ; Ref5 ; Ref6 . The magnetic field in heavy-ion collisions, while
averaged over many events, mostly obey a linear scaling with the centre of
mass energy ($\sqrt{s}$) and the impact parameter (b) of collisions, Ref7
i.e., $\big{\langle}eB_{y}\big{\rangle}\sim Zb\sqrt{s}$ for $b\leq 2R_{A}$
where Z is the charge number of the ions, $R_{A}$ is the radius of the
nucleus. We take the y axis perpendicular to the reaction plane as per the
convention, defined by the impact parameter(chosen as the x-axis) and the beam
direction(z-axis). Furthermore, the event-averaged electric fields are also
found to be of the same order of magnitude as the magnetic fields (e.g.,
$eB\approx eE\sim 10m_{\pi}^{2}$ at the topmost RHIC energy Au+Au collisions
$\sqrt{s_{NN}}=200$ GeV where $m_{\pi}$ is the pion mass).

It has been conjectured that in addition to the standard ohmic current driven
by the electric field, there might appear other new types of current in parity
(P) and charge conjugation (C) odd regions in QGP as responses to the
electromagnetic fields. One of this new type of currents is generated along
the background magnetic field, a.k.a. the Chiral Magnetic Effect (CME)Ref1 ;
Ref8 ; Ref9 ; Ref10 . In other words, in high-energy heavy-ion collisions,
special gluonic configurations (sphalerons and instantons) break the P and the
CP in the presence of a strong magnetic field. It results in a global electric
charge separation with respect to the reaction plane Ref11 ; Ref11a . This
charge separation occurs through the transition of the right-handed quarks to
the left-handed quarks and vice versa depending on the sign of topological
charges Ref1 . Because of their close association with axial anomaly and the
topologically nontrivial vacuum structure of QCD, the CME and other associated
phenomena such as chiral separation effect (CSE), the chiral electric
separation effect (CESE) is known as anomalous effects Huang:2015oca .

It is known that only the lowest Landau level contributes to the CME. In the
QED sector, combined electric (E) and magnetic fields (B) are responsible for
the transition of chiral fermions from the left-handed chirality branch to the
right-handed chirality branch at a rate $\sim e^{2}/(2\pi^{2}){\bf E}\cdot{\bf
B}$ Ref10 ; Huang:2015oca .

Similarly, in CSE, the axial current is known to be not conserved due to a
source term proportional to $\sim e^{3}/(2\pi^{2}){\bf E}\cdot{\bf B}$. The
same term also appears in the Chiral magnetic wave equation if ${\bf
E}\cdot{\bf B}$ is non-zero. In other words, ${\bf E}\cdot{\bf B}$ pumps
chirality into the system. In ref. Son:2009tf  it was shown that the current
conservation equation in a relativistic fluid with one conserved charge, with
a $U(1)$ anomaly, contains a source term proportional to $E^{\mu}B_{\mu}$. The
scalar product of the four vectors $E^{\mu}$ and $B^{\mu}$ in the fluid rest
frame is ${\bf E}\cdot{\bf B}$. Hence it is interesting to study ${\bf
E}\cdot{\bf B}$ for different collision geometry and its possible correlation
with the symmetry (participant) plane, with respect to which we search for the
CME signal. It is worthwhile to mention that although the event averaged
magnetic field shows a linear behavior with collision centrality, the electric
field, on the other hand, shows an opposite trend, i.e., maximum for the
central collisions and gradually decreases for higher centralities. In this
paper, we focus on the spatial distribution of ${\bf E}\cdot{\bf B}$ for
various centrality Au+Au, Ru+Ru, and Zr+Zr collisions at $\sqrt{s_{NN}}=200$
GeV to investigate their angular correlation with the geometry of the
fireball. To this end, we introduce the participant plane $\psi_{EB}$ defined
with the weight of ${\bf E}\cdot{\bf B}$, and we show the correlation of it
with the participant plane $\psi_{pp}$.

The rest of this paper is organized as follows: In Sec. II, we describe the
detail of calculating electromagnetic fields from the Glauber model on an
event-by-event basis. We also discuss their impact parameter dependence and
event averaged value. In Sec. III. we discuss the main results, which consists
of the impact parameter, space-time, and system size dependence of ${\bf
E}\cdot{\bf B}$ and its correlation with the participant plane. Finally, we
summarise this study in Sec. IV.

##  II Calculation of electric and magnetic field

Customarily the electromagnetic field generated by a relativistic charged
particle is calculated from the well known Liénard–Wiechert potentials,
however, we will calculate it from the second-rank antisymmetric
electromagnetic field tensor
$F^{\alpha\beta}=\partial^{\alpha}A^{\beta}-\partial^{\beta}A^{\alpha}$ using
the Lorentz transformation. Here $A^{\mu}$ is the four-potential due to an
electric charge, in the following calculations we assume the charged protons
inside the colliding nuclei move in a straight line trajectory and there are
neglegible change in momentum after the collision. The calculation goes as
follow Ref12 : first we calculate the component of electromagnetic fields and
corresponding $F^{\prime\gamma\delta}$ in the rest frame $S^{\prime}$ of the
charge particle. The fields in the laboratory frame is calculated from
$F^{\alpha\beta}$ which is obtained from $F^{\prime\gamma\delta}$ through the
Lorentz transformation:

$F^{\alpha\beta}=\frac{\partial x^{\alpha}}{\partial
x^{\prime\gamma}}\frac{\partial x^{\beta}}{\partial
x^{\prime\delta}}F^{\prime\gamma\delta},$ (1)

or in matrix notation $F=\Lambda F^{\prime}\tilde{\Lambda}$, where $\Lambda$
is the matrix representation of the Lorentz transformation and
$\tilde{x^{\mu}}$ corresponds transpose of $x^{\mu}$. We choose a boost
$\beta=v_{z}$ along the $z$ axis. In this case it can be easily shown that the
electric fields transform as

$\displaystyle E_{x}$ $\displaystyle=$ $\displaystyle\gamma
E_{x}^{\prime}+\gamma\beta B_{y}^{\prime},$ (2) $\displaystyle E_{y}$
$\displaystyle=$ $\displaystyle\gamma E_{y}^{\prime}-\gamma\beta
B_{x}^{\prime},$ (3) $\displaystyle E_{z}$ $\displaystyle=$ $\displaystyle
E_{z}^{\prime},$ (4)

and the magnetic fields transform as,

$\displaystyle B_{x}$ $\displaystyle=$ $\displaystyle\gamma
B_{x}^{\prime}-\gamma\beta E_{y}^{\prime},$ (5) $\displaystyle B_{y}$
$\displaystyle=$ $\displaystyle\gamma B_{y}^{\prime}+\gamma\beta
E_{x}^{\prime},$ (6) $\displaystyle B_{z}$ $\displaystyle=$ $\displaystyle
B_{z}^{\prime}.$ (7)

Since the charge is at rest in the $S^{\prime}$ frame
$B_{x}^{\prime}=B_{y}^{\prime}=B_{z}^{\prime}=0$, furthermore, it is easy to
verify ${\bf B}={\bf\beta}\times{\bf E}$. Next, we calculate ${\bf
E}^{\prime}$ at a point P $(x,y,z)$ at time $t$ for a charge at
($x^{\prime}_{c},y^{\prime}_{c},z^{\prime}_{c}$) at time $t^{\prime}$ by
noting that $z^{\prime}_{c}\approx\beta t^{\prime}$ (we assume that the origin
of the lab frame $S$ and the moving frame $S^{\prime}$ coincide at
$t=t^{\prime}=0$). The subscript $c$ corresponds to the charge. For
convenience, we denote the transverse distance
$\zeta=\sqrt{(x^{\prime}_{c}-x)^{2}+(y^{\prime}_{c}-y)^{2}}$, the distance
from the charge to $P$ is $r^{\prime}=\sqrt{\zeta^{2}+\beta^{2}t^{\prime 2}}$
(here we have taken the center of the nucleus to be at the origin of
$S^{\prime}$). Also, the positions of the charged particles in the transverse
plane are assumed to be frozen due to large Lorentz
$\gamma=(1-\beta^{2})^{-1/2}$. A straightforward calculation gives the
following values of the electric fields in $S$ frame

$\displaystyle E_{x}$ $\displaystyle=$ $\displaystyle\frac{\gamma
qx}{\left(\zeta^{2}+\beta^{2}\gamma^{2}\left(t-\beta
z\right)^{2}\right)^{3/2}},$ (8) $\displaystyle E_{y}$ $\displaystyle=$
$\displaystyle\frac{\gamma
qy}{\left(\zeta^{2}+\beta^{2}\gamma^{2}\left(t-\beta
z\right)^{2}\right)^{3/2}},$ (9) $\displaystyle E_{z}$ $\displaystyle=$
$\displaystyle\frac{q\beta\gamma(t-\beta
z)}{\left(\zeta^{2}+\beta^{2}\gamma^{2}\left(t-\beta
z\right)^{2}\right)^{3/2}},$ (10)

and the magnetic fields are given by

$\displaystyle B_{x}$ $\displaystyle=$ $\displaystyle\frac{-\gamma\beta
qy}{\left(\zeta^{2}+\beta^{2}\gamma^{2}\left(t-\beta
z\right)^{2}\right)^{3/2}},$ (11) $\displaystyle B_{y}$ $\displaystyle=$
$\displaystyle\frac{\gamma\beta
qx}{\left(\zeta^{2}+\beta^{2}\gamma^{2}\left(t-\beta
z\right)^{2}\right)^{3/2}},$ (12) $\displaystyle B_{z}$ $\displaystyle=$
$\displaystyle 0.$ (13)

The total electromagnetic field at any point is evaluated using the principle
of superposition i.e., calculating fields using Eq.(8) - (13) for all the
protons inside the nucleus. We use a cutoff value of $\zeta$ = 0.3 fm while
calculating the electric and magnetic field usig Eq.(8) - (13) We note that
this cutoff value was chosen as an average effective distance between the
quarks inside the nucleons, and it was also reported Ref6  that there is a
weak dependence of the field values on $\zeta$ in the range 0.3 to 0.6 fm.
Since the colliding nucleus at $\sqrt{s_{NN}}=200$ GeV has Lorentz $\gamma\sim
100$, we can safely assume the nucleus as a flat disk that has a vanishing
thickness along the $z$ axis. Also, due to the time-dilation, the nucleons
will appear as frozen inside the nucleus, and all nucleons effectively move
along $z$ with constant $v_{z}$ i.e ${\bf v_{n}}\equiv$ (0,0,$v_{z}$). As per
the convention, we take the velocity of the target nucleus as $+v_{z}$, and
the velocity of the projectile nucleus is $-v_{z}$. $v_{z}$ is calculated from
the ratio of the relativistic momentum and the energy of a proton

$v_{z}=\sqrt{1-\Big{(}\frac{2m_{p}}{\sqrt{s_{NN}}}\Big{)}^{2}}.$ (14)

To obtain the nucleon positions we use the MC-Glauber model Ref13 . We also
calculate the initial spatial eccetricity ($\epsilon$, defined later) and the
number of participating nucleons $(N_{\rm{part}})$ for a given impact
parameter from the MC-Glauber model. In the MC-Glauber model, the positions of
the nucleons inside the nucleus are determined by the nuclear density function
measured in low-energy electron scattering experimentsRef14 . The functional
form of this distribution is:

$\rho(r,\theta)=\frac{\rho_{0}}{1+exp\big{[}\frac{r-R\big{(}1+\beta_{2}Y_{2}^{0}(\theta)+\beta_{4}Y_{4}^{0}(\theta)\big{)}}{a}\big{]}},$
(15)

where $\rho_{0}$ corresponds to the nuclear density at the center, $R$ is the
radius of the nucleus, $a$ is the skin depth (it controls how quickly the
nuclear density falls off near the edge of the nucleus). The spherical
harmonics $Y_{l}^{m}(\theta)$ and parameters $\beta_{2}$ and $\beta_{4}$ are
used to measure the deformation from spherical shape. For our study, we take
$R=6.38$ fm, $a=0.535$ fm, and $\beta_{2}=\beta_{4}=0$ for the $Au_{79}^{197}$
nucleus. We use parameter $\beta_{2}^{Ru}$ =0.158 , $\beta_{2}^{Zr}$=0.08,
$R^{Ru}=5.085$ fm, $R^{Zr}=5.02$fm and a = 0.46 fm for both Ru and Zr Ref14a ;
Ref14b ; Ref14c . $\beta_{4}$ is taken 0 for both nuclei.

We sample the nucleon positions assuming that they are randomly distributed
with the given distribution $4\pi r^{2}\rho(r)$ (integrating on $\theta$ and
$\phi$ ) for Au nucleus and $r^{2}\sin(\theta)\rho(r,\theta)$ for Ru and Zr
nuclei respectively.
The impact parameters $b$ of the collisions are randomly selected from the
distribution $\frac{dN}{db}\sim b$ upto a maximum value of $\simeq 20$ fm
$>2R$. The center of the target and projectile nuclei are shifted to
$(-\frac{b}{2},0,0)$ and $(\frac{b}{2},0,0)$ respectively. We use the
inelastic nucleon-nucleon cross section $\sigma_{NN}=42$ mb for the top RHIC
energy $\sqrt{s_{NN}}=200$ GeV for calculating the probability of an
interaction between the target and the projectile nucleonsRef15 ; Ref16 . To
show the centrality dependence, we calculate the centrality of the collisions
using $N_{\rm{part}}$ and the number of binary collisions $(N_{\rm{coll}})$
obtained from the MC Glauber model . The multiplicity for a given
$N_{\rm{part}}$ and $(N_{\rm{coll}})$ is calculated using the two component
model as

$\frac{dN_{ch}}{d\eta}=n_{\rm{pp}}\left[(1-x)\frac{N_{\rm{part}}}{2}+xN_{\rm{coll}}\right],$
(16)

where $x$ is the fraction of hard scattering, $n_{\rm{pp}}$ is the average
multiplicity per unit pseudo-rapidity in pp collisions. The above two-
component model of the particle production is based on the assumption that the
average particles produced through the soft interactions are proportional to
the $N_{\rm{part}}$, and the probability of hard interactions is proportional
to $N_{\rm{coll}}$. We calculate the centrality of a given collision in the
following way: the number of independent particle emitting sources for a given
impact parameter are $(1-x)\frac{N_{\rm{part}}}{2}+xN_{\rm{coll}}$. Each of
these sources produces particles following a negative binomial distribution
(NBD) with a mean $\mu$ and the width $\sim$ 1/k,

$\textit{P}_{\mu,k}(n)=\frac{\Gamma(n+k)}{\Gamma(n+1)\Gamma(k)}\Big{(}\frac{\mu}{\mu+k}\Big{)}^{n}\Big{(}\frac{k}{\mu+k}\Big{)}^{k}.$
(17)

$\textit{P}_{\mu,k}(n)$ is the probability of measuring n hits per independent
sources. The mean of this NBD distribution is calculated from the pseudo-
rapidity density of the charged multiplicity for the non-single diffractive
$\bar{p}p$ collisions at a given $\sqrt{s_{NN}}$ energy Ref17 :

$\mu=\mathcal{A}\ln^{2}{(s_{NN})}-\mathcal{B}\ln{(s_{NN})}+\mathcal{C},$ (18)

where $\mathcal{A}=0.023\pm 0.008$, $\mathcal{B}=0.25\pm 0.19$, and
$\mathcal{C}=2.5\pm 1.0$. The charged particle multiplicity data for Au+Au 200
GeV collisions measured by the STAR collaboration are explained for $x=0.13$
and $k=1.7$, and $\mu=2.08$ for the pseudo-rapidity range
i.e$\mid\eta\mid<0.5$ Ref18 . For example, we show the charged particle
multiplicity distribution for Au+Au collisions at $\sqrt{s_{NN}}=200$ GeV for
$|\eta|<0.5$ in Fig. 1.

Figure 1: (Color online) Probability distribution of the charged particles
multiplicity in Au+Au $\sqrt{s_{NN}}=200$ GeV collisions.

To calculate the centrality of collisions, we subdivide the total area in Fig.
1 into different bins with the condition that the fractional area corresponds
to a particular centrality. For example, the bin boundaries $n40$ and $n50$
for the 40$\%$-50$\%$ centrality are defined in such a way that the following
relation holds:
$\frac{\int_{\infty}^{n40}P(N_{ch})dN_{ch}}{\int_{\infty}^{0}P(N_{ch})dN_{ch}}=0.4$,
and
$\frac{\int_{\infty}^{n50}P(N_{ch})dN_{ch}}{\int_{\infty}^{0}P(N_{ch})dN_{ch}}=0.5$.

We use three centrality bins 0$\%$-5$\%$, 40$\%$-50$\%$ and 70$\%$-80$\%$ for
our calculation of the electric and magnetic field; corresponding impact
parameter ranges are $0-3.2$, $9.3-10.6$, and $12.2-13.5$ fm, which are very
similar to the values given in Ref18 .

As mentioned earlier, the topology of the electromagnetic fields in heavy-ion
collisions has non-trivial dependence on the centrality (possibly also on the
$\sqrt{s_{\rm{NN}}}$). Consequently, the source ($\bf{E}\cdot\bf{B}$) of the
chiral current in the transverse plane also has a non-trivial centrality
dependence. The axial current generated by the magnetic field is supposed to
predominantly flow along the direction perpendicular the participant plane.
Hence, we investigate here how the sources $\bf{E}\cdot\bf{B}$ of this current
is correlated to the participant plane. From the perspective of heavy-ion
collisions it is customary to use the Milne co-ordinates i.e., we use the
longitudinal proper time $\tau=\sqrt{t^{2}-z^{2}}$ ,$x$,$y$, and the space-
time rapidity $\eta=\frac{1}{2}\log(\frac{t+z}{t-z})$ instead of the Cartesian
co-ordinate. In Fig.2 we show the distribution of ${\bf E}\cdot{\bf B}$ for
40$\%$-50$\%$ centrality with $\eta$ (left plot) and $\tau$ (right plot). In
left plot, we calculate $\bf{E}\cdot\bf{B}$ in the forward light-cone spanned
by the region for $\tau$ = 0.4 and $-1.0\leq\eta\leq 1.0$. In right plot, we
also calculate $\bf{E}\cdot\bf{B}$ in the forward light-cone. But for this
plot, phase space is spanned by the region for $\eta$ = 0.4 and
$0.1\leq\tau\leq 0.34$. While calculating the dot product, we transform the
field components $B_{x(y)}$ from the Cartesian to the Milne coordinate
$\tilde{B}_{x(y)}$ by the following expression
$\tilde{B}_{x}=B_{x}/\cosh\eta,\tilde{B}_{y}=B_{y}/\cosh\eta$ and
$\tilde{B}_{z}=B_{z}/\tau$. The components of the electric field transform
similarly.

Figure 2: (Color online) Left panel: event averaged distribution of
$\bf{E}\cdot\bf{B}$ for 40$\%$-50$\%$ centrality Au+Au collisions at
$\sqrt{s_{NN}}=200$ GeV as a function of $\eta$ at constant proper time
$\tau$=0.4. Rght panel: same as the left panel but as a function of $\tau$ at
constant $\eta$=0.4.

To investigate the distribution of $\bf{E}\cdot\bf{B}$ (from now on denoted as
$\mathcal{E}$) to the participant plane, we introduce the $\bf{E}\cdot\bf{B}$
symmetry plane $\psi_{\mathcal{E}}$ defined as Ref19 ; Ref20

$\epsilon_{n}e^{in\psi_{\mathcal{E}}}=-\frac{\int
dxdyr^{n}e^{in\varphi}\mathcal{E}(x,y)}{\int dxdyr^{n}\mathcal{E}(x,y)},$ (19)

where $r^{2}=(x-<x>)^{2}+(y-<y>)^{2}$ and $tan(\varphi)=\frac{y-<y>}{x-<x>}$.
Here $(<x>,<y>)$ corresponds to the mean position of the participating
nucleons. Using these definitions and Eq.(19) we obtain $\psi_{\mathcal{E}}$
as

$\psi_{\mathcal{E}}=\frac{1}{n}arctan\frac{\int
dxdyr^{n}\sin(n\varphi)\mathcal{E}(x,y)}{\int
dxdyr^{n}\cos(n\varphi)\mathcal{E}(x,y)}+\frac{\pi}{n}.$ (20)

Before going into the main results of this paper, let us very briefly go
through the impact parameter dependence of the electric and magnetic field
produced in Au+Au collisions at $\sqrt{s_{\rm{NN}}}=200$ GeV. These results
are not new and have already been reported in several works Ref6 ; Ref7 ;
Huang:2015oca ; Ref20ab , but we include them for the sake of completeness.

###  II.1 Impact parameter dependence of the field

We calculate fields on a regular space-time grid and consider one million
events while calculating event-averaged quantities. The magnitude of the
electric and magnetic fields may become very large near the charges due to the
obvious $r$ dependence of Coulomb law, relativistic enhancement of field, and
due to the clustering of charges due to the quantum fluctuations of nuclear
wavefunction Ref20a . But these fluctuations smoothes out when taking event-
average of the field due to its vector nature. These fluctuations might play
an essential role in CME; however, here, we show the event-averaged values of
electromagnetic fields as a function of the impact parameter of the
collisions. The impact parameter dependence of electric and magnetic field at
the origin, i.e., ($x$=0, $y$=0 in our grid space) at $t$=0 is shown in Fig.3.
Because of the symmetry in the system considered here, $\langle E_{x}\rangle$
and $\langle E_{y}\rangle$ are zero at the origin. It is also interesting to
note that $\langle\mid E_{x}\mid\rangle\approx\langle\mid
E_{y}\mid\rangle\approx\langle\mid B_{x}\mid\rangle$ (figure Fig.3). From
these two figures, we also notice that the electric field decreases as the
impact parameter increases while the magnetic field follows the opposite
trend. Our results seems to be consistent with Ref6 ; Ref7 .

Figure 3: (Color online) Top panel: event averaged absolute value of $B_{x}$
and $B_{y}$ (in unit of $m_{\pi}^{2}$) at $\textbf{r}=0$ and t=0 vs impact
parameter for Au+Au collisions at $\sqrt{s_{NN}}=200$ GeV. Bottom panel: same
as top panel but for the electric fields.

Figure 4: (Color online) (top panel) histogram of $\bf{E}\cdot\bf{B}$ at
$\textbf{r}=0$ and t=0 for 0-5$\%$, 40-50$\%$ and 70-80$\%$ centrality of
Au+Au collisions at $\sqrt{s_{NN}}=200$ GeV. (bottom panel) Event averaged
absolute value of $\bf{E}\cdot\bf{B}$ at $x=y=z=0$ and t=0 fm as a function of
the impact parameter for Au+Au collisions at $\sqrt{s_{NN}}=200$ GeV.

We end this section with this brief discussion; let us turn to the quantity of
our interest in the next section.

##  III Results and discussion

###  III.1  impact parameter dependence of $\bf{E}\cdot\bf{B}$

In Fig.4, we show one dimensional histogram of $\mathcal{E}(0,0)$ distribution
for $z=t=0$ and for three different centralities 0$\%$-5$\%$ (black circles),
40$\%$-50$\%$ (red triangles), and 70$\%$-80$\%$ (open blue circles) Au+Au
collisions at $\sqrt{s_{NN}}=200$ GeV. First, we note that there is a non-
monotonic dependence of $\mathcal{E}$ on the collision centrality. For
peripheral collisions maximum events have $\mathcal{E}\sim 0$, and the
distribution also becomes narrower compared to the central/mid-central
collisions. This behaviour can be understood as a consequence of near
vanishing electric fields at the centre of the collision zone in peripheral
collisions at $t=0$ and at midrapidity. It is clear from top panel of Fig.4
that although the mean of $\mathcal{E}$ (at the origin) is zero the variance
is non-zero. Hence it is more relevant to study the absolute value of the
event averaged $\mathcal{E}$. In the bottom panel of Fig.4, and in both panels
of Fig.5 we show the event averaged absolute values of $\mathcal{E}(0,0)$ for
$t=z=0$ fm, and $t$=0.5 fm, $z=\pm 0.1$,$z=\pm 0.4$ respectively. The
important difference between these two results is that for the first case
($t=z=0$ fm) electromagnetic fields from the two colliding nuclei almost
equally contributed in $\mathcal{E}$, whereas, for the other case, the fields
due to each nucleus will be significant for $|z|\sim t$ and is dominated by
the nearest nucleus. From the bottom panel of Fig.4 we observe that for
$t=z=0$ fm $\mathcal{E}$ is almost flat up to impact parameter $b\sim 10$ fm,
and after that, it falls rapidly. This observed impact parameter dependence of
$\mathcal{E}$ can be attributed to the fact that the magnetic field increases
with impact parameter, whereas electric fields diminish. The magnitude of
$\mathcal{E}$ (expressed in the unit of pion mass) is comparable to the
corresponding magnetic fields in central collisions. It may be an over-
optimistic claim at this stage; however, this large values of $\mathcal{E}$ at
mid-rapidity at the initial time possibly indicates that the CME signal may
have a significant contribution from $\mathcal{E}$ along with $B$. To get the
complete picture, we must wait for the late time behavior of $\mathcal{E}$
discussed next. For the other case, we consider fields at later time $t=0.5$
fm, and at forward and backward regions, i.e., $z\neq 0$. The top panel of
Fig.5 shows the dependence of $\mathcal{E}$ as a function of $b$ for $z$=0
(blue squares), $z=\pm 0.1$ (open and filled circles). It is not surprising
that $\mathcal{E}$ for this case is approximately six orders of magnitude
smaller than $t=z=0$ case, this is because the electromagnetic fields decay
rapidly after the collision, and in this case, only one nucleus significantly
contributes to the fields.

From the top panel of Fig.5 we also observe that $\mathcal{E}$ increases
almost linearly with the impact parameter; this is almost opposite to what we
observe for $t=z=0$. The impact parameter dependence of $\mathcal{E}$ at
finite $z$ is, however, non-trivial, as can be seen from the bottom panel of
Fig.5, where the same result is shown but for $z=\pm 0.4$. Here one notices
that $\mathcal{E}$ rises almost linearly for small $b$ ($<10$ fm), but after
that, it starts saturating. Since $z=\pm 0.4$ at time $0.5$ fm is nearer to
the receding nuclei, we get a larger value of $\mathcal{E}$ compared to $z$=0
, and $z=\pm 0.1$ (top panel). To conclude this section, we note that at
peripheral collisions, charge separation is experimentally observed to be
larger than central collisions Ref21 ; Ref22 , and it might be linked to the
observed $b$ dependence $\mathcal{E}$, along with the magnetic fields, which
are also most prominent in mid-central/peripheral collisions.

Figure 5: (Color online) Event averaged absolute values of $\bf{E}\cdot\bf{B}$
at $x=y=0$ for $|z|=0.1$,$z=0$ (top panel) and $|z|=0.4$ fm (bottom panel)
with the impact parameter for Au+Au collisions at $\sqrt{s_{NN}}=200$ GeV. All
results are for t=0.5 fm.

###  III.2 $\bf{E}\cdot\bf{B}$ correlation with participant plane

In Ref23 , the correlation of the fluctuating magnetic field with the
participant plane showed that a sizable suppression of the angular
correlations exists between the magnetic field and the second and fourth
harmonic participant planes were found in very central and very peripheral
collisions. The importance of space averaged $e^{2}{\bf E}\cdot{\bf B}$ was
studied recently in Ref24  as a function of time for 200 GeV Au+Au collisions
at $t=0.08$ fm and for b= 9 fm. We notice that our finding of the spatial
distribution of $\mathcal{E}$ in Au+Au collisions is similar to Ref24 . In
this section, we further investigate the spatial distribution $\mathcal{E}$
and its correlation with the participant plane $\psi_{p}$ by calculating the
symmetry plane defined in Eq.(20). $\psi_{p}$ is calculated from Eq.(20) using
the positions of wounded nucleons, and by setting $\mathcal{E}=1$ which gives
the usual definition used in literature.

Since the isobaric collisions of Ru+Ru and Zr+Zr are important for searching
the CME signal, we include results for these two nuclei along with the Au+Au
collisions discussed in the previous section.

Let us first discuss the result for Au+Au collisions. We show the distribution
of $\psi_{\mathcal{E}}$ and $\psi_{P}$ at $z$=0 for time $t$=0 fm in Fig.6 for
perfectly head on ($b$=0 fm) Au+Au collisions at $\sqrt{s_{NN}}=200$ GeV.
Since a head-on collision creates an almost symmetric overlap zone, the
existence of a particular symmetry plane due to the participants ($\psi_{p}$)
may be ruled out in this case. That is what we observe here from Fig.6, where
black circles show $\psi_{P}^{2}$; the distribution is almost flat. The
distribution of $\psi_{\mathcal{E}}^{2}$ is also similar to $\psi_{P}^{2}$;
the third and fifth-order symmetry plane show a similar trend. Interestingly,
the rotational symmetry in head-on collisions seems to be broken for
$\psi_{\mathcal{E}}^{4}$. The reason behind this behavior, however, is unclear
to us. We know that the probability of occurrence of a perfectly head-on
collision is approximately zero. Hence, next in Fig.7 we show results for
0$\%$-5$\%$ centrality Au+Au collisions at $t=z=0$ fm.

Figure 6: (Color online) distribution of $\psi_{\mathcal{E}}^{n}$ and
$\psi_{P}^{n}$ ($n$=2-5) for impact parameter b = 0 fm Au+Au collisions at
$\sqrt{s_{NN}}=200$ GeV.

As expected, in contrast to the $b=0$ case, in Fig.7 we see that due to the
overlap geometry and the fluctuating nucleon positions, the distribution of
the second-order participant plane (black circles) reflects the broken
rotational symmetry of the collision zone. $\psi_{\mathcal{E}}^{2}$ (red
triangles) due to the electromagnetic fields seems to be highly correlated
with $\psi_{P}^{2}$. Other higher order $\psi_{P}$’s in central collisions
known to be fluctuating widely and the same is observed here as well. Notably,
$\psi_{\mathcal{E}}^{4}$ shows a different trend than $\psi_{P}^{4}$, this is
because in central collisions inside the fireball the resultant electric
fields due to the target and the projectile are much smaller than the magnetic
fields; the magnetic fields have a dipole nature, and the corresponding
symmetry plane almost coincides with $\psi_{P}^{2}$. This can be more clearly
seen from Fig. 8 for 40$\%$-50$\%$ centrality collisions, where the electric
fields become vanishingly small, and the magnetic fields are larger, in that
case $\psi_{\mathcal{E}}^{4}$ (bottom panel) becomes more oriented along
$\psi_{P}^{2}$ (top panel). If we further increase the collision centrality
and consider 70$\%$-80$\%$ collisions (see Fig. 9) we observe a noticeable
change in $\psi_{\mathcal{E}}^{2}$ as compared to the mid-central collisions.
It is clear that the distribution of $\mathcal{E}$ has a $\pi/2$ rotation
compared to the central collisions. To better understand this rotation of
symmetry plane for peripheral collisions we we show the contours of
$\mathcal{E}$ in the transverse plane for the 40$\%$-50$\%$ (top panel), and
70$\%$-80$\%$ (bottom panel) centralities at $z=0$ and $t=0$ fm in Fig.10. We
can see that a quadrupole like structure appears for 70$\%$-80$\%$ collisions.
From the above discussion, we can conclude that $\mathcal{E}$ distribution in
the transverse plane for Au+Au collisions at 200 GeV per nucleon is highly
correlated with the geometry of the fireball.

Figure 7: (Color online) distribution of $\psi_{\mathcal{E}}^{n}$ and
$\psi_{P}^{n}$ ($n$=2-5) for 0$\%$-5$\%$ centrality Au+Au collisions at
$\sqrt{s_{NN}}=200$ GeV. Figure 8: (Color online) distribution of
$\psi_{\mathcal{E}}^{n}$ and $\psi_{P}^{n}$ ($n$=2-5) for 40$\%$-50$\%$
centrality Au+Au collisions at $\sqrt{s_{NN}}=200$ GeV. Figure 9: (Color
online) distribution of $\psi_{\mathcal{E}}^{n}$ and $\psi_{P}^{n}$ ($n$=2-5)
for 70$\%$-80$\%$ centrality Au+Au collisions at $\sqrt{s_{NN}}=200$ GeV.

Ruthenium and Zirconium nuclei carry the same number of nucleons (96), but Ru
has 44 protons, and Zr has 40 protons. In other words, they have similar
shapes and sizes but different electrical charges, which implies different
electromagnetic fields generated in Ru+Ru and Zr+Zr collisions. This feature
makes them interesting systems for detecting CME by eliminating possible
backgrounds. For the following results we use a fixed impact parameter
collisions to keep things simple.

We checked that for $b=0$ Ru+Ru, and Zr+Zr collisions (not shown here),
results are very similar to what was observed for Au+Au collisions. In the top
panel of Fig.11, we show $\psi_{\mathcal{E}}^{i}$ and $\psi_{P}^{i}$ ($i=2-5$
) distribution for Ru+Ru collisions at $\sqrt{s_{NN}}=200$ GeV for $b$=5 fm.
The bottom panel of the same figure corresponds to results for $b$=10 fm
collisions. A similar result was obtained (not shown here) for the Zr+Zr
collisions. It is interesting to note that $\psi_{\mathcal{E}}$’s and
$\psi_{P}$’s in these small collision systems show a similar correlation as
was observed for the Au+Au collisions. Like peripheral Au+Au collisions, we
also observe the rotation of $\psi_{\mathcal{E}}$ by $\pi/2$ for the
peripheral Ru+Ru and Zr+Zr collisions. Because the electromagnetic field
produced in Ru+Ru and Zr+Zr collisions differs, we compared
$\psi_{\mathcal{E}}^{2}$ distribution for $b=0$ fm. This fact is shown in
Fig.12, the field is higher for Zr+Zr compared to Ru+Ru; possibly as a
consequence, we observe a slightly narrow peak for the Zr+Zr (black dots).

Figure 10: (Color online) Top panel: spatial distribution of $\mathcal{E}$ at
$z=t=0$ for 40$\%$ -50$\%$ centrality Au+Au collisions at $\sqrt{s_{NN}}=200$
GeV. Bottom panel: same as the top panel but for 70$\%$ -80$\%$ centrality.

Figure 11: (Color online) Top panel: distribution of $\psi_{\mathcal{E}}$ and
$\psi_{P}$ for Ru+Ru collisions at $\sqrt{s_{NN}}=200$ GeV for $b$=5 fm.
Bottom panel: same as above but for impact parameter b=10fm. Figure 12: (Color
online) distribution of the second order plane $\psi_{\mathcal{E}}^{2}$ for
Ru+Ru and Zr+Zr collisions at $\sqrt{s_{NN}}=200$ GeV for $b$=10 fm.

##  IV Conclusion and summary

In summary, we have studied the event-by-event fluctuations of the electric
and the magnetic fields and their possible correlation with the geometry of
the high-energy heavy-ion collisions. More particularly we studied the
distribution of $\bf{E}\cdot\bf{B}$($=\mathcal{E}$) in the transverse plane
for Au+Au, Ru+Ru, and Zr+Zr collisions at $\sqrt{s_{NN}}=200$ GeV. Further, we
show the $\tau$ and $\eta$ dependence of $\mathcal{E}$ in Au+Au at 200 GeV per
nucleon collisions. As expected, $\mathcal{E}$ is found to be symmetric in
$\eta$ (around $\eta=0$), and $\mathcal{E}$ quickly decays as a function of
$\tau$ at a given $\eta$. Because $\mathcal{E}$ may contribute to CME as a
source of the anomalous current, we investigate the centrality (impact
parameter) dependence of the symmetry plane angle $\psi_{\mathcal{E}}$ and its
possible correlation with the participant plane. We show that
$\psi_{\mathcal{E}}$ is strongly correlated with $\psi_{P}$ for second-fifth
order harmonics for Au+Au, Ru+Ru, and Zr+Zr collisions. The second-order
planes $\psi_{\mathcal{E}}$ and $\psi_{P}$ are not only correlated but also
mostly coincides with each other except for the peripheral collisions, where a
rotation by $\pi/2$ is observed for $\psi_{\mathcal{E}}$ irrespective of the
collision system size. This phenomenon seems to be happening due to the almost
cancellation of electric fields and dominating magnetic field pointing
perpendicular to the participant plane in peripheral collisions. To conclude,
in this exploratory study, we show that, like the magnetic fields,
$\mathcal{E}$ is also correlated to the geometry of the collision even when we
consider e-by-e fluctuation of nucleon positions.

## Acknowledgements

We are thankful to the grid computing facility at Variable Energy Cyclotron
Centre, Kolkata, for providing us CPU time. VR acknowledges financial support
from the DST Inspire faculty research grant (IFA-16-PH-167), India.

## References

  * (1) D.E. Kharzeev, L.D. McLerran, H.J. Warringa, Nucl. Phys. A 803 (2008) 227.
  * (2) V. Skokov, A.Y. Illarionov, V. Toneev, Int. J. Mod. Phys. A 24 (2009) 5925.
  * (3) M. Asakawa, A. Majumder, B. Muller, Phys. Rev. C 81 (2010) 064912.
  * (4) V. Voronyuk, V.D. Toneev, W. Cassing, E.L. Bratkovskaya, V.P. Konchakovski, S.A.Voloshin, Phys. Rev. C 83 (2011) 054911.
  * (5) L. Ou, B.A. Li, Phys. Rev. C 84 (2011) 064605.
  * (6) A. Bzdak, V. Skokov, Phys. Lett. B 710 (2012) 171.
  * (7) W.T. Deng, X.G. Huang, Phys. Rev. C 85 (2012) 044907
  * (8) A. A. Belavin, et al., Phys. Lett. 59B, 85 (1975).
  * (9) G.Hooft, Phys. Rev. Lett. 37 (1976) 8; Phys. Rev. D 14 (1976)3432.
  * (10) Kenji Fukushima,Dmitri E. Kharzeev,and Harmen J. Warringa, Phys. Rev D 78 (2008) 074033.
  * (11) D. T. Son and P. Surowka, Phys. Rev. Lett. 103, 191601 (2009) doi:10.1103/PhysRevLett.103.191601 [arXiv:0906.5044 [hep-th]].
  * (12) D. Kharzeev, Phys. Lett. B 633 (2006) 260.
  * (13) Sk Noor Alam, Subhasis Chattopadhyay, Nuclear Physics A 977 (2018) 208-216
  * (14) J.D Jackson Classical Electrodynamics (3rd Edition)
  * (15) Miller ML, Reygers K, Sanders SJ, Steinberg P. 2007. arXiv:nucl- ex/0701025.
  * (16) H. De Vries, C. W. De Jager, and C. De Vries. At Data Nucl Data Tables 36 (1987) 495
  * (17) S. Raman, C. W. G. Nestor, Jr and P. Tikkanen, Atom. Data Nucl. Data Tabl. 78 (2001) 1.
  * (18) B. Pritychenko, M. Birch, B. Singh and M. Horoi, Atom. Data Nucl. Data Tabl. 107 (2016) 1.
  * (19) P. Moller, J. R. Nix, W. D. Myers and W. J. Swiatecki, Atom. Data Nucl. Data Tabl. 59 (1995) 185.
  * (20) see https://twiki.cern.ch/twiki/bin/view/Main/LHCGlauberBaseline
  * (21) Yao YM, et al. J. Phys. G 33 (2006) 1.
  * (22) F. Abeet al.(CDF Collaboration),Phys. Rev. D41 (1990) 2330.
  * (23) B. I. Abelev et al. (STAR Collaboration),Phy. Rev. C79 (2009) 034909
  * (24) B. Alver and G. Roland, Phy. Rev. C81 (2010) 054905
  * (25) B.H. Alver, C.Gombeaud, M.Luzum, and J.Y. Ollitrault,Phys. Rev. C82 (2010) 034913
  * (26) X. G. Huang, Rept. Prog. Phys. 79, no.7, 076302 (2016) doi:10.1088/0034-4885/79/7/076302 [arXiv:1509.04073 [nucl-th]].
  * (27) Xin-Li Zhao,Guo-Liang Ma and Yu-Gang Ma, Phys. Rev. C99 (2019) 034903
  * (28) V.Roy and S.Pu Phys. ReV. C92 (2015) 064902
  * (29) B. I. Abelev et al. (STAR Collaboration), Phys. Rev. Lett.103 (2009) 251601
  * (30) B. Abelev et al. (ALICE Collaboration),Phys. Rev. Lett. 110(2013) 012301
  * (31) John Bloczynskia, Xu-Guang Huanga, Xilin Zhanga and Jinfeng Liaoa, Physics Letters B 718 (2013) 1529
  * (32) Irfan Siddique, Xin-Li Sheng and Qun Wang, https://arxiv.org/abs/2106.00478


spacing=nonfrench

# Alethe: Towards a Generic SMT Proof Format
(extended abstract)

Hans-Jörg Schurr  University of Lorraine, CNRS, Inria, and LORIA, Nancy,
France<EMAIL_ADDRESS>Johannes Kepler University Linz,
AustriaUniversidade Federal de Minas Gerais, Belo Horizonte, BrazilUniversity
of Liège, Belgium Mathias Fleury  Johannes Kepler University Linz, Austria
<EMAIL_ADDRESS>Universidade Federal de Minas Gerais, Belo Horizonte,
BrazilUniversity of Liège, Belgium Haniel Barbosa  Universidade Federal de
Minas Gerais, Belo Horizonte, Brazil<EMAIL_ADDRESS>University of Liège,
Belgium Pascal Fontaine  University of Liège, Belgium
<EMAIL_ADDRESS>
###### Abstract

The first iteration of the proof format used by the SMT solver veriT was
presented ten years ago at the first PxTP workshop. Since then the format has
matured. veriT proofs are used within multiple applications, and other solvers
generate proofs in the same format. We would now like to gather feedback from
the community to guide future developments. Towards this, we review the
history of the format, present our pragmatic approach to develop the format,
and also discuss problems that might arise when other solvers use the format.

Over the years the production of machine-consumable formal proofs of
unsatisfiability from SMT solvers [7] has attracted significant attention [5].
Such proofs enable users to certify unsatisfiability results similarly to how
satisfiable results may be certified via models. However, a major difficulty
that SMT proof formats must address is the complex and heterogeneous nature of
SMT solvers: a SAT solver drives multiple, often very different, theory
solvers; instantiation procedures generate ground instances; and heavily
theory-dependent simplification techniques ensure that the solvers are fast in
practice. Moreover, how each of these components works internally can also
differ from solver to solver. As a testament to these challenges proof formats
for SMT solvers have been mostly restricted to individual solvers and no
standard has emerged. To be adopted by several solvers, an SMT proof format
must be carefully designed to accommodate needs of specific solvers. This will
require repeated refinement and generalization.

The basis for our efforts in this field is the proof format implemented by the
SMT solver veriT [9] that is now mature and used by multiple systems. To
further improve the format, as well as to accommodate not only the reasoning
of the SMT solver veriT but also of other solvers, we are currently extending
the format and developing better tooling, such as an independent proof
checker. To facilitate this effort and overall usage, we are also writing a
full specification. To emphasize the independence of the format we are
baptizing it _Alethe_.111Alethe is a genus of small birds and the name
resembles _aletheia_ , the Greek word for truth. We do not presume to propose
a standard format a priori. Instead we believe that Alethe, together with its
tooling, can provide a basis for further discussions on how to achieve a
format to be used by multiple solvers.

##  1 The State of Alethe

Alethe combines two major ideas whose roots reach back ten years to the first
PxTP workshop in 2011 [8, 10]. It was proposed as an easy-to-produce format
with a term language very close to SMT-LIB [6], the standard input language of
SMT solvers, and rules with a varying level of granularity, allowing implicit
proof steps in the proof and thus relying on powerful proof checkers capable
of filling the gaps. Since then the format has been refined and extended [3].
It is now mature, supports coarse- and fine-grained proof steps capturing SMT
solving for the SMT-LIB logic UFLIRA222That is the logic for problems
containing a mix of any of quantifiers, uninterpreted functions, and linear
arithmetic. and can be reconstructed by the proof assistants Coq [2, 12] and
Isabelle [13, 15]. In particular, the integration with Coq was also used as a
bridge for the reconstruction of proofs from the SMT solver CVC4 [4] in Coq,
where its proofs in the LFSC format [16] were first translated into the veriT
format before reconstruction. Finally, the format will also be natively
supported in the upcoming cvc5.
solver333https://cvc4.github.io/2021/04/02/cvc5-announcement.html

On the one hand, Alethe uses a natural-deduction style calculus driven mostly
by resolution [8]. To handle first-order reasoning, dedicated quantifier
instantiation rules are used [10]. On the other hand, it implements novel
ideas to express reasoning typically used for processing, such as
Skolemization, renaming of variables, and other manipulations of bound
variables [3]. While the format was always inspired by the SMT-LIB language,
we recently [13] changed the syntax of Alethe to closely resemble the command
structure used within SMT-LIB. When possible Alethe uses existing SMT-LIB
features, such as the define-fun command to define constants and the :named
annotation to implement term sharing.

The following proof fragment gives a taste of the format. The fragment first
renames the bound variable in the term $\exists x.\,f(x)$ from $x$ to
$\mathit{vr}$ and then skolemizes the quantifier. A proof is a list of
commands. The _assume_ command introduces an assumption, _anchor_ starts a
subproof, and _step_ denotes an ordinary proof step. Steps are annotated with
an identifier, a rule, and premises. The SMT-LIB command _define-fun_ defines
a function. The rule _bind_ used by step t1 performs the renaming of the bound
variable. It uses a subproof (Steps t1.t1 and t1.t2). The subproof uses a
context to denote that x is equal to vr within the subproof. The anchor
command starts the subproof and introduces the context. The bind rule does not
only make it possible to rename bound variables, but within the subproof it is
possible to simplify the formula as done during preprocessing. The steps t2
and t3 use resolution to finish the renaming. In step t4 the bound variable is
skolemized. Skolemization uses the choice binder $\epsilon$ and derives
$f(\epsilon\mathit{vr}.\,f(\mathit{vr}))$ from
$\exists\mathit{vr}.\,f(\mathit{vr})$. To simplify the reconstruction the
choice term is introduced as a defined constant (by define-fun). Finally,
resolution is used again to finish the proof.

⬇

(assume a0 (exists ((x A)) (f x)))

(anchor :step t1 :args (:= x vr))

(step t1.t1 (cl (= x vr)) :rule cong)

(step t1.t2 (cl (= (f x) (f vr))) :rule cong)

(step t1 (cl (= (exists ((x A)) (f x))

(exists ((vr A)) (f vr)))) :rule bind)

(step t2 (cl (not (= (exists ((vr A)) (f x))

(exists ((vr A)) (f vr))))

(not (exists ((vr A)) (f x)))

(exists ((vr A)) (f vr))) :rule equiv_pos1)

(step t3 (cl (exists ((vr A)) (f vr))) :premises (a0 t1 t2) :rule resolution)

(define-fun X () A (choice ((vr A)) (f vr)))

(step t4 (cl (= (exists ((vr A)) (f vr)) (f X))) :rule sko_ex)

(step t5 (cl (not (= (exists ((vr A)) (f vr)) (f X)))

(not (exists ((vr A)) (f vr)))

(f X)) :rule equiv_pos1)

(step t6 (cl (f X)) :premises (t3 t4 t5) :rule resolution)

The output of Alethe proofs from veriT has now reached a certain level of
maturity. The 2021 version of the Isabelle theorem prover was released earlier
this year and supports the reconstruction of Alethe proofs generated by veriT.
Users of Isabelle/HOL can invoke the smt tactic. This tactic encodes the
current proof goal as an SMT-LIB problem and calls an SMT solver. Previously
only the SMT solver Z3 was supported. Now veriT is supported too. If the
solver produces a proof, the proof is reconstructed within the Isabelle
kernel. In practice, users will seldom choose the smt tactic themselves.
Instead, they call the Sledgehammer tool that calls external tools to find
relevant facts. Sometimes, the external tool finds a proof, but the proof
cannot be imported into Isabelle, requiring the user to write a proof
manually. The addition of the veriT-powered smt tactic halves [15] the rate of
this kind of failures. The improvement is especially pronounced for proofs
found by CVC4. A key reason for this improvement is the support for the
conflicting-instance instantiation technique within veriT. Z3, the singular
SMT solver supported previously, does not implement this technique.
Nevertheless, it is Alethe that allowed us to connect veriT to Isabelle, and
we hope that the support for Alethe in other solvers will ease this connection
between powerful SMT solvers and other tools in the future.

The process of implementing proof reconstruction in Isabelle also helped us to
improve the proof format. We found both, possible improvements in the format
(like providing the Farkas’ coefficient for lemmas of linear arithmetic) and
in the implementation (by identifying concrete errors). One major shortcoming
of the proofs were rules that combined several simplification steps into one.
We replaced these steps by multiple simple and well-defined rules. In
particular every simplification rule addresses a specific theory instead of
combining them. An interesting observation of the reconstruction in Isabelle
is that some steps can be skipped to improve performance. For example, the
proofs for the renaming of variables are irrelevant for Isabelle since this
uses De Bruijn indices. This shows that reconstruction specific optimizations
can counterbalance the proof length which is increased by fine-grained rules.
We will take this prospect into account as we further refine the format.

##  2 A Glance Into the Future

The development of the Alethe proof format so far was not a monolithic
process. Both practical considerations and research progress — such as
supporting fine-grained preprocessing rules — influenced the development
process. Due to this, the format is not fully homogeneous, but this approach
allowed us to quickly adapt the format when necessary. We will continue this
pragmatic approach.

### Speculative Specification.

We are writing a speculative specification.444The current version is available
at http://www.verit-solver.org/documentation/alethe-spec.pdf. During the
development of the Isabelle reconstruction it became necessary to document the
proof rules in a coherent and complete manner. When we started to develop the
reconstruction there was only an automatically generated list of rules with a
short comment for each rule. While this is enough for simple tautological
rules, it does not provide a clear definition of the more complex rules such
as the linear arithmetic rules. To rectify this, we studied veriT’s source
code and wrote an independent document with a list of all rules and a clear
mathematical definition of each rule. We chose a level of precision for these
descriptions that serves the implementer: precise enough to clarify the edge
case, but without the details that would make it a fully formal specification.
We are now extending this document to a full specification of the format. This
specification is speculative in the sense that it will not be cast in stone.
It will describe the format as it is in use at any point in time and will
develop in parallel with practical support for the format within SMT solvers,
proof checkers, and other tools.

### Flexible Rules.

The next solver that will gain support for the Alethe format is the upcoming
cvc5 solver. Implementing a proof format into another solver reveals where the
proof format is too tied to the current implementation of veriT. On the one
hand, new proof rules must be added to the format — e.g., veriT does not
support the theory of bitvectors, while cvc5 does. When CVC4 was integrated
into Coq via a translation of its LFSC proofs into Alethe proofs [12], an ad-
hoc extension with bitvector rules was made. A revised version of this
extension will now be incorporated into the upcoming specification of the
format so that cvc5 bitvector proofs can be represented in Alethe. Further
extensions to other theories supported by cvc5, like the theory of strings,
will eventually be made as well.

Besides new theories, cvc5 can also be stricter than veriT in the usage of
some rules. This strictness can simplify the reconstruction, since less search
is required. A good example of this is the trans rule that expresses
transitivity. This rule has a list of equalities as premises and the
conclusion is an equality derived by transitivity. In principle, this rule can
have three levels of “strictness”:

  1. 1.

The premises are ordered and the equalities are correctly oriented (like in
cvc5), e.g., $a=b$, $b=c$, and $c=d$ implies $a=d$.

  2. 2.

The premises are ordered but the equalities might not be correctly oriented
(like in veriT), e.g., $b=a$, $c=b$, and $d=c$ implies $d=a$.

  3. 3.

Neither are the assumptions ordered, nor are the equalities oriented, e.g.,
$c=b$, $b=a$, and $d=c$ implies $d=a$.

The most strict variant is the easiest to reconstruct: a straightforward
linear traversal of the premises suffices for checking. From the point of view
of producing it from the solver, however, this version is the hardest to
implement. This is due to implementations of the congruence closure decision
procedure [14, 11] in SMT solvers being generally agnostic to the order of
equalities, which can lead to implicit reorientations that can be difficult to
track. Anecdotally, for cvc5 to achieve this level of detail several months of
work were necessary, within the overall effort of redesigning from scratch
CVC4’s proof infrastructure. Since we cannot assume every solver developer
will, or even should, undertake such an effort, all the different levels of
granularity must be allowed by the format, each requiring different complexity
levels of checking.

To keep the proof format flexible and proofs easy to produce, we will provide
different versions of proof rules, with varying levels of granularity as in
the transitivity example case above, by _annotating_ them. This leverages the
rule _arguments_ , which are already used by some rules. For example, the
Farkas’ coefficient of the linear arithmetic rule are provided as arguments.
This puts pressure on proof checkers and reconstruction in proof assistants to
support all the variants or at least the most general one (at the cost of
efficiency). Hence, our design principle here is that the annotation is
optional: the absence of an annotation denotes the least strict version of the
rule.

### Powerful Tooling.

We believe that powerful software tools may greatly increase the utility of a
proof format. Towards this end we have started implementing an independent
proof checker for Alethe. In contrast to a proof-assistant-based
reconstruction, this checker will not be structured around a small, trusted
kernel, and correct-by-construction extensions. Instead, the user would need
to trust the implementation does not lead to wrong checking results. Instead,
its focus is on performance, support for multiple features and greater
flexibility for integrating extensions and refinements to the format. The
Isabelle checker is currently not suited to this task — one major issue is
that it does not support SMT-LIB input files.555A version capable of doing so
was developed for Z3 but it was unfortunately lost.

This independent checker will also serve as a proof “elaborator”. Rather than
checking, it will also allow converting a coarse-grained proof, containing
implicit steps, to a fine-grained one, with more detailed steps. The resulting
proof can then be more efficiently checked by the tool itself or via proof-
assistant reconstructions. An example of such elaboration is the transitivity
rule. If the rule is not in its most detailed version, with premises in the
correct order and none implicitly reordered, it can be elaborated by greedily
reordering the premises and adding proof steps using the symmetry of equality.
Note however that in the limit detailing coarse-grained steps can be as hard
as solving an SMT problem. Should such cases arise, the checker will rely on
internal proof-producing procedures capable of producing a detailed proof for
the given step. At first the veriT and cvc5 solvers, which can produce fine-
grained proofs for several aspects of SMT solving, could be used in such
cases.

A nice side effect of the use of an external checker is that it could prune
useless steps. Currently SMT solvers keep a full proof trace in memory and
print a pruned proof after solving finishes. This is in contrast to SAT
solvers that dump proofs on-the-fly. For SAT proofs, the pruned proof can be
obtained from a full trace by using a tool like Drat-Trim. There is some
ongoing work by Nikolaj Bjørner on Z3 to also generate proofs on-the-fly, but
it is not clear how to support preprocessing and
quantifiers.666https://github.com/Z3Prover/z3/discussions/4881

##  3 Conclusion

We have presented on overview of the current state of the Alethe proof format
and some ideas on how we intend to improve and extend the format, as well as
supporting tools. In designing a new proof format supported across two solvers
we hope to provide a first step towards a format adopted by more solvers. This
format allows several levels of detail, and is thus flexible enough to
reasonably easily produce proofs in various contexts. We intend to define a
precise semantics at each level though. This distinguishes our format from
other approaches, such as the TSTP format [17], that are probably easier to
adopt but only specify the syntax, leading to very different proofs generated
by the various provers supporting it.

One limit of our approach for proofs is that we cannot express global
transformations like symmetry breaking. SAT solvers are able to add clauses
(DRAT clauses) such that the overall problems is equisatisfiable. It is
unclear however how to add such clauses in the SMT context.

Overall, we hope to get feedback from users and developers to see what special
needs they have and exchange ideas on the proof format.

### Acknowledgment

We thank Bruno Andreotti for ongoing work on the proof checker and Hanna
Lachnitt for ongoing work on the cvc5 support. We are grateful for the helpful
comments provided to us by the anonymous reviewers. The first author has
received funding from the European Research Council (ERC) under the European
Union’s Horizon 2020 research and innovation program (grant agreement No.
713999, Matryoshka). The second author is supported by the LIT AI Lab funded
by the State of Upper Austria.

## References

  * [1]
  * [2] Michaël Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Théry & Benjamin Werner (2011): _A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses_.  In Jean-Pierre Jouannaud & Zhong Shao, editors: Certified Programs and Proofs, LNCS 7086, Springer, pp. 135–150, 10.1007/978-3-642-25379-912.
  * [3] Haniel Barbosa, Jasmin C. Blanchette, Mathias Fleury & Pascal Fontaine (2019): _Scalable Fine-Grained Proofs for Formula Processing_.  Journal of Automated Reasoning, 10.1007/s10817-018-09502-y.
  * [4] Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanović, Tim King, Andrew Reynolds & Cesare Tinelli (2011): _CVC4_.  In Ganesh Gopalakrishnan & Shaz Qadeer, editors: Computer Aided Verification (CAV), Springer, pp. 171–177, 10.1007/978-3-642-22110-114.
  * [5] Clark Barrett, Leonardo De Moura & Pascal Fontaine (2015): _Proofs in satisfiability modulo theories_.  All about proofs, Proofs for all 55(1), pp. 23–44.
  * [6] Clark Barrett, Pascal Fontaine & Cesare Tinelli (2017): _The SMT-LIB Standard: Version 2.6_.  Technical Report, Department of Computer Science, The University of Iowa.  Available at www.SMT-LIB.org.
  * [7] Clark W. Barrett & Cesare Tinelli (2018): _Satisfiability Modulo Theories_.  In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith & Roderick Bloem, editors: Handbook of Model Checking., Springer, pp. 305–343, 10.1007/978-3-319-10575-8_11.
  * [8] Frédéric Besson, Pascal Fontaine & Laurent Théry (2011): _A Flexible Proof Format for SMT: A Proposal_.  In Pascal Fontaine & Aaron Stump, editors: PxTP 2011, pp. 15–26.
  * [9] Thomas Bouton, Diego C. B. de Oliveira, David Déharbe & Pascal Fontaine (2009): _veriT: An Open, Trustable and Efficient SMT-solver_.  In Renate A. Schmidt, editor: CADE 22, LNCS 5663, Springer Berlin Heidelberg, pp. 151–156, 10.1007/978-3-642-02959-2_12.
  * [10] David Déharbe, Pascal Fontaine & Bruno Woltzenlogel Paleo (2011): _Quantifier Inference Rules for SMT Proofs_.  In Pascal Fontaine & Aaron Stump, editors: PxTP 2011, pp. 33–39.
  * [11] Peter J. Downey, Ravi Sethi & Robert Endre Tarjan (1980): _Variations on the Common Subexpression Problem_.  J. ACM 27(4), pp. 758–771, 10.1145/322217.322228.
  * [12] Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds & Clark Barrett (2017): _SMTCoq: A Plug-In for Integrating SMT Solvers into Coq_.  In Rupak Majumdar & Viktor Kunčak, editors: CAV 2017, LNCS 10426, Springer, pp. 126–133, 10.1007/978-3-319-63390-9_7.
  * [13] Mathias Fleury & Hans-Jörg Schurr (2019): _Reconstructing veriT Proofs in Isabelle/HOL_.  In Giselle Reis & Haniel Barbosa, editors: PxTP 2019, EPTCS 301, pp. 36–50, 10.4204/EPTCS.301.6.
  * [14] Greg Nelson & Derek C. Oppen (1980): _Fast Decision Procedures Based on Congruence Closure_.  J. ACM 27(2), pp. 356–364, 10.1145/322186.322198.
  * [15] Hans-Jörg Schurr, Mathias Fleury & Martin Desharnais (2021): _Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant_.  In: CADE 28, LNCS.
  * [16] Aaron Stump, Duckki Oe, Andrew Reynolds, Liana Hadarean & Cesare Tinelli (2013): _SMT proof checking using a logical framework_.  Formal Methods in System Design 42(1), pp. 91–118, 10.1007/s10703-012-0163-3.
  * [17] Geoff Sutcliffe, Jürgen Zimmer & Stephan Schulz (2004): _TSTP Data-Exchange Formats for Automated Theorem Proving Tools_.  In Weixiong Zhang & Volker Sorge, editors: Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems, Frontiers in Artificial Intelligence and Applications 112, IOS Press, pp. 201–215.