A finite-type field has finite relative algebraic constants

Fix a finite generating list $a_1,\dots ,a_m$ from [F1]. [construct] Scan the list in order, starting with $T_0=\mathrm{\varnothing }$. At stage $i$, adjoin $a_i$ to the selected set exactly when it is transcendental over the field generated by the previously selected elements. The selected set stays algebraically independent: if adjoining $a_i$ created a nonzero polynomial relation, its degree in $a_i$ would be positive, since a relation of degree zero would contradict independence of the preceding tuple. Write it as a polynomial in $a_i$; independence of the preceding tuple makes a nonzero coefficient remain after evaluation, so this would make $a_i$ algebraic over its generated field, a contradiction. Every omitted generator is algebraic over the field generated at its stage and stays algebraic after enlarging that field. Thus the final finite set $T$ is algebraically independent over $k$, and every $a_i$ is algebraic over $k(T)$. This finite scan uses no choice principle.

The field $K=k(T)(a_1,\dots ,a_m)$ is generated over $k(T)$ by finitely many elements algebraic over that field. [step 1.1, algebra] Hence [F4] makes $K\mathrm{/}k(T)$ finite. Set $n:=[K:k(T)]$; since both are fields, $n\ge 1$. If $m=0$, then $K=k$, $T$ is empty and $n=1$.

Let $E$ be any algebraic intermediate field $k\subseteq E\subseteq K$. The tuple $T$ remains algebraically independent over $E$. [step 1.1, algebra] Otherwise choose a nonempty subset $T^{\mathrm{\prime }}\subseteq T$ of least cardinality that is algebraically dependent over $E$, and choose $t\in T^{\mathrm{\prime }}$. The tuple $T^{\mathrm{\prime }}\setminus \{t\}$ is independent over $E$. A nonzero polynomial relation on $T^{\mathrm{\prime }}$ can be viewed as a polynomial in $t$ with coefficients in the other variables; independence of $T^{\mathrm{\prime }}\setminus \{t\}$ ensures at least one coefficient stays nonzero after evaluation. The relation must have positive degree in $t$, since degree zero would give a relation on the independent tuple $T^{\mathrm{\prime }}\setminus \{t\}$. Hence it gives a nonzero polynomial over $E(T^{\mathrm{\prime }}\setminus \{t\})$ vanishing at $t$, so $t$ is algebraic over that field.

Let $L$ be any finite intermediate extension $k\subseteq L\subseteq K$, write $d=[L:k]$, and choose a $k$-basis $b_1,\dots ,b_d$ of $L$. [step 1.1, step 2.1, step 2.2, algebra] Since $L\mathrm{/}k$ is finite, [F5] makes it algebraic, so step 2.2 applies and $T$ is algebraically independent over $L$. Suppose ${\sum }_{i=1}^d{b}_i{\lambda }_i=0,{\lambda }_i\in k(T)\mathrm{.}$ Let $P=k[X_t:t\in T]$ and let ${\mathrm{ev}}_k:P\to K$ evaluate each $X_t$ at $t$. By step 1.1 and [F9], ${\mathrm{ev}}_k$ is injective, so ${\mathrm{ev}}_k(g)\mathrm{\ne }0$ for every nonzero $g\in P$. The quotients ${\mathrm{ev}}_k(f)\mathrm{/}{\mathrm{ev}}_k(g)$, where $f,g\in P$ and $g\mathrm{\ne }0$, form the subfield generated by $k$ and $T$: they form a subfield containing those elements, and every subfield containing them contains all these quotients. By [F2], this is $k(T)$. Choose a common denominator $g$ and numerators $f_1,\dots ,f_d\in P$ with ${\lambda }_i={\mathrm{ev}}_k(f_i)\mathrm{/}{\mathrm{ev}}_k(g)$. Multiplying the displayed relation by its nonzero denominator gives ${\sum }_i{b}_i{\mathrm{ev}}_k(f_i)=0$. Algebraic independence over $L$ means the evaluation map $L[X_t:t\in T]\to K$ is injective, so the polynomial ${\sum }_i{b}_i{f}_i(X)$ in that ring is zero. For each monomial its coefficient is a $k$-linear combination of $b_1,\dots ,b_d$; their basis independence makes every coefficient in every $f_i$ zero. Thus all ${\lambda }_i$ are zero, and $b_1,\dots ,b_d$ are linearly independent over $k(T)$ inside $K$. Since $K$ has an $n$-element spanning set over $k(T)$, [F11] gives $[L:k]=d\le n\mathrm{.}$

Let $D$ be the set of degrees $[L:k]$ of finite intermediate fields $k\subseteq L\subseteq K$. [step 3.1, choose] It is nonempty because $k$ itself has degree $1$. Every degree in $D$ is a positive integer, since an intermediate field contains $1\mathrm{\ne }0$. Step 3.1 therefore puts $D$ inside $\{1,\dots ,n\}$. Start with the attained value $1\in D$ and inspect $2,\dots ,n$ in order, replacing the current value by $r$ exactly when $r\in D$. This finite scan yields a greatest member $d_0\in D$. By the definition of $D$, there is a finite intermediate field $L$ with $[L:k]=d_0$; fix one such witness. This is one existential choice from a nonempty set, not a choice function on a family.

Take any $a\in k_{\mathrm{a}\mathrm{l}\mathrm{g}}$. [step 4.1, algebra] It is algebraic over $k$ and therefore over $L$, since its nonzero polynomial over $k$ remains nonzero over $L$. By [F6], $L(a)\mathrm{/}L$ is finite; since $L\mathrm{/}k$ is finite, [F7] makes $L(a)\mathrm{/}k$ finite and $[L(a):k]=[L(a):L][L:k]\mathrm{.}$ Because $L(a)\subseteq K$, this degree lies in $D$, so it is at most $d_0=[L:k]$. The tower formula and $[L(a):L]\ge 1$ force $[L(a):L]=1$, whence $L(a)=L$ and $a\in L$. Thus $k_{\mathrm{a}\mathrm{l}\mathrm{g}}\subseteq L$. Conversely [F5] makes every element of the finite extension $L\mathrm{/}k$ algebraic over $k$, so $L\subseteq k_{\mathrm{a}\mathrm{l}\mathrm{g}}$. Therefore $k_{\mathrm{a}\mathrm{l}\mathrm{g}}=L$ and is a finite extension of $k$.

This proof includes the empty generator list and empty transcendence tuple. [step 1.1, step 2.1, step 2.2, step 3.1, step 4.1, step 5.1, algebra] If $n=1$, the only possible finite intermediate degree is $1$ and the maximum argument gives $k_{\mathrm{a}\mathrm{l}\mathrm{g}}=k$. No characteristic, separability, or perfectness hypothesis is used. AC is not used: the generator scan and degree bound are finite, and the basis and maximal-degree witness are each fixed only for one arbitrary finite intermediate field.