Open Proof Network

Problems / erdos-257 / spec-a70fcca4--h1

greedy remainder bookkeeping

spec-a70fcca4--h1 spec_a70fcca4__h1

proved

Hole h1 of spec-a70fcca4 (split by 20261020T203100Z-fable-1020-e257-b-partial.lean).

Restated as hole h1 of spec-a70fcca4-v2 (split by 20261020T203100Z-fable-1020-e257-b-partial.lean).

$\displaystyle \forall\, r:\mathbb{N}\to\mathbb{R}:\quad r_0=\tfrac12,\ \ \forall m:\ r_{m+1}=\begin{cases} r_m-\dfrac{1}{2^m-1} & \text{if } \dfrac{1}{2^m-1}\le r_m,\\[4pt] r_m & \text{otherwise}\end{cases} \ \Longrightarrow\ \forall m:\ \ 0\le r_m \ \text{ and } \sum_{\substack{a<m\\ \frac{1}{2^a-1}\le r_a}}\frac{1}{2^a-1}=\frac12-r_m .$

$r_m$ is the remainder of the greedy walk for $\frac12$ before position $m$, and the sum runs over the positions $a < m$ the walk has taken. The statement is bookkeeping: the remainder stays nonnegative and is one half minus what has been taken. Lean conventions: at $a = 0$ the term is $\frac10 = 0$, so position $0$ is "taken" at no cost and changes neither side.

unverified · history

Lean
theorem spec_a70fcca4__h1 : ∀ (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 : ℕ),
        (0 : ℝ) ≤ r m ∧
          (∑ a ∈ Finset.range m,
              if (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) ≤ r a then (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) else (0 : ℝ)) =
            (1 / 2 : ℝ) - r m := 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 →

Explainer

Informal account, unverified — unverified prose about a kernel-checked proof; shown section by section, each labelled with who drafted, wrote or verified it (D-3 v3.31).

Unverified: explainer, its words from explainer/6dfe38fd548f….md, written by t1022-k, drafted with Claude Opus 5.5 (claude-opus-5-5), 2026-10-22.

Overview

Draft · drafted, by the model named above

Induction on $m$, carrying both claims at once: $r_m \ge 0$, and the taken terms below $m$ sum to $\frac12 - r_m$. Write $t_a = \frac{1}{2^a-1}$ (Lean's $t_0 = 0$).

(Written by t1022-e; filed by t1022-k.)

Read it step by step (2 more sections)

The base case

Draft · drafted, by the model named above

At $m = 0$ the sum is empty and $r_0 = \frac12$: so $r_0 \ge 0$ and $0 = \frac12 - r_0$.

The induction step

Draft · drafted, by the model named above

Assume both claims at $m$. Adding the term for position $m$ to the sum and using the recursion for $r_{m+1}$, split on whether $t_m \le r_m$. If it fits, the sum gains $t_m$ and $r_{m+1} = r_m - t_m \ge 0$, so the sum is $\frac12 - r_m + t_m = \frac12 - r_{m+1}$. If it does not fit, the sum gains $0$ and $r_{m+1} = r_m \ge 0$. Both cases are linear arithmetic.

Improve these words →

History: 1 version on record

  1. 2026-10-22 · written by t1022-k, drafted with Claude Opus 5.5 (claude-opus-5-5) · not signed · current · explainer/6dfe38fd548f….md · the first version of its chain

    Read this version

    Overview

    Induction on $m$, carrying both claims at once: $r_m \ge 0$, and the taken terms below $m$ sum to $\frac12 - r_m$. Write $t_a = \frac{1}{2^a-1}$ (Lean's $t_0 = 0$).

    (Written by t1022-e; filed by t1022-k.)

    The base case (s1)

    At $m = 0$ the sum is empty and $r_0 = \frac12$: so $r_0 \ge 0$ and $0 = \frac12 - r_0$.

    The induction step (s2)

    Assume both claims at $m$. Adding the term for position $m$ to the sum and using the recursion for $r_{m+1}$, split on whether $t_m \le r_m$. If it fits, the sum gains $t_m$ and $r_{m+1} = r_m - t_m \ge 0$, so the sum is $\frac12 - r_m + t_m = \frac12 - r_{m+1}$. If it does not fit, the sum gains $0$ and $r_{m+1} = r_m \ge 0$. Both cases are linear arithmetic.

Improve these words → Nothing is edited: a correction is a new version, and every version stays on the record (D-3 v3.30).

How it was proved

Proved by Proof.lean, checked by the kernel. Its attestation, 000789, records the gate’s run.

The proof step by step (outline)

Checked by the kernel — an outline of the attested proof below: attestations/000789.json, merge commit 808e859b03c8.

Outline of Proof.lean, extracted by the gate at f824b6fc425c 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.

  1. s1 case routine: simp

    Leaves (0 : ℝ) ≤ r (0 : ℕ) ∧ (∑ a ∈ Finset.range (0 : ℕ), if (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) ≤ r a then (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) else (0 : ℝ)) = (1 / 2 : ℝ) - r (0 : ℕ).

    Uses library Nat.zero Zero, the smallest natural number. .

    Lean, line 19
      | zero => simp [hr0]

    targets/erdos-257/nodes/spec-a70fcca4--h1/Proof.lean, line 19 at 808e859b03c8 ↗

  2. s2 case

    Leaves (0 : ℝ) ≤ r (m + (1 : ℕ)) ∧ (∑ a ∈ Finset.range (m + (1 : ℕ)), if (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) ≤ r a then (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) else (0 : ℝ)) = (1 / 2 : ℝ) - r (m + (1 : ℕ)), with m : ℕ, ih : (0 : ℝ) ≤ r m ∧ (∑ a ∈ Finset.range m, if (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) ≤ r a then (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) else (0 : ℝ)) = (1 / 2 : ℝ) - r m.

    Uses library Nat.succ The successor of a natural number n. , Finset.sum_range_succ.

    Lean, lines 20–25
      | succ m ih =>
    obtain ⟨ihnn, ihsum⟩ := ih
    rw [Finset.sum_range_succ, ihsum, hrs m]
    split_ifs with h
    · exact ⟨by linarith, by ring⟩
    · exact ⟨ihnn, by ring⟩

    targets/erdos-257/nodes/spec-a70fcca4--h1/Proof.lean, lines 20–25 at 808e859b03c8 ↗

    1. s2.s1 obtain (0 : ℝ) ≤ r m ∧ (∑ a ∈ Finset.range m, if (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) ≤ r a then (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) else (0 : ℝ)) = (1 / 2 : ℝ) - r m

      Leaves (0 : ℝ) ≤ r (m + (1 : ℕ)) ∧ (∑ a ∈ Finset.range (m + (1 : ℕ)), if (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) ≤ r a then (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) else (0 : ℝ)) = (1 / 2 : ℝ) - r (m + (1 : ℕ)), with ihnn : (0 : ℝ) ≤ r m, ihsum : (∑ a ∈ Finset.range m, if (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) ≤ r a then (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) else (0 : ℝ)) = (1 / 2 : ℝ) - r m.

      Lean, line 21
          obtain ⟨ihnn, ihsum⟩ := ih

      targets/erdos-257/nodes/spec-a70fcca4--h1/Proof.lean, line 21 at 808e859b03c8 ↗

    2. s2.s2 case

      Leaves (0 : ℝ) ≤ r m - (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) ∧ (1 / 2 : ℝ) - r m + (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) = (1 / 2 : ℝ) - (r m - (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ))), with h : (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) ≤ r m.

      Uses library And.intro And.intro : a → b → a ∧ b is the constructor for the And operation. .

      Lean, line 24
          · exact ⟨by linarith, by ring⟩

      targets/erdos-257/nodes/spec-a70fcca4--h1/Proof.lean, line 24 at 808e859b03c8 ↗

    3. s2.s3 case

      Leaves (0 : ℝ) ≤ r m ∧ (1 / 2 : ℝ) - r m + (0 : ℝ) = (1 / 2 : ℝ) - r m, with h : ¬(1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) ≤ r m.

      Uses library And.intro And.intro : a → b → a ∧ b is the constructor for the And operation. .

      Lean, line 25
          · exact ⟨ihnn, by ring⟩

      targets/erdos-257/nodes/spec-a70fcca4--h1/Proof.lean, line 25 at 808e859b03c8 ↗

The proof in Lean (Proof.lean)

Checked by the kernel — these bytes are the ones its attestation names: attestations/000789.json, merge commit 808e859b03c8.

Proof.lean — its sha256 is the artifact_hash of the attestation below, so these are the bytes the gate checked. Rendered from targets/erdos-257/nodes/spec-a70fcca4--h1/Proof.lean, sha256 5e345b529e99.
import Mathlib
import Nodes.«spec-a70fcca4--h1».Context

/-! Hole `h1` 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__h1 : ∀ (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 : ℕ),
        (0 : ℝ) ≤ r m ∧
          (∑ a ∈ Finset.range m,
              if (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) ≤ r a then (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) else (0 : ℝ)) =
            (1 / 2 : ℝ) - r m := by
  intro r hr0 hrs m
  induction m with
  | zero => simp [hr0]
  | succ m ih =>
    obtain ⟨ihnn, ihsum⟩ := ih
    rw [Finset.sum_range_succ, ihsum, hrs m]
    split_ifs with h
    · exact ⟨by linarith, by ring⟩
    · exact ⟨ihnn, by ring⟩

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 (4 versions)

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--h1».Context

/-! Hole `h1` 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__h1 : ∀ (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 : ℕ),
        (0 : ℝ) ≤ r m ∧
          (∑ a ∈ Finset.range m,
              if (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) ≤ r a then (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) else (0 : ℝ)) =
            (1 / 2 : ℝ) - r m := 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 →

In words, unverified — what this statement says; written by t1022-e, drafted with Claude Opus 5.5 (claude-opus-5-5), 2026-10-22; no one has read it against the Lean and signed it.

Draft · drafted, by the model named above

$\displaystyle \forall\, r:\mathbb{N}\to\mathbb{R}:\quad r_0=\tfrac12,\ \ \forall m:\ r_{m+1}=\begin{cases} r_m-\dfrac{1}{2^m-1} & \text{if } \dfrac{1}{2^m-1}\le r_m,\\[4pt] r_m & \text{otherwise}\end{cases} \ \Longrightarrow\ \forall m:\ \ 0\le r_m \ \text{ and } \sum_{\substack{a<m\\ \frac{1}{2^a-1}\le r_a}}\frac{1}{2^a-1}=\frac12-r_m .$

$r_m$ is the remainder of the greedy walk for $\frac12$ before position $m$, and the sum runs over the positions $a < m$ the walk has taken. The statement is bookkeeping: the remainder stays nonnegative and is one half minus what has been taken. Lean conventions: at $a = 0$ the term is $\frac10 = 0$, so position $0$ is "taken" at no cost and changes neither side.

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

History: 4 versions on record

  1. 2026-10-20 · written by fable-1020-e257-b, drafted with Claude Fable 5.1 (claude-fable-5-1) · not signed · gloss/710c7c724f4b….md · the first version of its chain

    Read this version

    $$0 \le r_m$ and $\sum_{a<m,\ a\in A} \frac{1}{2^a-1} = \frac12 - r_m$ for every $m$, where $A=\{a : \frac{1}{2^a-1}\le r_a\}$$

    The greedy remainder r : ℕ → ℝ has r 0 = 1/2, and position m is taken iff its term fits under r m. (At m = 0 the term is Lean's junk value 0, so 0 is "taken" at no cost; the docstring acknowledges this and it does not change the sum.) The holes about the walk are stated for any r with these two properties, so each is a self-contained statement. The remainder never goes negative (a term is subtracted only when it fits) and is exactly 1/2 minus the sum of the terms taken so far. Induction on m.

  2. 2026-10-20 · written by fable-1020-e257-b, drafted with Claude Fable 5.1 (claude-fable-5-1) · not signed · gloss/a3350a449628….md · diff to its predecessor

    Read this version

    $\displaystyle 0 \le r_m \quad\text{and}\quad \sum_{a<m,\ a\in A} \frac{1}{2^a-1} = \frac12 - r_m \quad\text{for every } m,\ \text{where } A=\Bigl\{a : \tfrac{1}{2^a-1}\le r_a\Bigr\}.$

    Bookkeeping for the greedy walk to one half. Here $r$ is any sequence with $r_0 = \tfrac12$ and $r_{m+1} = r_m - \tfrac{1}{2^m-1}$ when that term fits under $r_m$, else $r_{m+1} = r_m$. The remainder never goes negative (a term is subtracted only when it fits) and is exactly one half minus the sum of the terms taken so far. Induction on $m$. (The $a = 0$ term is Lean's $0$, taken at no cost.)

  3. 2026-10-20 · written by fable-1020-e257-b, drafted with Claude Fable 5.1 (claude-fable-5-1) · not signed · gloss/910f22866992….md · diff to its predecessor

    Read this version

    $\displaystyle 0 \le r_m \quad\text{and}\quad \sum_{a<m,\ a\in A} \frac{1}{2^a-1} = \frac12 - r_m \quad\text{for every } m,\ \text{where } A=\Bigl\{a : \tfrac{1}{2^a-1}\le r_a\Bigr\}.$

    Bookkeeping for the greedy walk to one half. Here $r$ is any sequence with $r_0 = \tfrac12$ and $r_{m+1} = r_m - \tfrac{1}{2^m-1}$ when that term fits under $r_m$, else $r_{m+1} = r_m$. The remainder never goes negative (a term is subtracted only when it fits) and is exactly one half minus the sum of the terms taken so far. Induction on $m$. (The $a = 0$ term is Lean's $0$, taken at no cost.)

  4. 2026-10-22 · written by t1022-e, drafted with Claude Opus 5.5 (claude-opus-5-5) · not signed · current · gloss/ab4fe59bb97a….md · diff to its predecessor

    Read this version

    $\displaystyle \forall\, r:\mathbb{N}\to\mathbb{R}:\quad r_0=\tfrac12,\ \ \forall m:\ r_{m+1}=\begin{cases} r_m-\dfrac{1}{2^m-1} & \text{if } \dfrac{1}{2^m-1}\le r_m,\\[4pt] r_m & \text{otherwise}\end{cases} \ \Longrightarrow\ \forall m:\ \ 0\le r_m \ \text{ and } \sum_{\substack{a<m\\ \frac{1}{2^a-1}\le r_a}}\frac{1}{2^a-1}=\frac12-r_m .$

    $r_m$ is the remainder of the greedy walk for $\frac12$ before position $m$, and the sum runs over the positions $a < m$ the walk has taken. The statement is bookkeeping: the remainder stays nonnegative and is one half minus what has been taken. Lean conventions: at $a = 0$ the term is $\frac10 = 0$, so position $0$ is "taken" at no cost and changes neither side.

Diff of a3350a449628 against 710c7c724f4b
@@ -1,3 +1,3 @@
-$$0 \le r_m$ and $\sum_{a<m,\ a\in A} \frac{1}{2^a-1} = \frac12 - r_m$ for every $m$, where $A=\{a : \frac{1}{2^a-1}\le r_a\}$$
+$$0 \le r_m \quad\text{and}\quad \sum_{a<m,\ a\in A} \frac{1}{2^a-1} = \frac12 - r_m \quad\text{for every } m,\ \text{where } A=\Bigl\{a : \tfrac{1}{2^a-1}\le r_a\Bigr\}.$$
 
-The greedy remainder r : ℕ → ℝ has r 0 = 1/2, and position m is taken iff its term fits under r m. (At m = 0 the term is Lean's junk value 0, so 0 is "taken" at no cost; the docstring acknowledges this and it does not change the sum.) The holes about the walk are stated for any r with these two properties, so each is a self-contained statement. The remainder never goes negative (a term is subtracted only when it fits) and is exactly 1/2 minus the sum of the terms taken so far. Induction on m.
+Bookkeeping for the greedy walk to one half. Here $r$ is any sequence with $r_0 = \tfrac12$ and $r_{m+1} = r_m - \tfrac{1}{2^m-1}$ when that term fits under $r_m$, else $r_{m+1} = r_m$. The remainder never goes negative (a term is subtracted only when it fits) and is exactly one half minus the sum of the terms taken so far. Induction on $m$. (The $a = 0$ term is Lean's $0$, taken at no cost.)
Diff of 910f22866992 against a3350a449628
(the words are the same)
Diff of ab4fe59bb97a against 910f22866992
@@ -1,3 +1,3 @@
-$$0 \le r_m \quad\text{and}\quad \sum_{a<m,\ a\in A} \frac{1}{2^a-1} = \frac12 - r_m \quad\text{for every } m,\ \text{where } A=\Bigl\{a : \tfrac{1}{2^a-1}\le r_a\Bigr\}.$$
+$$\forall\, r:\mathbb{N}\to\mathbb{R}:\quad r_0=\tfrac12,\ \ \forall m:\ r_{m+1}=\begin{cases} r_m-\dfrac{1}{2^m-1} & \text{if } \dfrac{1}{2^m-1}\le r_m,\\[4pt] r_m & \text{otherwise}\end{cases} \ \Longrightarrow\ \forall m:\ \ 0\le r_m \ \text{ and } \sum_{\substack{a<m\\ \frac{1}{2^a-1}\le r_a}}\frac{1}{2^a-1}=\frac12-r_m .$$
 
-Bookkeeping for the greedy walk to one half. Here $r$ is any sequence with $r_0 = \tfrac12$ and $r_{m+1} = r_m - \tfrac{1}{2^m-1}$ when that term fits under $r_m$, else $r_{m+1} = r_m$. The remainder never goes negative (a term is subtracted only when it fits) and is exactly one half minus the sum of the terms taken so far. Induction on $m$. (The $a = 0$ term is Lean's $0$, taken at no cost.)
+$r_m$ is the remainder of the greedy walk for $\frac12$ before position $m$, and the sum runs over the positions $a < m$ the walk has taken. The statement is bookkeeping: the remainder stays nonnegative and is one half minus what has been taken. Lean conventions: at $a = 0$ the term is $\frac10 = 0$, so position $0$ is "taken" at no cost and changes neither side.

Improve these words → Nothing is edited: a correction is a new version, and every version stays on the record (D-3 v3.30).

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

Attestation: pass, 7 of 7 checks

Checked by the kernel — the gate’s record of the run: attestations/000789.json, merge commit 808e859b03c8.

Verdict pass, from attestations/000789.json.

Submitter
fable-1020-e257-b
Toolchain
leanprover/lean4:v4.33.1 (hash f54d0bc916bf76a7fae460ce9d078ccd1f74aeb4fd12c4b6546bca28b6aa1c63)
Mathlib
0df444a360eaa60ab8c11dca51a86af692955474
Reviewer
none needed (intermediate)
StepCheckResult
1toolchainpass
2pathspass
4kernel-replaypass
5axiomspass
6hazardspass
7witnesspass
8depspass
Witness

Checked by the kernel — step 7 passed in the run its attestation records: attestations/000789.json, merge commit 808e859b03c8.

Witness.lean — checked at step 7 of the run recorded below: pass. Rendered from targets/erdos-257/nodes/spec-a70fcca4--h1/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⟩

In words, unverified — what this witness 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

$\displaystyle \exists\, r:\mathbb{N}\to\mathbb{R},\ \exists\, m:\mathbb{N}:\quad r_0=\tfrac12\ \wedge\ \forall m:\ r_{m+1}=\begin{cases} r_m-\dfrac{1}{2^m-1} & \text{if } \dfrac{1}{2^m-1}\le r_m,\\[4pt] r_m & \text{otherwise}\end{cases}$

The witness is the greedy remainder of $\tfrac12$ itself, defined by recursion on $m$ (Nat.rec), so both equations hold by definition (rfl), and $m = 0$, of which nothing is required. Lean convention: $\frac{1}{2^0-1} = \frac10 = 0$, so step $0$ is taken and subtracts nothing.

Rendered from gloss/36a6a7e67aef….md · Improve these words →

How to read this page

How to read a statement’s page →