%
\label{thm:parallel-postulate}
Let $\ell$ be a line in $\tau^3$
and $p \in \tau^3 \setminus \ell$.
There exists a unique line $\ell'$ through~$p$
with $\ell' \cap \ell = \varnothing$.

Fix $a, b \in \ell$ with $a \neq b$.

\smallskip
\noindent\textbf{Step 1: Separation.}
Since $p \notin \ell$, Hausdorff separation
(Chapter~\ref{ch:cylinder-domains})
gives a stage $k_1$ with
$\pi_{k_1}(p) \notin \pi_{k_1}(\ell)$.

\smallskip
\noindent\textbf{Step 2: Unique parallel at each stage.}
For $k \geq k_1$, the CRT decomposition
$\mathbb{Z}/P_k \cong \prod_{i=1}^k \mathbb{Z}/p_i$
gives a product of prime-order affine spaces.
In each factor $\mathbb{Z}/p_i$
(a 1-dimensional affine space over $\mathbb{F}_{p_i}$),
the parallel through $\pi_k(p)$ is unique.
Call the product parallel $\ell_k'$.

\smallskip
\noindent\textbf{Step 3: Coherence.}
For $k < l$, the reduction $\pi_{k,l}(\ell_l')$
coincides with $\ell_k'$:
reduction maps preserve betweenness
and uniqueness at each stage
forces compatibility.

\smallskip
\noindent\textbf{Step 4: Inverse-limit assembly.}
The coherent family defines
\[
    \ell' \;=\; \varprojlim_k \ell_k'
    \;=\;
    \bigl\{\, x \in \tau^3
    \;\big|\;
    \pi_k(x) \in \ell_k'
    \text{ for all } k \geq k_1 \,\bigr\}.
\]
By construction, $p \in \ell'$
and $\ell' \cap \ell = \varnothing$
(cylinder separation lifts to the limit).

\smallskip
\noindent\textbf{Step 5: Uniqueness.}
If $\ell''$ is another parallel through~$p$,
then $\pi_k(\ell'')$ is a parallel to $\pi_k(\ell)$
through $\pi_k(p)$ at each stage.
Step~2 uniqueness forces
$\pi_k(\ell'') = \ell_k' = \pi_k(\ell')$
for all~$k$, so $\ell'' = \ell'$.