Existence of W(k) and a ramified quadratic extension W(k)[√ p ]

Let $p$ be a prime and let $k$ be an algebraically closed field of characteristic $p$. The theorem asserts the existence of the following data. First, a type $O^{nr}$ carrying a commutative ring structure making it a domain, a discrete valuation ring of characteristic zero, together with a $\mathbb{Z}_p$-algebra structure such that: $O^{nr}$ is adically complete (in Mathlib's IsAdicComplete sense, so complete and separated) for the ideal generated by the image of $p$ under $\mathbb{Z}_p \to O^{nr}$, that ideal is maximal, and there is a ring isomorphism $e$ from the residue field $O^{nr}/\mathfrak{m}$ onto $k$; moreover a ring homomorphism $\iota : W(\mathbb{F}_{p^2}) \to O^{nr}$ from the Witt vectors of the Galois field with $p^2$ elements, carried along as data with no compatibility required of it. Second, a type $O'$ carrying a commutative ring structure making it a domain, a discrete valuation ring of characteristic zero, together with an $O^{nr}$-algebra structure such that $O'$ is adically complete for its maximal ideal, an element $\varpi'$ of the maximal ideal of $O'$ with $\varpi'^2 =$ the image of $p$ under $O^{nr} \to O'$, and a ring homomorphism $\varphi' : O' \to k$ which is surjective and satisfies $\varphi' \circ (O^{nr} \to O') = e \circ (\text{residue map of } O^{nr})$.

This packages the absolutely unramified complete discrete valuation ring $W(k)$ with residue field $k$, a structural map from $W(\mathbb{F}_{p^2})$, and the ramified quadratic extension $W(k)[\sqrt{p}\,]$ with its reduction map to $k$, all delivered as an existence statement so that consumers may work with an abstract such pair. It is used in the Čerednik–Drinfeld part of the development, where special formal modules and fake elliptic curves are set up over such a base.