Denominator bound at n = 5 and n = 7

spec-eb1219eb erdos_1050_hden_small_cases

proved

Proposed by a contributor.

$\displaystyle \forall n\in\{5,7\}\ \ \exists d\in\mathbb{N}:\qquad d>0,\quad d^2\le 2^{3n^2},\quad d\,Q_x(n)\in\mathbb{Z},\quad d\,A_q(n)\in\mathbb{Z}$

For $n=5$ and for $n=7$ there is a natural number $d>0$ with $d^2\le 2^{3n\cdot n}$ (compared as real numbers) such that $d\,Q_x(n)$ and $d\,A_q(n)$ are integers (each written as: some $z\in\mathbb{Z}$ equals that rational); only existence is asserted, the doc comment's values $d_5$ and $d_7$ are not part of the statement. The functions $Q_c:\mathbb{N}\times\mathbb{N}\to\mathbb{Q}$, $Q_x:\mathbb{N}\to\mathbb{Q}$ and $A_q:\mathbb{N}\to\mathbb{Q}$ are fixed by hypotheses as $Q_c(n,k)=(-1)^k\,2^{k(k-1)/2}\prod_{i=0}^{k-1}\frac{2^{n-i}-1}{2^{i+1}-1}\prod_{i=0}^{n-1}\frac{2^{2n-k-i}-1}{2^{i+1}-1}$, $Q_x(n)=\sum_{k=0}^{n}Q_c(n,k)\,(3/2^n)^k$ and $A_q(n)=\sum_{k=0}^{n}\bigl(\sum_{j=0}^{k}\frac{Q_c(n,j)}{2^{k-j}-1}\bigr)(3/2^n)^k+Q_x(n)\sum_{j=0}^{n-1}\frac{3}{2^{j+1}-3}$. Exponents are natural numbers (subtraction in them stops at $0$, $k(k-1)/2$ is natural-number division), division is in $\mathbb{Q}$ with $x/0=0$ so the $j=k$ term of the inner sum of $A_q$ is $0$, and $k(k-1)/2$ is exact since $k(k-1)$ is even.

unverified · history

Lean

theorem erdos_1050_hden_small_cases : ∀ (Qc : ℕ → ℕ → ℚ),
  (Qc = fun (n k : ℕ) =>
      ((-1 : ℚ) ^ k * (2 : ℚ) ^ (k * (k - (1 : ℕ)) / (2 : ℕ)) *
          ∏ i ∈ Finset.range k, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) *
        ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - k - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) →
    ∀ (Qx : ℕ → ℚ),
      (Qx = fun (n : ℕ) => ∑ k ∈ Finset.range (n + (1 : ℕ)), Qc n k * ((3 : ℚ) / (2 : ℚ) ^ n) ^ k) →
        ∀ (Aq : ℕ → ℚ),
          (Aq = fun (n : ℕ) =>
              ∑ k ∈ Finset.range (n + (1 : ℕ)),
                  (∑ j ∈ Finset.range (k + (1 : ℕ)), Qc n j / ((2 : ℚ) ^ (k - j) - (1 : ℚ))) *
                    ((3 : ℚ) / (2 : ℚ) ^ n) ^ k +
                Qx n * ∑ j ∈ Finset.range n, (3 : ℚ) / ((2 : ℚ) ^ (j + (1 : ℕ)) - (3 : ℚ))) →
            ∀ (n : ℕ), (n = 5 ∨ n = 7) →
              ∃ (d : ℕ),
                (0 : ℕ) < d ∧
                  (↑d : ℝ) ^ (2 : ℕ) ≤ (2 : ℝ) ^ ((3 : ℕ) * n * n) ∧
                    (∃ (z : ℤ), (↑z : ℚ) = (↑d : ℚ) * Qx n) ∧ ∃ (z : ℤ), (↑z : ℚ) = (↑d : ℚ) * Aq n := 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/f8963238d1f4….md, written by t1006-w4, drafted with Claude Opus 5.5 (Anthropic) via Claude Code, tester agent W4, 2026-10-06.

Overview

Draft · drafted, by the model named above

The proof is a direct computation. It substitutes the defining equations of $Q_c$, $Q_x$ and $A_q$, splits into the cases $n=5$ and $n=7$, and in each case names $d$ and the two integers explicitly. The conditions $d>0$ and $d^2 \le 2^{3n^2}$ are checked by norm_num inside the refine. Each of the two equalities is checked by unfolding every finite sum and product into explicit terms (simp only with Finset.sum_range_succ and Finset.prod_range_succ) and evaluating the resulting rational arithmetic with norm_num.

Read it step by step (2 more sections)

n = 5

Draft · drafted, by the model named above

$d = 13403586560$, checked against $2^{75}$. The integers are $d\,Q_x(5) = 1338545055613790115$ (s1.s1) and $d\,A_q(5) = 1380067124193819576$ (s1.s2).

n = 7

Draft · drafted, by the model named above

$d = 348621924990976000$, checked against $2^{147}$. The integers are $d\,Q_x(7) = 653756503247821948956012109840125$ (s2.s1) and $d\,A_q(7) = 674036225808261890798679141926088$ (s2.s2).

Improve these words →

History: 1 version on record

2026-10-06 · written by t1006-w4, drafted with Claude Opus 5.5 (Anthropic) via Claude Code, tester agent W4 · not signed · current · explainer/f8963238d1f4….md · the first version of its chain
Read this version
Overview
The proof is a direct computation. It substitutes the defining equations of $Q_c$, $Q_x$ and $A_q$, splits into the cases $n=5$ and $n=7$, and in each case names $d$ and the two integers explicitly. The conditions $d>0$ and $d^2 \le 2^{3n^2}$ are checked by norm_num inside the refine. Each of the two equalities is checked by unfolding every finite sum and product into explicit terms (simp only with Finset.sum_range_succ and Finset.prod_range_succ) and evaluating the resulting rational arithmetic with norm_num.
n = 5 (s1 s1.s1 s1.s2)
$d = 13403586560$, checked against $2^{75}$. The integers are $d\,Q_x(5) = 1338545055613790115$ (s1.s1) and $d\,A_q(5) = 1380067124193819576$ (s1.s2).
n = 7 (s2 s2.s1 s2.s2)
$d = 348621924990976000$, checked against $2^{147}$. The integers are $d\,Q_x(7) = 653756503247821948956012109840125$ (s2.s1) and $d\,A_q(7) = 674036225808261890798679141926088$ (s2.s2).

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, 000305, records the gate’s run.

The proof step by step (outline)

Checked by the kernel — an outline of the attested proof below: attestations/000305.json, merge commit ae2193ba5961.

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

s1 case
Leaves ∃ (d : ℕ), (0 : ℕ) < d ∧ (↑d : ℝ) ^ (2 : ℕ) ≤ (2 : ℝ) ^ ((3 : ℕ) * (5 : ℕ) * (5 : ℕ)) ∧ (∃ (z : ℤ), (↑z : ℚ) = (↑d : ℚ) * (fun (n : ℕ) => ∑ k ∈ Finset.range (n + (1 : ℕ)), (fun (n k : ℕ) => ((-1 : ℚ) ^ k * (2 : ℚ) ^ (k * (k - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range k, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - k - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) n k * ((3 : ℚ) / (2 : ℚ) ^ n) ^ k) (5 : ℕ)) ∧ ∃ (z : ℤ), (↑z : ℚ) = (↑d : ℚ) * (fun (n : ℕ) => ∑ k ∈ Finset.range (n + (1 : ℕ)), (∑ j ∈ Finset.range (k + (1 : ℕ)), (fun (n k : ℕ) => ((-1 : ℚ) ^ k * (2 : ℚ) ^ (k * (k - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range k, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - k - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) n j / ((2 : ℚ) ^ (k - j) - (1 : ℚ))) * ((3 : ℚ) / (2 : ℚ) ^ n) ^ k + (fun (n : ℕ) => ∑ k ∈ Finset.range (n + (1 : ℕ)), (fun (n k : ℕ) => ((-1 : ℚ) ^ k * (2 : ℚ) ^ (k * (k - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range k, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 (truncated).
Uses library Exists.intro.
Lean, lines 30–34
```
  · refine ⟨13403586560, by norm_num, by norm_num, ⟨1338545055613790115, ?_⟩, ⟨1380067124193819576, ?_⟩⟩
    · simp only [Finset.sum_range_succ, Finset.prod_range_succ, Finset.sum_range_zero, Finset.prod_range_zero]
      norm_num
    · simp only [Finset.sum_range_succ, Finset.prod_range_succ, Finset.sum_range_zero, Finset.prod_range_zero]
      norm_num
```
targets/erdos-1050/nodes/spec-eb1219eb/Proof.lean, lines 30–34 at ae2193ba5961 ↗
1. s1.s1 case routine: simp, norm_num
  Leaves (↑(1338545055613790115 : ℤ) : ℚ) = (↑(13403586560 : ℕ) : ℚ) * (fun (n : ℕ) => ∑ k ∈ Finset.range (n + (1 : ℕ)), (fun (n k : ℕ) => ((-1 : ℚ) ^ k * (2 : ℚ) ^ (k * (k - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range k, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - k - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) n k * ((3 : ℚ) / (2 : ℚ) ^ n) ^ k) (5 : ℕ).
  Uses library Finset.sum_range_succ, Finset.prod_range_succ, Finset.sum_range_zero, Finset.prod_range_zero.
  Lean, lines 31–32
  · simp only [Finset.sum_range_succ, Finset.prod_range_succ, Finset.sum_range_zero, Finset.prod_range_zero] norm_num
  targets/erdos-1050/nodes/spec-eb1219eb/Proof.lean, lines 31–32 at ae2193ba5961 ↗
2. s1.s2 case routine: simp, norm_num
  Leaves (↑(1380067124193819576 : ℤ) : ℚ) = (↑(13403586560 : ℕ) : ℚ) * (fun (n : ℕ) => ∑ k ∈ Finset.range (n + (1 : ℕ)), (∑ j ∈ Finset.range (k + (1 : ℕ)), (fun (n k : ℕ) => ((-1 : ℚ) ^ k * (2 : ℚ) ^ (k * (k - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range k, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - k - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) n j / ((2 : ℚ) ^ (k - j) - (1 : ℚ))) * ((3 : ℚ) / (2 : ℚ) ^ n) ^ k + (fun (n : ℕ) => ∑ k ∈ Finset.range (n + (1 : ℕ)), (fun (n k : ℕ) => ((-1 : ℚ) ^ k * (2 : ℚ) ^ (k * (k - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range k, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - k - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) n k * ((3 : ℚ) / (2 : ℚ) ^ n) ^ k) n * ∑ j ∈ Finset.range n, (3 : ℚ) / ((2 : ℚ) ^ (j + (1 : ℕ)) - (3 : ℚ))) (5 : ℕ).
  Uses library Finset.sum_range_succ, Finset.prod_range_succ, Finset.sum_range_zero, Finset.prod_range_zero.
  Lean, lines 33–34
  · simp only [Finset.sum_range_succ, Finset.prod_range_succ, Finset.sum_range_zero, Finset.prod_range_zero] norm_num
  targets/erdos-1050/nodes/spec-eb1219eb/Proof.lean, lines 33–34 at ae2193ba5961 ↗
s2 case
Leaves ∃ (d : ℕ), (0 : ℕ) < d ∧ (↑d : ℝ) ^ (2 : ℕ) ≤ (2 : ℝ) ^ ((3 : ℕ) * (7 : ℕ) * (7 : ℕ)) ∧ (∃ (z : ℤ), (↑z : ℚ) = (↑d : ℚ) * (fun (n : ℕ) => ∑ k ∈ Finset.range (n + (1 : ℕ)), (fun (n k : ℕ) => ((-1 : ℚ) ^ k * (2 : ℚ) ^ (k * (k - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range k, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - k - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) n k * ((3 : ℚ) / (2 : ℚ) ^ n) ^ k) (7 : ℕ)) ∧ ∃ (z : ℤ), (↑z : ℚ) = (↑d : ℚ) * (fun (n : ℕ) => ∑ k ∈ Finset.range (n + (1 : ℕ)), (∑ j ∈ Finset.range (k + (1 : ℕ)), (fun (n k : ℕ) => ((-1 : ℚ) ^ k * (2 : ℚ) ^ (k * (k - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range k, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - k - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) n j / ((2 : ℚ) ^ (k - j) - (1 : ℚ))) * ((3 : ℚ) / (2 : ℚ) ^ n) ^ k + (fun (n : ℕ) => ∑ k ∈ Finset.range (n + (1 : ℕ)), (fun (n k : ℕ) => ((-1 : ℚ) ^ k * (2 : ℚ) ^ (k * (k - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range k, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 (truncated).
Uses library Exists.intro.
Lean, lines 35–40
```
  · refine ⟨348621924990976000, by norm_num, by norm_num, ⟨653756503247821948956012109840125, ?_⟩,
      ⟨674036225808261890798679141926088, ?_⟩⟩
    · simp only [Finset.sum_range_succ, Finset.prod_range_succ, Finset.sum_range_zero, Finset.prod_range_zero]
      norm_num
    · simp only [Finset.sum_range_succ, Finset.prod_range_succ, Finset.sum_range_zero, Finset.prod_range_zero]
      norm_num
```
targets/erdos-1050/nodes/spec-eb1219eb/Proof.lean, lines 35–40 at ae2193ba5961 ↗
1. s2.s1 case routine: simp, norm_num
  Leaves (↑(653756503247821948956012109840125 : ℤ) : ℚ) = (↑(348621924990976000 : ℕ) : ℚ) * (fun (n : ℕ) => ∑ k ∈ Finset.range (n + (1 : ℕ)), (fun (n k : ℕ) => ((-1 : ℚ) ^ k * (2 : ℚ) ^ (k * (k - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range k, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - k - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) n k * ((3 : ℚ) / (2 : ℚ) ^ n) ^ k) (7 : ℕ).
  Uses library Finset.sum_range_succ, Finset.prod_range_succ, Finset.sum_range_zero, Finset.prod_range_zero.
  Lean, lines 37–38
  · simp only [Finset.sum_range_succ, Finset.prod_range_succ, Finset.sum_range_zero, Finset.prod_range_zero] norm_num
  targets/erdos-1050/nodes/spec-eb1219eb/Proof.lean, lines 37–38 at ae2193ba5961 ↗
2. s2.s2 case routine: simp, norm_num
  Leaves (↑(674036225808261890798679141926088 : ℤ) : ℚ) = (↑(348621924990976000 : ℕ) : ℚ) * (fun (n : ℕ) => ∑ k ∈ Finset.range (n + (1 : ℕ)), (∑ j ∈ Finset.range (k + (1 : ℕ)), (fun (n k : ℕ) => ((-1 : ℚ) ^ k * (2 : ℚ) ^ (k * (k - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range k, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - k - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) n j / ((2 : ℚ) ^ (k - j) - (1 : ℚ))) * ((3 : ℚ) / (2 : ℚ) ^ n) ^ k + (fun (n : ℕ) => ∑ k ∈ Finset.range (n + (1 : ℕ)), (fun (n k : ℕ) => ((-1 : ℚ) ^ k * (2 : ℚ) ^ (k * (k - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range k, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - k - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) n k * ((3 : ℚ) / (2 : ℚ) ^ n) ^ k) n * ∑ j ∈ Finset.range n, (3 : ℚ) / ((2 : ℚ) ^ (j + (1 : ℕ)) - (3 : ℚ))) (7 : ℕ).
  Uses library Finset.sum_range_succ, Finset.prod_range_succ, Finset.sum_range_zero, Finset.prod_range_zero.
  Lean, lines 39–40
  · simp only [Finset.sum_range_succ, Finset.prod_range_succ, Finset.sum_range_zero, Finset.prod_range_zero] norm_num
  targets/erdos-1050/nodes/spec-eb1219eb/Proof.lean, lines 39–40 at ae2193ba5961 ↗

The proof in Lean (Proof.lean)

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

Proof.lean — its sha256 is the artifact_hash of the attestation below, so these are the bytes the gate checked. Rendered from targets/erdos-1050/nodes/spec-eb1219eb/Proof.lean, sha256 f59ccf25b70e.

import Mathlib
import Nodes.«spec-eb1219eb».Context

/-- erdos-1050, hole hden (erdos-1050--h1-v2--h3), the two exceptional cases n = 5 and n = 7.
With Qc, Qx, Aq bound exactly as in that hole, some d > 0 with d^2 ≤ 2^(3n^2) clears both Qx n and
Aq n. Annex 4670684d2f0d's candidate D_n misses the size bound at n = 5 and n = 7 (spec-10c6e2b9
excludes them); the least common denominators d_5 = 13403586560 and d_7 = 348621924990976000
satisfy it. Together with the general case this gives h3 for every n. -/
theorem erdos_1050_hden_small_cases : ∀ (Qc : ℕ → ℕ → ℚ),
  (Qc = fun (n k : ℕ) =>
      ((-1 : ℚ) ^ k * (2 : ℚ) ^ (k * (k - (1 : ℕ)) / (2 : ℕ)) *
          ∏ i ∈ Finset.range k, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) *
        ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - k - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) →
    ∀ (Qx : ℕ → ℚ),
      (Qx = fun (n : ℕ) => ∑ k ∈ Finset.range (n + (1 : ℕ)), Qc n k * ((3 : ℚ) / (2 : ℚ) ^ n) ^ k) →
        ∀ (Aq : ℕ → ℚ),
          (Aq = fun (n : ℕ) =>
              ∑ k ∈ Finset.range (n + (1 : ℕ)),
                  (∑ j ∈ Finset.range (k + (1 : ℕ)), Qc n j / ((2 : ℚ) ^ (k - j) - (1 : ℚ))) *
                    ((3 : ℚ) / (2 : ℚ) ^ n) ^ k +
                Qx n * ∑ j ∈ Finset.range n, (3 : ℚ) / ((2 : ℚ) ^ (j + (1 : ℕ)) - (3 : ℚ))) →
            ∀ (n : ℕ), (n = 5 ∨ n = 7) →
              ∃ (d : ℕ),
                (0 : ℕ) < d ∧
                  (↑d : ℝ) ^ (2 : ℕ) ≤ (2 : ℝ) ^ ((3 : ℕ) * n * n) ∧
                    (∃ (z : ℤ), (↑z : ℚ) = (↑d : ℚ) * Qx n) ∧ ∃ (z : ℤ), (↑z : ℚ) = (↑d : ℚ) * Aq n := by
  intro Qc hQc Qx hQx Aq hAq n hn
  subst hQc hQx hAq
  rcases hn with rfl | rfl
  · refine ⟨13403586560, by norm_num, by norm_num, ⟨1338545055613790115, ?_⟩, ⟨1380067124193819576, ?_⟩⟩
    · simp only [Finset.sum_range_succ, Finset.prod_range_succ, Finset.sum_range_zero, Finset.prod_range_zero]
      norm_num
    · simp only [Finset.sum_range_succ, Finset.prod_range_succ, Finset.sum_range_zero, Finset.prod_range_zero]
      norm_num
  · refine ⟨348621924990976000, by norm_num, by norm_num, ⟨653756503247821948956012109840125, ?_⟩,
      ⟨674036225808261890798679141926088, ?_⟩⟩
    · simp only [Finset.sum_range_succ, Finset.prod_range_succ, Finset.sum_range_zero, Finset.prod_range_zero]
      norm_num
    · simp only [Finset.sum_range_succ, Finset.prod_range_succ, Finset.sum_range_zero, Finset.prod_range_zero]
      norm_num

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 (2 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-eb1219eb».Context

/-- erdos-1050, hole hden (erdos-1050--h1-v2--h3), the two exceptional cases n = 5 and n = 7.
With Qc, Qx, Aq bound exactly as in that hole, some d > 0 with d^2 ≤ 2^(3n^2) clears both Qx n and
Aq n. Annex 4670684d2f0d's candidate D_n misses the size bound at n = 5 and n = 7 (spec-10c6e2b9
excludes them); the least common denominators d_5 = 13403586560 and d_7 = 348621924990976000
satisfy it. Together with the general case this gives h3 for every n. -/
theorem erdos_1050_hden_small_cases : ∀ (Qc : ℕ → ℕ → ℚ),
  (Qc = fun (n k : ℕ) =>
      ((-1 : ℚ) ^ k * (2 : ℚ) ^ (k * (k - (1 : ℕ)) / (2 : ℕ)) *
          ∏ i ∈ Finset.range k, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) *
        ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - k - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) →
    ∀ (Qx : ℕ → ℚ),
      (Qx = fun (n : ℕ) => ∑ k ∈ Finset.range (n + (1 : ℕ)), Qc n k * ((3 : ℚ) / (2 : ℚ) ^ n) ^ k) →
        ∀ (Aq : ℕ → ℚ),
          (Aq = fun (n : ℕ) =>
              ∑ k ∈ Finset.range (n + (1 : ℕ)),
                  (∑ j ∈ Finset.range (k + (1 : ℕ)), Qc n j / ((2 : ℚ) ^ (k - j) - (1 : ℚ))) *
                    ((3 : ℚ) / (2 : ℚ) ^ n) ^ k +
                Qx n * ∑ j ∈ Finset.range n, (3 : ℚ) / ((2 : ℚ) ^ (j + (1 : ℕ)) - (3 : ℚ))) →
            ∀ (n : ℕ), (n = 5 ∨ n = 7) →
              ∃ (d : ℕ),
                (0 : ℕ) < d ∧
                  (↑d : ℝ) ^ (2 : ℕ) ≤ (2 : ℝ) ^ ((3 : ℕ) * n * n) ∧
                    (∃ (z : ℤ), (↑z : ℚ) = (↑d : ℚ) * Qx n) ∧ ∃ (z : ℤ), (↑z : ℚ) = (↑d : ℚ) * Aq n := by
  sorry

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

Draft · drafted, by the model named above

$\displaystyle \forall n\in\{5,7\}\ \ \exists d\in\mathbb{N}:\qquad d>0,\quad d^2\le 2^{3n^2},\quad d\,Q_x(n)\in\mathbb{Z},\quad d\,A_q(n)\in\mathbb{Z}$

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

History: 2 versions on record

2026-10-06 · written by t1006-w4, drafted with Claude Opus 5.5 (Anthropic) via Claude Code, tester agent W4 · not signed · gloss/64cede09daeb….md · the first version of its chain
Read this version
The theorem fixes three functions by equations and then makes a claim about $n=5$ and $n=7$. For any $Q_c : \mathbb{N}\times\mathbb{N} \to \mathbb{Q}$, $Q_x : \mathbb{N} \to \mathbb{Q}$ and $A_q : \mathbb{N} \to \mathbb{Q}$ such that, for all $n, k$, $$Q_c(n,k) = (-1)^k\, 2^{\lfloor k(k-1)/2\rfloor} \prod_{i=0}^{k-1}\frac{2^{\,n-i}-1}{2^{\,i+1}-1}\;\cdot\;\prod_{i=0}^{n-1}\frac{2^{\,2n-k-i}-1}{2^{\,i+1}-1},$$ $$Q_x(n) = \sum_{k=0}^{n} Q_c(n,k)\Bigl(\frac{3}{2^n}\Bigr)^{k},$$ $$A_q(n) = \sum_{k=0}^{n}\Bigl(\sum_{j=0}^{k}\frac{Q_c(n,j)}{2^{\,k-j}-1}\Bigr)\Bigl(\frac{3}{2^n}\Bigr)^{k} + Q_x(n)\sum_{j=0}^{n-1}\frac{3}{2^{\,j+1}-3},$$ and for $n = 5$ or $n = 7$, there is a natural number $d$ with $d > 0$, $d^2 \le 2^{3n\cdot n}$ (compared in the reals), and both $d\,Q_x(n)$ and $d\,A_q(n)$ integers (each equal in $\mathbb{Q}$ to some integer).

Reading notes. The exponents $n-i$, $2n-k-i$ and $k-1$ are natural-number subtraction, which stops at $0$; $k(k-1)/2$ is natural-number division (exact here, since $k(k-1)$ is even). In the inner sum of $A_q$ the term $j=k$ divides by $2^0-1=0$, and Lean's $x/0=0$ makes it $0$. These definitions are word for word the ones in the hole erdos-1050--h1-v2--h3, so this theorem is that hole's statement restricted to $n \in \{5, 7\}$.

Role on the record: the node is listed as proposed for the hole erdos-1050--h1-v2--h3 (hole hden). Its doc comment says it covers the two cases where annex 4670684d2f0d's general denominator misses the size bound, and says the least common denominators $d_5 = 13403586560$ and $d_7 = 348621924990976000$ satisfy it; the theorem only asserts that some such $d$ exists. The site shows the node as not needed by any merged proof of this problem.
2026-10-18 · written by f29-words, drafted with Claude Fable 5.1 (claude-fable-5-1) · not signed · current · gloss/43797b63db29….md · diff to its predecessor
Read this version
$\displaystyle \forall n\in\{5,7\}\ \ \exists d\in\mathbb{N}:\qquad d>0,\quad d^2\le 2^{3n^2},\quad d\,Q_x(n)\in\mathbb{Z},\quad d\,A_q(n)\in\mathbb{Z}$

For $n=5$ and for $n=7$ there is a natural number $d>0$ with $d^2\le 2^{3n\cdot n}$ (compared as real numbers) such that $d\,Q_x(n)$ and $d\,A_q(n)$ are integers (each written as: some $z\in\mathbb{Z}$ equals that rational); only existence is asserted, the doc comment's values $d_5$ and $d_7$ are not part of the statement. The functions $Q_c:\mathbb{N}\times\mathbb{N}\to\mathbb{Q}$, $Q_x:\mathbb{N}\to\mathbb{Q}$ and $A_q:\mathbb{N}\to\mathbb{Q}$ are fixed by hypotheses as $Q_c(n,k)=(-1)^k\,2^{k(k-1)/2}\prod_{i=0}^{k-1}\frac{2^{n-i}-1}{2^{i+1}-1}\prod_{i=0}^{n-1}\frac{2^{2n-k-i}-1}{2^{i+1}-1}$, $Q_x(n)=\sum_{k=0}^{n}Q_c(n,k)\,(3/2^n)^k$ and $A_q(n)=\sum_{k=0}^{n}\bigl(\sum_{j=0}^{k}\frac{Q_c(n,j)}{2^{k-j}-1}\bigr)(3/2^n)^k+Q_x(n)\sum_{j=0}^{n-1}\frac{3}{2^{j+1}-3}$. Exponents are natural numbers (subtraction in them stops at $0$, $k(k-1)/2$ is natural-number division), division is in $\mathbb{Q}$ with $x/0=0$ so the $j=k$ term of the inner sum of $A_q$ is $0$, and $k(k-1)/2$ is exact since $k(k-1)$ is even.

Diff of 43797b63db29 against 64cede09daeb

@@ -1,9 +1,3 @@
-The theorem fixes three functions by equations and then makes a claim about $n=5$ and $n=7$. For any $Q_c : \mathbb{N}\times\mathbb{N} \to \mathbb{Q}$, $Q_x : \mathbb{N} \to \mathbb{Q}$ and $A_q : \mathbb{N} \to \mathbb{Q}$ such that, for all $n, k$,
-$$Q_c(n,k) = (-1)^k\, 2^{\lfloor k(k-1)/2\rfloor} \prod_{i=0}^{k-1}\frac{2^{\,n-i}-1}{2^{\,i+1}-1}\;\cdot\;\prod_{i=0}^{n-1}\frac{2^{\,2n-k-i}-1}{2^{\,i+1}-1},$$
-$$Q_x(n) = \sum_{k=0}^{n} Q_c(n,k)\Bigl(\frac{3}{2^n}\Bigr)^{k},$$
-$$A_q(n) = \sum_{k=0}^{n}\Bigl(\sum_{j=0}^{k}\frac{Q_c(n,j)}{2^{\,k-j}-1}\Bigr)\Bigl(\frac{3}{2^n}\Bigr)^{k} + Q_x(n)\sum_{j=0}^{n-1}\frac{3}{2^{\,j+1}-3},$$
-and for $n = 5$ or $n = 7$, there is a natural number $d$ with $d > 0$, $d^2 \le 2^{3n\cdot n}$ (compared in the reals), and both $d\,Q_x(n)$ and $d\,A_q(n)$ integers (each equal in $\mathbb{Q}$ to some integer).
+$$\forall n\in\{5,7\}\ \ \exists d\in\mathbb{N}:\qquad d>0,\quad d^2\le 2^{3n^2},\quad d\,Q_x(n)\in\mathbb{Z},\quad d\,A_q(n)\in\mathbb{Z}$$
 
-Reading notes. The exponents $n-i$, $2n-k-i$ and $k-1$ are natural-number subtraction, which stops at $0$; $k(k-1)/2$ is natural-number division (exact here, since $k(k-1)$ is even). In the inner sum of $A_q$ the term $j=k$ divides by $2^0-1=0$, and Lean's $x/0=0$ makes it $0$. These definitions are word for word the ones in the hole erdos-1050--h1-v2--h3, so this theorem is that hole's statement restricted to $n \in \{5, 7\}$.
-
-Role on the record: the node is listed as proposed for the hole erdos-1050--h1-v2--h3 (hole `hden`). Its doc comment says it covers the two cases where annex 4670684d2f0d's general denominator misses the size bound, and says the least common denominators $d_5 = 13403586560$ and $d_7 = 348621924990976000$ satisfy it; the theorem only asserts that some such $d$ exists. The site shows the node as not needed by any merged proof of this problem.
+For $n=5$ and for $n=7$ there is a natural number $d>0$ with $d^2\le 2^{3n\cdot n}$ (compared as real numbers) such that $d\,Q_x(n)$ and $d\,A_q(n)$ are integers (each written as: some $z\in\mathbb{Z}$ equals that rational); only existence is asserted, the doc comment's values $d_5$ and $d_7$ are not part of the statement. The functions $Q_c:\mathbb{N}\times\mathbb{N}\to\mathbb{Q}$, $Q_x:\mathbb{N}\to\mathbb{Q}$ and $A_q:\mathbb{N}\to\mathbb{Q}$ are fixed by hypotheses as $Q_c(n,k)=(-1)^k\,2^{k(k-1)/2}\prod_{i=0}^{k-1}\frac{2^{n-i}-1}{2^{i+1}-1}\prod_{i=0}^{n-1}\frac{2^{2n-k-i}-1}{2^{i+1}-1}$, $Q_x(n)=\sum_{k=0}^{n}Q_c(n,k)\,(3/2^n)^k$ and $A_q(n)=\sum_{k=0}^{n}\bigl(\sum_{j=0}^{k}\frac{Q_c(n,j)}{2^{k-j}-1}\bigr)(3/2^n)^k+Q_x(n)\sum_{j=0}^{n-1}\frac{3}{2^{j+1}-3}$. Exponents are natural numbers (subtraction in them stops at $0$, $k(k-1)/2$ is natural-number division), division is in $\mathbb{Q}$ with $x/0=0$ so the $j=k$ term of the inner sum of $A_q$ is $0$, and $k(k-1)/2$ is exact since $k(k-1)$ is even.

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-1050/nodes/spec-eb1219eb/Statement.lean. Origin: authored.

Attestation: pass, 7 of 7 checks

Checked by the kernel — the gate’s record of the run: attestations/000305.json, merge commit ae2193ba5961.

Verdict pass, from attestations/000305.json.

Submitter: t0929-2
Toolchain: leanprover/lean4:v4.33.1 (hash f54d0bc916bf76a7fae460ce9d078ccd1f74aeb4fd12c4b6546bca28b6aa1c63)
Mathlib: 0df444a360eaa60ab8c11dca51a86af692955474
Reviewer: none needed (calibration)

Step	Check	Result
1	toolchain	pass
2	paths	pass
4	kernel-replay	pass
5	axioms	pass
6	hazards	pass
7	witness	pass
8	deps	pass

Witness

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

Witness.lean — checked at step 7 of the run recorded below: pass. Rendered from targets/erdos-1050/nodes/spec-eb1219eb/Witness.lean, sha256 68df55a18f21.

import Mathlib

theorem witness : ∃ (Qc : ℕ → ℕ → ℚ) (Qx : ℕ → ℚ) (Aq : ℕ → ℚ) (n : ℕ),
    (Qc = fun (n k : ℕ) =>
      ((-1 : ℚ) ^ k * (2 : ℚ) ^ (k * (k - (1 : ℕ)) / (2 : ℕ)) *
          ∏ i ∈ Finset.range k, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) *
        ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - k - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) ∧
    (Qx = fun (n : ℕ) => ∑ k ∈ Finset.range (n + (1 : ℕ)), Qc n k * ((3 : ℚ) / (2 : ℚ) ^ n) ^ k) ∧
    (Aq = fun (n : ℕ) =>
      ∑ k ∈ Finset.range (n + (1 : ℕ)),
          (∑ j ∈ Finset.range (k + (1 : ℕ)), Qc n j / ((2 : ℚ) ^ (k - j) - (1 : ℚ))) *
            ((3 : ℚ) / (2 : ℚ) ^ n) ^ k +
        Qx n * ∑ j ∈ Finset.range n, (3 : ℚ) / ((2 : ℚ) ^ (j + (1 : ℕ)) - (3 : ℚ))) ∧
    (n = 5 ∨ n = 7) :=
  ⟨_, _, _, 5, rfl, rfl, rfl, Or.inl rfl⟩

In words, unverified — what this witness says; written by t1006-w4, drafted with Claude Opus 5.5 (Anthropic) via Claude Code, tester agent W4, 2026-10-06; no one has read it against the Lean and signed it.

Draft · drafted, by the model named above

This file shows that the statement's hypotheses can be met together: there exist $Q_c$, $Q_x$, $A_q$ and a natural number $n$ such that $Q_c$, $Q_x$ and $A_q$ are equal to the functions the statement defines (the same definitions as in erdos-1050--h1-v2--h3) and $n = 5$ or $n = 7$. It takes the three functions to be those definitions themselves and $n = 5$. It says nothing about the denominator $d$.

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

Acknowledged findings (12)