There are many ways to construct the real numbers, some more positive than others. Dedekind cuts give one such positive construction. In the reals as we know them, $\sqrt{2}\cdot\sqrt{2}=2$ is immediate; in the Dedekind-cut construction, one must prove that every rational below $2$ appears in the product cut. The proof below does that, by a route far longer than the identity deserves. I wrote the bulk of this proof over Thanksgiving break as a bonus problem for my IBL class. Upon reflection, it was also a lesson that elegance in mathematics relies on having the right machinery in place: remove enough of that machinery, and seemingly simple proofs can require an ordeal like the one below. At the end of the day, though, I thought the argument was pretty cool, and Thanksgiving in Chicago was warmer when spent with my blackboards indoors.
Definition (Dedekind cut).
A subset $A\subseteq\mathbb{Q}$ is a cut if:
The set of all cuts is called $\mathbb{R}$. A cut is, intuitively, the set of all rationals strictly below some real number, the number itself being exactly the cut. In particular,
$$ \sqrt{2} := \{x\in\mathbb{Q}\mid x<0\} \cup \{x\in\mathbb{Q}\mid x^2<2\}, \qquad \mathbf{2} := \{x\in\mathbb{Q}\mid x<2\}. $$
Definition (Multiplication of cuts).
You cannot multiply two cuts elementwise: each cut contains arbitrarily negative rationals, and products of large negatives would escape upward. So for cuts $A,B$ containing positive elements, we define
$$ A\otimes B = \{r\in\mathbb{Q}\mid r\le 0\} \cup \{ab\mid a\in A,\ b\in B,\ a>0,\ b>0\}. $$
We glue in the entire negative tail for free and multiply only positive representatives. Other sign cases are defined by $A\otimes B=-[(-A)\otimes B]$, and similarly for the remaining possibilities; they do not concern us here.
Lemma ($\mathbb{Q}$ is an ordered field).
Multiplying both sides of an inequality of rationals by a positive rational preserves the inequality.
We wish to prove the following.
Lemma.
$$ \sqrt{2}\otimes\sqrt{2} = \{x\in\mathbb{Q}\mid x<2\}. $$
Proof.
We first show that
$$ \sqrt{2}\otimes\sqrt{2} \subseteq \{x\in\mathbb{Q}\mid x<2\}. $$
By the definition of $\otimes$,
$$ \sqrt{2}\otimes\sqrt{2} = \{r\in\mathbb{Q}\mid r\leq 0\} \cup \{ab\mid a\in\sqrt{2},\ b\in\sqrt{2},\ a>0,\ b>0\}. $$
Recall that
$$ \sqrt{2} = \{x\in\mathbb{Q}\mid x<0\lor x^2<2\}. $$
For every $x\in\sqrt{2}$ such that $x>0$, the definition of this set gives $x^2<2$. Hence
$$ \sqrt{2}\otimes\sqrt{2} = \{r\in\mathbb{Q}\mid r\leq 0\} \cup \{ab\mid a^2<2,\ b^2<2,\ a>0,\ b>0\}. $$
Consider any $a,b\in\mathbb{Q}$ such that $a^2<2$, $b^2<2$, and $a,b>0$. Multiplying the first inequality by $b^2>0$ and the second by $2$ gives
$$ a^2b^2<2b^2 \qquad\text{and}\qquad 2b^2<2\cdot 2. $$
Therefore,
$$ a^2b^2<2^2 \implies (ab)^2<2^2 \implies ab<2, $$
where the last implication follows because $ab$ and $2$ are both positive. Thus every element of
$$ \{ab\mid a^2<2,\ b^2<2,\ a>0,\ b>0\} $$
is less than $2$. Hence
$$ \sqrt{2}\otimes\sqrt{2} \subseteq \{r\in\mathbb{Q}\mid r\leq 0\} \cup \{ab\mid ab<2,\ a>0,\ b>0\}, $$
which is the same as
$$ \sqrt{2}\otimes\sqrt{2} \subseteq \{x\in\mathbb{Q}\mid x\leq 0\lor(x<2\land x>0)\}, $$
and therefore
$$ \sqrt{2}\otimes\sqrt{2} \subseteq \{x\in\mathbb{Q}\mid x<2\}. $$
This completes the first set inclusion.
We now show that
$$ \{x\in\mathbb{Q}\mid x<2\} \subseteq \sqrt{2}\otimes\sqrt{2}. $$
By the same rewriting as above, we want to prove
$$ \{x\in\mathbb{Q}\mid x\leq 0\} \cup \{x\in\mathbb{Q}\mid 0<x<2\} \subseteq \{x\in\mathbb{Q}\mid x\leq 0\} \cup \{ab\mid a^2<2,\ b^2<2,\ a>0,\ b>0\}. $$
This reduces to
$$ \{x\in\mathbb{Q}\mid 0<x<2\} \subseteq \{ab\mid a^2<2,\ b^2<2,\ a>0,\ b>0\}. $$
Thus, given any $x\in\mathbb{Q}$ with $0<x<2$, we must find $a,b\in\mathbb{Q}$ such that
$$ ab=x, \qquad a^2<2, \qquad b^2<2. $$
In other words, every rational below $2$ must be exhibited explicitly as a product of two rationals whose squares remain below $2$.
We first prove the existence of $a$, then choose $b$ from $a$.
Write $x=\frac{a}{b}$ in lowest terms, where $a,b\in\mathbb{N}$. We want to show that there exist $p,q\in\mathbb{N}$ such that
$$ \frac{a}{b} < \frac{p^2}{q^2} < 2. $$
For some $k\in\mathbb{N}$, set
$$ q=b\cdot 2^k. $$
It is then enough to find $p\in\mathbb{N}$ such that
$$ ab\cdot 2^{2k} < p^2 < 2b^2\cdot 2^{2k}. $$
Consider the spacing of perfect squares. For any $m\in\mathbb{N}$,
$$ (m+1)^2-m^2=2m+1. $$
For any positive $m\in\mathbb{N}$, define
$$ \lfloor\sqrt{m}\rfloor = \max\{l\in\mathbb{N}\mid l^2\le m\}, \qquad \lceil\sqrt{m}\rceil = \min\{l\in\mathbb{N}\mid l^2\ge m\}. $$
The first set is nonempty and finite, and the second is nonempty, so these quantities are well-defined by the well-ordering of $\mathbb{N}$.
Hence the first perfect square strictly greater than $ab\cdot 2^{2k}$ is
$$ \left( \lfloor\sqrt{ab\cdot 2^{2k}}\rfloor+1 \right)^2 = \lfloor\sqrt{ab\cdot 2^{2k}}\rfloor^2 + 2\lfloor\sqrt{ab\cdot 2^{2k}}\rfloor + 1. $$
We want to choose $k$ so that
$$ \lfloor\sqrt{ab\cdot 2^{2k}}\rfloor^2 + 2\lfloor\sqrt{ab\cdot 2^{2k}}\rfloor + 1 < 2b^2\cdot 2^{2k}. $$
We now eliminate the floor and square-root functions by bounding them. First, for any $m\in\mathbb{N}$,
$$ \lfloor\sqrt{m}\rfloor^2\leq m, $$
and hence
$$ \lfloor\sqrt{ab\cdot 2^{2k}}\rfloor^2 \leq ab\cdot 2^{2k}. $$
Second, for any positive $m\in\mathbb{N}$, the definition of $\lceil\sqrt{m}\rceil$ gives
$$ m\cdot 2^{2k} \leq \left( \lceil\sqrt{m}\rceil\cdot 2^k \right)^2, $$
and hence
$$ \lfloor\sqrt{m\cdot 2^{2k}}\rfloor \leq \lceil\sqrt{m}\rceil\cdot 2^k. $$
Therefore,
$$ 2\lfloor\sqrt{ab\cdot 2^{2k}}\rfloor < 2^{k+1}\lceil\sqrt{ab}\rceil+2. $$
Combining the two bounds gives
$$ \lfloor\sqrt{ab\cdot 2^{2k}}\rfloor^2 + 2\lfloor\sqrt{ab\cdot 2^{2k}}\rfloor + 1 < ab\cdot 2^{2k} + 2^{k+1}\lceil\sqrt{ab}\rceil + 3. $$
So it suffices to show that for some $k\in\mathbb{N}$,
$$ \begin{aligned} ab\cdot 2^{2k} + 2^{k+1}\lceil\sqrt{ab}\rceil + 3 &< 2b^2\cdot 2^{2k}, \\ 2^{k+1}\lceil\sqrt{ab}\rceil+3 &< (2b^2-ab)\cdot 2^{2k}. \end{aligned} $$
A sufficient condition is
$$ \lceil\sqrt{ab}\rceil+3 < (2b^2-ab)\cdot 2^{k-1}, $$
using
$$ 2^{k+1}\lceil\sqrt{ab}\rceil+3 \leq 2^{k+1}\left(\lceil\sqrt{ab}\rceil+3\right) $$
and dividing by $2^{k+1}$.
Since $\frac{a}{b}<2$, we have
$$ 2b^2-ab\geq 1. $$
It is therefore enough to find $k$ such that
$$ \lceil\sqrt{ab}\rceil+3 < 2^{k-1}. $$
We know that $\lceil\sqrt{ab}\rceil+3\in\mathbb{N}$. Abstractly, given $m\in\mathbb{N}$, we must find $k\in\mathbb{N}$ such that
$$ m<2^{k-1}. $$
Let $k=m+2$. Then
$$ m<2^{m+1}=2^{k-1} $$
for every $m\in\mathbb{N}$.
Hence, for any $a,b\in\mathbb{N}$ with
$$ 0<\frac{a}{b}<2, $$
taking
$$ k=\lceil\sqrt{ab}\rceil+5 $$
gives
$$ \lfloor\sqrt{ab\cdot 2^{2k}}\rfloor^2 + 2\lfloor\sqrt{ab\cdot 2^{2k}}\rfloor + 1 < 2b^2\cdot 2^{2k}. $$
Recall that we want $p,q\in\mathbb{N}$ such that
$$ \frac{a}{b} < \frac{p^2}{q^2} < 2. $$
Let
$$ p^2 = \lfloor\sqrt{ab\cdot 2^{2k}}\rfloor^2 + 2\lfloor\sqrt{ab\cdot 2^{2k}}\rfloor + 1 $$
and
$$ q^2=b^2\cdot 2^{2k}. $$
Equivalently,
$$ p = \lfloor\sqrt{ab\cdot 2^{2k}}\rfloor+1, \qquad q=b\cdot 2^k. $$
Set
$$ \alpha=\frac{p}{q}. $$
This proves that there exists $\alpha\in\mathbb{Q}$ such that
$$ x<\alpha^2<2. $$
Now consider $\frac{x}{\alpha}$. If
$$ \left(\frac{x}{\alpha}\right)^2\geq x, $$
then
$$ \alpha^2\left(\frac{x}{\alpha}\right)^2 \geq \alpha^2x > x\cdot x = x^2. $$
But the left-hand side equals $x^2$, giving $x^2>x^2$, a contradiction. Thus
$$ \left(\frac{x}{\alpha}\right)^2 < x < 2. $$
Let
$$ \beta=\frac{x}{\alpha}. $$
We have selected $\alpha,\beta>0$ such that
$$ \beta^2<x<\alpha^2<2 \qquad\text{and}\qquad \alpha\beta=x. $$
Therefore, for every $x\in\mathbb{Q}$ with $0<x<2$, there exist $a,b\in\mathbb{Q}$ such that
$$ ab=x, \qquad a^2<2, \qquad b^2<2. $$
This proves
$$ \{x\in\mathbb{Q}\mid 0<x<2\} \subseteq \{ab\mid a^2<2,\ b^2<2,\ a>0,\ b>0\}, $$
and hence
$$ \{x\in\mathbb{Q}\mid x<2\} \subseteq \sqrt{2}\otimes\sqrt{2}. $$
Having proved both inclusions, we conclude that
$$ \sqrt{2}\otimes\sqrt{2} = \{x\in\mathbb{Q}\mid x<2\}. $$
This completes the proof. $\square$