[proofplan] We parametrize the unit circle by drawing lines of rational slope through the rational base point $(-1,0)$. First we verify directly that every value of the displayed formula is a rational point on the circle. Then we take an arbitrary rational point different from $(-1,0)$, form the rational slope $t = Y/(X+1)$ of the line through $(-1,0)$ and the point, and solve the resulting quadratic intersection equation. The excluded point is exactly the point obtained from the vertical line through $(-1,0)$. [/proofplan] [step:Verify that the displayed formula gives rational points on the unit circle] Let $t \in \mathbb{Q}$. Since $1+t^2 \neq 0$ in $\mathbb{Q}$, define \begin{align*} X_t &:= \frac{1-t^2}{1+t^2}, & Y_t &:= \frac{2t}{1+t^2}. \end{align*} Then $X_t,Y_t \in \mathbb{Q}$. We compute \begin{align*} X_t^2 + Y_t^2 &= \left(\frac{1-t^2}{1+t^2}\right)^2 + \left(\frac{2t}{1+t^2}\right)^2 \\ &= \frac{(1-t^2)^2 + 4t^2}{(1+t^2)^2} \\ &= \frac{1 - 2t^2 + t^4 + 4t^2}{(1+t^2)^2} \\ &= \frac{1 + 2t^2 + t^4}{(1+t^2)^2} \\ &= \frac{(1+t^2)^2}{(1+t^2)^2} \\ &= 1. \end{align*} Thus \begin{align*} \left(\frac{1-t^2}{1+t^2}, \frac{2t}{1+t^2}\right) \in C(\mathbb{Q}) \end{align*} for every $t \in \mathbb{Q}$. [/step] [step:Recover the parameter from any rational point other than $(-1,0)$] Let $(X,Y) \in C(\mathbb{Q})$ and assume $(X,Y) \neq (-1,0)$. Since $X^2 + Y^2 = 1$, if $X=-1$ then $Y^2=0$, so $Y=0$, contradicting $(X,Y) \neq (-1,0)$. Hence $X+1 \neq 0$. Define the rational number \begin{align*} t := \frac{Y}{X+1}. \end{align*} This is the slope of the non-vertical line through $(-1,0)$ and $(X,Y)$, and it gives \begin{align*} Y = t(X+1). \end{align*} Substituting this expression into the equation $X^2+Y^2=1$ gives \begin{align*} X^2 + t^2(X+1)^2 &= 1. \end{align*} Expanding and moving all terms to the left-hand side, \begin{align*} (1+t^2)X^2 + 2t^2X + t^2 - 1 &= 0. \end{align*} We factor the left-hand side: \begin{align*} (1+t^2)X^2 + 2t^2X + t^2 - 1 &= (X+1)\bigl((1+t^2)X + t^2 - 1\bigr). \end{align*} Since $X+1 \neq 0$, the second factor must vanish: \begin{align*} (1+t^2)X + t^2 - 1 &= 0. \end{align*} Solving for $X$ gives \begin{align*} X = \frac{1-t^2}{1+t^2}. \end{align*} Using $Y=t(X+1)$, we obtain \begin{align*} Y &= t\left(\frac{1-t^2}{1+t^2}+1\right) \\ &= t\left(\frac{1-t^2+1+t^2}{1+t^2}\right) \\ &= \frac{2t}{1+t^2}. \end{align*} Therefore every rational point of $C(\mathbb{Q})$ different from $(-1,0)$ has the displayed form for the rational parameter $t = Y/(X+1)$. [/step] [step:Account for the exceptional vertical line through $(-1,0)$] The point $(-1,0)$ is rational and satisfies \begin{align*} (-1)^2 + 0^2 = 1, \end{align*} so $(-1,0) \in C(\mathbb{Q})$. It is not obtained from a finite slope through $(-1,0)$ because the expression \begin{align*} \frac{Y}{X+1} \end{align*} is undefined at $X=-1$. Geometrically, this is the vertical line through $(-1,0)$. Its intersection with the unit circle is only $(-1,0)$: if $X=-1$ and $X^2+Y^2=1$, then \begin{align*} 1+Y^2=1, \end{align*} hence $Y=0$. Combining the parametrized points from the first step, the recovery argument from the second step, and the exceptional point just handled, we obtain \begin{align*} C(\mathbb{Q}) = \left\{ \left(\frac{1-t^2}{1+t^2}, \frac{2t}{1+t^2}\right) : t \in \mathbb{Q} \right\} \cup \{(-1,0)\}. \end{align*} This proves the theorem. [/step]