Provably undecidable number inequality? Here is a question that popped into my head right as I fell asleep last night. 
I was thinking about constructions of irrational numbers, like pi. I was wondering if there are two constructions (any constructions, the pair doesn't have to include pi itself) such that:


*

*We have good reason to believe they are different numbers. 

*We have a demonstration that, if they are in fact different, then their difference must be small enough that there is no way we will ever find this difference. By this I mean, the number of calculations it would take to find the difference would take more computational resources than the energy of the Universe would allow.  


Heads up, I'm an amateur computer science enthusiast, and am neither a mathematician nor a physicist, but this question involves a mix of all three, so some of the phrasing might be awkward, and the whole question could be conceptually confused. If you think it is, please let me know!    
The inspiration for this question comes from reading about hash functions in software version control. It seems like one of the reasons that numbers are "useful" from a computational standpoint, is that they are easy to compare for equality. This probably has something to do with the ease with which they are placed in order. So the puzzle I was pondering was, if we know that numbers can be ordered by definition, do we also have numbers that we can't, in physical reality, put into an order? 
Is this question reducible to some incompleteness argument? Has it been asked before? Apologies if this is too open-ended a question for Math Overflow. Any and all suggestions would be greatly appreciated.   
 A: I think your question needs some clarification (in particular, what you mean by "find the difference"). Let $x$ be Chaitin's constant for some prefix-free universal computable function.


*

*We have good reason to believe $x$ and 0 are different numbers (because they are, in fact, different numbers).

*Their difference $x - 0$ is uncomputable, so in a sense we will never "find the difference". (A real number is computable iff its Dedekind cut is at level $\Delta_1$ of the arithmetical hierarchy.)
Another example: Let $x$ be a super-omega. Then $x - 0$ is not even limit-computable (i.e., in $\Delta_2$).
Another example: Fix an enumeration of first-order formulas that define arithmetical sets. Consider the real number $x \in [0, 1]$ whose $n$th binary digit after the decimal point is 1 iff $n$ is not in the set defined by the $n$th formula. Then $x - 0$ is not even arithmetical. (See here.)

Alternatively, we could use a construction analogous to Rayo's number: Fix a theory T. Let $\varepsilon$ be a positive real number smaller than any positive real number that can be named by an expression in the language of T with at most googolplex symbols. Then, by definition, there does not exist a positive real number $\delta$ that can be named by an expression with at most googolplex symbols which lower-bounds $\varepsilon$:
$$ 0 < \delta < \varepsilon$$
A: I think standard examples are like this ... Enumerate the cases of Goldbach's conjecture.  Let $a_n = 0$ if the $n$th case is true, and $a_n = 1$ if false.  Consider the number $A = \sum_{k=1}^\infty a_k 2^{-k}$ with the binary expansion $(a_n)$.  We may compute $A$ as accurately as we like.  But $A=0$ is equivalent to Goldbach's conjecture.
Repeat this with many other undecidable propositions instead of Goldbach.
