Counting Eulerian circuits in subexponential time, assuming the new #SAT algorithms

Counting the Eulerian circuits of an undirected graph is #P-complete, even for planar 4-regular graphs, while for directed graphs the BEST theorem counts them in polynomial time. However, we are unaware of any exact algorithm for undirected graphs of bounded degree that runs in time $2^{o(m)}$, where $m$ is the number of edges. We show that such an algorithm follows from the exact counting of Hamiltonian cycles that we proved earlier on top of Anthropic's claimed #SAT algorithm. The reduction is classical: by Kotzig's description, the Eulerian circuits of $G$ are in bijection with the Hamiltonian cycles of the line graph of the double subdivision of $G$, which has $3m$ vertices and at most $(\Delta+1)m$ edges. We prove in Lean 4 (theoremEuler, theoremEuler_noIso, theoremEuler_rate; axioms propext, Classical.choice, Quot.sound) that for every $\delta>0$ and $\Delta$ a finite-alphabet Mathlib Turing machine outputs the number of Eulerian circuits of every graph of maximum degree at most $\Delta$ within $\lfloor C(n+2)^C 2^{\delta m}\rfloor$ steps, and within $\lfloor C 2^{\delta m}\rfloor$ steps when there is no isolated vertex; and that one machine does so for all graphs within $\lfloor C(n+2)^C 2^{Cm\log_2(\Delta+2)/\sqrt{\log_2(m+2)}}\rfloor$ steps. The factor $(n+2)^C$ pays for reading the $n^2$-bit adjacency matrix and cannot be dropped. The bijection is checked by brute force on twelve small graphs, for example 132 circuits for $K_5$. The formal object is Kotzig's transition-system definition; its agreement with Mathlib's Eulerian walks is not formalised. The constants are astronomical, and the proof rests on Anthropic's Lean development of its claimed refutation of the Exponential Time Hypothesis, which is under review.