A formal-coordinate fibre is an Aut O torsor

The individual coordinate set is nonempty by F1. The maps in F3 preserve the defining complete-algebra and ideal conditions in F2. Their action satisfies $(\tau \cdot {\rho }_1)\cdot {\rho }_2={\varphi }_{{\rho }_2}^{-1}{\varphi }_{{\rho }_1}^{-1}\tau ={\varphi }_{{\rho }_1{\rho }_2}^{-1}\tau =\tau \cdot ({\rho }_1{\rho }_2)\mathrm{.}$ If $\tau \cdot \rho =\tau$, surjectivity of $\tau$ gives ${\varphi }_{\rho }^{-1}=\mathrm{i}\mathrm{d}$ and hence $\rho (t)=t$. Thus this is a free right action.

Given ${\tau }_1,{\tau }_2\in {\mathrm{Coord}}_{X,p}$, the continuous ring automorphism ${\tau }_1\circ {\tau }_2^{-1}$ preserves $(t)$. Let $\rho$ be its unique substitution series, so ${\varphi }_{\rho }={\tau }_1\circ {\tau }_2^{-1}$. Then ${\varphi }_{\rho }^{-1}\circ {\tau }_1={\tau }_2$, or ${\tau }_1\cdot \rho ={\tau }_2$. Freeness gives uniqueness, proving simple transitivity on the individual fiber.

For two relative coordinates over $W$, the composition ${\tau }_1\circ {\tau }_2^{-1}$ is a continuous ${\mathcal{O}}_W$-algebra sheaf automorphism preserving $(t)$. Its image of $t$ has holomorphic coefficients and unit linear term, and F3 identifies it with a unique ${\varphi }_{\rho }$. Thus ${\tau }_1\cdot \rho ={\tau }_2$; the action law and freeness hold by the same composition identities as in step 1.1. This proves the torsor assertion whenever the relative-coordinate set is nonempty. For each $s\in W$, restriction means reduction of every finite jet modulo the maximal ideal at $s$, followed by inverse limit; it gives a continuous isomorphism ${\widehat{\mathcal{O}}}_{X_s,s_i(s)}\to \mathbb{C}\mathrm{⟦}t\mathrm{⟧}$. For this identification choose base coordinates z and a total coordinate w whose differential complements those of $z\circ \pi$. The map $(z\circ \pi ,w)$ is locally biholomorphic: after normalizing its invertible derivative it has form $I+H$ with $\mathrm{\parallel }dH\mathrm{\parallel }<1\mathrm{/}2$ on a small ball, so iteration of $x=y-H(x)$ converges locally uniformly to its holomorphic inverse. Subtracting the holomorphic value of w on the section gives a local vertical coordinate vanishing there. Its finite jet rings are ${\mathcal{O}}_{W,s}[t]\mathrm{/}(t^k)$, proving the identification before passage to the inverse limit. The resulting coordinate makes the fiber set nonempty; the algebraic argument of step 2.1 proves simple transitivity there without any projective-presentation assumption on $X_s$. Every complex substitution series lifts to the relative group by constant coefficient functions, so the restriction is equivariant and its image is the whole individual torsor. No assertion that every individual coordinate extends as a holomorphic chart germ is needed.