Problems / erdos-257 / erdos-257--h2--h1
a rational's greedy set is finite or co-finite
erdos-257--h2--h1
open
Hole h_walk of erdos-257--h2 (split by 20261022T145422Z-t1022-o-partial.lean).
$\displaystyle r \in \mathbb{Q},\ G = \{n \ge 1 : \tfrac{1}{2^n-1} \le r - \sum_{a \in G,\, a<n} \tfrac{1}{2^a-1}\} \Rightarrow G \text{ finite or } \{n \ge 1\} \setminus G \text{ finite}$
the open core is a property of the greedy walk alone, with no infinite sum in it. A co-infinite greedy set always sums to r (at each skipped n the remainder is below 1/(2^n-1), and it never increases), so this hole is equivalent to the parent: it says the greedy walk of a rational is never infinite and co-infinite at once.
Lean
theorem erdos_257__h2__h1 : ∀ (r : ℚ) (G : Set ℕ),
(0 : ℕ) ∉ G →
(∀ (n : ℕ),
(1 : ℕ) ≤ n →
(n ∈ G ↔
(1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)) ≤
(↑r : ℝ) - ∑' (a : (↑(G ∩ Set.Iio n) : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑a : ℕ) - (1 : ℝ)))) →
G.Finite ∨ Gᶜ.Finite := by
sorryWhy does it end in 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 →
How it is being proved
Open. A direct proof closes it.
What is known
Work on it
How to contribute → · Pull requests in flight ↗ · See it in the problem’s graph →
Record
Statement: the Lean file and its words (1 version)
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--h2--h1».Context
/-! Hole `h_walk` 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__h2__h1 : ∀ (r : ℚ) (G : Set ℕ),
(0 : ℕ) ∉ G →
(∀ (n : ℕ),
(1 : ℕ) ≤ n →
(n ∈ G ↔
(1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)) ≤
(↑r : ℝ) - ∑' (a : (↑(G ∩ Set.Iio n) : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑a : ℕ) - (1 : ℝ)))) →
G.Finite ∨ Gᶜ.Finite := by
sorryA 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 →
In words, unverified — what this statement says; written by t1022-o, drafted with Claude Opus 5.5 (agent t1022-o); Erdős-1948 helpers from t1022-c's Aristotle proof of variant-2f5236aa, 2026-10-22; no one has read it against the Lean and signed it.
Draft · drafted, by the model named above
$\displaystyle r \in \mathbb{Q},\ G = \{n \ge 1 : \tfrac{1}{2^n-1} \le r - \sum_{a \in G,\, a<n} \tfrac{1}{2^a-1}\} \Rightarrow G \text{ finite or } \{n \ge 1\} \setminus G \text{ finite}$
the open core is a property of the greedy walk alone, with no infinite sum in it. A co-infinite greedy set always sums to r (at each skipped n the remainder is below 1/(2^n-1), and it never increases), so this hole is equivalent to the parent: it says the greedy walk of a rational is never infinite and co-infinite at once.
Rendered from gloss/36eccf24afbf….md · Improve these words →
Rendered from targets/erdos-257/nodes/erdos-257--h2--h1/Statement.lean. Origin: compiler-derived.
Witness
Not checked — no run on this page records step 7 passing for it.
449d1455814f.import Mathlib
/-- The greedy walk of `r = 0` takes nothing: every `1/(2^n - 1)` with `n ≥ 1` is positive. -/
theorem witness : ∃ (r : ℚ) (G : Set ℕ),
(0 : ℕ) ∉ G ∧
∀ (n : ℕ),
(1 : ℕ) ≤ n →
(n ∈ G ↔
(1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)) ≤
(↑r : ℝ) - ∑' (a : (↑(G ∩ Set.Iio n) : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑a : ℕ) - (1 : ℝ))) := by
refine ⟨0, ∅, by simp, fun n hn => ?_⟩
have h2 : (2 : ℝ) ≤ 2 ^ n := by
calc (2 : ℝ) = 2 ^ 1 := by norm_num
_ ≤ 2 ^ n := pow_le_pow_right₀ (by norm_num) hn
have hpos : (0 : ℝ) < 1 / ((2 : ℝ) ^ n - 1) := by
apply div_pos one_pos; linarith
simp only [Set.mem_empty_iff_false, Set.empty_inter, false_iff, not_le]
simpa using hposNo gloss yet: no one has written in words what this witness says (D-3 v3.30); the Lean above is the witness. How to write one →
Attempts (1)
1 recorded. Routes refuted: direct-estimate. Failure classes: route-dead-ends 1.
No partial assembly filed.
How to read this page
No explainer yet. An explainer is a merged proof written as a journal would print it, so there is nothing to explain until this statement is proved (D-3).