C.29.1:5.4 - Return a rational result from a real-number construction

A calculation accepts positive rational settings x and needs |x² − 2| ≤ 0.01. If a rational candidate is already supplied, substituting it can settle this question. The following construction uses an available positive real root of x² = 2 to obtain a rational candidate.

The inclusion of the rationals in the reals retains their equality, order, addition and multiplication. The larger domain also contains limits of rational sequences that have no rational limit. This supplies new mathematical objects without merging distinct rational inputs. The needed return is still a rational setting satisfying the original inequality.

Compute rational bounds:

1.414² = 1.999396 < 2
1.415² = 2.002225 > 2

Squaring is increasing on the positive reals, so the root lies between those endpoints. Choose the rational setting x = 1.414 and check the requested result: |x² − 2| = 0.000604 ≤ 0.01. The returned setting and its error calculation answer the original question. C.29.2 develops a procedure when obtaining such bounds requires one.

Now change the requirement to a rational setting with x² = 2. Suppose x = p/q is in lowest terms, with integers p and nonzero q. Then p² = 2q², so p is even. Substituting p = 2r shows that q is also even, contradicting lowest terms. The real root therefore has no rational counterpart. Return that obstruction; the requester can retain a tolerance or change the allowed number domain.

The extension supports a useful approximation and an existence argument in the larger domain. Which result can be returned depends on the requested property and the allowed source settings.