No, you shouldn't need any choice for this, and it should still be true if you replace $\overline{\mathbb{Q}}$ with any other algebraic closure of $\mathbb{Q}$. Let $K$ be a field (which in our application will be $\overline{\mathbb{Q}}$) and let $G$ be a finite group of automorphisms of $K$. Then $K/K^G$ is always a degree $\#(G)$ extension. (See EG Milne Corollary 2.14 and Theorem 3.4.)

The Artin-Schreier theorem says that $K/F$ is a finite degree extension and $K$ is algebraically closed, then $[K:F] \leq 2$.

Combining the two statements, if $G$ is a finite subgroup of $\text{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})$, then $\#(G) \leq 2$.

There is no use of choice in the proof of either of the big tools that I'm using.

No, you shouldn't need any choice for this, and it should still be true if you replace $\overline{\mathbb{Q}}$ with any other algebraic closure of $\mathbb{Q}$. Let $K$ be a field (which in our application will be $\overline{\mathbb{Q}}$) and let $G$ be a finite group of automorphisms of $K$. Then $K/K^G$ is always a degree $\#(G)$ extension. (See, e.g., Milne - Fields and Galois theory Corollary 2.14 and Theorem 3.4.)

The Artin–Schreier theorem says that, if $K/F$ is a finite degree extension and $K$ is algebraically closed, then $[K:F] \leq 2$.

Combining the two statements, if $G$ is a finite subgroup of $\operatorname{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})$, then $\#(G) \leq 2$.

There is no use of choice in the proof of either of the big tools that I'm using.

No, you shouldn't need any choice for this, and it should still be true if you replace $\overline{\mathbb{Q}}$ with any other algebraic closure of $\mathbb{Q}$. Let $K$ be a field (which in our application will be $\overline{\mathbb{Q}}$) and let $G$ be a finite group of automorphisms of $K$. Then $K/K^G$ is always a degree $\#(G)$ extension. (See EG Milne Corollary 2.14 and Theorem 3.4.)

The Artin-Schreier theorem says that $K/F$ is a finite degree extension and $K$ is algebraically closed, and $[K:F] \leq 2$.

Combining the two statements, if $G$ is a finite subgroup of $\text{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})$, then $\#(G) \leq 2$.

There is no use of choice in the proof of either of the big tools that I'm using.

No, you shouldn't need any choice for this, and it should still be true if you replace $\overline{\mathbb{Q}}$ with any other algebraic closure of $\mathbb{Q}$. Let $K$ be a field (which in our application will be $\overline{\mathbb{Q}}$) and let $G$ be a finite group of automorphisms of $K$. Then $K/K^G$ is always a degree $\#(G)$ extension. (See EG Milne Corollary 2.14 and Theorem 3.4.)

The Artin-Schreier theorem says that $K/F$ is a finite degree extension and $K$ is algebraically closed, then $[K:F] \leq 2$.

Combining the two statements, if $G$ is a finite subgroup of $\text{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})$, then $\#(G) \leq 2$.

There is no use of choice in the proof of either of the big tools that I'm using.