Division is defined as multiplying by the reciprocal:
¥ x/y †p = x·(/y †p)
(The †p indicates a proof of y <> 0).

Since multiplication and the reciprocal are compatible with equality, so is division:
¥ If x1 = x2 and y1 = y2, and p1 and p2 prove y1 <> 0 and y2 <> 0 respectively, then x1 / y1 †p1 = x2 / y2 †p2.
Suppose x1 = x2 and y1 = y2. Then /y1 †p1 = /y2 †p2. Therefore x1 / y1 †p1 = x1 · (/y1 †p1) = x2 · (/y2 †p2) = x2 / y2 †p2.

A quick lemma to help with automated proofs:
¥ If r ∈ x[k] and s ∈ y[max{k, find_zeroless(y, p)}], then r/s ∈ (x/y †p)[k].
If s ∈ y[max{k, find_zeroless(y, p)}], we have /s ∈ (x/y †p)[k]. Given this and r ∈ x[k], we have r/s = r·(/s) ∈ (x·(/y †p))[k] = (x/y †p)[k].

Division is the inverse of multiplication. A few ways of stating this:
¥ If y <> 0, (x · y) / y = x.
¥ If y <> 0, (x / y) · y = x.
These can be proven automatically.

Another way to say this:
¥ If y <> 0, x / y = z if and only if x = z · y.
1. Suppose x / y = z. Then x = (x / y) · y = z · y.
2. Suppose x = z · y. Then x / y = (z · y) / y = z.

You can divide both sides of an inequality by a positive number. Dividing both sides by a negative number reverses the direction of the inequality.
¥ If z > 0, then x < y if and only if x / z < y / z.
¥ If z > 0, then x ≤ y if and only if x / z ≤ y / z.
¥ If z < 0, then x < y if and only if x / z > y / z.
¥ If z < 0, then x ≤ y if and only if x / z ≥ y / z.
These follow trivially from the related theorems about multiplication, and the fact that the reciprocal of a positive number is positive, and the reciprocal of a negative number is negative.

Next is completeness.

>>9512
Hope you don't mind waiting a while, but I think I need a bit of time before I can digest and make a proper response to anything math.

>>9512
>What would be a good way to make these numbers easily available for people here to play around with them?
I really don't know anything about programming, but an interactive website like you mentioned is probably the best way. This stuff is way over my head and I'm a visual/interactive learning person.
Math... we must destroy it.

>>9514
No rush, it will probably be a bit before I work on this. I'm going to start proving stuff about completeness next, and I'll probably write the programs to convert to and from decimal representations as part of that. I think these theorems are going to be more interesting than proving elementary properties of the basic arithmetic operations.

There are several versions of the completeness axiom for the real numbers. Probably the most commonly used one is the supremum property, also known as the least-upper-bound property or Dedekind completeness. I talked about this axiom in >>9492, and it's the only one on the list I haven't proven yet.

There's a fun paper called "Real Analysis in Reverse" which examines lots of different properties of the real numbers, and talks about which ones, taken together with the ordered field axioms (every axiom in >>9492 except the last one, or in other words, most of what you learned in high school algebra), imply the supremum property, and which ones don't.
https://arxiv.org/abs/1204.4483

The author suggests treating the paper as a series of puzzles:
>It’s been fun for me to write this article, and I have a concrete suggestion for how the reader may have the same kind of fun. Start by reading the second section and trying to decide on your own which of the properties are equivalent to completeness and which aren’t. If you’re stumped in some cases, and suspect but cannot prove that some particular properties aren’t equivalent to completeness, read the third section to see if any of the ordered fields discussed there provide a way to see the inequivalence. And if you’re still stumped, read the fourth section. You can treat the article as a collection of math puzzles, some (but not all) of which can be profitably contemplated in your head.

You may want to try them out for yourself. Here's the list of properties from the paper (you may want to read them in the paper itself, where the typesetting will be better):
>(1) The Dedekind Completeness Property: Suppose S is a nonempty subset of R that is bounded above. Then there exists a number c that is an upper bound of S such that every upper bound of S is greater than or equal to c.
>(2) The Archimedean Property: For every x ∈ R there exists n ∈ N with n > x. Equivalently, for every x ∈ R with x > 0 there exists n ∈ N with 1/n < x.
>(3) The Cut Property: Suppose A and B are nonempty disjoint subsets of R whose union is all of R, such that every element of A is less than every element of B. Then there exists a cutpoint c ∈ R such that every x < c is in A and every x > c is in B . (Or, if you prefer: Every x ∈ A is ≤ c, and every x ∈ B is ≥ c. It’s easy to check that the two versions are equivalent.) Since this property may be unfamiliar, we remark that the Cut Property follows immediately from Dedekind completeness (take c to be the least upper bound of A).
>(4) Topological Connectedness: Say S ⊆ R is open if for every x in S there exists ϵ > 0 so that every y with |y−x| < ϵ is also in S. Then there is no way to express R as a union of two disjoint nonempty open sets. That is, if R = A ∪ B with A, B nonempty and open, then A ∩ B is nonempty.
>(5) The Intermediate Value Property: If f is a continuous function from [a, b] to R, with f(a) < 0 and f(b) > 0, then there exists c in (a, b) with f(c) = 0.
>(6) The Bounded Value Property: If f is a continuous function from [a, b] to R, there exists B in R with f(x) ≤ B for all x in [a, b].
>(7) The Extreme Value Property: If f is a continuous function from [a, b] to R, there exists c in [a, b] with f(x) ≤ f(c) for all x in [a, b].
>(8) The Mean Value Property: Suppose f : [a, b] → R is continuous on [a, b] and differentiable on (a, b). Then there exists c in (a, b) such that f′(c) = (f(b)−f(a))/(b−a).
>(9) The Constant Value Property: Suppose f : [a, b] → R is continuous on [a, b] and differentiable on (a, b), with f′(x) = 0 for all x in (a, b). Then f(x) is constant on [a, b].
>(10) The Convergence of Bounded Monotone Sequences: Every monotone increasing (or decreasing) sequence in R that is bounded converges to some limit.
>(11) The Convergence of Cauchy Sequences: Every Cauchy sequence in R is convergent.
>(12) The Fixed Point Property for Closed Bounded Intervals: Suppose f is a continuous map from [a, b] ⊂ R to itself. Then there exists x in [a, b] such that f(x) = x.
>(13) The Contraction Map Property: Suppose f is a map from R to itself such that for some constant c < 1, |f(x)−f(y)| ≤ c|x−y| for all x, y. Then there exists x in R such that f(x) = x.
>(14) The Alternating Series Test: If a₁ ≥ a₂ ≥ a₃ ≥ ... and a_n → 0, then ∑_{n=1}^∞ (−1)ⁿ a_n converges.
>(15) The Absolute Convergence Property: If ∑_{n=1}^∞ |a_n| converges in R, then ∑_{n=1}^∞ a_n converges in R.
>(16) The Ratio Test: If | a_{n+1} / a_n | → L in R as n → ∞, with L < 1, then ∑_{n=1}^∞ a_n converges in R.
>(17) The Shrinking Interval Property: Suppose I₁ ⊇ I₂ ⊇ ... are bounded closed intervals in R with lengths decreasing to 0. Then the intersection of the I_n’s is nonempty.
>(18) The Nested Interval Property: Suppose I₁ ⊇ I₂ ⊇ ... are bounded closed intervals in R. Then the intersection of the I_n’s is nonempty.

Some of these imply the supremum property, and some don't. And sometimes two of the properties taken individually don't imply the supremum property, but do imply it when taken together.

The particular properties I'm planning to talk about over the next few posts are (1), (2), (3), (11), and (17).

>>9526
Let's start by proving the Archimedean property.

But first we'll need to be able to convert between various number types. Let's follow the pattern of Q2R in denoting the conversion functions. These already exist in the Coq standard library (although not by the name we're giving them here):
¥ N2Z converts natural numbers to integers
¥ Z2Q converts integers to rational numbers
¥ Z2N converts integers to natural numbers (The result for negative numbers is unspecified. As implemented, it's 0, but we should avoid relying on that.)
We can easily define the additional functions N2Q, N2R, and Z2R by combining these and our own Q2R.

With that done, we now prove the Archimedean property:
¥ For every real number x, there is a natural number n such that N2R(n) > x.
This proof is pretty simple. Because of the way we represent real numbers, we already have a series of rational upper bounds for x. So we can just take the first upper bound and use the first natural number integer greater than it. To be specific, let
n = Z2N(max{Qfloor(max(x[0])) + 1, 0})
where Qfloor is a function (from the standard libary) which for a given rational number returns the greatest integer less than or equal to it. Note that max{Qfloor(max(x[0])) + 1, 0} ≥ 0. Then we have
N2R(n) = Z2R(N2Z(Z2N(max{Qfloor(max(x[0])) + 1, 0}))) = Z2R(max{Qfloor(max(x[0])) + 1, 0}) ≥ Z2R(Qfloor(max(x[0])) + 1) > Q2R(max(x[0])) ≥ x.

This has the important corollary:
¥ For every real number x, if x > 0, there is a natural number n such that /N2R(n) < x.
(Recall that we use /x to denote the reciprocal of x.)
Since x > 0, /x is defined and is also > 0. By the previous theorem, there is an n such that N2R(n) > /x. Since N2R(n) > /x > 0, we have /N2R(n) < //x = x.

>>9526
Next up:
>(17) The Shrinking Interval Property: Suppose I₁ ⊇ I₂ ⊇ ... are bounded closed intervals in R with lengths decreasing to 0. Then the intersection of the I_n’s is nonempty.

This is reminiscent of how we constructed our real numbers in the first place. The main difference is that in our construction of the real numbers, the endpoints of the intervals had to be rational numbers, but in this theorem, the endpoints are themselves real numbers.

Since we're trying to be constructive whenever possible, rather than just proving the existence of a number in the intersection, we'd like to have an algorithm to calculate it. Calculating the number, as usual, means computing a sequence of nested intervals with rational endpoints that converge to the right result, based on the sequences of intervals that represent the input numbers. The efficiency of the algorithm matters. We're going to be using it later on to compute infinite sums. I've personally gone through a few designs for this algorithm in my head, and I'll post my current design once it's implemented and proven.

You might be able to come up with something better than what I've got. How would you do it?

>>9533
Design 3 turned out not to work. I think design 4 will work though.

>>9533
Our input is a sequence of pairs of real numbers, representing upper and lower bounds. And we're representing the real numbers themselves as sequences of pairs of rational numbers, representing upper and lower bounds. So we have a sequence of pairs of sequences of pairs of rational numbers. And our output needs to be a sequence of pairs of rational numbers.

design 1
My first idea here was the simple idea of making a sequence where the kth output lower bound is the kth rational lower bound from the kth real lower bound, and the kth output upper bound is the kth rational upper bound from the kth real upper bound.

The problem is that while this gives us valid upper and lower bounds for the number, they don't necessarily converge. To see why, consider the sequence of real intervals

[0A, 0A], [0B, 0B], [0C, 0C], ...

where the 0A, 0B, 0C, ... are all different representations of the real number 0, with

0A = [-1/1, 1/1]Q, [-1/2, 1/2]Q, [-1/3, 1/3]Q, [-1/4, 1/4]Q, ...
0B = [-1/1, 1/1]Q, [-1/1, 1/1]Q, [-1/2, 1/2]Q, [-1/3, 1/3]Q, ...
0C = [-1/1, 1/1]Q, [-1/1, 1/1]Q, [-1/1, 1/1]Q, [-1/2, 1/2]Q, ...

Even though the interval sequences defining the real numbers converge to zero, and the sequence of real numbers converges to zero, if we merge them together with the simple recipe, we get the sequence

[-1/1, 1/1]Q, [-1/1, 1/1]Q, [-1/1, 1/1]Q, ...

which doesn't converge at all! So we'll have to do something a bit smarter.

>>9533
>>9535
design 2
An obvious modification to design 1 which ought to make it converge: Instead of just using the kth rational lower bound from the kth real lower bound, look at all the kth rational lower bounds from real lower bounds 0 through k and take the best (the largest). Similarly look at all the kth rational upper bounds from real upper bounds 0 through k and take the best (the smallest).

For the example from >>9535 that broke convergence for design 1, we get
¥ [-1/1, 1/1]Q, [-1/2, 1/2]Q, [-1/3, 1/3]Q, ...
converging to zero as desired.

It's a simple solution, but it feels like it might require us to do some needless work. Let's look at how it would perform in a concrete example. We'll try using nested real intervals to calculate tan⁻¹(√(1/2)).

One way to calculate √(1/2) is the simple method in >>8908. We can work out one decimal place at a time by squaring the candidate number and seeing if it comes out lower than 1/2. We get the following sequence:
¥ [0.7, 0.8]Q, [0.70, 0.71]Q, [0.707, 0.708]Q, [0.7071, 0.7072]Q, [0.70710, 0.70711]Q, ...

The arctangent function has the following power series, which converges when |x| ≤ 1:
¥ tan⁻¹(x) = x - x³/3 + x⁵/5 - x⁷/7 + x⁹/9 - x¹¹/11 + ...

A nice thing about this series is that it's an alternating series, meaning the terms we're adding are alternately positive and negative. This combined with the fact that the absolute value of the terms is decreasing means that each partial sum is a new bound on the number. So we immediately get the following nested interval representation for the case 0 ≤ x ≤ 1 (when -1 ≤ x ≤ 0, the intervals need to be in the other direction):
¥ tan⁻¹(x) = the number in the intersection of
¥ [x - x³/3, x],
¥ [x - x³/3, x - x³/3 + x⁵/5],
¥ [x - x³/3 + x⁵/5 - x⁷/7, x - x³/3 + x⁵/5],
¥ [x - x³/3 + x⁵/5 - x⁷/7, x - x³/3 + x⁵/5 - x⁷/7 + x⁹/9],
¥ [x - x³/3 + x⁵/5 - x⁷/7 + x⁹/9 - x¹¹/11, x - x³/3 + x⁵/5 - x⁷/7 + x⁹/9],
¥ ...

Note that to handle the case of irrational x, these need to be intervals with real number endpoints. So we'll have to use the algorithm we're writing to find it.

Let's start by working out the real numbers involved. With our existing algorithms for arithmetic operations we would get
¥ x = [0.7, 0.8]Q, [0.70, 0.71]Q, [0.707, 0.708]Q, [0.7071, 0.7072]Q, [0.70710, 0.70711]Q, ...
¥ x - x³/3 = [0.7 - 0.8³/3, 0.8 - 0.7³/3]Q, [0.70 - 0.71³/3, 0.71 - 0.70³/3]Q, [0.707 - 0.708³/3, 0.708 - 0.707³/3]Q, ...
¥ x - x³/3 + x⁵/5 = [0.7 - 0.8³/3 + 0.7⁵/5, 0.8 - 0.7³/3 + 0.8⁵/5]Q, [0.70 - 0.71³/3 + 0.70⁵/5, 0.71 - 0.70³/3 + 0.71⁵/5]Q, [0.707 - 0.708³/3 + 0.707⁵/5, 0.708 - 0.707³/3 + 0.708⁵/5]Q, ...
¥ x - x³/3 + x⁵/5 - x⁷/7 = [0.7 - 0.8³/3 + 0.7⁵/5 - 0.8⁷/7, 0.8 - 0.7³/3 + 0.8⁵/5 - 0.7⁷/7]Q, [0.70 - 0.71³/3 + 0.70⁵/5 - 0.71⁷/7, 0.71 - 0.70³/3 + 0.71⁵/5 - 0.70⁷/7]Q, [0.707 - 0.708³/3 + 0.707⁵/5 - 0.708⁷/7, 0.708 - 0.707³/3 + 0.708⁵/5 - 0.707⁷/7]Q, ...

Merging the bounds together with the design 2 algorithm, we get
¥ tan⁻¹(x) =
¥ [max{0.7 - 0.8³/3}, min{0.8}]Q,
¥ [max{0.70 - 0.71³/3, 0.70 - 0.71³/3}, min{0.71, 0.71 - 0.70³/3 + 0.71⁵/5}]Q,
¥ [max{0.707 - 0.708³/3, 0.707 - 0.708³/3, 0.707 - 0.708³/3 + 0.707⁵/5 - 0.708⁷/7}, min{0.708, 0.708 - 0.707³/3 + 0.708⁵/5, 0.708 - 0.707³/3 + 0.708⁵/5}]Q,
¥ ...

It's honestly not as bad as I thought it would be. On the one hand, we're clearly doing a lot of unnecessary comparisons. It's obvious in this case that the best bound out of each set that we're taking the max/min of will be the last bound. But I thought computing the extraneous bounds would require a lot of extra work, when in fact they can be computed with work we would have to do anyway. It's enough to make me consider implementing this simple algorithm instead of design 4. But before I do that, I'll write out design 4 so I can see if it's really that much more complex when I write out all the details.

design 3
Let m index the pairs of real number bounds, and let n index the pairs of rational number bounds that define each real number. At a particular m and n, you have four rational numbers. There are two real numbers, an upper bound and a lower bound, and at stage n each of those real numbers has a rational upper and lower bound.

The motivation: Notice that if we fix m and increase n, we get increasingly better bounds, but only up to a point. Unless the two real numbers are actually equal, eventually the lower bound on the upper bound becomes larger than the upper bound on the lower bound. This creates a limit on how close the upper bound on the upper bound and the lower bound on the lower bound can get to each other. If the next pair of real numbers (real number pair m+1) has upper bounds on the upper bound and lower bounds on the lower bound that are inside this gap, then the real number m is guaranteed to be no longer useful for computing better approximations to our target value. I've drawn a crude picture to try to explain what I mean.

The idea of design 3 was to increment n at each step, but only increment m if you encounter a situation like the one I just described. And at each such step, use the upper bound on the upper bound and the lower bound on the lower bound as rational bounds on the target value.

But I hadn't entirely thought this idea through, and after further thought I realized that the situation triggering an advance in m wasn't guaranteed to happen, even if real number pair m exhibited a gap preventing further progress. After some further thinking, I came to design 4, which I think will work.

design 4
This is pretty similar to the previous except with a different condition for triggering m to increment. This time, the trigger is when for real number pair m the gap between the lower bound on the upper bound and the upper bound on the lower bound is at least half the distance between the upper bound on the upper bound and lower bound on the lower bound. As before, we use the upper bound on the upper bound and the lower bound on the lower bound as bounds on the target value. A complication is that these bounds are not guaranteed to be nested, but that can be fixed by taking the minimum of all the upper bounds found so far, and the maximum of all the lower bounds found so far.

I think that since this version of the real numbers has been focused on simplicity, and the efficiency problems weren't as bad as I thought, I'm going to go with design 2 for now. I might look at design 4 again when I try for a more efficient version.

>>9462
I had another idea regarding signed digits. The digits could be written as something like

↓1, ↓2, ↓3, ↓4, ↓5, ↓6, ↓7, ↓8, ↓9, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9

with the ↓ representing -10. So for example 2.65000↓37 would be equal to 2.6499937.

You could also write it as a line through all the previous digits until you encounter a nonzero one, like 2.6500037. Since there's no ↓0 digit, there's no ambiguity here; you can tell the strikethrough is coming from the ↓3. This wouldn't work if the negative digit was the first nonzero digit, but in that case, you could just use a negative sign in front of the whole number and adjust how you write digits accordingly.

The nice thing about this is that it makes it easy to convert the result into standard form.

I'm thinking maybe I should start working on conversion to / from decimals earlier than I planned so I can have something for people to play around with as I talked about in >>9512.

In other news, some small bits of progress as I work on the proof of the nested interval theorem:

Proved some more missed theorems that ought to have proven earlier.
>>8977
>>9513
Proofs are by the usual automatic method.
¥ Q2R(r - s) = Q2R(r) - Q2R(s)
¥ If s <> 0 and Q2R(s) <> 0 by p, then Q2R (r / s) = Q2R(r) / Q2R(s) † p.

>>8920
A useful lemma about proving x < y:
¥ For any k1 and k2, if max(x[k1]) < min(y[k2]), then x < y.
Let k be the larger of k1 and k2. Then max(x[k]) ≤ max(x[k1]) < min(y[k2]) ≤ min(y[k]), proving x < y.

Also some progress on proof automation. Coq has some nice tactics called ring and field that can be used to automate reasoning about basic algebra, like proving (a - b) + (b - c) = a - c. To use them, you first have to prove the ring / field axioms (already done, although I had to reverse the direction of some equations), then declare the structure a ring / field to Coq. I had to use the less powerful ring option (which can't do stuff with division) for the technical reason that Coq's field tactic expects division to take only two numbers as arguments, whereas we have to feed in an additional proof that the denominator is nonzero.

>>6896
>If the number happens to be exactly one, it might even cause our program to get into an infinite loop.
But why though ?
Can you give a little explanation on what that is ?

>>9594
>Can you give a little explanation on what that is ?
Can you give a little explanation on why that is ?

>>9594
Because the number may be exactly 1 but we don't know if it's exactly 1. In order to output that first "1" digit instead of a "0" we need to compute the number to sufficient precision to know that it's not less than 1. But if the number happens to be exactly 1, infinite precision is required. We can't output "0." either, because the number could be slightly larger than 1, and in order to know this isn't the case, we need infinite precision.

To give a more concrete example, think about what happens when we first compute √2 and then square it. Computing √2 means being able to compute ever-better approximations to √2. With more computation, we can know that the value is between 1.4 and 1.5, between 1.41 and between 1.42, between 1.414 and 1.415, and so on. More computation means better precision. What does that tell us about the square of this number? First we know it's between 1.96 and 2.25, then we know it's between 1.9881 and 2.0164, then we know it's between 1.999396 and 2.002225. But we never have it precisely enough to know if it starts with 1.9 or with 2.0.

There might be a more rigorous proof using what I've learned are called "fugitive sequences." I've mentioned these before in >>8947 :
>Why do we expect not to be able to prove trichotomy constructively? Because that would mean that we have a way to compute for any given pair of real numbers whether or not they are equal. Confirming that two numbers are equal would in general require us to compute both numbers to infinite precision. To make the impossibility more clear, we could define a real number in decimal form as follows: It starts with 0.999 and the 9's go on until a given Turing machine halts. Is this number equal to 1? We can't know without solving the halting problem.
That said, I don't know the proof. Maybe solving >>9012 would help.

Here's an interesting paper I found about various ways people have found to construct the real numbers:
https://arxiv.org/pdf/1506.03467.pdf

The implementation I'm working on now is essentially the same as Bachmann's construction.

>>6896
>Cauchy sequences in their full generality feel a bit too complicated for my taste. It's possible the complexity at the beginning makes the implementation of stuff later on easier, though. But I'm going to try something else first.

I should say that after trying various things I appreciate the Cauchy sequence construction (actually due to Cantor, it turns out) a lot more. In particular the fact that you can define arithmetic operations simply by doing the operations termwise on the the input sequences is really nice.

Making the modulus of convergence explicit, which is necessary to actually compute the number, also reduces the apparent complexity of the Cauchy sequence construction a bit. To explain this a bit more: If I just look at a finite number of terms in a Cauchy sequence, I have no idea what the number is. You need an infinite number of terms to know what limit the sequence converges to, and you can't compute that. What you have to do instead is go to the proof that the sequence is Cauchy. If I have some precision ε > 0 which which I want to know the number, the proof (assuming it's constructive) gives me an N beyond which the terms in the sequence have to be less than ε apart from each other, and it can be proven that at that point in the sequence, you are no more than ε away from the limit. A modulus of convergence is an explicit function that takes ε and gives you the appropriate N. Suppose we call this function f. Instead of saying
> for every ε > 0 there exists an N such that for m,n > N, |x_m - x_n| < ε
we can just say
> for every ε > 0 and m,n > f(ε), |x_m - x_n| < ε
which, although it says the same thing, is potentially easier to wrap your head around because of the smaller number of nested quantifiers.

>>9540
Time for the formal proof that design 2 works.

First some new notation. We've been denoting the minimum and maximum of a closed interval [a, b] as min([a, b]) = a and max([a, b]) = b. Because we'll be working with sequences of intervals whose endpoints are also sequences of intervals, a notation that can be chained more cleanly will be helpful. So instead we'll use [a, b].min = a and [a, b].max = b.

We define the intersection of nested shrinking intervals of real numbers as
¥ nested_RI_int(I, p, q)[n] = [max{I[m].min[n].min | m ≤ n}, min{I[m].max[n].max | m ≤ n}]Q
where I is a sequence of bounded closed intervals with two real numbers as endpoints,
where p is a proof that the intervals are nested, meaning
¥ k2 ≥ k1 implies I[k2].min, I[k2].max ∈ I[k1],
and where q is a proof that the widths of the intervals converge to zero, meaning
¥ for every real number eps > 0 there is a k such that I[k].max - I[k].min < eps.

(Strictly speaking the intervals converging to zero would be the stronger statement that
for every real number eps > 0 there is an n such that k ≥ n implies I[k].max - I[k].min < eps.
In other words, the intervals get sufficiently small and stay that way forever. This stronger statement can be deduced from p and q together since p prevents intervals from having widths larger than previous intervals. So we won't need it as a condition.)

max{f(m) | m ≤ n} is computed recursively:
¥ max{f(m) | m ≤ 0} = f(0)
¥ max{f(m) | m ≤ n+1} = max{max{f(m) | m ≤ n}, f(n+1)}
as is min{f(m) | m ≤ n}:
¥ min{f(m) | m ≤ 0} = f(0)
¥ min{f(m) | m ≤ n+1} = min{min{f(m) | m ≤ n}, f(n+1)}

To say that our function returns real numbers we need proofs of
¥ nestedness and
¥ convergence.

We also need to show
¥ compatibility with equality (changing one of the inputs to a different representation of the same real number shouldn't change the output) and
¥ proof the number constructed lies within all the intervals.

And we should also show
¥ uniqueness: there is only one real number in the intersection.

But first we need some lemmas about the min/max of a finite set of rationals as defined recursively above.

¥ There is a k ≤ n such that min{f(m) | m ≤ n} = f(k).
Proceed by induction. The base case f(0) = f(0) is trivial. Assume for some n that there is a k ≤ n such that min{f(m) | m ≤ n} = f(k). Then either min{f(m) | m ≤ n+1} = min{f(m) | m ≤ n} = f(k) or min{f(m) | m ≤ n+1} = f(n+1).

¥ If k ≤ n, then min{f(m) | m ≤ n} ≤ f(k).
Again proceed by induction. In the base case, k ≤ 0 implies k = 0, so we only need to show f(0) ≤ f(0), which is trivial. Assume for some n that k ≤ n implies min{f(m) | m ≤ n} ≤ f(k). Given k ≤ n+1, we either have k ≤ n or k = n+1. If k ≤ n, then min{f(m) | m ≤ n+1} = min{min{f(m) | m ≤ n}, f(n+1)} ≤ min{f(m) | m ≤ n} ≤ f(k). If k = n+1, then min{f(m) | m ≤ n+1} = min{min{f(m) | m ≤ n}, f(n+1)} ≤ f(n+1) = f(k).

By similar proofs, we have:
¥ There is an m ≤ n such that max{f(n) | m ≤ n} = f(m).
¥ If k ≤ n, then max{f(m) | m ≤ n} ≥ f(k).

nestedness

We need to show
¥ whenever n2 ≥ n1,
¥ max{I[m].min[n1].min | m ≤ n1} ≤ max{I[m].min[n2].min | m ≤ n2} ≤ min{I[m].max[n1].max | m ≤ n1} and
¥ max{I[m].min[n1].min | m ≤ n1} ≤ min{I[m].max[n2].max | m ≤ n2} ≤ min{I[m].max[n1].max | m ≤ n1}.

¥ max{I[m].min[n1].min | m ≤ n1} ≤ max{I[m].min[n2].min | m ≤ n2}
There is a k ≤ n1 such that max{I[m].min[n1].min | m ≤ n1} = I[k].min[n1].min. Since n2 ≥ n1 and the intervals defining I[k].min are nested, we have I[k].min[n1].min ≤ I[k].min[n2].min. Since k ≤ n1 ≤ n2, I[k].min[n2].min ≤ max{I[m].min[n2].min | m ≤ n2}, completing the proof.

¥ min{I[m].max[n2].max | m ≤ n2} ≤ min{I[m].max[n1].max | m ≤ n1}
Similar to the previous. There is a k ≤ n1 such that min{I[m].max[n1].max | m ≤ n1} = I[k].max[n1].max. Since n2 ≥ n1 and the intervals defining I[k].max are nested, we have I[k].max[n1].max ≥ I[k].max[n2].max. Since k ≤ n1 ≤ n2, I[k].max[n2].max ≥ min{I[m].max[n2].max | m ≤ n2}, completing the proof.

Now we need to do the parts
¥ max{I[m].min[n2].min | m ≤ n2} ≤ min{I[m].max[n1].max | m ≤ n1}
¥ max{I[m].min[n1].min | m ≤ n1} ≤ min{I[m].max[n2].max | m ≤ n2}.

From the fact that the intervals I are nested we can show
¥ I[m1].min ≤ I[m2].max for any m1, m2.
Either m1 ≥ m2, in which case I[m1].min ∈ I[m2], or m2 ≥ m1, in which case I[m2].max ∈ I[m1].

To prove p ≤ q for rational p and q, it is sufficient to disprove p > q.
1. Suppose max{I[m].min[n2].min | m ≤ n2} > min{I[m].max[n1].max | m ≤ n1}. Then there are j, k such that I[j].min[n2].min > I[k].max[n1].max, showing I[j].min > I[k].max. This contradicts I[j].min ≤ I[k].max.
2. Suppose max{I[m].min[n1].min | m ≤ n1} > min{I[m].max[n2].max | m ≤ n2}. Then there are j, k such that I[j].min[n1].min > I[k].max[n2].max, showing I[j].min > I[k].max. Again, this contradicts I[j].min ≤ I[k].max.

>>9598
convergence

We need to show
¥ for every rational number eps > 0 there is an n such that
¥ min{I[m].max[n].max | m ≤ n} - max{I[m].min[n].min | m ≤ n} < eps.

Since eps/3 > 0, there is an k such that
width(I[k]) = I[k].max - I[k].min < eps/3
and therefore
I[k].max[n].min - I[k].min[n].max ≤ I[k].max - I[k].min < eps/3.

Furthermore there is an n1 such that
width(I[k].min[n1]) < eps/3
and an n2 such that
width(I[k].max[n2]) < eps/3.
Let n = max{k, n1, n2}. Then
width(I[k].min[n]) < eps/3
width(I[k].max[n]) < eps/3.

Adding together
width(I[k].max[n]) < eps/3
I[k].max[n].min - I[k].min[n].max < eps/3
width(I[k].min[n]) < eps/3
we obtain
I[k].max[n].max - I[k].min[n].min < eps.

Since k ≤ n, we have I[k].max[n].max ≥ min{I[m].max[n].max | m ≤ n} and I[k].min[n].min ≤ max{I[m].min[n].min | m ≤ n}. Thus
min{I[m].max[n].max | m ≤ n} - max{I[m].min[n].min | m ≤ n} ≤ I[k].max[n].max - I[k].min[n].min < eps.

proof the number constructed lies within all the intervals

We need to show
¥ for any k, nested_RI_int(I, p, q) ∈ I[k].

By nested_RI_int(I, p, q) ∈ I[k], we mean I[k].min ≤ nested_RI_int(I, p, q) ≤ I[k].max.

1. Assume to the contrary that I[k].min > nested_RI_int(I, p, q). Then there is an n such that I[k].min[n].min > nested_RI_int(I, p, q)[n].max. Let n' = max{n,k}; then
I[k].min[n'].min ≥ I[k].min[n].min > nested_RI_int(I, p, q)[n].max ≥ nested_RI_int(I, p, q)[n'].min = max{I[m].min[n'].min | m ≤ n'}.
But since k ≤ n', I[k].min[n'].min ≤ max{I[m].min[n'].min | m ≤ n'}, a contradiction.

2. Assume to the contrary that I[k].max < nested_RI_int(I, p, q). Then there is an n such that I[k].max[n].max < nested_RI_int(I, p, q)[n].min. Let n' = max{n,k}; then
I[k].max[n'].max ≤ I[k].max[n].max < nested_RI_int(I, p, q)[n].min ≤ nested_RI_int(I, p, q)[n'].max = min{I[m].max[n'].max | m ≤ n'}.
But since k ≤ n', I[k].max[n'].max ≥ min{I[m].max[n'].max | m ≤ n'}, a contradiction.

uniqueness

We need to show
¥ If I is a sequence of nested closed intervals whose widths converge to zero, and we have both x ∈ I[k] for all k and y ∈ I[k] for all k, then x = y.

For this we won't need the nestedness part. So we can restate this with fewer conditions as
¥ If I is a sequence of closed intervals in which we can find an interval with width smaller than any positive real number eps, and we have both x ∈ I[k] for all k and y ∈ I[k] for all k, then x = y.
(we can't say the widths converge to zero anymore because that's not true without the nestedness condition)

Assume to the contrary that x <> y. Either x > y or y > x. If x > y, let eps = x - y, and note eps > 0. Then there is a k such that I[k].max - I[k].min < eps. Since x ≤ I[k].max and y ≥ I[k].min, we have eps = x - y ≤ I[k].max - I[k].min, a contradition. If y > x, the argument is the same with x and y interchanged. Therefore x = y.

compatibility with equality

We need to show
¥ if I1[k].min = I2[k].min and I1[k].max = I2[k].max for all k, then nested_RI_int(I1, p1, q1) = nested_RI_int(I2, p2, q2).

We know nested_RI_int(I1, p1, q1) ∈ I1[k] for all k. Since the bounds for I1 and I2 are the same, nested_RI_int(I1, p1, q1) ∈ I2[k] for all k. Since we also have nested_RI_int(I2, p2, q2) ∈ I2[k] for all k, and the real number in this intersection is unique, it follows that nested_RI_int(I1, p1, q1) = nested_RI_int(I2, p2, q2).

Our proofs about nested real intervals are now complete.

When I started this thread I said
>This has been done many times before and probably much better than I will manage
but I learned of an implementation of this concept in a surprisingly ubiquitous place.

On a phone that runs Android, open the default Android calculator app and input any expression that has infinitely many decimals in the answer. Then in the place where the result is displayed, swipe left.

>>9731
some more exposition of this feature

>>9731
that's kinda cool

Going to make a conscious effort to go and reread through this thread again after having beefed up my mathematical knowledge a bit. Hopefully this time nothing goes over my head

>>11068
Thanks for the interest. Does everything make sense now?

I've been making progress toward getting a demo calculator site working using the stuff I've programmed so far, by converting the Coq code into OCaml and then converting the OCaml code to Javascript. One missing ingredient I need to add is some friendly output, something that can be used to extract decimal digits from a number.

Let's define a function round(x) that takes a real number as input and returns either the number rounded down or rounded up (which we get will depend not just on the value of the number but also on how it's computed). To do this, we just need to iterate through the sequence of intervals (using the Coq library function constructive_ground_epsilon_nat) until we find the first natural number k such that
¥ floor(max(x[k])) ≤ ceil(min(x[k])).
where ceil and floor are ceiling and floor functions for rational numbers. Then we just return
¥ floor(max(x[k])).

We must first prove that such a k exists so that the iteration is guaranteed to terminate. From our definition of real numbers, we know there exists a k such that max(x[k]) - min(x[k]) < 1. For this k we have floor(max(x[k])) - ceil(min(x[k])) ≤ max(x[k]) - min(x[k]) < 1. Thus floor(max(x[k])) - ceil(min(x[k])) ≤ 0, and floor(max(x[k])) ≤ ceil(min(x[k])).

Next we want to show that the function works as intended, meaning that
¥ round(x) - 1 < x < round(x) + 1.
For the first part:
round(x) - 1 = floor(max(x[k])) - 1 ≤ ceil(min(x[k])) - 1 < min(x[k]) ≤ x
For the second part:
round(x) + 1 = floor(max(x[k])) + 1 > max(x[k]) ≥ x

To extract n decimal digits of the number x, we can simply compute
¥ round(10^n * x)
and format the result by putting the decimal point in the proper place. The result will either correct rounded down or rounded up.

Next step is to build a parser for the calculator input.

>>9512
>>11139
I've got the little demo calculator site online now. It still needs a lot of work, but you can play with it at:
https://ccd0.github.io/toyreals0/

>>11164
I added a bit of documentation. Currently the default input is

¥ intersect (i => repeat i (x => [4 / (min x + max x), (min x + max x) / 2]) [1, 2])

which computes the square root of two. You can see what's going on by trying out

¥ (i => repeat i (x => [4 / (min x + max x), (min x + max x) / 2]) [1, 2]) 0
¥ (i => repeat i (x => [4 / (min x + max x), (min x + max x) / 2]) [1, 2]) 1
¥ (i => repeat i (x => [4 / (min x + max x), (min x + max x) / 2]) [1, 2]) 2

and so on to display the intervals it's computing which converge to sqrt(2).

>>11169
After the latest update this should be
¥ intersect (repeat (xs => let avg := (min xs + max xs) / 2 in [2 / avg, avg]) [1, 2])
and
¥ repeat (xs => let avg := (min xs + max xs) / 2 in [2 / avg, avg]) [1, 2] 0
¥ repeat (xs => let avg := (min xs + max xs) / 2 in [2 / avg, avg]) [1, 2] 1
¥ repeat (xs => let avg := (min xs + max xs) / 2 in [2 / avg, avg]) [1, 2] 2
to see how it works.

>>9477
Correction:
> Assuming Markov, x = y if and only if x <> y is true.
¥ Assuming Markov, x = y is false if and only if x <> y is true.

While fiddling with the expression in >>11171 to see if I could turn it into a general square root function, I realized we need a way to define piecewise functions.

Specifically, I want to be able to do
¥ piecewise(a,f,g)
and get a function such that
¥ piecewise(a,f,g)(x) = f(x) for x ≤ a
¥ piecewise(a,f,g)(x) = g(x) for x ≥ a.

You might wonder why we can't just do something like
¥ if x < a then f(x) else g(x).
The problem is that when x = a exactly, the comparison requires infinite precision and never terminates. So we'll have to do things a bit differently.

We'll need the two parts meet at a common value:
¥ f(a) = g(a).
Otherwise we would have to compute x to infinite precision in order to decide whether to use f or g.

I found I wasn't able to prove the convergence of the result without assuming a stronger condition than above, namely that
¥ if f(x) <> g(x), then x <> a.

One way to prove this for a given a, f, and g would be to first prove the three conditions
¥ f(a) = g(a)
¥ if f(x) <> f(a), then x <> a
¥ if g(x) <> g(a), then x <> a.

Let's first prove that for any x, y, and z,
¥ if x <> z, then x <> y or y <> z.
If x < z, we have y < z or x < y. If z < x, we have y < x or z < y. In either case, x <> y or y <> z.
This also gives us a slightly shorter proof of the transitivity of equality than the one in >>8925:
¥ If x = y and y = z, then x = z.
Assume to the contrary that x <> z. Then x <> y or y <> z, both of which contradict the premises.

It will also be useful to extend this out to longer chains:
¥ If w <> z, then w <> x, x <> y, or y <> z.
Proof: w <> z implies w <> x or x <> z. The second case implies x <> y or y <> z.

Back to proving that
¥ f(a) = g(a)
¥ if f(x) <> f(a), then x <> a
¥ if g(x) <> g(a), then x <> a
imply
¥ if f(x) <> g(x), then x <> a.
Suppose f(x) <> g(x). Then either f(x) <> f(a), implying x <> a, or f(a) <> g(a), contradicting our premises, or g(a) <> g(x), implying x <> a.

So far, when we've defined a function we've usually been proving that it's respectful of real number equality in the sense that
¥ if x = a, then f(x) = f(a).
but now we're interested in
¥ if f(x) <> f(a), then x <> a.
Classical logic would allow us to deduce the former from the latter (Markov's principle would also suffice per >>8966). But we'd like to avoid invoking axioms if possible since they cause Coq's execution to get stuck. It might be useful to go back and prove the apartness version for some of the functions we've already defined. Alternatively we should be able to get it as a consequence of the usual definition of continuity of f at x = a, namely
¥ f is continuous at a if for every eps > 0 there exists a delta > 0 such that |x - a| < delta implies |f(x) - f(a)| < eps.
If f(x) <> f(a), then |f(x) - f(a)| > 0, so there exists delta > 0 such that |x - a| < delta implies |f(x) - f(a)| < |f(x) - f(a)| and is therefore false. Thus |x - a| ≥ delta > 0 and x <> a.
But we need to construct absolute values first, at least if we want to use absolute values rather than having to write out things like a - delta < x < a + delta.

We'll define our piecewise function making function as
¥ piecewise(a,f,g,p)(x)[k] = f(x)[k] if x[k] < a[k]
¥ piecewise(a,f,g,p)(x)[k] = g(x)[k] if x[k] > a[k]
¥ piecewise(a,f,g,p)(x)[k] = [min {f(x)[k].min, g(x)[k].min}, max {f(x)[k].max, g(x)[k].max}]Q otherwise
(remember: [a,b]Q < [c,d]Q if b < c)
where p is a proof that
¥ for all x, f(x) <> g(x) implies x <> a.

As usual, we will need to show that this defines a real number. These are always kind of tedious, but hopefully I won't have to do too many more of these, and instead I'll be able to define new functions in terms of stuff I've already written. In particular, this piecewise function stuff will get us the absolute value function as well as functions returning the lesser and greater of two arguments.

Some useful lemmas first:

¥ If x and y are real numbers and k2 ≥ k1, then x[k1] < y[k1] implies x[k2] < y[k2].
Proof: x[k2].max ≤ x[k1].max < y[k1].min ≤ y[k2].min
This can also be used to simplify the proof of one of the lemmas in >>9460:
¥ If a < b and c < d, then there is a natural number k such that a[k] < b[k] and c[k] < d[k].
Suppose a < b and c < d. Then there is a k1 such that a[k1] < b[k1] and a k2 such that c[k2] < d[k2]. Let k be the larger of k1 and k2. Then a[k] < b[k] and c[k] < d[k].

Another lemma, this one extracted from the proof of >>8969:
¥ Given two nonempty closed rational intervals u and v, if neither u < v nor v < u, there is a rational number r such that r ∈ u and r ∈ v, specifically max {u.min, v.min}.
Clearly r ≥ u.min and r ≥ v.min. Either r = min(x[k]) or r = min(y[k]). If r = u.min, then we have r = u.min ≤ u.max since u is nonempty, and r = u.min ≤ v.max since v < u is false. Similarly, if r = v.min, we have r = v.min ≤ v.max since v is nonempty, and we have r = v.min ≤ u.max since u < v is false. Thus r ∈ u and r ∈ v.

A third lemma will be useful to show that our first and second cases are actually distinct:
¥ Given two nonempty closed rational intervals u and v, if u < v, then it is not the case that v < u.
Proof: u.min ≤ u.max < v.min ≤ v.max, so v.max < u.min is false.

As the last lemma, we note that
¥ if r ∈ [a, b]Q, c ≤ a, and b ≤ d, then r ∈ [c, d]Q
since c ≤ a ≤ r and r ≤ b ≤ d
which we can extend to work on two elements at a time:
¥ If r, s ∈ [a, b]Q, c ≤ a, and b ≤ d, then r, s ∈ [c, d]Q.

Now back to the main proof.
First, we must prove that the intervals are nested:
¥ If k2 ≥ k1, then piecewise(a,f,g,p)(x)[k2].min ∈ piecewise(a,f,g,p)(x)[k1] and piecewise(a,f,g,p)(x)[k2].max ∈ piecewise(a,f,g,p)(x)[k1].
Suppose k2 ≥ k1. There are three cases.
1) If x[k1] < a[k1], then x[k2] < a[k2]. Thus piecewise(a,f,g,p)(x)[k2] = f(x)[k2], whose minimum and maximum are both in f(x)[k1] = piecewise(a,f,g,p)(x)[k1].
2) If x[k1] > a[k1], then x[k2] > a[k2]. Thus piecewise(a,f,g,p)(x)[k2] = g(x)[k2], whose minimum and maximum are both in g(x)[k1] = piecewise(a,f,g,p)(x)[k1].
3) Otherwise, piecewise(a,f,g,p)(x)[k1] = [min {f(x)[k1].min, g(x)[k1].min}, max {f(x)[k1].max, g(x)[k1].max}]Q.
It suffices to show that piecewise(a,f,g,p)(x)[k2].min and piecewise(a,f,g,p)(x)[k2].max are within
u = [min {f(x)[k2].min, g(x)[k2].min}, max {f(x)[k2].max, g(x)[k2].max}]Q.
Once we have that, we know that they are within piecewise(a,f,g,p)(x)[k1] since
f(x)[k1].min ≤ f(x)[k2].min and f(x)[k1].max ≤ f(x)[k2].max and
g(x)[k1].min ≤ g(x)[k2].min and g(x)[k1].max ≤ g(x)[k2].max
imply
min {f(x)[k1].min, g(x)[k1].min} ≤ min {f(x)[k2].min, g(x)[k2].min} and max {f(x)[k2].max, g(x)[k2].max} ≤ max {f(x)[k1].max, g(x)[k1].max}.
We have three subcases:
3a) If x[k2] < a[k2], then piecewise(a,f,g,p)(x)[k2] = f(x)[k2].
Since f(x)[k2] is nonempty, its min and max are within f(x)[k2].
Since min {f(x)[k2].min, g(x)[k2].min} ≤ f(x)[k2].min and f(x)[k2].max ≤ max {f(x)[k2].max, g(x)[k2].max}, they are also within u.
3b) If x[k2] > a[k2], then piecewise(a,f,g,p)(x)[k2] = g(x)[k2].
Since g(x)[k2] is nonempty, its min and max are within g(x)[k2].
Since min {f(x)[k2].min, g(x)[k2].min} ≤ f(x)[k2].min and f(x)[k2].max ≤ max {f(x)[k2].max, g(x)[k2].max}, they are also within u.
3c) If x[k2] > a[k2], then piecewise(a,f,g,p)(x)[k2] = u.
We know u is nonempty since min {f(x)[k2].min, g(x)[k2].min} ≤ f(x)[k2].min ≤ f(x)[k2].max ≤ max {f(x)[k2].max, g(x)[k2].max}.
Therefore the min and max of u are within u.

Second, we must prove that the widths of the intervals converge to zero:
¥ For every rational eps > 0 there is a k such that piecewise(a,f,g,p)(x)[k].max - piecewise(a,f,g,p)(x)[k].min < eps.
There is a k1 such that width(f(x)[k1]) < eps/2 and a k2 such that width(g(x)[k2]) < eps/2. Consider two cases:
1) Either f(x)[k1] < g(x)[k2] or g(x)[k2] < f(x)[k1].
Then we have f(x) <> g(x), and it follows that x <> a. Two subcases:
1a) x < a
Then there is a k3 such that x[k3] < a[k3]. Let k = max {k1, k3}; we have x[k] < a[k] and thus width(piecewise(a,f,g,p)(x)[k]) = width(f(x)[k]) ≤ width(f(x)[k1]) < eps/2 < eps.
1b) x > a
Then there is a k3 such that x[k3] > a[k3]. Let k = max {k2, k3}; we have x[k] > a[k] and thus width(piecewise(a,f,g,p)(x)[k]) = width(g(x)[k]) ≤ width(g(x)[k2]) < eps/2 < eps.
The remaining case:
2) Neither f(x)[k1] < g(x)[k2] nor g(x)[k2] < f(x)[k1].
Then there is a rational number r = max {f(x)[k1].min, g(x)[k2].min} such that r ∈ f(x)[k1] and r ∈ g(x)[k2]. Let k = max {k1, k2}.
We must consider three subcases:
2a) If x[k] < a[k], then
width(piecewise(a,f,g,p)(x)[k]) = width(f(x)[k]) ≤ width(f(x)[k1]) < eps/2 < eps.
2b) If x[k] > a[k], then
width(piecewise(a,f,g,p)(x)[k]) = width(g(x)[k]) ≤ width(g(x)[k2]) < eps/2 < eps.
2c) Otherwise:
Since r ≥ f(x)[k1].min and f(x)[k].max ≤ f(x)[k1].max, we have f(x)[k].max - r ≤ f(x)[k1].max - f(x)[k1].min < eps/2.
Since r ≥ g(x)[k2].min and g(x)[k].max ≤ g(x)[k2].max, we have g(x)[k].max - r ≤ g(x)[k2].max - g(x)[k2].min < eps/2.
We know that max {f(x)[k].max, g(x)[k].max} is either f(x)[k].max or g(x)[k].max. In either case, max {f(x)[k].max, g(x)[k].max} - r < eps/2.
Since r ≤ f(x)[k1].max and f(x)[k].min ≥ f(x)[k1].min, we have r - f(x)[k].min ≤ f(x)[k1].max - f(x)[k1].min < eps/2.
Since r ≤ g(x)[k2].max and g(x)[k].min ≥ g(x)[k2].min, we have r - g(x)[k].min ≤ g(x)[k2].max - g(x)[k2].min < eps/2.
We know that min {f(x)[k].min, g(x)[k].min} is either f(x)[k].min or g(x)[k].min. In either case, r - min {f(x)[k].min, g(x)[k].min} < eps/2.
Thus width(piecewise(a,f,g,p)(x)[k]) = max {f(x)[k].max, g(x)[k].max} - min {f(x)[k].min, g(x)[k].min} = (max {f(x)[k].max, g(x)[k].max} - r) + (r - min {f(x)[k].min, g(x)[k].min}) < eps/2 + eps/2 = eps.

Our function returns real numbers, as it should!

A next obvious thing to do is to prove that our piecewise function making function behaves as we want; that is, that
¥ x ≤ a implies piecewise(a,f,g,p)(x) = f(x) and
¥ x ≥ a implies piecewise(a,f,g,p)(x) = g(x).

It turns out to be more useful to first show
¥ piecewise(a,f,g,p)(x) <> f(x) implies x > a and
¥ piecewise(a,f,g,p)(x) <> g(x) implies x < a.
1) Suppose piecewise(a,f,g,p)(x) <> f(x).
Then there is a k such that piecewise(a,f,g,p)(x)[k] < f(x)[k] or piecewise(a,f,g,p)(x)[k] > f(x)[k].
There are three cases:
1a) If x[k] < a[k], then
piecewise(a,f,g,p)(x)[k] = f(x)[k], so we have f(x)[k] < f(x)[k] meaning f(x)[k].max < f(x)[k].min, which is impossible since f(x)[k] is nonempty.
1b) If x[k] > a[k], then
x > a, and we are done.
1c) Otherwise,
piecewise(a,f,g,p)(x)[k] = [min {f(x)[k].min, g(x)[k].min}, max {f(x)[k].max, g(x)[k].max}]Q, so we have
max {f(x)[k].max, g(x)[k].max} < f(x)[k].min ≤ f(x)[k].max or
f(x)[k].min ≤ f(x)[k].max < min {f(x)[k].min, g(x)[k].min},
both of which are impossible.
2) Suppose piecewise(a,f,g,p)(x) <> g(x).
This is substantially identical to (1), but I've written it out anyway. There are again three cases:
2a) If x[k] < a[k], then
x < a, and we are done.
2b) If x[k] > a[k], then
piecewise(a,f,g,p)(x)[k] = g(x)[k], so we have g(x)[k].max < g(x)[k].min, which is impossible.
2c) Otherwise,
piecewise(a,f,g,p)(x)[k] = [min {f(x)[k].min, g(x)[k].min}, max {f(x)[k].max, g(x)[k].max}]Q, so we have
max {f(x)[k].max, g(x)[k].max} < g(x)[k].min ≤ g(x)[k].max or
g(x)[k].min ≤ g(x)[k].max < min {f(x)[k].min, g(x)[k].min},
both of which are impossible.

The originally desired results
¥ x ≤ a implies piecewise(a,f,g,p)(x) = f(x) and
¥ x ≥ a implies piecewise(a,f,g,p)(x) = g(x).
are obtained by taking the contrapositive.

Another thing we want to prove is that our piecewise function is compatible with equality. Let's prove a similar result involving apartness first:
¥ If piecewise(a1,f1,g1,p1)(x1) <> piecewise(a2,f2,g2,p2)(x2), then a1 <> a2, f1(x1) <> f2(x2), g1(x1) <> g2(x2), or x1 <> x2.
Suppose piecewise(a1,f1,g1,p1)(x1) <> piecewise(a2,f2,g2,p2)(x2). Then piecewise(a1,f1,g1,p1)(x1) <> f1(x1), f1(x1) <> f2(x2), or f2(x2) <> piecewise(a2,f2,g2,p2)(x2). From these we can conclude that
x1 > a1, f1(x1) <> f2(x2), or x2 > a2.
Similarly, we have piecewise(a1,f1,g1,p1)(x1) <> g1(x1), g1(x1) <> g2(x2), or g2(x2) <> piecewise(a2,f2,g2,p2)(x2). We can conclude that
x1 < a1, g1(x1) <> g2(x2), or x2 < a2.
In the cases where f1(x1) <> f2(x2) or g1(x1) <> g2(x2), we are done. The cases where x1 > a1 and x1 < a1 or where x2 > a2 and x2 < a2 are contradictory. The remaining cases are:
1) x1 > a1 and x2 < a2
From x2 < a2 we have either a1 < a2, and we are done, or x2 < a1, implying x2 < a1 < x1.
2) x2 > a2 and x1 < a1
From x1 < a1 we have either a2 < a1, and we are done, or x1 < a2, implying x1 < a2 < x2.

We can now prove that
¥ If a1 = a2, f1(x1) = f2(x2), g1(x1) = g2(x2), and x1 = x2, then piecewise(a1,f1,g1,p1)(x1) = piecewise(a2,f2,g2,p2)(x2).
Assume to the contrary that piecewise(a1,f1,g1,p1)(x1) <> piecewise(a2,f2,g2,p2)(x2). Then a1 <> a2, f1(x1) <> f2(x2), g1(x1) <> g2(x2), or x1 <> x2, all of which contradict our premises.

I've added the piecewise function generating function to the calculator demo:
https://ccd0.github.io/toyreals0/

So you can now do things like this:
let abs := piecewise 0 (x => -x) (x => x) in abs (-4.5)

>>9012
Been thinking about this question again. Haven't solved it, but I noticed we can remove this condition:
>Suppose also that we know that at least one of the programs (possibly both) does not halt.

Suppose we have the desired algorithm, and we feed it two computer programs, both of which halt. In the original question, the behavior of the algorithm is unspecified, so it may give either answer, or some nonsense answer, or simply never halt. We can produce a modified algorithm by running the original algorithm in parallel with programs A and B. If both A and B halt before the original algorithm halts, or if the original algorithm halts first with nonsense output, let the modified algorithm output the choice "A" (arbitrarily chosen, "B" would work just as well for this argument). Otherwise, let the modified algorithm await the result of the original algorithm and halt with that output. The modified algorithm is guaranteed to halt in all cases, and is guaranteed to output "A" if A does not halt but B does halt, and is guaranteed to output "B" if B does not halt but A does halt. Furthermore, any algorithm with this property meets the original specification.

Thus we can restate the problem as follows:
¥Is it possible to write an algorithm which, given two computer programs A and B, correctly concludes, in a finite amount of time, either that "if A halts then B halts" or that "if B halts then A halts"? If it's not possible, how can we prove that?

>>11360
I think I've got it using a variation on the original halting problem argument.

Suppose we have a function compare_halt with four arguments
¥compare_halt(prog0, data0, prog1, data1)
satisfying the specification
¥if prog(data0) halts and prog(data1) does not halt, the output is 0
¥if prog(data1) halts and prog(data0) does not halt, the output is 1
¥otherwise the output can be either 0 or 1.

Consider the program

function F([i, prog]) {
if compare_halt(prog, [0, prog], prog, [1, prog]) == i then
infinite_loop()
else
return
}


If compare_halt(F, [0, F], F, [1, F]) evaluates to 0, then F([0, F]) hangs and F([1, F]) halts.
But the specification says compare_halt(F, [0, F], F, [1, F]) must evaluate to 1 in this case.

If compare_halt(F, [0, F], F, [1, F]) evaluates to 1, then F([0, F]) halts and F([1, F]) hangs.
But the specification says compare_halt(F, [0, F], F, [1, F]) must evaluate to 0 in this case.

Thus the proposed compare_halt function is impossible.

>>11361
Some corrolaries.

¥There is no general algorithm which, given two programs that output infinite decimals as streams, computes the infinite decimal representing their sum.
Let A and B be two computer programs.
Let x start with "0." followed by 0's until program A halts, at which point the digits change to 1's.
Let y start with "0." followed by 9's until program B halts, at which point the digits change to 8's.
If A halts and B does not halt, then x+y > 1, and the ones place of x+y must be 1. If B halts and A does not halt, then x+y < 1, and the ones place of x+y must be 0. Thus there is no way to calculate the ones place of x+y.

Note that it's possible to get around this problem by using more than 10 digits. For example, infinite decimals built using the digits -9 through 9, like I talked about in >>9462, don't have this problem.

¥There is no general algorithm which converts an object of our real number type to a stream of digits giving an infinite decimal representation of the number.
In >>9596 I mentioned I didn't know a proof of this; now we have one. We can easily convert a stream of digits into a stream of nested rational intervals. For example, 3.14... becomes [3,4], [3.1,3.2], [3.14,3.15], ... . If we could convert back into an infinite decimal stream, then we could take the two infinite decimal streams from the previous proof, convert them into nested interval streams, add them, then convert to the desired inifinite decimal stream.

Note that there would be no problem converting to infinite decimal form if we allow the digits -9 through 9. Also, there's no problem with doing what's done now in
https://ccd0.github.io/toyreals0/
which is to produce the number of digits desired which the guarantee that the result is either rounded up or rounded down. This is different from outputting an infinite stream of digits since a result like
1.000
can change to
0.9999
when another digit is required.

¥There is no general algorithm which, given two numbers x and y for which x*y = 0, correctly names either x or y as the number that equals 0.
As I mentioned in >>9015, this was the original problem that got me thinking about this. Let A and B be two computer programs. Let x[k] = [0, 1/k] if A has not halted by the kth step, and x[k] = [1/n, 1/n] if A halts at step n and k ≥ n. Define y from B similarly. Under this construction, x=0 if and only if A halts, and similarly for y and B. If we know x*y = 0, we know either x=0 or y=0, but we don't necessarily know which. Suppose we did have a procedure which, given x and y for which x*y = 0, could correctly conclude "x=0" or "y=0". This is the same as concluding correctly that "A does not halt" or "B does not halt" under the condition that at least one of A and B do not halt. By the argument in >>11360, this is equivalent to the impossible algorithm in >>11361.

>>9444
I was thinking about how to hand-multiply infinite (signed-digit) decimals again. Pic related might be more work than necessary, but it does have the advantage of making it less confusing. It also has the advantage of giving the greatest possible number of digits for a fixed number of digits of the input, which might be helpful if further digits of the numbers you're multiplying are difficult to compute.

Most of the process should be self-explanatory, but some things I should explain. First of all, obviously we can't multiply infinitely many digits. The goal here is a process that if carried on long enough, could give you arbitrarily many digits of the answer, assuming you can get the required number of digits of the two numbers you're multiplying.

Second, as mentioned in >>9462, I'm using signed digits. Digits can be anything in {-9,-8,-7,-6,-5,-4,-3,-2,-1,0,1,2,3,4,5,6,7,8,9}. To represent the negative digits, I draw a line over the digit. Everything is still in base 10, but there are now more ways to represent the same number. For example, early on in the computation, I add 140 + 56 and write the answer as 20(-4) rather than 196. When adding the numbers, I chose to convert the 6 to 1(-4) and carry the 1. I'll explain why I did that in a moment.

When a signed-digit infinite decimal number is truncated to a finite number of digits, the uncertainty in the number is ±1 in the final digit. For example, 1.414 could be the truncation of any number between 1.414[(-9)(-9)(-9),repeating] and 1.414[999,repeating] inclusive, which are the same thing as 1.413 and 1.415 respectively. At various stages in the calculation, I've computed the uncertainty in the answer at that point. For example, when multiplying numbers truncated to 1.414*1.414, the result is 2.00(-1)404 with an uncertainty of ±0.002829. The uncertainty can be calculated by adding 1414+1414+1. By considering the uncertainty, we can figure out which digits can be taken as final digits of the answer. At the 1.414*1.414 stage, the digits 2.00 can be taken as final since 2.00(-1)404 ± 0.002829 is guaranteed to be between 2.0(-1) and 2.01 inclusive. In the pic, I've drawn boxes around the digits which have been taken as final.

This should explain why I wrote the answer to 1.4*1.4 as 2.0(-4) instead of 1.96. The first digit of 2.0(-4) can be taken as final since 2.0(-4) ± 0.29 is guaranteed to be between 2.(-1) and 2.1 inclusive. But the first digit of 1.96 ± 0.29 cannot be taken as final. If the answer had been written as 1.96, I would have had to rewrite it as 2.(-1)6 or 2.0(-4) in order to take the first digit as final. To increase the likelihood that I would get digits that can be taken as final, I was choosing to write digits in the range {-5,-4,-3,-2,-1,0,1,2,3,4,5} when possible.

This stuff is far, far above my mental capacity, but I'm glad to see you're still doing it!

>>11943
You're probably underrating your mental capacity. Some of the stuff in this thread might be complicated, but >>11942 is just me getting closer and closer to the result of a multiplication problem by repeatedly adding a digit to each of the two numbers I'm multiplying.

1 * 1 = 1
1.4 * 1 = 1.4
1.4 * 1.4 = 2.0(-4) [another way of writing 1.96]
1.41 * 1.4 = 2.0(-3)4 [another way of writing 1.974]
and so on indefinitely.

In this case the two numbers I'm multiplying are both the square root of 2, which is
1.4142135623730950488016887... (continues infinitely)
so the result should be 2. But you could use the same algorithm to multiply any two infinite decimals.

The ± thing is me calculating how far the current result could possibly be from the correct answer, which lets me know how many of digits I've calculated so far are necessarily correct. I drew a box around the digits I know are correct at each stage.

>>11942
The same algorithm with a bit less writing. It's nice that it works out so you can see what you need to multiply at each step by simply looking at the digit you're at and the digits in the other column above it. I've also reduced the use of negative digits.

>>9731
I found a paper they wrote about that functionality after they implemented it:
https://cacm.acm.org/magazines/2017/8/219594-small-data-computing/fulltext

It's an interesting read. Also it usefully gives the error guarantees on the calculation:
>We wanted to ensure at a minimum that the displayed final answer was never off by one or more in the final displayed digit.
That's what I expected, but it's nice to know it instead of guessing. It's also the same standard I used for >>11164.

They made use of a preexisting Java library to do the calculations:
https://www.hboehm.info/crcalc/

I want to try to get to the answer of questions like >>8932 about precisely what axioms we need to add to Coq in order to reason about "all" the real numbers as discussed in >>8919, in the sense that we can prove the versions of the completeness property commonly used in classical mathematics. After that, maybe we'll look at countability and subcountability.

In order to do that, I need to finish off what I planned out in >>9526 and write proofs of some more of those properties. Some of those properties require adding axioms to Coq, and some don't. Without using any additional axioms, we've already proven
> (1) The Archimedean property
in >>9532 and
> (17) The Shrinking Interval Property
in >>9598 and the posts that follow. In classical mathematics these two together are enough to prove the other properties, but since Coq uses only constructive reasoning by default, we'll need to use axioms for some of them.

The next property I want to attack is
> (11) The Convergence of Cauchy Sequences: Every Cauchy sequence in R is convergent.

Both "Cauchy sequence" and "convergent" are usually defined using the absolute value function. So we'll have to define that first.

The absolute value function should satisfy
¥ |x| = -x for x ≤ 0
¥ |x| = x for x ≥ 0.
We've already defined a function for making piecewise functions in >>11198. We can use this to define the absolute value as
¥ |x| = piecewise(0, (x => -x), (x => x), p)(x)
where p is the necessesary proof of
¥ if -x <> x, then x <> 0
which can be obtained by subtracting x from both sides, then dividing by -2.

It follows immediately from the theorems we've already proven about the piecewise function making function that our absolute value function is compatible with equality
¥ x = y implies |x| = |y|
and that
¥ |x| = -x for x ≤ 0
¥ |x| = x for x ≥ 0
as desired.

Now comes the time to prove theorems about the absolute value function. To avoid spending too long on this, for now I'm going to limit the list to things which I know I need or for which I've needed the analogous theorem in the rational numbers. We can add more theorems later as needed. For now we want to show:
¥ |x| ≥ 0
¥ |-x| = |x|
¥ x ≤ |x|
¥ |x + y| ≤ |x| + |y|
¥ |x * y| = |x| * |y|
¥ |x - y| ≤ z if and only if x ∈ [y - z, y + z]

The obvious way to prove theorems like these in classical logic would be to split into the two cases x ≤ 0 and x ≥ 0, and prove the results in each case. For a moment it seems that not assuming the excluded middle will get in our way, since we don't have a proof that x ≤ 0 or x ≥ 0, only of its double negation. Fortunately it's not as bad as it looks. All statements involving ≤ and = are negative statements; we have defined ≤ as not > and = as not <>. It turns out that in intuitionistic logic, if we want to prove a negative statement, then we can use any fact that we've proven the double negation of. To say this more precisely,
¥ If P implies not Q, then not not P implies not Q.
Proof: Given that P implies not Q, and given not not P, assume to the contrary that Q is true. If we also assume P, then we obtain not Q, which contradicts Q; thus we have not P. But not P contradicts not not P; from this contradiction we conclude not Q.

Since we have the double negation of x ≤ y or x ≥ y from >>8947, an immediate corrolary is that
¥ given any statement P, we can prove not P by proving that not P follows from x ≤ y and that not P follows from x ≥ y.

We can now grind through the theorems:
¥ |x| ≥ 0
If x ≤ 0, then |x| = -x ≥ 0.
If x ≥ 0, then |x| = x ≥ 0.
¥ |-x| = |x|
If x ≤ 0, then -x ≥ 0; thus |-x| = -x = |x|.
If x ≥ 0, then -x ≤ 0; thus |-x| = -(-x) = x = |x|.
¥ x ≤ |x|
If x ≤ 0, then 2x ≤ 0 and x ≤ -x = |x|.
If x ≥ 0, then x = |x|.
¥ |x + y| ≤ |x| + |y|
If x + y ≤ 0, then |x + y| = -(x + y) = (-x) + (-y) ≤ |-x| + |-y| = |x| + |y|.
If x + y ≥ 0, then |x + y| = x + y ≤ |x| + |y|.
¥ |x * y| = |x| * |y|
If x ≤ 0 and y ≤ 0, then -x * -y ≥ 0; thus |x * y| = |-x * -y| = -x * -y = |x| * |y|.
If x ≤ 0 and y ≥ 0, then -x * y ≥ 0; thus |x * y| = |-x * y| = x * -y = |x| * |y|.
If x ≥ 0 and y ≤ 0, then x * -y ≥ 0; thus |x * y| = |x * -y| = x * -y = |x| * |y|.
If x ≥ 0 and y ≥ 0, then x * y ≥ 0; thus |x * y| = x * y = |x| * |y|.
¥ |x - y| ≤ z if and only if x ∈ [y - z, y + z]
Suppose |x - y| ≤ z.
Then -(x - y) ≤ |-(x - y)| = |x - y| ≤ z; thus -z ≤ x - y and y - z ≤ x.
Also x - y ≤ |x - y| ≤ z, so x ≤ y + z.
Suppose x ∈ [y - z, y + z], meaning y - z ≤ x ≤ y + z.
If x - y ≤ 0, then |x - y| = -(x - y). Since -z ≤ x - y, we have |x - y| = -(x - y) ≤ z.
If x - y ≥ 0, then |x - y| = x - y ≤ z.

An anon on IRC asked if I could explain why 0.999... = 1. So I'm going to switch tracks to infinite decimals for a bit.

We can, of course, give a definition of what a infinite decimal means and dryly conclude from our definition that 0.999... = 1. I think this is not particularly enlightening because it answers the wrong question. What we really want to know is why it is pragmatic to define infinite decimals in such a manner that 0.999... = 1.

Let's start by reminding ourselves why we need infinite decimals in the first place. The idea of decimal fractions was popularized in the West by Simon Stevin in a 1585 booklet called De Thiende. He described how to do arithmetic with these decimals, which was much simpler than arithmetic with general fractions. Eventually he demonstrates how to do the problem that we would today write as 0.4 ÷ 0.03. He notes that the calculation produces infinitely many 3's, and pragmatically recommends truncating the calculation at the precision required. Centuries later, you were likely introduced to infinite decimals by a similar calculation. Let's look at it in more detail.

Using the modern algorithm, we would begin by converting 0.4 ÷ 0.03 to the equivalent division problem 40 ÷ 3. We then ask how many times 3 goes into 4, the tens place of 40; the answer is 1 time. We write 1 in the tens place of our answer, and subtract 10*3=30 from 40, obtaining the remainder 10. From the presence of the remainder we know that the answer is greater than 10. But we also know at this point of the calculation that the answer is less than 20; otherwise the 3 would have gone in 2 times instead of 1 time. We can write
¥ 10 < 0.4 ÷ 0.03 < 20.

At the next step in the division process, when we see that 3 goes into 10 3 times but not 4 times, and there is still a remainder, we know that
¥ 13 < 0.4 ÷ 0.03 < 14.

Continuing the calculation, we learn that
¥ 13.3 < 0.4 ÷ 0.03 < 13.4
¥ 13.33 < 0.4 ÷ 0.03 < 13.34
¥ 13.333 < 0.4 ÷ 0.03 < 13.334
and so on for as far as we care to compute. Although the division algorithm never gives us an exact answer, it does give us an arbitrarily extendable list of upper and lower bounds on the answer.

For this division problem, we could have used fractions to obtain an exact answer 13 1/3. But some quantities can't be expressed as a fraction, at least not if we restrict the numerator and denominator to integers (whole numbers, possibly negative). For example, there is no fraction meeting those conditions whose square is 2, even though we need a square root of 2 to compute basic things like the diagonal of a square. We can make a similar calculation for the square root of 2. Since 1^2 = 1 is too small and 2^2 = 4 is too large, the square root of 2 must be between 1 and 2:
¥ 1 < √2 < 2

And since 1.4^2 = 1.96 is too small while 1.5^2 = 2.25 is too large, we have
¥ 1.4 < √2 < 1.5.

We can continue:
¥ 1.41 < √2 < 1.42
¥ 1.414 < √2 < 1.415
¥ 1.4142 < √2 < 1.4143
¥ 1.41421 < √2 < 1.41422
¥ 1.414213 < √2 < 1.414214
...

You might wonder if we can invent a quantity ε such that
¥ 0 < ε < 1
¥ 0 < ε < 0.1
¥ 0 < ε < 0.01
¥ 0 < ε < 0.001
and so on indefinitely. I'll examine this more in the next installment.

For now, was that clear enough for everyone to understand? Any questions?

>>12033
Let's assume for a moment that a number like ε satisfying
¥ 0 < ε < 1
¥ 0 < ε < 0.1
¥ 0 < ε < 0.01
¥ 0 < ε < 0.001,
and so on indefinitely, exists, and let's look at some properties that number would have.

I won't be proving these in Coq, at least for the moment, because we're talking about number systems that are different from the one I'm describing in the project. The basic assumptions I'm making about a number system containing ε are that it satisfies the properties of an ordered field, which means all the properties listed in >>9492 except the least-upper-bound property.

First of all, ε is smaller than any positive rational number.
(A rational number is a number that can be written as a fraction with integers for the numerator and denominator. Since we are not French speakers, positive means greater than zero, and negative means less than zero; zero itself is neither positive nor negative.)
The proof: Given a positive rational number p/q, let n be the number of digits of q. Then 10^n, that is, 1 followed by n zeros, will be greater than q, and 1/10^n will be less than p/q. Since ε < 1/10^n, it is also less than p/q.

Since ε is positive, it's also obvious that ε is larger than any negative rational number.

Definition:
¥ An infinitesimal number is a number smaller than every positive rational number and larger than every negative rational number.
Our hypothetical number ε is an infinitesimal number by this definition. So is zero.

Let's look at what happens when we multiply ε by 2. We should expect that
¥ 0 < 2ε < 2
¥ 0 < 2ε < 0.2
¥ 0 < 2ε < 0.02
¥ 0 < 2ε < 0.002,
and so on indefinitely. Notice that 0.2 is less than 1, 0.02 is less than 0.1, and so on. We can conclude
¥ 0 < 2ε < 1
¥ 0 < 2ε < 0.1
¥ 0 < 2ε < 0.01,
meaning that 2ε satisfies the same upper and lower bounds that ε did. By the same logic we used to show ε was an infinitesimal number, 2ε is also an infinitesimal number.

In fact, multiplying an infinitesimal number by any rational number will give us another infinitesimal number. Let x be an infinitesimal number. For any positive integers p and q, by definition we have
-p/q < x < p/q.
Let's see what happens when we multiply x by the positive rational number r/s, with r and s being positive integers. Let p and q be arbitrary positive integers. Since p*s and q*r are both positive integers, we have
-(p*s)/(q*r) < x < (p*s)/(q*r).
Multiplying both inequalities by r/s, we get
-p/q < x*(r/s) < p/q.
Thus x*(r/s) is also an infinitesimal number.
The same thing happens if we multiply x by a negative number -r/s, with r and s being positive integers again. Let p and q be arbitrary positive integers, and we again have
-(p*s)/(q*r) < x < (p*s)/(q*r).
Multiplying both inequalities by -r/s, we get
p/q > x*(-r/s) > -p/q.
Since we multiplied by a negative number, the directions of the inequalities flip. But the result is the same; x*(-r/s) is an infinitesimal number.
The last case is multiplying by 0. Since x*0 = 0 and 0 is infinitesimal, this case works too.

Another notable feature of ε is that if its reciprocal exists, it will be larger than any positive integer:
¥ 1/ε > 1
¥ 1/ε > 10
¥ 1/ε > 100
¥ 1/ε > 1000
...
Any positive integer number we can name, we can take 10^n where n is the number of digits in that positive number, and get a bigger positive number, and we've just said that 1/ε is even bigger than that.

Yet another thing to know about ε: When dividing 0.4 ÷ 0.03, we found that
¥ 13 < 0.4 ÷ 0.03 < 14
¥ 13.3 < 0.4 ÷ 0.03 < 13.4
¥ 13.33 < 0.4 ÷ 0.03 < 13.34
¥ 13.333 < 0.4 ÷ 0.03 < 13.334
and so on indefinitely. If we add ε to the quotient, then we have
¥ 0.4 ÷ 0.03 + ε < 13.4 + 0.1 = 13.5
¥ 0.4 ÷ 0.03 + ε < 13.34 + 0.01 = 13.35
¥ 0.4 ÷ 0.03 + ε < 13.334 + 0.001 = 13.335
and so on.
Since 13.5, 13.35, and 13.335 are less than 14, 13.4, and 13.34 respectively, we also have
¥ 13 < 0.4 ÷ 0.03 + ε < 14
¥ 13.3 < 0.4 ÷ 0.03 + ε < 13.4
¥ 13.33 < 0.4 ÷ 0.03 + ε < 13.34
and so on. Thus 0.4 ÷ 0.03 + ε satisfies the same bounds we found for the original number 0.4 ÷ 0.03.

The same situation applies to √2 + ε. Here it goes even further:
¥ for any two rational numbers that √2 is between, √2 + ε is between the same rational numbers.
Proof: Assume to the contrary that there are rational numbers p/q and r/s (p,q,r,s integers) such that
p/q < √2 < r/s
but
r/s ≤ √2 + ε.
Then
2 < (r/s)^2 < (√2 + ε)^2
2 < r^2/s^2 < 2 + 2ε√2 + ε^2
0 < r^2/s^2 - 2 < 2ε√2 + ε^2
0 < (r^2-2s^2)/s^2 < 2ε√2 + ε^2 = ε(2√2 + ε) < 3ε < every positive rational.
This is a contradiction; if (r^2-2s^2)/s^2 is positive and rational, it cannot be be less than every positive rational number.

Correction: There are some < signs in >>12035 that should be ≤ signs.
Instead of
> 2 < (r/s)^2 < (√2 + ε)^2
> 2 < r^2/s^2 < 2 + 2ε√2 + ε^2
> 0 < (r^2-2s^2)/s^2 < 2ε√2 + ε^2 = ε(2√2 + ε) < 3ε < every positive rational.
it should say
2 < (r/s)^2 ≤ (√2 + ε)^2
2 < r^2/s^2 ≤ 2 + 2ε√2 + ε^2
0 < (r^2-2s^2)/s^2 ≤ 2ε√2 + ε^2 = ε(2√2 + ε) < 3ε < every positive rational.

>>12033
>>12035
So to answer the question of whether there's a number system with a number ε such that
¥ 0 < ε < 1
¥ 0 < ε < 0.1
¥ 0 < ε < 0.01
¥ 0 < ε < 0.001,
and so on, the answer is yes, there are many. There are the hyperreal numbers which are useful as an alternate way to do calculus. There are the surreal numbers which arose out of game theory. And you can even just postulate such a number ε and add it to the reals sort of like how we add i to make the complex numbers. In the case of the complex numbers, you get the complex numbers from all the linear functions of i. If you add ε, your new set of numbers consists of all the rational functions (polynomial divided by polynomial) of ε.

But we can see that a nonzero infinitesimal number like ε will cause trouble if we want our numbers to be expressed by infinite decimals. The whole idea behind infinite decimals is that we can identify a number by comparing it with finite decimals. If we allow ε into our system, then we can no longer distinguish ε from 2ε, or 0.4 ÷ 0.03 from 0.4 ÷ 0.03 + ε, or √2 from √2 + ε by comparing them with finite decimals. We would need something else. For example, in the surreal numbers, ε is the simplest number between {0} and {1, 1/2, 1/4, 1/8, ...}, and 2ε is the simplest number between {ε} and {1, 1/2, 1/4, 1/8, ...}.

Another definition:
¥ Two numbers are infinitesimally close if the difference between them is infinitesimal.

There are many equivalent ways to construct the real numbers, but all of them are designed so that we never construct a real number infinitesimally close to another real number. I don't think anyone knows whether it's possible for two real-life quantities (such as distances, times, weights, and volumes) to be infinitesimally close to each other yet not equal. If it is possible, then when we model these infinitesimally close quantities with real numbers, we are choosing to ignore any infinitesimal difference and assign the same real number to both.

A simple way to avoid constructing numbers infinitesimally close to other numbers is to change the less-than signs in the construction of √2
> 1.41 < √2 < 1.42
> 1.414 < √2 < 1.415
> 1.4142 < √2 < 1.4143
> 1.41421 < √2 < 1.41422
> 1.414213 < √2 < 1.414214
> ...
to at-most signs:
¥ 1.41 ≤ √2 ≤ 1.42
¥ 1.414 ≤ √2 ≤ 1.415
¥ 1.4142 ≤ √2 ≤ 1.4143
¥ 1.41421 ≤ √2 ≤ 1.41422
¥ 1.414213 ≤ √2 ≤ 1.414214
¥ ...

That way, instead of constructing a number ε such that
> 0 < ε < 1
> 0 < ε < 0.1
> 0 < ε < 0.01
> 0 < ε < 0.001
> ...
we get
¥ 0 ≤ ε ≤ 1
¥ 0 ≤ ε ≤ 0.1
¥ 0 ≤ ε ≤ 0.01
¥ 0 ≤ ε ≤ 0.001
¥ ...
which is satisfied by ε = 0.

And instead of constructing a number x such that
¥ 0 < x < 1
¥ 0.9 < x < 1
¥ 0.99 < x < 1
¥ 0.999 < x < 1
¥ ...,
which would be infinitesimally close to 1, and which would get us an infinitesimal number by just doing 1-x, we get
¥ 0 ≤ x ≤ 1
¥ 0.9 ≤ x ≤ 1
¥ 0.99 ≤ x ≤ 1
¥ 0.999 ≤ x ≤ 1
¥ ...
which is satisfied by x = 1.

This is how we've been modeling real numbers in this thread since >>8908 which has the full details.

>>11996
>They made use of a preexisting Java library to do the calculations:
>https://www.hboehm.info/crcalc/

I said that like they just used someone else's code, but on second look I see the guy who wrote that library is the author of the CACM paper. He developed it while he was working at SGI and then got hired by Google to work on Android stuff.

>>11942
>>11948
I've been thinking again about how to do hand arithmetic with infinite decimals, in this case division. I've tried this before, but my calculation of the error on the result at each step was an ugly and unmemorable formula. I think I've found a better way to think about the error on the result, which is to first work out the error on the remainder at each step. There are two contributions, one from the truncation error on the dividend, and one from the error on what's been subtracted from the dividend (due to truncation error on the divisor). Then the error bound on the result is
(|remainder| + |error on remainder|) / (lower bound on |divisor|).
You could also forgo taking the absolute value of the remainder and work out separately the error bounds in each direction, which could occasionally help squeeze out a digit of the quotient a bit earlier.

Moved to >>>/maho/113.