定規とコンパスによる作図

方針：1 は ex-rcc-bisector の計算を一般の長さで行う。2 は 1 に帰着させ、3 は 2 を 2 回使う。
段 1（1 の証明）。$AB=2s$（$s>0$）とし、$A(-s,0)$、$B(s,0)$ となるように座標を置く。$A$ を中心とする半径 $AB$ の円と、$B$ を中心とする半径 $AB$ の円は
$$ (x+s)^2+y^2=4s^2,\qquad (x-s)^2+y^2=4s^2 $$
である。2 式を引くと $(x+s)^2-(x-s)^2=4sx=0$ なので $x=0$ である。1 つ目の式に入れて $s^2+y^2=4s^2$、$y=\pm\sqrt3\,s$ となる。交点 $C(0,\sqrt3 s)$、$D(0,-\sqrt3 s)$ は作図できる点であり、直線 $CD$ は $y$ 軸である。$y$ 軸は $AB$ の中点 $(0,0)$ を通り $AB$ に垂直なので、$AB$ の垂直二等分線である。中点は直線 $AB$ と直線 $CD$ の交点として作図できる。
段 2（2 の証明、$P$ が $\ell$ の上にないとき）。$\ell$ を定める作図済みの点のうち 1 つを $Q$ とする。$P$ を中心とする半径 $PQ$ の円を描く。この円と $\ell$ の交点は $Q$ のほかにもう 1 つ $Q'$ があるか、$Q$ だけかのどちらかである。

• $Q'\ne Q$ があるとき：$PQ=PQ'$ なので、$P$ は線分 $QQ'$ の両端から等距離にある。線分の両端から等距離にある点は垂直二等分線の上にある（$QQ'$ を $x$ 軸の上に $Q(-s,0)$、$Q'(s,0)$ と置くと、$(x+s)^2+y^2=(x-s)^2+y^2$ から $x=0$）。よって段 1 で引いた $QQ'$ の垂直二等分線は $P$ を通り、$\ell$ に垂直である。
• 交点が $Q$ だけのとき：円は $\ell$ に $Q$ で接している。接線は接点を通る半径に垂直なので（円と直線の位置関係）、直線 $PQ$ が $\ell$ に垂直である。
  段 3（2 の証明、$P$ が $\ell$ の上にあるとき）。$\ell$ の上の作図済みの点で $P$ と異なるもの $Q$ をとる（$\ell$ を定める 2 点のうち、少なくとも一方は $P$ と異なる）。$P$ を中心とする半径 $PQ$ の円は $\ell$ と $Q$ と、$P$ について $Q$ と反対側の点 $Q''$ で交わる。$P$ は線分 $QQ''$ の中点なので、段 1 の $QQ''$ の垂直二等分線が $P$ を通り $\ell$ に垂直な直線である。
  段 4（3 の証明）。2 により、$P$ を通り $\ell$ に垂直な直線 $m$ が引ける。$m$ は作図できる 2 点を通る。もう一度 2 を使い、$P$ を通り $m$ に垂直な直線 $n$ を引く。$n$ と $\ell$ はどちらも $m$ に垂直なので平行である。$\square$

段 1（点から座標へ）。$(x,y)$ が作図できるとする。lem-rcc-basic の 2 により、$(x,y)$ を通り $x$ 軸に垂直な直線が引け、$x$ 軸との交点 $(x,0)$ が作図できる。同じように $y$ 軸に垂直な直線と $y$ 軸の交点 $(0,y)$ が作図できる。$O$ を中心とし $O$ と $(0,y)$ の距離 $|y|$ を半径とする円は、$x$ 軸と $(y,0)$、$(-y,0)$ で交わる。よって $x$、$y$ は作図できる数である。
段 2（座標から点へ）。$x$、$y$ が作図できるとする。$O$ を中心とする半径 $|y|$ の円と $y$ 軸の交点として $(0,y)$ が作図できる。$(x,0)$ を通り $x$ 軸に垂直な直線と、$(0,y)$ を通り $y$ 軸に垂直な直線を引くと、その交点が $(x,y)$ である。$\square$

方針：和と差はコンパスで長さを継ぎ足す。積と商は平行線でできる相似な三角形を使う。平方根は、直径の上に立てた垂線の長さを使う。
段 1（和と差）。$b=0$ なら $a\pm b=a$ なので、$b\ne0$ とする。$(a,0)$ を中心とし、$O$ と $(b,0)$ の距離 $|b|$ を半径とする円を描く。この円は $x$ 軸と $(a+|b|,0)$、$(a-|b|,0)$ で交わる。$b\ge0$ でも $b<0$ でも、この 2 点は $(a+b,0)$ と $(a-b,0)$ である。
段 2（積）。$a=0$ または $b=0$ なら $ab=0$ は作図できる。$-a$、$-b$ も作図できるので（def-rcc-number の後の注意）、$a>0$、$b>0$ の場合に示せば、符号を付けかえて一般の場合が得られる。lem-rcc-coordinates により $A(0,a)$ と $B(b,0)$ は作図できる。直線 $EA$ を引き、lem-rcc-basic の 3 により $B$ を通って $EA$ に平行な直線を引く。この直線と $y$ 軸の交点を $P$ とする。三角形 $OEA$ と三角形 $OBP$ は、$O$ の角が共通の直角で、$EA\parallel BP$ より同位角 $\angle OEA=\angle OBP$ が等しいので相似である（三角形の相似条件）。対応する辺の比から
$$ \frac{OP}{OA}=\frac{OB}{OE},\qquad OP=OA\cdot\frac{OB}{OE}=a\cdot\frac b1=ab $$
となる。$P=(0,ab)$ なので、lem-rcc-coordinates により $ab$ は作図できる。
段 3（商）。$a=0$ なら $\dfrac ab=0$ は作図できる。$a\ne0$ のときは、段 2 と同じく $a>0$、$b>0$ としてよい。直線 $BA$ を引き、$E$ を通って $BA$ に平行な直線と $y$ 軸の交点を $Q$ とする。三角形 $OBA$ と三角形 $OEQ$ は相似なので
$$ \frac{OQ}{OA}=\frac{OE}{OB},\qquad OQ=a\cdot\frac1b=\frac ab $$
である。よって $\dfrac ab$ は作図できる。
段 4（平方根）。$a>0$ とする。$P(-1,0)$ と $A(a,0)$ は作図できるので、線分 $PA$ の中点 $C\left(\dfrac{a-1}2,0\right)$ が作図できる（lem-rcc-basic の 1）。$C$ を中心とし、半径 $CA=\dfrac{a+1}2$ の円（$PA$ を直径とする円）を描き、$y$ 軸との交点を $H(0,h)$（$h>0$）とする。$H$ は円の上にあるので
$$ \left(0-\frac{a-1}2\right)^2+h^2=\left(\frac{a+1}2\right)^2 $$
である。整理すると
$$ h^2=\frac{(a+1)^2-(a-1)^2}{4}=\frac{4a}4=a $$
なので $h=\sqrt a$ である。$H$ から $\sqrt a$ が作図できる（lem-rcc-coordinates）。$\square$

方針：「$\sqrt d$ は $F$ に入らない」という仮定を、分母が $0$ にならないことと、書き方がただ 1 通りであることに使う。
段 1（1 の証明）。$q\ne q'$ とすると、$p+q\sqrt d=p'+q'\sqrt d$ を $\sqrt d$ について解いて
$$ \sqrt d=\frac{p-p'}{q'-q} $$
となる。右辺は $F$ の数どうしの差と商なので $F$ に入る。これは $\sqrt d$ が $F$ に入らないことに反する。よって $q=q'$ であり、そのとき $p=p'$ である。
段 2（和・差・積）。$p,q,p',q'\in F$ について
$$ (p+q\sqrt d)\pm(p'+q'\sqrt d)=(p\pm p')+(q\pm q')\sqrt d, $$
$$ (p+q\sqrt d)(p'+q'\sqrt d)=(pp'+qq'd)+(pq'+qp')\sqrt d $$
である。$F$ は四則で閉じていて $d\in F$ なので、右辺の $\sqrt d$ の前後にある数はすべて $F$ に入る。
段 3（商）。$p+q\sqrt d\ne0$ とする。まず $p^2-q^2d\ne0$ を示す。$q=0$ なら $p\ne0$ なので $p^2-q^2d=p^2\ne0$ である。$q\ne0$ で $p^2-q^2d=0$ なら $d=\left(\dfrac pq\right)^2$ となり、$\sqrt d=\left|\dfrac pq\right|$ が $F$ に入ってしまう。よって $p^2-q^2d\ne0$ である。そこで分母を有理化すると
$$ \frac{1}{p+q\sqrt d}=\frac{p-q\sqrt d}{(p+q\sqrt d)(p-q\sqrt d)}=\frac{p}{p^2-q^2d}+\frac{-q}{p^2-q^2d}\sqrt d $$
となり、これは $F(\sqrt d)$ に入る。一般の商は、この逆数と段 2 の積で書ける。
段 4（$F$ を含む）。$F$ の数 $p$ は $p+0\cdot\sqrt d$ と書けるので $F(\sqrt d)$ に入る。とくに $0,1$ を含む。$\square$

方針：直線は 1 次方程式、円は 2 次方程式で表される。交点を求めることは、係数が $F$ に入る連立方程式を解くことで、途中で解くのは高々 2 次方程式である。
段 1（直線と円の式）。座標が $F$ に入る 2 点 $(x_1,y_1)\ne(x_2,y_2)$ を通る直線は
$$ (y_2-y_1)(x-x_1)-(x_2-x_1)(y-y_1)=0 $$
である（直線の方程式と点と直線の距離）。展開すると $ax+by+c=0$ の形になり、$a,b,c$ は $F$ に入り、$a$、$b$ の少なくとも一方は $0$ でない。座標が $F$ に入る点 $(p,q)$ を中心とし、座標が $F$ に入る 2 点の距離 $r$ を半径とする円は $(x-p)^2+(y-q)^2=r^2$ である。$r^2$ は 2 点の座標の差の 2 乗の和なので $F$ に入る。展開すると
$$ x^2+y^2+ux+vy+w=0,\qquad u=-2p,\ v=-2q,\ w=p^2+q^2-r^2 $$
で、$u,v,w$ は $F$ に入る。
段 2（2 直線の交点）。$ax+by+c=0$ と $a'x+b'y+c'=0$ が 1 点で交わるとき、$ab'-a'b\ne0$ で、連立 1 次方程式を解くと
$$ x=\frac{bc'-b'c}{ab'-a'b},\qquad y=\frac{a'c-ac'}{ab'-a'b} $$
である。どちらも $F$ の数の四則で書けるので $F$ に入る。1 が成り立つ。
段 3（直線と円の交点）。直線 $ax+by+c=0$ で $b\ne0$ とする（$b=0$ なら $a\ne0$ なので、以下の $x$ と $y$ の役割を入れかえる）。$y=-\dfrac{ax+c}{b}$ を円の式に代入して分母を払うと、$x$ についての 2 次方程式
$$ Ax^2+Bx+C=0,\qquad A=a^2+b^2>0 $$
が得られ、$A,B,C$ は $F$ に入る。交点の $x$ 座標はこの方程式の実数解なので、判別式 $D=B^2-4AC$ は $0$ 以上であり（判別式（高校数学））、$D$ は $F$ に入る。解の公式から
$$ x=\frac{-B\pm\sqrt D}{2A} $$
である。$\sqrt D$ が $F$ に入れば $x$ は $F$ に入り、1 が成り立つ（$D=0$ のときも $\sqrt D=0$ なのでこの場合）。$\sqrt D$ が $F$ に入らなければ、$D>0$ であり、$x=\dfrac{-B}{2A}\pm\dfrac{1}{2A}\sqrt D$ は $F(\sqrt D)$ に入る。どちらの場合も $y=-\dfrac{ax+c}{b}$ は $x$ と同じ集まりに入る（lem-rcc-extension の 2）。
段 4（2 円の交点）。2 円 $x^2+y^2+ux+vy+w=0$、$x^2+y^2+u'x+v'y+w'=0$ の交点は、2 つの式の両方を満たす。2 つの式を引くと
$$ (u-u')x+(v-v')y+(w-w')=0 $$
となる。中心が同じなら $u=u'$、$v=v'$ で、相異なる 2 円なので $w\ne w'$ となり、この式を満たす点はない（同心の相異なる円は交わらない）。中心が違えば $(u-u',v-v')\ne(0,0)$ なので、これは係数が $F$ に入る直線の式である。2 円の交点は、この直線と 1 つ目の円の交点と一致する（2 円の式を満たすことと、引いた式と 1 つ目の式を満たすことは同じ）。よって段 3 に帰着する。この直線は 2 円の根軸であり、根軸と根心 で詳しく扱う。$\square$

方針：2 ⇒ 1 は thm-rcc-arithmetic を列にそって使う。1 ⇒ 2 は、作図の 1 手ごとに lem-rcc-intersection を使い、集まりの列を 1 段ずつ伸ばす。
段 1（2 ⇒ 1）。$F_i$ の数がすべて作図できることを、$i$ についての帰納法で示す。$i=0$：ex-rcc-first により正の整数は作図でき、$0$ と負の整数も作図できる（def-rcc-number の後の注意）。整数どうしの商も thm-rcc-arithmetic により作図できるので、有理数はすべて作図できる。$i-1$ で正しいとする。$d_i$ は $F_{i-1}$ の正の数なので作図でき、thm-rcc-arithmetic により $\sqrt{d_i}$ も作図できる。$F_i$ の数 $p+q\sqrt{d_i}$（$p,q\in F_{i-1}$）は、作図できる数の積と和なので作図できる。よって $F_r$ に入る $a$ は作図できる。
段 2（1 ⇒ 2 の準備）。$a$ が作図できるとし、def-rcc-point の手順で作図済みの点が $P_1=O$、$P_2=E$、$P_3$、…、$P_n=(a,0)$ の順に得られたとする。次の主張を $k$ についての帰納法で示す。
主張：列 $\mathbb{Q}=F_0\subset\cdots\subset F_{r_k}$（各段は def-rcc-adjoin の形）で、$P_1,\dots,P_k$ の座標がすべて $F_{r_k}$ に入るものがある。
段 3（帰納法）。$k=2$：$O$、$E$ の座標は $0$、$1$ なので $\mathbb{Q}=F_0$ に入る（$r_2=0$）。$k-1$ で主張が正しいとし、$F:=F_{r_{k-1}}$ とおく。$P_k$ は、座標が $F$ に入る点 $P_1,\dots,P_{k-1}$ から引いた直線と円のうち相異なる 2 つの交点である。lem-rcc-intersection により、$P_k$ の座標は $F$ に入るか、ある $F(\sqrt D)$ に入る。前者なら同じ列のままで（$r_k=r_{k-1}$）、後者なら列の最後に $F(\sqrt D)$ を付け加える（$r_k=r_{k-1}+1$）。どちらでも $P_1,\dots,P_k$ の座標は列の最後の集まりに入る（$F\subset F(\sqrt D)$ なので、前の点の座標も入る）。
段 4（結論）。$k=n$ とすると、$P_n=(a,0)$ の $x$ 座標 $a$ は列の最後の集まりに入る。これが 2 である。$\square$

thm-rcc-characterization の 1 ⇒ 2 の対偶である。$\square$

段 1（作図できること）。thm-rcc-arithmetic により $\sqrt2$ と $\sqrt3$ はどちらも作図でき、その和も作図できる。
段 2（列を作る）。$F_1=\mathbb{Q}(\sqrt2)$ とする。$\sqrt2$ は無理数なので（実数とは何か：無理数の証明）、$\sqrt2$ は $\mathbb{Q}$ に入らず、これは def-rcc-adjoin の形である。次に $\sqrt3$ が $F_1$ に入らないことを示す。$\sqrt3=p+q\sqrt2$（$p,q$ は有理数）と書けたとすると、両辺を 2 乗して
$$ 3=p^2+2q^2+2pq\sqrt2 $$
となる。lem-rcc-extension の 1（書き方はただ 1 通り）により、$2pq=0$ かつ $p^2+2q^2=3$ である。

• $q=0$ なら $p^2=3$ となるが、$\sqrt3$ は無理数なので、これを満たす有理数 $p$ はない。
• $p=0$ なら $2q^2=3$、つまり $(2q)^2=6$ となるが、$\sqrt6$ も無理数なので、これを満たす有理数 $q$ はない。
  どちらも矛盾なので、$\sqrt3$ は $F_1$ に入らない。そこで $F_2=F_1(\sqrt3)$ とおくと、$\mathbb{Q}=F_0\subset F_1\subset F_2$ は thm-rcc-characterization の形の列で、$\sqrt2+\sqrt3=0+1\cdot\sqrt3+\sqrt2$ は $F_2$ に入る（$\sqrt2\in F_1\subset F_2$、$\sqrt3\in F_2$ で、$F_2$ は和で閉じる）。$\square$