Arithmetic of powers of three

The four-point catalogue reduces to a handful of Diophantine facts about powers of three. This file isolates them. Everything is stated over ℤ; the geometric files produce the corresponding real equations and transfer them by exact_mod_cast.

theorem Erdos132ThreeChain.one_le_pow3 (n : ℕ) : 1 ≤ 3 ^ n

theorem Erdos132ThreeChain.pow3_pos (n : ℕ) : 0 < 3 ^ n

theorem Erdos132ThreeChain.three_le_pow3 {n : ℕ} (h : n ≠ 0) : 3 ≤ 3 ^ n

theorem Erdos132ThreeChain.three_dvd_pow3 {n : ℕ} (h : n ≠ 0) : 3 ∣ 3 ^ n

theorem Erdos132ThreeChain.nine_dvd_pow3 {n : ℕ} (h : 2 ≤ n) : 9 ∣ 3 ^ n

theorem Erdos132ThreeChain.pow3_inj {m n : ℕ} (h : 3 ^ m = 3 ^ n) : m = n

theorem Erdos132ThreeChain.pow3_trichotomy (n : ℕ) : 3 ^ n = 1 ∨ 3 ^ n = 3 ∨ 9 ≤ 3 ^ n

A power of three is 1, is 3, or is at least 9.

theorem Erdos132ThreeChain.pow3_eq_four_mul_pow3_sub_one {j l : ℕ} (h : 3 ^ l = 4 * 3 ^ j - 1) : j = 0 ∧ l = 1

4 * 3 ^ j - 1 is a power of three only in the trivial instance 4 - 1 = 3.

theorem Erdos132ThreeChain.one_le_pow3R (n : ℕ) : 1 ≤ 3 ^ n

theorem Erdos132ThreeChain.three_le_pow3R {n : ℕ} (h : n ≠ 0) : 3 ≤ 3 ^ n

theorem Erdos132ThreeChain.nine_le_pow3R {n : ℕ} (h : 2 ≤ n) : 9 ≤ 3 ^ n

theorem Erdos132ThreeChain.exp_tri {c : ℝ} (hc : 0 < c) {p q r : ℕ} (hpq : p ≤ q) (hqr : q ≤ r) (h : (c * 3 ^ r - c * 3 ^ p - c * 3 ^ q) ^ 2 ≤ 4 * (c * 3 ^ p) * (c * 3 ^ q)) : r = q ∨ p = q ∧ r = p + 1

Exponent rigidity of a chain triangle. If a triangle has squared sides c * 3 ^ p, c * 3 ^ q, c * 3 ^ r with p ≤ q ≤ r, then either the two largest exponents agree, or the two smallest agree and the largest exceeds them by exactly one.

theorem Erdos132ThreeChain.isoceles_pair_solution {j k l : ℕ} (hjk : j ≤ k) (hcase : j = k ∨ l = j ∧ k = j + 1 ∨ l = k) (heq : 3 ^ j * 3 ^ j + 3 ^ k * 3 ^ k + 3 ^ l * 3 ^ l - 2 * (3 ^ j * 3 ^ k) - 2 * (3 ^ j * 3 ^ l) - 2 * (3 ^ k * 3 ^ l) + 3 ^ l = 0) : j = 0 ∧ k = 0 ∧ l = 1

The four-point equation for two points equidistant from the ends of the shortest edge.

theorem Erdos132ThreeChain.mixed_pair_solution {j l : ℕ} (heq : (3 ^ j - 3 ^ l) ^ 2 - 3 * 3 ^ l + 3 = 0) : j = 0 ∧ l = 0

The four-point equation for one point equidistant from the ends of the shortest edge and one point spanning it.

theorem Erdos132ThreeChain.pow3_ne_four {l : ℕ} : 3 ^ l ≠ 4

theorem Erdos132ThreeChain.pow3_ne_seven {l : ℕ} : 3 ^ l ≠ 7