임의의 유리수 e>0에 대해
x²<2<(x+e)²을 만족하는 유리수 x가 존재한다.

"실수"를 본격적으로 구성하기 전,
"유리수"까지만 구성한 시점에서
이 명제를 구성적으로 증명할 수 있나요?

즉,

임의의 유리수 e에 대해
x²<2<(x+e)²을 만족하는 유리수 x를
유리수 e에 대한 명시적인 함수꼴로 잡아줄 수 있나요?
"실수"를 구성하지 않은 상태에서요.

구성적 증명은 찾아봐도 안나오는 거 같은데

"구성적 증명이 불가능" 함이 증명 된 건지,
아직 "증명방법이 알려져있지 않은" 건지
궁금합니다.

- dc official App