IsarMathLib

The goal of the Real_ZF series of theory files is to provide a contruction of the set of real numbers. There are several ways to construct real numbers. Most common start from the rational numbers and use Dedekind cuts or Cauchy sequences. Real_ZF_x.thy series formalizes an alternative approach that constructs real numbers directly from the group of integers. Our formalization is mostly based on \cite{Arthan2004}. Different variants of this contruction are also described in \cite{Campo2003} and \cite{Street2003}. I recommend to read these papers, but for the impatient here is a short description: we take a set of maps \(s : Z\rightarrow Z\) such that the set \(\{s(m+n)-s(m)-s(n)\}_{n,m \in Z}\) is finite (\(Z\) means the integers here). We call these maps slopes. Slopes form a group with the natural addition \((s+r)(n) = s(n)+r(n)\). The maps such that the set \(s(Z)\) is finite (finite range functions) form a subgroup of slopes. The additive group of real numbers is defined as the quotient group of slopes by the (sub)group of finite range functions. The multiplication is defined as the projection of the composition of slopes into the resulting quotient (coset) space.

This section contains the construction of the ring of real numbers as classes of slopes - integer almost homomorphisms. The real definitions are in Group_ZF_2 theory, here we just specialize the definitions of almost homomorphisms, their equivalence and operations to the additive group of integers from the general case of abelian groups considered in Group_ZF_2.

The set of slopes is defined as the set of almost homomorphisms on the additive group of integers.

The first operation on slopes (pointwise addition) is a special case of the first operation on almost homomorphisms.

The second operation on slopes (composition) is a special case of the second operation on almost homomorphisms.

Bounded integer maps are functions from integers to integers that have finite range. They play a role of zero in the set of real numbers we are constructing.

Bounded integer maps form a normal subgroup of slopes. The equivalence relation on slopes is the (group) quotient relation defined by this subgroup.

The set of real numbers is the set of equivalence classes of slopes.

The addition on real numbers is defined as the projection of pointwise addition of slopes on the quotient. This means that the additive group of real numbers is the quotient group: the group of slopes (with pointwise addition) defined by the normal subgroup of bounded integer maps.

Multiplication is defined as the projection of composition of slopes on the quotient. The fact that it works is probably the most surprising part of the construction.

We first show that we can use theorems proven in some proof contexts (locales). The locale group1 requires assumption that we deal with an abelian group. The next lemma allows to use all theorems proven in the context called group1.

Real numbers form a ring. This is a special case of the theorem proven in Ring_ZF_1.thy, where we show the same in general for almost homomorphisms rather than slopes.

We can use theorems proven in group0 and group1 contexts applied to the group of real numbers.

Let's define some notation.

In real0 context all theorems proven in the ring0, context are valid.

Lets try out our notation to see that zero and one are real numbers.

The lemma below lists some properties that require one real number to state.

The lemma below lists some properties that require two real numbers to state.

Multiplication of reals is associative.

Addition is distributive with respect to multiplication.

A simple rearrangement with four real numbers.

RealAddition is defined as the projection of the first operation on slopes (that is, slope addition) on the quotient (slopes divided by the "almost equal" relation. The next lemma plays with definitions to show that this is the same as the operation induced on the appriopriate quotient group. The names AH, Op1 and FR are used in group1 context to denote almost homomorphisms, the first operation on AH and finite range functions resp.

The symbol \( 0 \) in the real0 context is defined as the neutral element of real addition. The next lemma shows that this is the same as the neutral element of the appriopriate quotient group.

Zero is the class of any finite range function.

We will need a couple of results from Group_ZF_3.thy The first two that state that the definition of addition and multiplication of real numbers are consistent, that is the result does not depend on the choice of the slopes representing the numbers. The second one implies that what we call SlopeEquivalenceRel is actually an equivalence relation on the set of slopes. We also show that the neutral element of the multiplicative operation on reals (in short number \(1\)) is the class of the identity function on integers.

A one-side implication of the equivalence from Real_ZF_1_L10: the class of a bounded integer map is the real zero.

The next lemma is rephrases the result from Group_ZF_3.thy that says that the negative (the group inverse with respect to real addition) of the class of a slope is the class of that slope composed with the integer additive group inverse. The result and proof is not very readable as we use mostly generic set theory notation with long names here. Real_ZF_1.thy contains the same statement written in a more readable notation: \([-s] = -[s]\).

Two classes are equal iff the slopes that represent them are almost equal.

Identity function on integers is a slope. This lemma concludes the easy part of the construction that follows from the fact that slope equivalence classes form a ring. It is easy to see that multiplication of classes of almost homomorphisms is not commutative in general. The remaining properties of real numbers, like commutativity of multiplication and the existence of multiplicative inverses have to be proven using properties of the group of integers, rather that in general setting of abelian groups. This is done in the Real_ZF_1 theory.