Existence of irrational ^ irrational becomes rational

Stream: Is there code for X?

[Seewoo Lee]

There's a well known proof (using the law of excluded middle) which shows existence of $a \not\in\mathbb{Q}$ and $b \not\in\mathbb{Q}$ such that $a^b \in \mathbb{Q}$, using $\sqrt{2}^{\sqrt{2}}$ (I don't know the original reference, but here's an argument). I just wrote the proof yesterday, and realized that it is not in mathlib4 yet. So I may make PR for this, and I wonder if there are any comments for that.
One comment I got is that we also have $\sqrt{2}^{\log_{\sqrt{2}}(3)} = 3$ so that we don't need law of excluded middle (source) - although I haven't formalized this yet (but it shouldn't be hard).

[Junyan Xu]

There's one previous discussion of the first proof, and I'm surprised I couldn't find more ...

[Seewoo Lee]

FYI, here's a proof that hasn't golfed yet:

/-
Prove that there exists a, b ∉ ℚ such that a^b ∈ ℚ.

Here's a proof in natural language:

Consider c = √2^√2. If c is rational, we are done. If c is irrational, then c^√2 = 2 is rational, so we are done.
-/

import Mathlib.Algebra.Algebra.Rat
import Mathlib.Data.Real.Irrational
import Mathlib.Analysis.SpecialFunctions.Pow.Real

open Classical Real Set

-- Proof of irrationality of √2 already exists in mathlib.
theorem sqrt2_irrational : Irrational (√2) := irrational_sqrt_two

theorem sqrt2_pow_sqrt2_pow_sqrt2_eq_2 : (√2 ^ √2) ^ √2 = 2 := by
  have h2s : √2 * √2 = 2 := mul_self_sqrt (by norm_num)
  rw [← rpow_mul, h2s, rpow_two, sq_sqrt]
  norm_num
  exact sqrt_nonneg 2

theorem ne_irrational_eq_rational (a : ℝ) : ¬ Irrational a ↔ ∃ (q : ℚ), a = q := by
  constructor
  · intro h
    rw [Irrational, not_not, mem_range] at h
    obtain ⟨q, ha⟩ := h
    use q
    simp [ha]
  · rintro ⟨q, ha⟩ h
    rw [Irrational, mem_range] at h
    apply h
    use q
    simp [ha]

theorem exist_irrat_power_rat : ∃ a b : ℝ, Irrational a ∧ Irrational b
    ∧ ∃ (q : ℚ), a ^ b = q := by
  let c := √2 ^ √2
  by_cases hc : Irrational c
  · -- c is irrational
    use c, √2
    constructor
    · exact hc
    · constructor
      · exact sqrt2_irrational
      · use 2
        exact sqrt2_pow_sqrt2_pow_sqrt2_eq_2
  · -- c is rational
    use √2, √2
    constructor
    · exact sqrt2_irrational
    · constructor
      · exact sqrt2_irrational
      · rw [ne_irrational_eq_rational] at hc
        obtain ⟨q, hc⟩ := hc
        use q

[Matt Diamond]

import Mathlib

open Real

example : ∃ (a b : ℝ) (_ : Irrational a) (_ : Irrational b), ¬Irrational (a ^ b) :=
by
  by_cases h : Irrational (√2 ^ √2)
  · use √2 ^ √2, √2, h, irrational_sqrt_two, by simp [← rpow_mul (sqrt_nonneg _)]
  · use √2, √2, irrational_sqrt_two, irrational_sqrt_two, h

[Yury G. Kudryashov]

You should assume that a is positive (it's trivial), otherwise Mathlib definition of rpow is very strange.

[Matt Diamond]

oh, are you saying that a ^ b doesn't necessarily mean what we think it means unless we assume a is positive?

[Matt Diamond]

ah, I see docs#Real.rpow_def_of_neg ... good point

[Kevin Buzzard]

I guess that depends on what you think (-1)^(1/2) means!

[Jz Pan]

Seewoo Lee said:

so that we don't need law of excluded middle

But in mathlib, in order to define √2 we need to use axiom of choice anyway...

import Mathlib

open Real

noncomputable def test : ℝ := √2

-- 'test' depends on axioms: [propext, Classical.choice, Quot.sound]
#print axioms test

[Seewoo Lee]

Jz Pan 말함:

Seewoo Lee said:

so that we don't need law of excluded middle

But in mathlib, in order to define √2 we need to use axiom of choice anyway...

import Mathlib

open Real

noncomputable def test : ℝ := √2

-- 'test' depends on axioms: [propext, Classical.choice, Quot.sound]
#print axioms test

Oh I see.. where they use AC to define √2? I never realized this.

[Seewoo Lee]

Here's a slight modification of @Matt Diamond 's one with positivity assumption:

example : ∃ (a b : ℝ) (_: Irrational a) (_: Irrational b) (_: 0 < a),
    ¬Irrational (a ^ b) := by
  by_cases h : Irrational (√2 ^ √2)
  · use √2 ^ √2, √2, h, irrational_sqrt_two, NNReal.rpow_pos (by norm_num),
    (by rw [← rpow_mul, mul_self_sqrt (by norm_num), rpow_two]; norm_num; norm_num)
  · use √2, √2, irrational_sqrt_two, irrational_sqrt_two, by norm_num, h

[Kevin Buzzard]

Probably what's actually used is LEM but in lean this is proved using AC

[Daniel Weber]

Following the definition choice also comes from docs#StrictMono.orderIsoOfSurjective and docs#Real.toNNReal

[Seewoo Lee]

So back to my original question, if I willing to put this in mathlib, then I may consider it under Mathlib.Data.Real.Irrational - any other suggestions (or shouldn't I make PR?)

[Ruben Van de Velde]

I'm a bit confused - we (that is, the mathematical community excluding me) know which of those branches is true, right?

[Seewoo Lee]

Yes, $\sqrt{2}^{\sqrt{2}}$ is irrational by Gelfond-Schneider. So there are two things here:

• It might be better to use $\sqrt{2}^{2 \log_2 3} = 3$ instead of $(\sqrt{2}^{\sqrt{2}})^{\sqrt{2}} = 2$ since we don't need branch for the former.
• But also, the initial argument itself is pretty famous and good to be somewhere IMO (for archive purpose), so I'm not sure if $\sqrt{2}^{2 \log_2 3}$ is "better". One possibility is to add both but I should ask this first - are there any theorems in mathlib that are proven twice but with different proofs?

[Edward van de Meent]

imo, since this proof really is about giving a counterexample to build intuition, i'd say that the current (branching) proof is satisfactory for this purpose.

[Eric Wieser]

Do we actually want this result in Mathlib, or should it go in Counterexamples? It's not obvious to me that anything would ever use this theorem in it's current form.

[Eric Wieser]

But as a nice example it probably would be fine in Counterexamples or Archive

[Eric Wieser]

If in the former, I would expect the statement to be the equivalent:

theorem not_irrational_rpow : ¬ ∀ a b : ℝ, Irrational a → Irrational b → 0 < a → Irrational (a ^ b) := by

[Seewoo Lee]

Thanks! Here’s a PR.

[Violeta Hernández]

Nit but 0 < a can be replaced with 0 ≤ a

[Mario Carneiro]

Eric Wieser said:

If in the former, I would expect the statement to be the equivalent:

theorem not_irrational_rpow : ¬ ∀ a b : ℝ, Irrational a → Irrational b → 0 < a → Irrational (a ^ b) := by

which has the nice property of being intuitionistically provable (no LEM needed for the classic proof, if you ignore the LEM used in the current construction of the sqrt function)

[Eric Wieser]

Violeta Hernández said:

Nit but 0 < a can be replaced with 0 ≤ a

That makes the statement weaker not stronger

[Eric Wieser]

But this is also why counterexamples aren't great for Mathlib itself, as it's hard to decide when to stop adding extra characterizations to strengthen the example.

[Matt Diamond]

does allowing a to be 0 make a difference if 0 is already ruled out by the Irrational a assumption?