The horror conjecture on recursive axiomatization of curve-counting conditions

Let $T^+$ be the theory under consideration, and let $(K_\infty,\sigma,\chi)$ be a structure satisfying $\widetilde{\operatorname{ACPF}}$ and Axioms

$$–$$

of $T^+$. For $g\geq 1$, a prime power $p^k$, and a genus-$g$ curve $C$ over $K_1$ with Jacobian $J$, write $\chi_{p^k}(C(K_1))$ for the relevant counting component, and let $J[p^k]$ and $\mathbb{G}_m[p^k]$ denote the corresponding $p^k$-torsion groups.

The horror conjecture. In the language of $T^+$, there are sentences $\tau_{g,p^k,n}$ depending recursively on the parameters such that, for every $g\geq 1$, every prime power $p^k$, and every such structure, the following are equivalent:

1. $(K_\infty,\sigma,\chi)$ satisfies $\bigwedge_{n=1}^{\infty}\tau_{g,p^k,n}$.
2. For every genus-$g$ curve $C$ over $K_1$ with Jacobian $J$,

$$\chi_{p^k}(C(K_1))=1-\operatorname{Tr}(\sigma\mid J[p^k])+\operatorname{Tr}(\sigma\mid\mathbb{G}_m[p^k]).$$

The conjecture would make the additional geometric axioms of $T^+$ recursively enumerable, completing the intended recursive axiomatization. The paper describes it as almost certainly true but leaves the formal verification for future work.