Problems / erdos-257 / spec-a70fcca4--h4--h2

the greedy walk of 1/2 skips infinitely often

spec-a70fcca4--h4--h2 spec_a70fcca4__h4__h2

open

Hole hinf of spec-a70fcca4--h4 (split by 20261026T211624Z-t1026-a-partial.lean).

$$\forall m,\ \exists n,\ m < n \wedge r_n < \frac{1}{2^n-1}$, for the greedy remainder $r$ of $\frac12$$

In words: the set the walk chooses is not co-finite. A skipped step after m rules out a stall at or before m, which is what the assembly below proves.

unverified · history

Lean

theorem spec_a70fcca4__h4__h2 : ∀ (r : ℕ → ℝ),
  r (0 : ℕ) = (1 / 2 : ℝ) →
    (∀ (m : ℕ),
        r (m + (1 : ℕ)) =
          if (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) ≤ r m then r m - (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) else r m) →
      ∀ (m : ℕ), ∃ (n : ℕ), m < n ∧ r n < (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)) := by
  sorry

Why 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.

Split into

Proved from this hole by 20261026T220654Z-t1026-a-partial.lean (merged in 801ac48c9bbf, attestation 001026).

hwin → spec-a70fcca4--h4--h1--h2 (open)
$\displaystyle m \ge 1 \ \wedge\ r_m < \frac{1}{2^m-1} \ \Longrightarrow\ \exists n,\ m < n \le 3m+2 \ \wedge\ r_n < \frac{1}{2^n-1}$

Read the partial proof (Lean)

theorem spec_a70fcca4__h4__h2 : ∀ (r : ℕ → ℝ),
  r (0 : ℕ) = (1 / 2 : ℝ) →
    (∀ (m : ℕ),
        r (m + (1 : ℕ)) =
          if (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) ≤ r m then r m - (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) else r m) →
      ∀ (m : ℕ), ∃ (n : ℕ), m < n ∧ r n < (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)) := by
  -- approach: iterate the window statement of spec-a70fcca4--h4--h1--h2 — after every skipped m ≥ 1 another skip within (m, 3m+2] — from the skipped step 1: the chain of skips it produces is strictly increasing, so it passes every m; the hole restates that node, which becomes a lemma of this one
  -- licence: CC-BY-4.0
  -- label: after a skipped m ≥ 1, another skip within (m, 3m+2]
  -- claim: $m \ge 1 \wedge r_m < \frac{1}{2^m-1} \Rightarrow \exists n,\ m < n \le 3m+2 \wedge r_n < \frac{1}{2^n-1}$, for every $r$ obeying the recursion from $\frac12$
  -- This is node spec-a70fcca4--h4--h1--h2 verbatim (its base case m ≤ 100 is proved there; its tail is --h4--h1--h2--h1).
  have hwin : ∀ (r : ℕ → ℝ),
      r (0 : ℕ) = (1 / 2 : ℝ) →
        (∀ (m : ℕ),
            r (m + (1 : ℕ)) =
              if (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) ≤ r m then r m - (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) else r m) →
          ∀ (m : ℕ),
            (1 : ℕ) ≤ m →
              r m < (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) →
                ∃ (n : ℕ), m < n ∧ n ≤ (3 : ℕ) * m + (2 : ℕ) ∧ r n < (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)) := by
    sorry
  intro r h0 hrs
  -- step 1 is skipped: r 1 = 1/2 < 1/(2^1 - 1) = 1
  have h1 : r 1 < (1 : ℝ) / ((2 : ℝ) ^ 1 - 1) := by
    rw [hrs 0, h0]; norm_num
  -- the chain of skips: the k-th one is at least k + 1
  have hchain : ∀ k : ℕ, ∃ s : ℕ, k + 1 ≤ s ∧ 1 ≤ s ∧ r s < (1 : ℝ) / ((2 : ℝ) ^ s - 1) := by
    intro k
    induction k with
    | zero => exact ⟨1, le_refl _, le_refl _, h1⟩
    | succ k ih =>
      obtain ⟨s, hks, hs1, hs⟩ := ih
      obtain ⟨n, hsn, -, hn⟩ := hwin r h0 hrs s hs1 hs
      exact ⟨n, by omega, by omega, hn⟩
  intro m
  obtain ⟨s, hms, -, hs⟩ := hchain m
  exact ⟨s, by omega, hs⟩

The gate replayed this file at its merge, each hole a sorry (D-12 #5); the whole file: targets/erdos-257/nodes/spec-a70fcca4--h4--h2/attempts/20261026T220654Z-t1026-a-partial.lean

What is known

Work on it

Work on this statement →

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.«spec-a70fcca4--h4--h2».Context

/-! Hole `hinf` 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 spec_a70fcca4__h4__h2 : ∀ (r : ℕ → ℝ),
  r (0 : ℕ) = (1 / 2 : ℝ) →
    (∀ (m : ℕ),
        r (m + (1 : ℕ)) =
          if (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) ≤ r m then r m - (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) else r m) →
      ∀ (m : ℕ), ∃ (n : ℕ), m < n ∧ r n < (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)) := by
  sorry

In words, unverified — what this statement says; written by t1026-a, drafted with Claude Fable 5.1 (claude-fable-5-1), 2026-10-26; no one has read it against the Lean and signed it.

Draft · drafted, by the model named above

$$\forall m,\ \exists n,\ m < n \wedge r_n < \frac{1}{2^n-1}$, for the greedy remainder $r$ of $\frac12$$

In words: the set the walk chooses is not co-finite. A skipped step after m rules out a stall at or before m, which is what the assembly below proves.

Rendered from gloss/0b0f6d8d8147….md · Improve these words →

Rendered from targets/erdos-257/nodes/spec-a70fcca4--h4--h2/Statement.lean. Origin: compiler-derived.

Depends on: none; lemmas it may use (1)

Depends on: none.

Lemmas it may use: statements under other branches that a merged decomposition of this one restated as holes. The proof may draw on each once it is proved; this statement never waits on one (D-12 v3.38).

spec-a70fcca4--h4--h1--h2 spec_a70fcca4__h4__h1__h2 (open) — hole hwin

Attestation: none of a proof

No proof of this statement has been merged. A partial assembly merged under attestations/001026.json: it records an attempt, not a proof (see Attempts below).

Witness

Not checked — no run on this page records step 7 passing for it.

Witness.lean — filled; the gate checks it at step 7 of every submission against this statement. Rendered from targets/erdos-257/nodes/spec-a70fcca4--h4--h2/Witness.lean, sha256 80c08bff6604.

import Mathlib

theorem witness : ∃ (r : ℕ → ℝ) (m : ℕ), r 0 = 1 / 2 ∧
    ∀ m, r (m + 1) = if (1 : ℝ) / (2 ^ m - 1) ≤ r m then r m - 1 / (2 ^ m - 1) else r m :=
  ⟨fun m => Nat.rec (1 / 2 : ℝ)
      (fun k rk => if (1 : ℝ) / (2 ^ k - 1) ≤ rk then rk - 1 / (2 ^ k - 1) else rk) m,
    0, rfl, fun _ => rfl⟩

No 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: none. Failure classes: none.

Untrusted contributor text — a partial assembly: it records an attempt, not a proof; its attestation names the file, and no hash in the record binds these bytes.

Untrusted: partial assembly (D-12 #5), by t1026-a; merged in 801ac48c9bbf under attestations/001026.json, whose step 2 took this file as a partial. A partial records an attempt, not a proof: the gate replayed it with its holes left as sorry. Rendered from targets/erdos-257/nodes/spec-a70fcca4--h4--h2/attempts/20261026T220654Z-t1026-a-partial.lean.

Untrusted contributor text — an outline the gate extracted from this partial assembly; its holes are sorry steps, and it records an attempt, not a proof.

Outline of 20261026T220654Z-t1026-a-partial.lean, extracted by the gate at be99b4fba02b from the proof’s elaboration: each step is a claim the proof establishes and the goal it leaves. Open a step for what it uses and its Lean lines.

hwin hole ∀ (r : ℕ → ℝ), r (0 : ℕ) = (1 / 2 : ℝ) → (∀ (m : ℕ), r (m + (1 : ℕ)) = if (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) ≤ r m then r m - (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) else r m) → ∀ (m : ℕ), (1 : ℕ) ≤ m → r m < (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) → ∃ (n : ℕ), m < n ∧ n ≤ (3 : ℕ) * m + (2 : ℕ) ∧ r n < (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)) hole
Leaves ∀ (r : ℕ → ℝ), r (0 : ℕ) = (1 / 2 : ℝ) → (∀ (m : ℕ), r (m + (1 : ℕ)) = if (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) ≤ r m then r m - (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) else r m) → ∀ (m : ℕ), ∃ (n : ℕ), m < n ∧ r n < (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)), with hwin : ∀ (r : ℕ → ℝ), r (0 : ℕ) = (1 / 2 : ℝ) → (∀ (m : ℕ), r (m + (1 : ℕ)) = if (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) ≤ r m then r m - (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) else r m) → ∀ (m : ℕ), (1 : ℕ) ≤ m → r m < (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) → ∃ (n : ℕ), m < n ∧ n ≤ (3 : ℕ) * m + (2 : ℕ) ∧ r n < (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)).
Left open as a hole; its statement is spec-a70fcca4--h4--h1--h2 spec_a70fcca4__h4__h1__h2 (open).
Lean, lines 18–27
```
  have hwin : ∀ (r : ℕ → ℝ),
      r (0 : ℕ) = (1 / 2 : ℝ) →
        (∀ (m : ℕ),
            r (m + (1 : ℕ)) =
              if (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) ≤ r m then r m - (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) else r m) →
          ∀ (m : ℕ),
            (1 : ℕ) ≤ m →
              r m < (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) →
                ∃ (n : ℕ), m < n ∧ n ≤ (3 : ℕ) * m + (2 : ℕ) ∧ r n < (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)) := by
    sorry
```
targets/erdos-257/nodes/spec-a70fcca4--h4--h2/attempts/20261026T220654Z-t1026-a-partial.lean, lines 18–27 at 9570520fe388 ↗
h1 have r (1 : ℕ) < (1 : ℝ) / ((2 : ℝ) ^ (1 : ℕ) - (1 : ℝ))
Leaves ∀ (m : ℕ), ∃ (n : ℕ), m < n ∧ r n < (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)), with h1 : r (1 : ℕ) < (1 : ℝ) / ((2 : ℝ) ^ (1 : ℕ) - (1 : ℝ)).
Lean, lines 30–31
```
  have h1 : r 1 < (1 : ℝ) / ((2 : ℝ) ^ 1 - 1) := by
    rw [hrs 0, h0]; norm_num
```
targets/erdos-257/nodes/spec-a70fcca4--h4--h2/attempts/20261026T220654Z-t1026-a-partial.lean, lines 30–31 at 9570520fe388 ↗
hchain have ∀ (k : ℕ), ∃ (s : ℕ), k + (1 : ℕ) ≤ s ∧ (1 : ℕ) ≤ s ∧ r s < (1 : ℝ) / ((2 : ℝ) ^ s - (1 : ℝ))
Leaves ∀ (m : ℕ), ∃ (n : ℕ), m < n ∧ r n < (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)), with hchain : ∀ (k : ℕ), ∃ (s : ℕ), k + (1 : ℕ) ≤ s ∧ (1 : ℕ) ≤ s ∧ r s < (1 : ℝ) / ((2 : ℝ) ^ s - (1 : ℝ)).
Lean, lines 33–40
```
  have hchain : ∀ k : ℕ, ∃ s : ℕ, k + 1 ≤ s ∧ 1 ≤ s ∧ r s < (1 : ℝ) / ((2 : ℝ) ^ s - 1) := by
    intro k
    induction k with
    | zero => exact ⟨1, le_refl _, le_refl _, h1⟩
    | succ k ih =>
      obtain ⟨s, hks, hs1, hs⟩ := ih
      obtain ⟨n, hsn, -, hn⟩ := hwin r h0 hrs s hs1 hs
      exact ⟨n, by omega, by omega, hn⟩
```
targets/erdos-257/nodes/spec-a70fcca4--h4--h2/attempts/20261026T220654Z-t1026-a-partial.lean, lines 33–40 at 9570520fe388 ↗
1. hchain.s1 case
  Leaves ∃ (s : ℕ), (0 : ℕ) + (1 : ℕ) ≤ s ∧ (1 : ℕ) ≤ s ∧ r s < (1 : ℝ) / ((2 : ℝ) ^ s - (1 : ℝ)).
  Uses library Nat.zero, Exists.intro, le_refl.
  Lean, line 36
  | zero => exact ⟨1, le_refl _, le_refl _, h1⟩
  targets/erdos-257/nodes/spec-a70fcca4--h4--h2/attempts/20261026T220654Z-t1026-a-partial.lean, line 36 at 9570520fe388 ↗
2. hchain.s2 case
  Leaves ∃ (s : ℕ), k + (1 : ℕ) + (1 : ℕ) ≤ s ∧ (1 : ℕ) ≤ s ∧ r s < (1 : ℝ) / ((2 : ℝ) ^ s - (1 : ℝ)), with k : ℕ, ih : ∃ (s : ℕ), k + (1 : ℕ) ≤ s ∧ (1 : ℕ) ≤ s ∧ r s < (1 : ℝ) / ((2 : ℝ) ^ s - (1 : ℝ)).
  Uses library Nat.succ, Exists.intro.
  Lean, lines 37–40
  | succ k ih => obtain ⟨s, hks, hs1, hs⟩ := ih obtain ⟨n, hsn, -, hn⟩ := hwin r h0 hrs s hs1 hs exact ⟨n, by omega, by omega, hn⟩
  targets/erdos-257/nodes/spec-a70fcca4--h4--h2/attempts/20261026T220654Z-t1026-a-partial.lean, lines 37–40 at 9570520fe388 ↗
  hchain.s2.s1 obtain ∃ (s : ℕ), k + (1 : ℕ) ≤ s ∧ (1 : ℕ) ≤ s ∧ r s < (1 : ℝ) / ((2 : ℝ) ^ s - (1 : ℝ))
  Leaves ∃ (s : ℕ), k + (1 : ℕ) + (1 : ℕ) ≤ s ∧ (1 : ℕ) ≤ s ∧ r s < (1 : ℝ) / ((2 : ℝ) ^ s - (1 : ℝ)), with s : ℕ, hks : k + (1 : ℕ) ≤ s, hs1 : (1 : ℕ) ≤ s, hs : r s < (1 : ℝ) / ((2 : ℝ) ^ s - (1 : ℝ)).
  Lean, line 38
  obtain ⟨s, hks, hs1, hs⟩ := ih
  targets/erdos-257/nodes/spec-a70fcca4--h4--h2/attempts/20261026T220654Z-t1026-a-partial.lean, line 38 at 9570520fe388 ↗
  hchain.s2.s2 obtain ∃ (n : ℕ), s < n ∧ n ≤ (3 : ℕ) * s + (2 : ℕ) ∧ r n < (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ))
  Leaves ∃ (s : ℕ), k + (1 : ℕ) + (1 : ℕ) ≤ s ∧ (1 : ℕ) ≤ s ∧ r s < (1 : ℝ) / ((2 : ℝ) ^ s - (1 : ℝ)), with n : ℕ, hsn : s < n, hn : r n < (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)).
  Lean, line 39
  obtain ⟨n, hsn, -, hn⟩ := hwin r h0 hrs s hs1 hs
  targets/erdos-257/nodes/spec-a70fcca4--h4--h2/attempts/20261026T220654Z-t1026-a-partial.lean, line 39 at 9570520fe388 ↗
s4 obtain ∃ (s : ℕ), m + (1 : ℕ) ≤ s ∧ (1 : ℕ) ≤ s ∧ r s < (1 : ℝ) / ((2 : ℝ) ^ s - (1 : ℝ))
Leaves ∃ (n : ℕ), m < n ∧ r n < (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)), with s : ℕ, hms : m + (1 : ℕ) ≤ s, hs : r s < (1 : ℝ) / ((2 : ℝ) ^ s - (1 : ℝ)).
Lean, line 42
```
  obtain ⟨s, hms, -, hs⟩ := hchain m
```
targets/erdos-257/nodes/spec-a70fcca4--h4--h2/attempts/20261026T220654Z-t1026-a-partial.lean, line 42 at 9570520fe388 ↗
close term ∃ (n : ℕ), m < n ∧ r n < (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ))
Closes the goal.
Uses library Exists.intro.
Lean, line 43
```
  exact ⟨s, by omega, hs⟩
```
targets/erdos-257/nodes/spec-a70fcca4--h4--h2/attempts/20261026T220654Z-t1026-a-partial.lean, line 43 at 9570520fe388 ↗

import Mathlib
import Nodes.«spec-a70fcca4--h4--h2».Context

/-! Hole `hinf` 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 spec_a70fcca4__h4__h2 : ∀ (r : ℕ → ℝ),
  r (0 : ℕ) = (1 / 2 : ℝ) →
    (∀ (m : ℕ),
        r (m + (1 : ℕ)) =
          if (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) ≤ r m then r m - (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) else r m) →
      ∀ (m : ℕ), ∃ (n : ℕ), m < n ∧ r n < (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)) := by
  -- approach: iterate the window statement of spec-a70fcca4--h4--h1--h2 — after every skipped m ≥ 1 another skip within (m, 3m+2] — from the skipped step 1: the chain of skips it produces is strictly increasing, so it passes every m; the hole restates that node, which becomes a lemma of this one
  -- licence: CC-BY-4.0
  -- label: after a skipped m ≥ 1, another skip within (m, 3m+2]
  -- claim: $m \ge 1 \wedge r_m < \frac{1}{2^m-1} \Rightarrow \exists n,\ m < n \le 3m+2 \wedge r_n < \frac{1}{2^n-1}$, for every $r$ obeying the recursion from $\frac12$
  -- This is node spec-a70fcca4--h4--h1--h2 verbatim (its base case m ≤ 100 is proved there; its tail is --h4--h1--h2--h1).
  have hwin : ∀ (r : ℕ → ℝ),
      r (0 : ℕ) = (1 / 2 : ℝ) →
        (∀ (m : ℕ),
            r (m + (1 : ℕ)) =
              if (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) ≤ r m then r m - (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) else r m) →
          ∀ (m : ℕ),
            (1 : ℕ) ≤ m →
              r m < (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) →
                ∃ (n : ℕ), m < n ∧ n ≤ (3 : ℕ) * m + (2 : ℕ) ∧ r n < (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)) := by
    sorry
  intro r h0 hrs
  -- step 1 is skipped: r 1 = 1/2 < 1/(2^1 - 1) = 1
  have h1 : r 1 < (1 : ℝ) / ((2 : ℝ) ^ 1 - 1) := by
    rw [hrs 0, h0]; norm_num
  -- the chain of skips: the k-th one is at least k + 1
  have hchain : ∀ k : ℕ, ∃ s : ℕ, k + 1 ≤ s ∧ 1 ≤ s ∧ r s < (1 : ℝ) / ((2 : ℝ) ^ s - 1) := by
    intro k
    induction k with
    | zero => exact ⟨1, le_refl _, le_refl _, h1⟩
    | succ k ih =>
      obtain ⟨s, hks, hs1, hs⟩ := ih
      obtain ⟨n, hsn, -, hn⟩ := hwin r h0 hrs s hs1 hs
      exact ⟨n, by omega, by omega, hn⟩
  intro m
  obtain ⟨s, hms, -, hs⟩ := hchain m
  exact ⟨s, by omega, hs⟩

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).

How to read a statement’s page →