Irrationality of squares of real fourth roots and of integer combinations

For a nonnegative real number x, the square of the fourth root x ^ (1 / 4 : ℝ) is √x, so (x ^ (1 / 4 : ℝ)) ^ 2 is irrational if and only if √x is irrational (TauCeti.irrational_rpow_one_quarter_sq_iff). In particular, for any prime p — and specifically for p = 2 (TauCeti.irrational_two_rpow_one_quarter_sq) — the square of (p : ℝ) ^ (1 / 4 : ℝ) is irrational. This supplies the irrational-square condition Irrational (c ^ 2) for rank-one non-integral lattices c ℤ ⊆ ℝ such as 2 ^ (1 / 4) ℤ.

If θ₁ or θ₂ is irrational, an integer matrix of nonzero determinant cannot send (θ₁, θ₂) into ℚ²: for j ≠ 0 and a d - b c ≠ 0, j (a θ₁ + b θ₂) and j (c θ₁ + d θ₂) are not both integers (TauCeti.notMem_range_intCast_or_notMem_range_intCast_of_irrational). These are the twists of the powers and finite-cover pullbacks of a flat line over a torus with holonomy exp (2πiθ₁), exp (2πiθ₂).

Main statements

• TauCeti.irrational_rpow_one_quarter_sq_iff: for 0 ≤ x, Irrational ((x ^ (1 / 4 : ℝ)) ^ 2) ↔ Irrational √x.
• Nat.Prime.irrational_rpow_one_quarter_sq: for prime p, Irrational (((p : ℝ) ^ (1 / 4 : ℝ)) ^ 2).
• TauCeti.irrational_two_rpow_one_quarter_sq: Irrational (((2 : ℝ) ^ (1 / 4 : ℝ)) ^ 2).
• TauCeti.notMem_range_intCast_or_notMem_range_intCast_of_irrational: if θ₁ or θ₂ is irrational, j ≠ 0 and a d - b c ≠ 0, then j (a θ₁ + b θ₂) or j (c θ₁ + d θ₂) is not an integer.

theorem TauCeti.irrational_rpow_one_quarter_sq_iff {x : ℝ} (hx : 0 ≤ x) : Irrational ((x ^ (1 / 4)) ^ 2) ↔ Irrational √x

For a nonnegative real number x, the square of x ^ (1 / 4) equals √x and is therefore irrational if and only if √x is irrational. Nonnegativity cannot be dropped: at x = -2, ((-2) ^ (1 / 4)) ^ 2 = √2 / 2 is irrational whereas √(-2) = 0 is rational.

theorem Nat.Prime.irrational_rpow_one_quarter_sq {p : ℕ} (hp : Prime p) : Irrational ((↑p ^ (1 / 4)) ^ 2)

For a prime p, the square of (p : ℝ) ^ (1 / 4) is √p, hence irrational.

theorem TauCeti.irrational_two_rpow_one_quarter_sq : Irrational ((2 ^ (1 / 4)) ^ 2)

The square of 2 ^ (1 / 4 : ℝ) is √2, hence irrational.

theorem TauCeti.notMem_range_intCast_or_notMem_range_intCast_of_irrational {θ₁ θ₂ : ℝ} (hθ : Irrational θ₁ ∨ Irrational θ₂) {j a b c d : ℤ} (hj : j ≠ 0) (hdet : a * d - b * c ≠ 0) : ↑j * (↑a * θ₁ + ↑b * θ₂) ∉ Set.range Int.cast ∨ ↑j * (↑c * θ₁ + ↑d * θ₂) ∉ Set.range Int.cast

Powers and finite-cover pullbacks of a flat line with infinite holonomy are nontrivial. If θ₁ or θ₂ is irrational, then for every nonzero integer j and every integer matrix (a, b; c, d) of nonzero determinant, j (a θ₁ + b θ₂) and j (c θ₁ + d θ₂) are not both integers. These are the twists of the j-th power of the line with holonomy exp (2πiθ₁), exp (2πiθ₂) along the sublattice basis a ω₁ + b ω₂, c ω₁ + d ω₂.