dvrs as regular local rings

Every nonzero $a\in R$ is $t^{v(a)}u$ with $v(u)=0$, so $u$ is a unit. Thus the nonunits form $(t)$, the unique maximal ideal. In each nonzero ideal, choose an element of least valuation; it divides every element of that ideal and hence generates it. The zero ideal is principal too, so $R$ is Noetherian. A nonzero proper prime contains some $t^{n}u$ with $n\ge 1$, hence contains $t$ and equals $(t)$. Since $R\subseteq K$ is a domain and $(t)\mathrm{\ne }0$, its only primes are $(0)$ and $(t)$, giving dimension one. These choices are of one element for a fixed ideal, not of a family.

Since $t\mathrm{\notin }(t^2)$ by valuation, the map $k=R\mathrm{/}(t)\to (t)\mathrm{/}(t^2)$ sending $a+(t)$ to $at+(t^2)$ is bijective: surjectivity is immediate, and cancellation proves injectivity. Thus the cotangent dimension is one, $R$ is regular local, and its minimal generating tuple $(t)$ is a regular system of parameters.

For each $n\ge 0$, the map $a+(t)\mapsto a{t}^n+(t^{n+1})$ is well-defined and identifies $k$ with $(t^n)\mathrm{/}(t^{n+1})$, again by cancellation and principality. Multiplication of these classes agrees with polynomial multiplication. Hence the graded map $k[T]\to {\mathrm{gr}}_{(t)}R$ sending $T$ to $t+(t^2)$ is an isomorphism in every degree, and therefore an isomorphism of graded rings. No choice principle is used.