Regular points of locally Noetherian schemes

Noetherian local stalk. Fix $x$. By [F1], there is an affine open neighborhood $U=\mathrm{Spec}B$ of $x$ with $B$ Noetherian. Because the sheaf on $U$ is the restriction from $X$ [F2], neighborhoods of $x$ contained in $U$ are cofinal among its neighborhoods in $X$; the stalk-colimit description [F3] therefore identifies ${\mathcal{O}}_{X,x}$ with ${\mathcal{O}}_{U,x}$. Let $\mathfrak{p}\subset B$ be the prime corresponding to $x$. By [F4], $R\cong B_{\mathfrak{p}}$, and [F6] makes this a nonzero local ring with maximal ideal $\mathfrak{p}{B}_{\mathfrak{p}}$. We verify Noetherianity directly. Let $J$ be any ideal of $B_{\mathfrak{p}}$ and contract it to $I=\{b\in B:b\mathrm{/}1\in J\}$. This is an ideal of $B$, hence a submodule of its regular module [F7]; by [F8], take a finite generating list $b_1,\dots ,b_q$ of $I$. If $a\mathrm{/}s\in J$, then [F5] and the ideal property give $a\mathrm{/}1=(s\mathrm{/}1)(a\mathrm{/}s)\in J$, so $a\in I$ and $a={\sum }_i{c}_i{b}_i$. It follows that $a\mathrm{/}s={\sum }_i(c_i\mathrm{/}s)(b_i\mathrm{/}1)$. Conversely every $b_i\mathrm{/}1$ lies in $J$, so these images generate $J$. Thus every ideal of $B_{\mathfrak{p}}$ is finitely generated and $R$ is Noetherian. This uses a chart for the fixed point and a finite list for the fixed ideal, not a simultaneous choice over all points or ideals.

Intrinsic tangent dimension and regularity. By step 1.1, $R$ is Noetherian local, so its maximal ideal is finitely generated by [F7, F8]. The images of a finite generating list span $V={\mathfrak{m}}_x\mathrm{/}{\mathfrak{m}}_x^2$ over $\kappa (x)$; hence $V$ is finite-dimensional. A finite basis of $V$ gives the same number of dual basis vectors, so [F9] yields ${\dim }_{\kappa (x)}{T}_{x}X={\dim }_{\kappa (x)}V=\mathrm{edim}R$ by [F10]. Therefore $R$ is regular local if and only if ${\dim }_{\kappa (x)}{T}_{x}X=\dim R$, proving both directions. If $\dim R=0$ or $1$, this is respectively the equality $\mathrm{edim}R=0$ or $1$; if ${\mathfrak{m}}_x=0$, both criteria reduce to $0=\dim R$. Since $T_{x}X$ is finite-dimensional, an infinite value of $\dim R$ cannot satisfy either criterion. If $X$ is empty, there is no point to test. The argument uses only finite generation and finite-dimensional linear algebra, so neither AC nor DC is used.