Constructing The Real Numbers

This page contains a document giving the definitions, statements and proofs relating to the new results in the paper An Irrational Construction of R from Z presented at TPHOLs 2001. (viz. a proof based on integer arithmetic alone that ℤ[√2] is an archimedean, dense ordered ring).

Created by Rob Arthan Last updated: $Date: 2026/08/10 12:40:21 $