every other infinite set (what is left)

Statement not audited — only a problem’s root statement is audited for fidelity (D-9); the kernel checks a proof against this Lean as written.

import Mathlib
import Nodes.«erdos-257--h18».Context

/-! Hole `h_rest` of a merged partial proof, as a node (D-12 #5, D-29).
Statement generated by the gate from the assembly; immutable (D-3). -/

theorem erdos_257__h18 : ∀ (A : Set ℕ),
  A.Infinite →
    A = Set.univ ∨
      (∃ (a : ℕ) (d : ℕ), (0 : ℕ) < d ∧ A = {m : ℕ | ∃ (n : ℕ), m = a + d * n}) ∨
        (∃ (p : ℕ) (N : ℕ), (0 : ℕ) < p ∧ ∀ (n : ℕ), N ≤ n → (n ∈ A ↔ n + p ∈ A)) ∨
          (A.Pairwise Nat.Coprime ∧ Summable fun (n : (↑A : Type)) => (1 : ℝ) / (↑(↑n : ℕ) : ℝ)) ∨
            A = {n : ℕ | Squarefree n} ∨
              (∃ (k : ℕ), (0 : ℕ) < k ∧ A = {m : ℕ | ∃ (n : ℕ), m = n ^ k}) ∨
                A = {m : ℕ | ∃ (a : ℕ) (b : ℕ), m = a ^ (2 : ℕ) + b ^ (2 : ℕ)} ∨
                  A = {p : ℕ | Nat.Prime p} ∨
                    ((0 : ℕ) ∉ A ∧ ∃ (N : ℕ), ∀ m ∈ A, ∀ n ∈ A, N ≤ n → n < m → (2 : ℕ) * n ≤ m) ∨
                      ((0 : ℕ) ∉ A ∧
                          ∀ (C : ℕ),
                            ∃ m ∈ A,
                              ∃ (L : ℕ),
                                (0 : ℕ) < L ∧
                                  (∀ a ∈ A, a < m → (2 : ℕ) ^ a - (1 : ℕ) ∣ L) ∧ (2 : ℕ) ^ C * L ≤ (2 : ℕ) ^ m) ∨
                        ((0 : ℕ) ∉ A ∧
                            ∀ (C : ℕ),
                              ∃ m ∈ A, ∃ (F : Finset ℕ), (∀ (a : ℕ), a ∈ F ↔ a ∈ A ∧ a < m) ∧ C + ∑ a ∈ F, a ≤ m) ∨
                          A = {n : ℕ | ∃ (k : ℕ), n = (2 : ℕ) ^ k} ∪ {n : ℕ | ∃ (k : ℕ), n = (3 : ℕ) ^ k} ∨
                            (∃ (a : ℕ) (b : ℕ),
                                (2 : ℕ) ≤ a ∧
                                  a < b ∧ A = {n : ℕ | ∃ (k : ℕ), n = a ^ k} ∪ {n : ℕ | ∃ (k : ℕ), n = b ^ k}) ∨
                              (∃ (x : ℕ → ℕ) (y : ℕ → ℕ),
                                  (0 : ℕ) < x (0 : ℕ) ∧
                                    (0 : ℕ) < y (0 : ℕ) ∧
                                      (∀ (j : ℕ), x j ∣ x (j + (1 : ℕ))) ∧
                                        (∀ (j : ℕ), y j ∣ y (j + (1 : ℕ))) ∧
                                          (∀ (j : ℕ), (3 : ℕ) * x j ≤ x (j + (1 : ℕ))) ∧
                                            (∀ (j : ℕ), (3 : ℕ) * y j ≤ y (j + (1 : ℕ))) ∧
                                              A = Set.range x ∪ Set.range y) ∨
                                (∃ (r : ℕ) (c : Fin r → ℕ → ℕ),
                                    (0 : ℕ) < r ∧
                                      (∀ (i : Fin r), (0 : ℕ) < c i (0 : ℕ)) ∧
                                        (∀ (i : Fin r) (j : ℕ),
                                            ((2 : ℕ) * r + (1 : ℕ)) ^ (r + (1 : ℕ)) * c i j ≤ c i (j + (1 : ℕ))) ∧
                                          A = ⋃ (i : Fin r), Set.range (c i)) ∨
                                  Irrational (∑' (n : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ))) := by
  sorry

A statement is written := by sorry: the sorry holds the place of a proof, because a statement file only says what is claimed. A proof the gate checked is its own file, Proof.lean. How to read a proof page →

@@ -1,3 +1,21 @@
-$$A \text{ infinite} \Rightarrow A \in \mathcal{C}_1 \cup \cdots \cup \mathcal{C}_{15} \lor \sum_{n \in A} \frac{1}{2^n - 1} \notin \mathbb{Q}$$
+$$A \subseteq \mathbb{N} \text{ infinite} \Rightarrow A \in \mathcal{C}_1 \cup \cdots \cup \mathcal{C}_{15} \ \lor\ \sum_{n \in A} \frac{1}{2^n - 1} \notin \mathbb{Q}$$
 
-The fifteen classes are those of the holes above, in order; an infinite A in none of them has an irrational sum. Stated positively, as a disjunction, so that it can be witnessed.
+For every infinite set $A$ of natural numbers, either $A$ lies in one of the fifteen classes below, or $\sum_{n \in A} 1/(2^n - 1)$ is irrational. Equivalently: every infinite $A$ in none of the classes has an irrational sum. The classes are the special cases of Erdős 257 already on the graph, each a lemma of the root:
+
+1. $A = \mathbb{N}$;
+2. $A = \{a + dn : n \ge 0\}$ for some $a \ge 0$, $d \ge 1$;
+3. $A$ eventually periodic: for some $p \ge 1$ and $N$, $n \in A \iff n + p \in A$ for all $n \ge N$;
+4. $A$ pairwise coprime with $\sum_{a \in A} 1/a < \infty$;
+5. $A$ = the squarefree numbers;
+6. $A = \{n^k : n \ge 0\}$ for some $k \ge 1$;
+7. $A$ = the sums of two squares $\{a^2 + b^2\}$;
+8. $A$ = the primes;
+9. $0 \notin A$ and, for some $N$, $n < m$ in $A$ with $n \ge N$ implies $m \ge 2n$;
+10. $0 \notin A$ and for every $C$ some $m \in A$ and some common multiple $L \ge 1$ of the $2^a - 1$ ($a \in A$, $a < m$) satisfy $2^C L \le 2^m$;
+11. $0 \notin A$ and for every $C$ some $m \in A$ satisfies $m \ge C + \sum_{a \in A,\, a < m} a$;
+12. $A = \{2^k\} \cup \{3^k\}$;
+13. $A = \{a^k\} \cup \{b^k\}$ for some $2 \le a < b$;
+14. $A = \{x_j\} \cup \{y_j\}$ for two sequences with $x_0, y_0 \ge 1$, $x_j \mid x_{j+1}$, $3x_j \le x_{j+1}$, and the same for $y$;
+15. $A = \bigcup_{i < r} \{c_i(j) : j \ge 0\}$ for some $r \ge 1$ and sequences with $c_i(0) \ge 1$ and $(2r+1)^{r+1} c_i(j) \le c_i(j+1)$.
+
+Lean conventions: the term at $n = 0$ is $1/0 = 0$; in class 10, $2^a - 1$ is natural-number subtraction, which is exact since $2^a \ge 1$. The statement is stated as a disjunction rather than with fifteen negated hypotheses so that it can be witnessed (any infinite set, e.g. $\mathbb{N}$, meets its one hypothesis).

Rendered from targets/erdos-257/nodes/erdos-257--h18/Statement.lean. Origin: compiler-derived.

1 recorded. Routes refuted: none. Failure classes: budget-exhausted 1.

No partial assembly filed.

How to read a statement’s page →