Problems / erdos-1050 / spec-f2b55478
Padé remainder coefficient identity
spec-f2b55478 erdos_1050_pade_remainder_coeff
proved
Proposed by a contributor.
$\displaystyle \forall n<m:\quad \sum_{j=0}^{n}\frac{(-1)^j\,2^{j(j-1)/2}\prod_{i=0}^{j-1}\frac{2^{\,n-i}-1}{2^{\,i+1}-1}\prod_{i=0}^{n-1}\frac{2^{\,2n-j-i}-1}{2^{\,i+1}-1}}{2^{\,m-j}-1} \;=\;\frac{2^{n^2}\prod_{i=0}^{n-1}(2^{\,i+1}-1)\prod_{i=0}^{n-1}\frac{2^{\,m-n-1-i}-1}{2^{\,i+1}-1}}{\prod_{j=0}^{n}(2^{\,m-j}-1)}$
For natural numbers $n<m$ this identity holds in $\mathbb{Q}$; the numerator of the $j$-th term on the left is $Q_c(n,j)$ as the Padé family defines it, so the left side is $\sum_{j=0}^{n}Q_c(n,j)/(2^{m-j}-1)$. All subtractions in exponents are natural-number subtraction, which stops at $0$, and $j(j-1)/2$ is natural-number division: since $j\le n<m$ no denominator is $0$ and $n-i$, $2n-j-i$ never truncate, while $m-n-1-i$ does when $m\le 2n$ (the factor $i=m-n-1$ is then $2^0-1=0$ and both sides are $0$). The doc comment's reading as a power-series coefficient, and its sign claim for $m>2n$, are not part of the statement.
Lean
theorem erdos_1050_pade_remainder_coeff (n m : ℕ) (hnm : n < m) :
∑ j ∈ Finset.range (n + 1),
(-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - 1) / 2) *
(∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1)) *
(∏ i ∈ Finset.range n, ((2 : ℚ) ^ (2 * n - j - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1)) /
((2 : ℚ) ^ (m - j) - 1) =
(2 : ℚ) ^ (n * n) * (∏ i ∈ Finset.range n, ((2 : ℚ) ^ (i + 1) - 1)) *
(∏ i ∈ Finset.range n, ((2 : ℚ) ^ (m - n - 1 - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1)) /
∏ j ∈ Finset.range (n + 1), ((2 : ℚ) ^ (m - j) - 1) := 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 →
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/4f07acacf80f….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
Write $c_j$ for the $j$-th numerator on the left, $c_j = (-1)^j 2^{\lfloor j(j-1)/2\rfloor}\prod_{i<j}\frac{2^{n-i}-1}{2^{i+1}-1}\prod_{i<n}\frac{2^{2n-j-i}-1}{2^{i+1}-1}$, and put $$N(x) = \prod_{i=0}^{n-1}\bigl(x - 2^{\,n+1+i}\bigr), \qquad D(x) = \prod_{k=0}^{n}\bigl(x - 2^{k}\bigr).$$ The proof shows that both sides of the theorem equal $N(2^m)/D(2^m)$. The left side is rewritten as $\sum_j c_j 2^j/(2^m-2^j)$ (hl), which is the partial-fraction expansion of $N(x)/D(x)$ at $x = 2^m$ (hpf, resting on the residue identity hres); the right side is rewritten directly as $N(2^m)/D(2^m)$ (hr). The last two lines are rw [hl, hr]; exact hpf. Code comments label hres, hpf, hl, hr as steps 4, 3, 1, 2 of the annex fcdb7a3a on this node.
Read it step by step (4 more sections)
The residue identity
Draft · drafted, by the model named above
hres: for each $j \le n$, $$c_j \cdot 2^j \cdot \prod_{k \le n,\, k \ne j}(2^j - 2^k) = N(2^j).$$ Write $n = j + r$ (hres.s1). Four product evaluations do the work. hres.E1test splits the product over $k \ne j$ into $k<j$ and $k = j+1+x$ with $x<r$ (by induction on $r$: hres.E1test.s1, hres.E1test.s2). hres.E2test: $\prod_{k<j}(2^j-2^k) = 2^{j(j-1)/2}\prod_{i<j}(2^{i+1}-1)$. hres.E3test: $\prod_{x<r}(2^j-2^{j+1+x}) = (-1)^r 2^{jr}\prod_{i<r}(2^{i+1}-1)$. hres.E4test: $N(2^j) = (-1)^{j+r}2^{j(j+r)}\prod_{i<j+r}(2^{r+1+i}-1)$. Then hres.F1 and hres.F2 reverse the order of the two numerator products of $c_j$ so that both become products of $2^{r+1+i}-1$, and hres.F3 splits $\prod_{i<j+r}(2^{i+1}-1)$ into its first $r$ and last $j$ factors. hres.hp collects the powers of two: $2\lfloor j(j-1)/2\rfloor + j + jr = j(j+r)$, using that $j(j-1)$ is even (hres.hp.h2; cases $j=0$, hres.hp.s2, and $j \ge 1$, hres.hp.s3). With every denominator product nonzero (hres.hQ, hres.hA and their instances hres.hQj, hres.hQr, hres.hAj), field_simp closes the identity.
Partial fractions by Lagrange interpolation
Draft · drafted, by the model named above
hpf: $\sum_{j=0}^{n} c_j 2^j/(2^m-2^j) = N(2^m)/D(2^m)$. The nodes $2^0,\dots,2^n$ are distinct (hpf.hinj), and $N$ has degree $n$, less than the number of nodes (hpf.hdeg), so $N$ equals its own Lagrange interpolant on those nodes (hpf.key, Mathlib's Lagrange.eq_interpolate_of_eval_eq). Evaluating both at $x = 2^m$ (hpf.hev) writes $N(2^m)$ as $\sum_j N(2^j)\prod_{k\ne j}\frac{2^m-2^k}{2^j-2^k}$. Dividing by $D(2^m) = (2^m-2^j)\prod_{k \ne j}(2^m-2^k)$ term by term, and substituting hres for $N(2^j)$, gives the left side. The divisions are legitimate because $j < m$ (hpf.hj'), so $2^m \ne 2^j$ (hpf.hxj), and the products $\prod_{k\ne j}(2^m-2^k)$ and $\prod_{k \ne j}(2^j - 2^k)$ are nonzero (hpf.hE1, hpf.hE2).
Rewriting the left side
Draft · drafted, by the model named above
hl: each term $c_j/(2^{m-j}-1)$ equals $c_j 2^j/(2^m-2^j)$. Since $j \le n < m$ (hl.hj'), $2^m = 2^{m-j}2^j$ (hl.h2), so $2^m - 2^j = (2^{m-j}-1)2^j$, and $2^j \ne 0$ (hl.hp) can be cancelled.
Rewriting the right side
Draft · drafted, by the model named above
hr: the right side equals $N(2^m)/D(2^m)$. First the factor $\prod_{i<n}(2^{i+1}-1)$, which is nonzero (hr.hB), cancels against the denominators inside the middle product, leaving $2^{n\cdot n}\prod_{i<n}(2^{m-n-1-i}-1)\big/\prod_{j\le n}(2^{m-j}-1)$ (hr.key). Then two cases.
If $m > 2n$ (hr.s3): no exponent truncates, and factoring out powers of two gives $\prod_{i<n}(2^{m-n-1-i}-1) = N(2^m)/2^{\sum_{i<n}(n+1+i)}$ (hr.s3.hA, from $2^m = 2^{m-n-1-i}2^{n+1+i}$, hr.s3.hA.e) and $\prod_{j \le n}(2^{m-j}-1) = D(2^m)/2^{\sum_{j\le n} j}$ (hr.s3.hD, from hr.s3.hD.e). The exponents differ by exactly $n\cdot n$ (hr.s3.hs: $\sum_{i<n}(n+1+i) = n\cdot n + \sum_{j\le n} j$), which cancels $2^{n\cdot n}$; with $D(2^m) \ne 0$ (hr.s3.hDX), field_simp finishes.
If $m \le 2n$ (hr.s4): the index $i = m-n-1$ lies below $n$, its factor $2^{m-n-1-i}-1$ is $2^0-1 = 0$ (hr.s4.hz1), and the same index makes the factor $2^m - 2^{n+1+i}$ of $N(2^m)$ zero (hr.s4.hz2), so both expressions are $0$.
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/4f07acacf80f….md · the first version of its chain
Read this version
Overview
Write $c_j$ for the $j$-th numerator on the left, $c_j = (-1)^j 2^{\lfloor j(j-1)/2\rfloor}\prod_{i<j}\frac{2^{n-i}-1}{2^{i+1}-1}\prod_{i<n}\frac{2^{2n-j-i}-1}{2^{i+1}-1}$, and put $$N(x) = \prod_{i=0}^{n-1}\bigl(x - 2^{\,n+1+i}\bigr), \qquad D(x) = \prod_{k=0}^{n}\bigl(x - 2^{k}\bigr).$$ The proof shows that both sides of the theorem equal $N(2^m)/D(2^m)$. The left side is rewritten as $\sum_j c_j 2^j/(2^m-2^j)$ (
hl), which is the partial-fraction expansion of $N(x)/D(x)$ at $x = 2^m$ (hpf, resting on the residue identityhres); the right side is rewritten directly as $N(2^m)/D(2^m)$ (hr). The last two lines arerw [hl, hr]; exact hpf. Code comments labelhres,hpf,hl,hras steps 4, 3, 1, 2 of the annex fcdb7a3a on this node.The residue identity (hres hres.s1 hres.E1test hres.E1test.s1 hres.E1test.s2 hres.E2test hres.E3test hres.E4test hres.hQ hres.hQ.this hres.hA hres.hA.this hres.F1 hres.F2 hres.F3 hres.hp hres.hp.h2 hres.hp.s2 hres.hp.s3 hres.hQj hres.hQr hres.hAj)
hres: for each $j \le n$, $$c_j \cdot 2^j \cdot \prod_{k \le n,\, k \ne j}(2^j - 2^k) = N(2^j).$$ Write $n = j + r$ (hres.s1). Four product evaluations do the work.hres.E1testsplits the product over $k \ne j$ into $k<j$ and $k = j+1+x$ with $x<r$ (by induction on $r$:hres.E1test.s1,hres.E1test.s2).hres.E2test: $\prod_{k<j}(2^j-2^k) = 2^{j(j-1)/2}\prod_{i<j}(2^{i+1}-1)$.hres.E3test: $\prod_{x<r}(2^j-2^{j+1+x}) = (-1)^r 2^{jr}\prod_{i<r}(2^{i+1}-1)$.hres.E4test: $N(2^j) = (-1)^{j+r}2^{j(j+r)}\prod_{i<j+r}(2^{r+1+i}-1)$. Thenhres.F1andhres.F2reverse the order of the two numerator products of $c_j$ so that both become products of $2^{r+1+i}-1$, andhres.F3splits $\prod_{i<j+r}(2^{i+1}-1)$ into its first $r$ and last $j$ factors.hres.hpcollects the powers of two: $2\lfloor j(j-1)/2\rfloor + j + jr = j(j+r)$, using that $j(j-1)$ is even (hres.hp.h2; cases $j=0$,hres.hp.s2, and $j \ge 1$,hres.hp.s3). With every denominator product nonzero (hres.hQ,hres.hAand their instanceshres.hQj,hres.hQr,hres.hAj),field_simpcloses the identity.Partial fractions by Lagrange interpolation (hpf hpf.hinj hpf.hdeg hpf.key hpf.hev hpf.hj' hpf.hxj hpf.hxj.this hpf.hE1 hpf.hE1.hk' hpf.hE1.this hpf.hE2)
hpf: $\sum_{j=0}^{n} c_j 2^j/(2^m-2^j) = N(2^m)/D(2^m)$. The nodes $2^0,\dots,2^n$ are distinct (hpf.hinj), and $N$ has degree $n$, less than the number of nodes (hpf.hdeg), so $N$ equals its own Lagrange interpolant on those nodes (hpf.key, Mathlib'sLagrange.eq_interpolate_of_eval_eq). Evaluating both at $x = 2^m$ (hpf.hev) writes $N(2^m)$ as $\sum_j N(2^j)\prod_{k\ne j}\frac{2^m-2^k}{2^j-2^k}$. Dividing by $D(2^m) = (2^m-2^j)\prod_{k \ne j}(2^m-2^k)$ term by term, and substitutinghresfor $N(2^j)$, gives the left side. The divisions are legitimate because $j < m$ (hpf.hj'), so $2^m \ne 2^j$ (hpf.hxj), and the products $\prod_{k\ne j}(2^m-2^k)$ and $\prod_{k \ne j}(2^j - 2^k)$ are nonzero (hpf.hE1,hpf.hE2).Rewriting the left side (hl hl.hj' hl.h2 hl.hp)
hl: each term $c_j/(2^{m-j}-1)$ equals $c_j 2^j/(2^m-2^j)$. Since $j \le n < m$ (hl.hj'), $2^m = 2^{m-j}2^j$ (hl.h2), so $2^m - 2^j = (2^{m-j}-1)2^j$, and $2^j \ne 0$ (hl.hp) can be cancelled.Rewriting the right side (hr hr.hB hr.hB.this hr.key hr.s3 hr.s3.hA hr.s3.hA.e hr.s3.hD hr.s3.hD.e hr.s3.hs hr.s3.hDX hr.s3.hDX.this hr.s4 hr.s4.hz1 hr.s4.hz2)
hr: the right side equals $N(2^m)/D(2^m)$. First the factor $\prod_{i<n}(2^{i+1}-1)$, which is nonzero (hr.hB), cancels against the denominators inside the middle product, leaving $2^{n\cdot n}\prod_{i<n}(2^{m-n-1-i}-1)\big/\prod_{j\le n}(2^{m-j}-1)$ (hr.key). Then two cases.If $m > 2n$ (
hr.s3): no exponent truncates, and factoring out powers of two gives $\prod_{i<n}(2^{m-n-1-i}-1) = N(2^m)/2^{\sum_{i<n}(n+1+i)}$ (hr.s3.hA, from $2^m = 2^{m-n-1-i}2^{n+1+i}$,hr.s3.hA.e) and $\prod_{j \le n}(2^{m-j}-1) = D(2^m)/2^{\sum_{j\le n} j}$ (hr.s3.hD, fromhr.s3.hD.e). The exponents differ by exactly $n\cdot n$ (hr.s3.hs: $\sum_{i<n}(n+1+i) = n\cdot n + \sum_{j\le n} j$), which cancels $2^{n\cdot n}$; with $D(2^m) \ne 0$ (hr.s3.hDX),field_simpfinishes.If $m \le 2n$ (
hr.s4): the index $i = m-n-1$ lies below $n$, its factor $2^{m-n-1-i}-1$ is $2^0-1 = 0$ (hr.s4.hz1), and the same index makes the factor $2^m - 2^{n+1+i}$ of $N(2^m)$ zero (hr.s4.hz2), so both expressions are $0$.
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, 000222, records the gate’s run.
The proof step by step (outline)
Checked by the kernel — an outline of the attested proof below: attestations/000222.json, merge commit 4148e3125651.
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.
hreshave∀ j ∈ Finset.range (n + (1 : ℕ)), (((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * (2 : ℚ) ^ j * ∏ k ∈ (Finset.range (n + (1 : ℕ))).erase j, ((2 : ℚ) ^ j - (2 : ℚ) ^ k) = ∏ i ∈ Finset.range n, ((2 : ℚ) ^ j - (2 : ℚ) ^ (n + (1 : ℕ) + i))Leaves
∑ j ∈ Finset.range (n + (1 : ℕ)), (((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) / ((2 : ℚ) ^ (m - j) - (1 : ℚ)) = (((2 : ℚ) ^ (n * n) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (m - n - (1 : ℕ) - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) / ∏ j ∈ Finset.range (n + (1 : ℕ)), ((2 : ℚ) ^ (m - j) - (1 : ℚ)), withhres : ∀ j ∈ Finset.range (n + (1 : ℕ)), (((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * (2 : ℚ) ^ j * ∏ k ∈ (Finset.range (n + (1 : ℕ))).erase j, ((2 : ℚ) ^ j - (2 : ℚ) ^ k) = ∏ i ∈ Finset.range n, ((2 : ℚ) ^ j - (2 : ℚ) ^ (n + (1 : ℕ) + i)).Uses library
Finset.rangerange nis the set of natural numbers less thann. ,Finset.mem_range,Finset.prod_div_distrib,pow_add.Lean, lines 21–112
have hres : ∀ j ∈ Finset.range (n + 1), ((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - 1) / 2) * (∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1)) * (∏ i ∈ Finset.range n, ((2 : ℚ) ^ (2 * n - j - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1))) * (2 : ℚ) ^ j * ∏ k ∈ (Finset.range (n + 1)).erase j, ((2 : ℚ) ^ j - (2 : ℚ) ^ k) = ∏ i ∈ Finset.range n, ((2 : ℚ) ^ j - (2 : ℚ) ^ (n + 1 + i)) := by intro j hj rw [Finset.mem_range] at hj obtain ⟨r, rfl⟩ : ∃ r, n = j + r := ⟨n - j, by omega⟩ have E1test : ∀ j r : ℕ, ∏ k ∈ (Finset.range (j + r + 1)).erase j, ((2:ℚ)^j - 2^k) = (∏ k ∈ Finset.range j, ((2:ℚ)^j - 2^k)) * ∏ x ∈ Finset.range r, ((2:ℚ)^j - 2^(j+1+x)) := by intro j r induction r with | zero => simp [Finset.range_add_one] | succ r ih => rw [show j + (r + 1) + 1 = (j + r + 1) + 1 by ring, Finset.range_add_one, Finset.erase_insert_of_ne (by omega), Finset.prod_insert (by simp), ih, Finset.prod_range_succ] rw [show j + 1 + r = j + r + 1 by ring] ring have E2test : ∀ j : ℕ, ∏ k ∈ Finset.range j, ((2:ℚ)^j - 2^k) = 2 ^ (j * (j - 1) / 2) * ∏ i ∈ Finset.range j, ((2:ℚ)^(i+1) - 1) := by intro j rw [← Finset.prod_range_reflect (fun i => (2:ℚ)^(i+1) - 1)] rw [show (2:ℚ) ^ (j * (j - 1) / 2) = ∏ k ∈ Finset.range j, (2:ℚ)^k by rw [Finset.prod_pow_eq_pow_sum, Finset.sum_range_id], ← Finset.prod_mul_distrib] apply Finset.prod_congr rfl intro k hk rw [Finset.mem_range] at hk rw [show j - 1 - k + 1 = j - k by omega, mul_sub, ← pow_add, show k + (j - k) = j by omega] ring have E3test : ∀ j r : ℕ, ∏ x ∈ Finset.range r, ((2:ℚ)^j - 2^(j+1+x)) = (-1) ^ r * 2 ^ (j * r) * ∏ i ∈ Finset.range r, ((2:ℚ)^(i+1) - 1) := by intro j r rw [show (-1:ℚ) ^ r * 2 ^ (j * r) = ∏ _x ∈ Finset.range r, (-(2:ℚ) ^ j) by rw [Finset.prod_const, Finset.card_range, pow_mul, ← mul_pow, neg_one_mul], ← Finset.prod_mul_distrib] apply Finset.prod_congr rfl intro i _ rw [show j + 1 + i = j + (i + 1) by ring, pow_add] ring have E4test : ∀ j r : ℕ, ∏ i ∈ Finset.range (j + r), ((2:ℚ)^j - 2^(j + r + 1 + i)) = (-1) ^ (j + r) * 2 ^ (j * (j + r)) * ∏ i ∈ Finset.range (j + r), ((2:ℚ)^(r + 1 + i) - 1) := by intro j r rw [show (-1:ℚ) ^ (j + r) * 2 ^ (j * (j + r)) = ∏ _x ∈ Finset.range (j + r), (-(2:ℚ) ^ j) by rw [Finset.prod_const, Finset.card_range, pow_mul, ← mul_pow, neg_one_mul], ← Finset.prod_mul_distrib] apply Finset.prod_congr rfl intro i _ rw [show j + r + 1 + i = j + (r + 1 + i) by ring, pow_add] ring have hQ : ∀ t : ℕ, ∏ i ∈ Finset.range t, ((2 : ℚ) ^ (i + 1) - 1) ≠ 0 := by intro t rw [Finset.prod_ne_zero_iff] intro i _ have : (1 : ℚ) < 2 ^ (i + 1) := one_lt_pow₀ (by norm_num) (by omega) linarith have hA : ∀ t : ℕ, ∏ i ∈ Finset.range t, ((2 : ℚ) ^ (r + 1 + i) - 1) ≠ 0 := by intro t rw [Finset.prod_ne_zero_iff] intro i _ have : (1 : ℚ) < 2 ^ (r + 1 + i) := one_lt_pow₀ (by norm_num) (by omega) linarith have F1 : ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (j + r - i) - 1) = ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (r + 1 + i) - 1) := by rw [← Finset.prod_range_reflect (fun i => (2 : ℚ) ^ (r + 1 + i) - 1)] apply Finset.prod_congr rfl intro i hi rw [Finset.mem_range] at hi rw [show r + 1 + (j - 1 - i) = j + r - i by omega] have F2 : ∏ i ∈ Finset.range (j + r), ((2 : ℚ) ^ (2 * (j + r) - j - i) - 1) = ∏ i ∈ Finset.range (j + r), ((2 : ℚ) ^ (r + 1 + i) - 1) := by rw [← Finset.prod_range_reflect (fun i => (2 : ℚ) ^ (r + 1 + i) - 1)] apply Finset.prod_congr rfl intro i hi rw [Finset.mem_range] at hi rw [show r + 1 + (j + r - 1 - i) = 2 * (j + r) - j - i by omega] have F3 : ∏ i ∈ Finset.range (j + r), ((2 : ℚ) ^ (i + 1) - 1) = (∏ i ∈ Finset.range r, ((2 : ℚ) ^ (i + 1) - 1)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (r + 1 + i) - 1) := by rw [add_comm j r, Finset.prod_range_add] congr 1 apply Finset.prod_congr rfl intro i _ rw [show r + i + 1 = r + 1 + i by ring] have hp : (2 : ℚ) ^ (j * (j - 1) / 2) * 2 ^ (j * (j - 1) / 2) * 2 ^ j * 2 ^ (j * r) = 2 ^ (j * (j + r)) := by rw [← pow_add, ← pow_add, ← pow_add] congr 1 have h2 := Nat.two_mul_div_two_of_even (Nat.even_mul_pred_self j) rcases j with _ | s · simp · simp only [Nat.add_sub_cancel] at h2 ⊢ zify at h2 ⊢ linear_combination h2 rw [Finset.prod_div_distrib, Finset.prod_div_distrib, F1, F2, F3, E1test, E2test, E3test, E4test] have hQj := hQ j have hQr := hQ r have hAj := hA j rw [← hp, pow_add (-1 : ℚ)] field_simptargets/erdos-1050/nodes/spec-f2b55478/Proof.lean, lines 21–112 at
4148e3125651↗hres.s1obtain∃ (r : ℕ), n = j + rLeaves
(((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (j + r - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range (j + r), ((2 : ℚ) ^ ((2 : ℕ) * (j + r) - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * (2 : ℚ) ^ j * ∏ k ∈ (Finset.range (j + r + (1 : ℕ))).erase j, ((2 : ℚ) ^ j - (2 : ℚ) ^ k) = ∏ i ∈ Finset.range (j + r), ((2 : ℚ) ^ j - (2 : ℚ) ^ (j + r + (1 : ℕ) + i)), withr : ℕ,hnm : j + r < m,hj : j < j + r + (1 : ℕ).Uses library
Exists.introExistential introduction. .Lean, line 26
obtain ⟨r, rfl⟩ : ∃ r, n = j + r := ⟨n - j, by omega⟩
targets/erdos-1050/nodes/spec-f2b55478/Proof.lean, line 26 at
4148e3125651↗hres.E1testhave∀ (j r : ℕ), ∏ k ∈ (Finset.range (j + r + (1 : ℕ))).erase j, ((2 : ℚ) ^ j - (2 : ℚ) ^ k) = (∏ k ∈ Finset.range j, ((2 : ℚ) ^ j - (2 : ℚ) ^ k)) * ∏ x ∈ Finset.range r, ((2 : ℚ) ^ j - (2 : ℚ) ^ (j + (1 : ℕ) + x))Leaves
(((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (j + r - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range (j + r), ((2 : ℚ) ^ ((2 : ℕ) * (j + r) - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * (2 : ℚ) ^ j * ∏ k ∈ (Finset.range (j + r + (1 : ℕ))).erase j, ((2 : ℚ) ^ j - (2 : ℚ) ^ k) = ∏ i ∈ Finset.range (j + r), ((2 : ℚ) ^ j - (2 : ℚ) ^ (j + r + (1 : ℕ) + i)), withE1test : ∀ (j r : ℕ), ∏ k ∈ (Finset.range (j + r + (1 : ℕ))).erase j, ((2 : ℚ) ^ j - (2 : ℚ) ^ k) = (∏ k ∈ Finset.range j, ((2 : ℚ) ^ j - (2 : ℚ) ^ k)) * ∏ x ∈ Finset.range r, ((2 : ℚ) ^ j - (2 : ℚ) ^ (j + (1 : ℕ) + x)).Uses library
Finset.rangerange nis the set of natural numbers less thann. .Lean, lines 27–38
have E1test : ∀ j r : ℕ, ∏ k ∈ (Finset.range (j + r + 1)).erase j, ((2:ℚ)^j - 2^k) = (∏ k ∈ Finset.range j, ((2:ℚ)^j - 2^k)) * ∏ x ∈ Finset.range r, ((2:ℚ)^j - 2^(j+1+x)) := by intro j r induction r with | zero => simp [Finset.range_add_one] | succ r ih => rw [show j + (r + 1) + 1 = (j + r + 1) + 1 by ring, Finset.range_add_one, Finset.erase_insert_of_ne (by omega), Finset.prod_insert (by simp), ih, Finset.prod_range_succ] rw [show j + 1 + r = j + r + 1 by ring] ringtargets/erdos-1050/nodes/spec-f2b55478/Proof.lean, lines 27–38 at
4148e3125651↗hres.E1test.s1case routine: simpLeaves
∏ k ∈ (Finset.range (j + (0 : ℕ) + (1 : ℕ))).erase j, ((2 : ℚ) ^ j - (2 : ℚ) ^ k) = (∏ k ∈ Finset.range j, ((2 : ℚ) ^ j - (2 : ℚ) ^ k)) * ∏ x ∈ Finset.range (0 : ℕ), ((2 : ℚ) ^ j - (2 : ℚ) ^ (j + (1 : ℕ) + x)).Uses library
Nat.zeroZero, the smallest natural number. ,Finset.range_add_one.Lean, lines 31–32
| zero => simp [Finset.range_add_one]targets/erdos-1050/nodes/spec-f2b55478/Proof.lean, lines 31–32 at
4148e3125651↗hres.E1test.s2caseLeaves
∏ k ∈ (Finset.range (j + (r + (1 : ℕ)) + (1 : ℕ))).erase j, ((2 : ℚ) ^ j - (2 : ℚ) ^ k) = (∏ k ∈ Finset.range j, ((2 : ℚ) ^ j - (2 : ℚ) ^ k)) * ∏ x ∈ Finset.range (r + (1 : ℕ)), ((2 : ℚ) ^ j - (2 : ℚ) ^ (j + (1 : ℕ) + x)), withr : ℕ,ih : ∏ k ∈ (Finset.range (j + r + (1 : ℕ))).erase j, ((2 : ℚ) ^ j - (2 : ℚ) ^ k) = (∏ k ∈ Finset.range j, ((2 : ℚ) ^ j - (2 : ℚ) ^ k)) * ∏ x ∈ Finset.range r, ((2 : ℚ) ^ j - (2 : ℚ) ^ (j + (1 : ℕ) + x)).Uses library
Nat.succThe successor of a natural numbern. ,Finset.range_add_one,Finset.erase_insert_of_ne,Finset.prod_insert,Finset.prod_range_succ.Lean, lines 33–38
| succ r ih => rw [show j + (r + 1) + 1 = (j + r + 1) + 1 by ring, Finset.range_add_one, Finset.erase_insert_of_ne (by omega), Finset.prod_insert (by simp), ih, Finset.prod_range_succ] rw [show j + 1 + r = j + r + 1 by ring] ringtargets/erdos-1050/nodes/spec-f2b55478/Proof.lean, lines 33–38 at
4148e3125651↗
hres.E2testhave∀ (j : ℕ), ∏ k ∈ Finset.range j, ((2 : ℚ) ^ j - (2 : ℚ) ^ k) = (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))Leaves
(((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (j + r - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range (j + r), ((2 : ℚ) ^ ((2 : ℕ) * (j + r) - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * (2 : ℚ) ^ j * ∏ k ∈ (Finset.range (j + r + (1 : ℕ))).erase j, ((2 : ℚ) ^ j - (2 : ℚ) ^ k) = ∏ i ∈ Finset.range (j + r), ((2 : ℚ) ^ j - (2 : ℚ) ^ (j + r + (1 : ℕ) + i)), withE2test : ∀ (j : ℕ), ∏ k ∈ Finset.range j, ((2 : ℚ) ^ j - (2 : ℚ) ^ k) = (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ)).Uses library
Finset.rangerange nis the set of natural numbers less thann. ,Finset.prod_range_reflect,Finset.prod_pow_eq_pow_sum,Finset.sum_range_idGauss' summation formula ,Finset.prod_mul_distrib,Finset.prod_congr,rflrfl : a = ais the unique constructor of the equality type. ,Finset.mem_range,mul_subAlias ofmul_sub_left_distrib. ,pow_add.Lean, lines 39–49
have E2test : ∀ j : ℕ, ∏ k ∈ Finset.range j, ((2:ℚ)^j - 2^k) = 2 ^ (j * (j - 1) / 2) * ∏ i ∈ Finset.range j, ((2:ℚ)^(i+1) - 1) := by intro j rw [← Finset.prod_range_reflect (fun i => (2:ℚ)^(i+1) - 1)] rw [show (2:ℚ) ^ (j * (j - 1) / 2) = ∏ k ∈ Finset.range j, (2:ℚ)^k by rw [Finset.prod_pow_eq_pow_sum, Finset.sum_range_id], ← Finset.prod_mul_distrib] apply Finset.prod_congr rfl intro k hk rw [Finset.mem_range] at hk rw [show j - 1 - k + 1 = j - k by omega, mul_sub, ← pow_add, show k + (j - k) = j by omega] ringtargets/erdos-1050/nodes/spec-f2b55478/Proof.lean, lines 39–49 at
4148e3125651↗hres.E3testhave∀ (j r : ℕ), ∏ x ∈ Finset.range r, ((2 : ℚ) ^ j - (2 : ℚ) ^ (j + (1 : ℕ) + x)) = (-1 : ℚ) ^ r * (2 : ℚ) ^ (j * r) * ∏ i ∈ Finset.range r, ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))Leaves
(((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (j + r - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range (j + r), ((2 : ℚ) ^ ((2 : ℕ) * (j + r) - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * (2 : ℚ) ^ j * ∏ k ∈ (Finset.range (j + r + (1 : ℕ))).erase j, ((2 : ℚ) ^ j - (2 : ℚ) ^ k) = ∏ i ∈ Finset.range (j + r), ((2 : ℚ) ^ j - (2 : ℚ) ^ (j + r + (1 : ℕ) + i)), withE3test : ∀ (j r : ℕ), ∏ x ∈ Finset.range r, ((2 : ℚ) ^ j - (2 : ℚ) ^ (j + (1 : ℕ) + x)) = (-1 : ℚ) ^ r * (2 : ℚ) ^ (j * r) * ∏ i ∈ Finset.range r, ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ)).Uses library
Finset.rangerange nis the set of natural numbers less thann. ,Finset.prod_const,Finset.card_range,pow_mul,mul_pow,neg_one_mulThe additive inverse of one multiplied by an element of a ring is the element's additive inverse. ,Finset.prod_mul_distrib,Finset.prod_congr,rflrfl : a = ais the unique constructor of the equality type. ,pow_add.Lean, lines 50–58
have E3test : ∀ j r : ℕ, ∏ x ∈ Finset.range r, ((2:ℚ)^j - 2^(j+1+x)) = (-1) ^ r * 2 ^ (j * r) * ∏ i ∈ Finset.range r, ((2:ℚ)^(i+1) - 1) := by intro j r rw [show (-1:ℚ) ^ r * 2 ^ (j * r) = ∏ _x ∈ Finset.range r, (-(2:ℚ) ^ j) by rw [Finset.prod_const, Finset.card_range, pow_mul, ← mul_pow, neg_one_mul], ← Finset.prod_mul_distrib] apply Finset.prod_congr rfl intro i _ rw [show j + 1 + i = j + (i + 1) by ring, pow_add] ringtargets/erdos-1050/nodes/spec-f2b55478/Proof.lean, lines 50–58 at
4148e3125651↗hres.E4testhave∀ (j r : ℕ), ∏ i ∈ Finset.range (j + r), ((2 : ℚ) ^ j - (2 : ℚ) ^ (j + r + (1 : ℕ) + i)) = (-1 : ℚ) ^ (j + r) * (2 : ℚ) ^ (j * (j + r)) * ∏ i ∈ Finset.range (j + r), ((2 : ℚ) ^ (r + (1 : ℕ) + i) - (1 : ℚ))Leaves
(((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (j + r - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range (j + r), ((2 : ℚ) ^ ((2 : ℕ) * (j + r) - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * (2 : ℚ) ^ j * ∏ k ∈ (Finset.range (j + r + (1 : ℕ))).erase j, ((2 : ℚ) ^ j - (2 : ℚ) ^ k) = ∏ i ∈ Finset.range (j + r), ((2 : ℚ) ^ j - (2 : ℚ) ^ (j + r + (1 : ℕ) + i)), withE4test : ∀ (j r : ℕ), ∏ i ∈ Finset.range (j + r), ((2 : ℚ) ^ j - (2 : ℚ) ^ (j + r + (1 : ℕ) + i)) = (-1 : ℚ) ^ (j + r) * (2 : ℚ) ^ (j * (j + r)) * ∏ i ∈ Finset.range (j + r), ((2 : ℚ) ^ (r + (1 : ℕ) + i) - (1 : ℚ)).Uses library
Finset.rangerange nis the set of natural numbers less thann. ,Finset.prod_const,Finset.card_range,pow_mul,mul_pow,neg_one_mulThe additive inverse of one multiplied by an element of a ring is the element's additive inverse. ,Finset.prod_mul_distrib,Finset.prod_congr,rflrfl : a = ais the unique constructor of the equality type. ,pow_add.Lean, lines 59–67
have E4test : ∀ j r : ℕ, ∏ i ∈ Finset.range (j + r), ((2:ℚ)^j - 2^(j + r + 1 + i)) = (-1) ^ (j + r) * 2 ^ (j * (j + r)) * ∏ i ∈ Finset.range (j + r), ((2:ℚ)^(r + 1 + i) - 1) := by intro j r rw [show (-1:ℚ) ^ (j + r) * 2 ^ (j * (j + r)) = ∏ _x ∈ Finset.range (j + r), (-(2:ℚ) ^ j) by rw [Finset.prod_const, Finset.card_range, pow_mul, ← mul_pow, neg_one_mul], ← Finset.prod_mul_distrib] apply Finset.prod_congr rfl intro i _ rw [show j + r + 1 + i = j + (r + 1 + i) by ring, pow_add] ringtargets/erdos-1050/nodes/spec-f2b55478/Proof.lean, lines 59–67 at
4148e3125651↗hres.hQhave∀ (t : ℕ), ∏ i ∈ Finset.range t, ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ)) ≠ (0 : ℚ)Leaves
(((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (j + r - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range (j + r), ((2 : ℚ) ^ ((2 : ℕ) * (j + r) - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * (2 : ℚ) ^ j * ∏ k ∈ (Finset.range (j + r + (1 : ℕ))).erase j, ((2 : ℚ) ^ j - (2 : ℚ) ^ k) = ∏ i ∈ Finset.range (j + r), ((2 : ℚ) ^ j - (2 : ℚ) ^ (j + r + (1 : ℕ) + i)), withhQ : ∀ (t : ℕ), ∏ i ∈ Finset.range t, ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ)) ≠ (0 : ℚ).Uses library
Finset.rangerange nis the set of natural numbers less thann. ,Finset.prod_ne_zero_iff.Lean, lines 68–73
have hQ : ∀ t : ℕ, ∏ i ∈ Finset.range t, ((2 : ℚ) ^ (i + 1) - 1) ≠ 0 := by intro t rw [Finset.prod_ne_zero_iff] intro i _ have : (1 : ℚ) < 2 ^ (i + 1) := one_lt_pow₀ (by norm_num) (by omega) linarithtargets/erdos-1050/nodes/spec-f2b55478/Proof.lean, lines 68–73 at
4148e3125651↗hres.hQ.thishave(1 : ℚ) < (2 : ℚ) ^ (i + (1 : ℕ))Leaves
(2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ) ≠ (0 : ℚ), withthis : (1 : ℚ) < (2 : ℚ) ^ (i + (1 : ℕ)).Uses library
one_lt_pow₀.Lean, line 72
have : (1 : ℚ) < 2 ^ (i + 1) := one_lt_pow₀ (by norm_num) (by omega)
targets/erdos-1050/nodes/spec-f2b55478/Proof.lean, line 72 at
4148e3125651↗
hres.hAhave∀ (t : ℕ), ∏ i ∈ Finset.range t, ((2 : ℚ) ^ (r + (1 : ℕ) + i) - (1 : ℚ)) ≠ (0 : ℚ)Leaves
(((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (j + r - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range (j + r), ((2 : ℚ) ^ ((2 : ℕ) * (j + r) - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * (2 : ℚ) ^ j * ∏ k ∈ (Finset.range (j + r + (1 : ℕ))).erase j, ((2 : ℚ) ^ j - (2 : ℚ) ^ k) = ∏ i ∈ Finset.range (j + r), ((2 : ℚ) ^ j - (2 : ℚ) ^ (j + r + (1 : ℕ) + i)), withhA : ∀ (t : ℕ), ∏ i ∈ Finset.range t, ((2 : ℚ) ^ (r + (1 : ℕ) + i) - (1 : ℚ)) ≠ (0 : ℚ).Uses library
Finset.rangerange nis the set of natural numbers less thann. ,Finset.prod_ne_zero_iff.Lean, lines 74–79
have hA : ∀ t : ℕ, ∏ i ∈ Finset.range t, ((2 : ℚ) ^ (r + 1 + i) - 1) ≠ 0 := by intro t rw [Finset.prod_ne_zero_iff] intro i _ have : (1 : ℚ) < 2 ^ (r + 1 + i) := one_lt_pow₀ (by norm_num) (by omega) linarithtargets/erdos-1050/nodes/spec-f2b55478/Proof.lean, lines 74–79 at
4148e3125651↗hres.hA.thishave(1 : ℚ) < (2 : ℚ) ^ (r + (1 : ℕ) + i)Leaves
(2 : ℚ) ^ (r + (1 : ℕ) + i) - (1 : ℚ) ≠ (0 : ℚ), withthis : (1 : ℚ) < (2 : ℚ) ^ (r + (1 : ℕ) + i).Uses library
one_lt_pow₀.Lean, line 78
have : (1 : ℚ) < 2 ^ (r + 1 + i) := one_lt_pow₀ (by norm_num) (by omega)
targets/erdos-1050/nodes/spec-f2b55478/Proof.lean, line 78 at
4148e3125651↗
hres.F1have∏ i ∈ Finset.range j, ((2 : ℚ) ^ (j + r - i) - (1 : ℚ)) = ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (r + (1 : ℕ) + i) - (1 : ℚ))Leaves
(((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (j + r - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range (j + r), ((2 : ℚ) ^ ((2 : ℕ) * (j + r) - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * (2 : ℚ) ^ j * ∏ k ∈ (Finset.range (j + r + (1 : ℕ))).erase j, ((2 : ℚ) ^ j - (2 : ℚ) ^ k) = ∏ i ∈ Finset.range (j + r), ((2 : ℚ) ^ j - (2 : ℚ) ^ (j + r + (1 : ℕ) + i)), withF1 : ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (j + r - i) - (1 : ℚ)) = ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (r + (1 : ℕ) + i) - (1 : ℚ)).Uses library
Finset.rangerange nis the set of natural numbers less thann. ,Finset.prod_range_reflect,Finset.prod_congr,rflrfl : a = ais the unique constructor of the equality type. ,Finset.mem_range.Lean, lines 80–85
have F1 : ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (j + r - i) - 1) = ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (r + 1 + i) - 1) := by rw [← Finset.prod_range_reflect (fun i => (2 : ℚ) ^ (r + 1 + i) - 1)] apply Finset.prod_congr rfl intro i hi rw [Finset.mem_range] at hi rw [show r + 1 + (j - 1 - i) = j + r - i by omega]targets/erdos-1050/nodes/spec-f2b55478/Proof.lean, lines 80–85 at
4148e3125651↗hres.F2have∏ i ∈ Finset.range (j + r), ((2 : ℚ) ^ ((2 : ℕ) * (j + r) - j - i) - (1 : ℚ)) = ∏ i ∈ Finset.range (j + r), ((2 : ℚ) ^ (r + (1 : ℕ) + i) - (1 : ℚ))Leaves
(((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (j + r - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range (j + r), ((2 : ℚ) ^ ((2 : ℕ) * (j + r) - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * (2 : ℚ) ^ j * ∏ k ∈ (Finset.range (j + r + (1 : ℕ))).erase j, ((2 : ℚ) ^ j - (2 : ℚ) ^ k) = ∏ i ∈ Finset.range (j + r), ((2 : ℚ) ^ j - (2 : ℚ) ^ (j + r + (1 : ℕ) + i)), withF2 : ∏ i ∈ Finset.range (j + r), ((2 : ℚ) ^ ((2 : ℕ) * (j + r) - j - i) - (1 : ℚ)) = ∏ i ∈ Finset.range (j + r), ((2 : ℚ) ^ (r + (1 : ℕ) + i) - (1 : ℚ)).Uses library
Finset.rangerange nis the set of natural numbers less thann. ,Finset.prod_range_reflect,Finset.prod_congr,rflrfl : a = ais the unique constructor of the equality type. ,Finset.mem_range.Lean, lines 86–91
have F2 : ∏ i ∈ Finset.range (j + r), ((2 : ℚ) ^ (2 * (j + r) - j - i) - 1) = ∏ i ∈ Finset.range (j + r), ((2 : ℚ) ^ (r + 1 + i) - 1) := by rw [← Finset.prod_range_reflect (fun i => (2 : ℚ) ^ (r + 1 + i) - 1)] apply Finset.prod_congr rfl intro i hi rw [Finset.mem_range] at hi rw [show r + 1 + (j + r - 1 - i) = 2 * (j + r) - j - i by omega]targets/erdos-1050/nodes/spec-f2b55478/Proof.lean, lines 86–91 at
4148e3125651↗hres.F3have∏ i ∈ Finset.range (j + r), ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ)) = (∏ i ∈ Finset.range r, ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (r + (1 : ℕ) + i) - (1 : ℚ))Leaves
(((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (j + r - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range (j + r), ((2 : ℚ) ^ ((2 : ℕ) * (j + r) - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * (2 : ℚ) ^ j * ∏ k ∈ (Finset.range (j + r + (1 : ℕ))).erase j, ((2 : ℚ) ^ j - (2 : ℚ) ^ k) = ∏ i ∈ Finset.range (j + r), ((2 : ℚ) ^ j - (2 : ℚ) ^ (j + r + (1 : ℕ) + i)), withF3 : ∏ i ∈ Finset.range (j + r), ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ)) = (∏ i ∈ Finset.range r, ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (r + (1 : ℕ) + i) - (1 : ℚ)).Uses library
Finset.rangerange nis the set of natural numbers less thann. ,add_comm,Finset.prod_range_add,Finset.prod_congr,rflrfl : a = ais the unique constructor of the equality type. .Lean, lines 92–97
have F3 : ∏ i ∈ Finset.range (j + r), ((2 : ℚ) ^ (i + 1) - 1) = (∏ i ∈ Finset.range r, ((2 : ℚ) ^ (i + 1) - 1)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (r + 1 + i) - 1) := by rw [add_comm j r, Finset.prod_range_add] congr 1 apply Finset.prod_congr rfl intro i _ rw [show r + i + 1 = r + 1 + i by ring]targets/erdos-1050/nodes/spec-f2b55478/Proof.lean, lines 92–97 at
4148e3125651↗hres.hphave(2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * (2 : ℚ) ^ j * (2 : ℚ) ^ (j * r) = (2 : ℚ) ^ (j * (j + r))Leaves
(((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (j + r - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range (j + r), ((2 : ℚ) ^ ((2 : ℕ) * (j + r) - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * (2 : ℚ) ^ j * ∏ k ∈ (Finset.range (j + r + (1 : ℕ))).erase j, ((2 : ℚ) ^ j - (2 : ℚ) ^ k) = ∏ i ∈ Finset.range (j + r), ((2 : ℚ) ^ j - (2 : ℚ) ^ (j + r + (1 : ℕ) + i)), withhp : (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * (2 : ℚ) ^ j * (2 : ℚ) ^ (j * r) = (2 : ℚ) ^ (j * (j + r)).Uses library
pow_add.Lean, lines 98–106
have hp : (2 : ℚ) ^ (j * (j - 1) / 2) * 2 ^ (j * (j - 1) / 2) * 2 ^ j * 2 ^ (j * r) = 2 ^ (j * (j + r)) := by rw [← pow_add, ← pow_add, ← pow_add] congr 1 have h2 := Nat.two_mul_div_two_of_even (Nat.even_mul_pred_self j) rcases j with _ | s · simp · simp only [Nat.add_sub_cancel] at h2 ⊢ zify at h2 ⊢ linear_combination h2targets/erdos-1050/nodes/spec-f2b55478/Proof.lean, lines 98–106 at
4148e3125651↗hres.hp.h2have(2 : ℕ) * (j * (j - (1 : ℕ)) / (2 : ℕ)) = j * (j - (1 : ℕ))Leaves
j * (j - (1 : ℕ)) / (2 : ℕ) + j * (j - (1 : ℕ)) / (2 : ℕ) + j + j * r = j * (j + r), withh2 : (2 : ℕ) * (j * (j - (1 : ℕ)) / (2 : ℕ)) = j * (j - (1 : ℕ)).Uses library
Nat.two_mul_div_two_of_even,Nat.even_mul_pred_self.Lean, line 101
have h2 := Nat.two_mul_div_two_of_even (Nat.even_mul_pred_self j)
targets/erdos-1050/nodes/spec-f2b55478/Proof.lean, line 101 at
4148e3125651↗hres.hp.s2case routine: simpLeaves
(0 : ℕ) * ((0 : ℕ) - (1 : ℕ)) / (2 : ℕ) + (0 : ℕ) * ((0 : ℕ) - (1 : ℕ)) / (2 : ℕ) + (0 : ℕ) + (0 : ℕ) * r = (0 : ℕ) * ((0 : ℕ) + r).hres.hp.s3caseLeaves
(s + (1 : ℕ)) * (s + (1 : ℕ) - (1 : ℕ)) / (2 : ℕ) + (s + (1 : ℕ)) * (s + (1 : ℕ) - (1 : ℕ)) / (2 : ℕ) + (s + (1 : ℕ)) + (s + (1 : ℕ)) * r = (s + (1 : ℕ)) * (s + (1 : ℕ) + r).Uses library
Nat.add_sub_cancel.Lean, lines 104–106
· simp only [Nat.add_sub_cancel] at h2 ⊢ zify at h2 ⊢ linear_combination h2targets/erdos-1050/nodes/spec-f2b55478/Proof.lean, lines 104–106 at
4148e3125651↗
hres.hQjhave∏ i ∈ Finset.range j, ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ)) ≠ (0 : ℚ)Leaves
(-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ((∏ i ∈ Finset.range j, ((2 : ℚ) ^ (r + (1 : ℕ) + i) - (1 : ℚ))) / ∏ x ∈ Finset.range j, ((2 : ℚ) ^ (x + (1 : ℕ)) - (1 : ℚ))) * ((∏ i ∈ Finset.range (j + r), ((2 : ℚ) ^ (r + (1 : ℕ) + i) - (1 : ℚ))) / ((∏ i ∈ Finset.range r, ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (r + (1 : ℕ) + i) - (1 : ℚ)))) * (2 : ℚ) ^ j * (((2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ((-1 : ℚ) ^ r * (2 : ℚ) ^ (j * r) * ∏ i ∈ Finset.range r, ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ)))) = (-1 : ℚ) ^ (j + r) * (2 : ℚ) ^ (j * (j + r)) * ∏ i ∈ Finset.range (j + r), ((2 : ℚ) ^ (r + (1 : ℕ) + i) - (1 : ℚ)), withhQj : ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ)) ≠ (0 : ℚ).Lean, line 108
have hQj := hQ j
targets/erdos-1050/nodes/spec-f2b55478/Proof.lean, line 108 at
4148e3125651↗hres.hQrhave∏ i ∈ Finset.range r, ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ)) ≠ (0 : ℚ)Leaves
(-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ((∏ i ∈ Finset.range j, ((2 : ℚ) ^ (r + (1 : ℕ) + i) - (1 : ℚ))) / ∏ x ∈ Finset.range j, ((2 : ℚ) ^ (x + (1 : ℕ)) - (1 : ℚ))) * ((∏ i ∈ Finset.range (j + r), ((2 : ℚ) ^ (r + (1 : ℕ) + i) - (1 : ℚ))) / ((∏ i ∈ Finset.range r, ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (r + (1 : ℕ) + i) - (1 : ℚ)))) * (2 : ℚ) ^ j * (((2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ((-1 : ℚ) ^ r * (2 : ℚ) ^ (j * r) * ∏ i ∈ Finset.range r, ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ)))) = (-1 : ℚ) ^ (j + r) * (2 : ℚ) ^ (j * (j + r)) * ∏ i ∈ Finset.range (j + r), ((2 : ℚ) ^ (r + (1 : ℕ) + i) - (1 : ℚ)), withhQr : ∏ i ∈ Finset.range r, ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ)) ≠ (0 : ℚ).Lean, line 109
have hQr := hQ r
targets/erdos-1050/nodes/spec-f2b55478/Proof.lean, line 109 at
4148e3125651↗hres.hAjhave∏ i ∈ Finset.range j, ((2 : ℚ) ^ (r + (1 : ℕ) + i) - (1 : ℚ)) ≠ (0 : ℚ)Leaves
(-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ((∏ i ∈ Finset.range j, ((2 : ℚ) ^ (r + (1 : ℕ) + i) - (1 : ℚ))) / ∏ x ∈ Finset.range j, ((2 : ℚ) ^ (x + (1 : ℕ)) - (1 : ℚ))) * ((∏ i ∈ Finset.range (j + r), ((2 : ℚ) ^ (r + (1 : ℕ) + i) - (1 : ℚ))) / ((∏ i ∈ Finset.range r, ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (r + (1 : ℕ) + i) - (1 : ℚ)))) * (2 : ℚ) ^ j * (((2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ((-1 : ℚ) ^ r * (2 : ℚ) ^ (j * r) * ∏ i ∈ Finset.range r, ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ)))) = (-1 : ℚ) ^ (j + r) * (2 : ℚ) ^ (j * (j + r)) * ∏ i ∈ Finset.range (j + r), ((2 : ℚ) ^ (r + (1 : ℕ) + i) - (1 : ℚ)), withhAj : ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (r + (1 : ℕ) + i) - (1 : ℚ)) ≠ (0 : ℚ).Lean, line 110
have hAj := hA j
targets/erdos-1050/nodes/spec-f2b55478/Proof.lean, line 110 at
4148e3125651↗
hpfhave∑ j ∈ Finset.range (n + (1 : ℕ)), (((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * (2 : ℚ) ^ j / ((2 : ℚ) ^ m - (2 : ℚ) ^ j) = (∏ i ∈ Finset.range n, ((2 : ℚ) ^ m - (2 : ℚ) ^ (n + (1 : ℕ) + i))) / ∏ k ∈ Finset.range (n + (1 : ℕ)), ((2 : ℚ) ^ m - (2 : ℚ) ^ k)Leaves
∑ j ∈ Finset.range (n + (1 : ℕ)), (((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) / ((2 : ℚ) ^ (m - j) - (1 : ℚ)) = (((2 : ℚ) ^ (n * n) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (m - n - (1 : ℕ) - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) / ∏ j ∈ Finset.range (n + (1 : ℕ)), ((2 : ℚ) ^ (m - j) - (1 : ℚ)), withhpf : ∑ j ∈ Finset.range (n + (1 : ℕ)), (((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * (2 : ℚ) ^ j / ((2 : ℚ) ^ m - (2 : ℚ) ^ j) = (∏ i ∈ Finset.range n, ((2 : ℚ) ^ m - (2 : ℚ) ^ (n + (1 : ℕ) + i))) / ∏ k ∈ Finset.range (n + (1 : ℕ)), ((2 : ℚ) ^ m - (2 : ℚ) ^ k).Uses library
Finset.rangerange nis the set of natural numbers less thann. ,Lagrange.interpolate_apply,Polynomial.eval_finsetSum,Polynomial.eval_mul,Polynomial.eval_C,Lagrange.basisLagrange basis polynomials indexed bys : Finset ι, defined at nodesv ifor a mapv : ι → F. ,Polynomial.eval_prodPolynomial evaluation commutes withFinset.prod,Lagrange.basisDivisorbasisDivisor x yis the unique linear or constant polynomial such that when evaluated atxit gives1andyit gives0(where whenx = yit is identically0). ,Polynomial.eval_sub,Polynomial.eval_X,Finset.sum_div,Finset.sum_congr,rflrfl : a = ais the unique constructor of the equality type. ,Finset.mul_prod_eraseTaking a product overs : Finset ιis the same as multiplying the value on a single elementf aby the product ofs.erase a. ,Finset.prod_mul_distrib,Finset.prod_inv_distrib.Lean, lines 114–156
have hpf : ∑ j ∈ Finset.range (n + 1), ((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - 1) / 2) * (∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1)) * (∏ i ∈ Finset.range n, ((2 : ℚ) ^ (2 * n - j - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1))) * (2 : ℚ) ^ j / ((2 : ℚ) ^ m - (2 : ℚ) ^ j) = (∏ i ∈ Finset.range n, ((2 : ℚ) ^ m - (2 : ℚ) ^ (n + 1 + i))) / (∏ k ∈ Finset.range (n + 1), ((2 : ℚ) ^ m - (2 : ℚ) ^ k)) := by classical have hinj : Set.InjOn (fun k : ℕ => (2 : ℚ) ^ k) (Finset.range (n + 1) : Set ℕ) := by intro a _ b _ h exact (pow_right_inj₀ (by norm_num) (by norm_num)).mp h have hdeg : (∏ i ∈ Finset.range n, (Polynomial.X - Polynomial.C ((2 : ℚ) ^ (n + 1 + i)))).degree < ((Finset.range (n + 1)).card : WithBot ℕ) := by rw [Polynomial.degree_prod] simp only [Polynomial.degree_X_sub_C, Finset.sum_const, Finset.card_range, nsmul_eq_mul, mul_one] exact_mod_cast Nat.lt_succ_self n have key := Lagrange.eq_interpolate_of_eval_eq (fun j => (∏ i ∈ Finset.range n, (Polynomial.X - Polynomial.C ((2 : ℚ) ^ (n + 1 + i)))).eval ((2 : ℚ) ^ j)) hinj hdeg (fun i _ => rfl) have hev := congrArg (Polynomial.eval ((2 : ℚ) ^ m)) key rw [Lagrange.interpolate_apply, Polynomial.eval_finsetSum] at hev simp only [Polynomial.eval_mul, Polynomial.eval_C, Lagrange.basis, Polynomial.eval_prod, Lagrange.basisDivisor, Polynomial.eval_sub, Polynomial.eval_X] at hev rw [hev, Finset.sum_div] apply Finset.sum_congr rfl intro j hj have hj' : j < m := by rw [Finset.mem_range] at hj omega have hxj : (2 : ℚ) ^ m - 2 ^ j ≠ 0 := by have : (2 : ℚ) ^ j < 2 ^ m := pow_lt_pow_right₀ (by norm_num) hj' linarith have hE1 : ∏ k ∈ (Finset.range (n + 1)).erase j, ((2 : ℚ) ^ m - 2 ^ k) ≠ 0 := by rw [Finset.prod_ne_zero_iff] intro k hk have hk' : k < m := by rw [Finset.mem_erase, Finset.mem_range] at hk omega have : (2 : ℚ) ^ k < 2 ^ m := pow_lt_pow_right₀ (by norm_num) hk' linarith have hE2 : ∏ k ∈ (Finset.range (n + 1)).erase j, ((2 : ℚ) ^ j - 2 ^ k) ≠ 0 := by rw [Finset.prod_ne_zero_iff] intro k hk rw [Finset.mem_erase] at hk intro h0 exact hk.1 (hinj (Finset.mem_coe.mpr hj) (Finset.mem_coe.mpr hk.2) (sub_eq_zero.mp h0)).symm rw [← Finset.mul_prod_erase _ _ hj, Finset.prod_mul_distrib, Finset.prod_inv_distrib, ← hres j hj] field_simptargets/erdos-1050/nodes/spec-f2b55478/Proof.lean, lines 114–156 at
4148e3125651↗hpf.hinjhaveSet.InjOn (fun (k : ℕ) => (2 : ℚ) ^ k) (↑(Finset.range (n + (1 : ℕ))) : Set ℕ)Leaves
∑ j ∈ Finset.range (n + (1 : ℕ)), (((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * (2 : ℚ) ^ j / ((2 : ℚ) ^ m - (2 : ℚ) ^ j) = (∏ i ∈ Finset.range n, ((2 : ℚ) ^ m - (2 : ℚ) ^ (n + (1 : ℕ) + i))) / ∏ k ∈ Finset.range (n + (1 : ℕ)), ((2 : ℚ) ^ m - (2 : ℚ) ^ k), withhinj : Set.InjOn (fun (k : ℕ) => (2 : ℚ) ^ k) (↑(Finset.range (n + (1 : ℕ))) : Set ℕ).Uses library
Set.InjOnfis injective onsif the restriction offtosis injective. ,Finset.rangerange nis the set of natural numbers less thann. ,SetA set is a collection of elements of some typeα. ,pow_right_inj₀.Lean, lines 117–119
have hinj : Set.InjOn (fun k : ℕ => (2 : ℚ) ^ k) (Finset.range (n + 1) : Set ℕ) := by intro a _ b _ h exact (pow_right_inj₀ (by norm_num) (by norm_num)).mp htargets/erdos-1050/nodes/spec-f2b55478/Proof.lean, lines 117–119 at
4148e3125651↗hpf.hdeghave(∏ i ∈ Finset.range n, (Polynomial.X - (Polynomial.C : ℚ → Polynomial ℚ) ((2 : ℚ) ^ (n + (1 : ℕ) + i)))).degree < (↑(Finset.range (n + (1 : ℕ))).card : WithBot ℕ)Leaves
∑ j ∈ Finset.range (n + (1 : ℕ)), (((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * (2 : ℚ) ^ j / ((2 : ℚ) ^ m - (2 : ℚ) ^ j) = (∏ i ∈ Finset.range n, ((2 : ℚ) ^ m - (2 : ℚ) ^ (n + (1 : ℕ) + i))) / ∏ k ∈ Finset.range (n + (1 : ℕ)), ((2 : ℚ) ^ m - (2 : ℚ) ^ k), withhdeg : (∏ i ∈ Finset.range n, (Polynomial.X - (Polynomial.C : ℚ → Polynomial ℚ) ((2 : ℚ) ^ (n + (1 : ℕ) + i)))).degree < (↑(Finset.range (n + (1 : ℕ))).card : WithBot ℕ).Uses library
Finset.rangerange nis the set of natural numbers less thann. ,Polynomial.XXis the polynomial variable (aka indeterminate). ,Polynomial.CC ais the constant polynomiala. ,WithBotAttach⊥to a type. ,Polynomial.degree_prodThe degree of a product of polynomials is equal to the sum of the degrees, where the degree of the zero polynomial is ⊥. ,Polynomial.degree_X_sub_C,Finset.sum_const,Finset.card_range,nsmul_eq_mul,mul_one,Nat.lt_succ_self.Lean, lines 120–124
have hdeg : (∏ i ∈ Finset.range n, (Polynomial.X - Polynomial.C ((2 : ℚ) ^ (n + 1 + i)))).degree < ((Finset.range (n + 1)).card : WithBot ℕ) := by rw [Polynomial.degree_prod] simp only [Polynomial.degree_X_sub_C, Finset.sum_const, Finset.card_range, nsmul_eq_mul, mul_one] exact_mod_cast Nat.lt_succ_self ntargets/erdos-1050/nodes/spec-f2b55478/Proof.lean, lines 120–124 at
4148e3125651↗hpf.keyhave∏ i ∈ Finset.range n, (Polynomial.X - (Polynomial.C : ℚ → Polynomial ℚ) ((2 : ℚ) ^ (n + (1 : ℕ) + i))) = (Lagrange.interpolate (Finset.range (n + (1 : ℕ))) fun (k : ℕ) => (2 : ℚ) ^ k : (ℕ → ℚ) → Polynomial ℚ) fun (j : ℕ) => Polynomial.eval ((2 : ℚ) ^ j) (∏ i ∈ Finset.range n, (Polynomial.X - (Polynomial.C : ℚ → Polynomial ℚ) ((2 : ℚ) ^ (n + (1 : ℕ) + i))))Leaves
∑ j ∈ Finset.range (n + (1 : ℕ)), (((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * (2 : ℚ) ^ j / ((2 : ℚ) ^ m - (2 : ℚ) ^ j) = (∏ i ∈ Finset.range n, ((2 : ℚ) ^ m - (2 : ℚ) ^ (n + (1 : ℕ) + i))) / ∏ k ∈ Finset.range (n + (1 : ℕ)), ((2 : ℚ) ^ m - (2 : ℚ) ^ k), withkey : ∏ i ∈ Finset.range n, (Polynomial.X - (Polynomial.C : ℚ → Polynomial ℚ) ((2 : ℚ) ^ (n + (1 : ℕ) + i))) = (Lagrange.interpolate (Finset.range (n + (1 : ℕ))) fun (k : ℕ) => (2 : ℚ) ^ k : (ℕ → ℚ) → Polynomial ℚ) fun (j : ℕ) => Polynomial.eval ((2 : ℚ) ^ j) (∏ i ∈ Finset.range n, (Polynomial.X - (Polynomial.C : ℚ → Polynomial ℚ) ((2 : ℚ) ^ (n + (1 : ℕ) + i)))).Uses library
Lagrange.eq_interpolate_of_eval_eq,Finset.rangerange nis the set of natural numbers less thann. ,Polynomial.XXis the polynomial variable (aka indeterminate). ,Polynomial.CC ais the constant polynomiala. ,rflrfl : a = ais the unique constructor of the equality type. .Lean, lines 125–127
have key := Lagrange.eq_interpolate_of_eval_eq (fun j => (∏ i ∈ Finset.range n, (Polynomial.X - Polynomial.C ((2 : ℚ) ^ (n + 1 + i)))).eval ((2 : ℚ) ^ j)) hinj hdeg (fun i _ => rfl)targets/erdos-1050/nodes/spec-f2b55478/Proof.lean, lines 125–127 at
4148e3125651↗hpf.hevhavePolynomial.eval ((2 : ℚ) ^ m) (∏ i ∈ Finset.range n, (Polynomial.X - (Polynomial.C : ℚ → Polynomial ℚ) ((2 : ℚ) ^ (n + (1 : ℕ) + i)))) = Polynomial.eval ((2 : ℚ) ^ m) ((Lagrange.interpolate (Finset.range (n + (1 : ℕ))) fun (k : ℕ) => (2 : ℚ) ^ k : (ℕ → ℚ) → Polynomial ℚ) fun (j : ℕ) => Polynomial.eval ((2 : ℚ) ^ j) (∏ i ∈ Finset.range n, (Polynomial.X - (Polynomial.C : ℚ → Polynomial ℚ) ((2 : ℚ) ^ (n + (1 : ℕ) + i)))))Leaves
∑ j ∈ Finset.range (n + (1 : ℕ)), (((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * (2 : ℚ) ^ j / ((2 : ℚ) ^ m - (2 : ℚ) ^ j) = (∏ i ∈ Finset.range n, ((2 : ℚ) ^ m - (2 : ℚ) ^ (n + (1 : ℕ) + i))) / ∏ k ∈ Finset.range (n + (1 : ℕ)), ((2 : ℚ) ^ m - (2 : ℚ) ^ k), withhev : Polynomial.eval ((2 : ℚ) ^ m) (∏ i ∈ Finset.range n, (Polynomial.X - (Polynomial.C : ℚ → Polynomial ℚ) ((2 : ℚ) ^ (n + (1 : ℕ) + i)))) = Polynomial.eval ((2 : ℚ) ^ m) ((Lagrange.interpolate (Finset.range (n + (1 : ℕ))) fun (k : ℕ) => (2 : ℚ) ^ k : (ℕ → ℚ) → Polynomial ℚ) fun (j : ℕ) => Polynomial.eval ((2 : ℚ) ^ j) (∏ i ∈ Finset.range n, (Polynomial.X - (Polynomial.C : ℚ → Polynomial ℚ) ((2 : ℚ) ^ (n + (1 : ℕ) + i))))).Uses library
congrArgCongruence in the function argument: ifa₁ = a₂thenf a₁ = f a₂for any (nondependent) functionf. ,Polynomial.evaleval x pis the evaluation of the polynomialpatx.Lean, line 128
have hev := congrArg (Polynomial.eval ((2 : ℚ) ^ m)) key
targets/erdos-1050/nodes/spec-f2b55478/Proof.lean, line 128 at
4148e3125651↗hpf.hj'havej < mLeaves
(((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * (2 : ℚ) ^ j / ((2 : ℚ) ^ m - (2 : ℚ) ^ j) = ((∏ x ∈ Finset.range n, ((2 : ℚ) ^ j - (2 : ℚ) ^ (n + (1 : ℕ) + x))) * ∏ x ∈ (Finset.range (n + (1 : ℕ))).erase j, ((2 : ℚ) ^ j - (2 : ℚ) ^ x)⁻¹ * ((2 : ℚ) ^ m - (2 : ℚ) ^ x)) / ∏ k ∈ Finset.range (n + (1 : ℕ)), ((2 : ℚ) ^ m - (2 : ℚ) ^ k), withhj' : j < m.Uses library
Finset.mem_range.Lean, lines 135–137
have hj' : j < m := by rw [Finset.mem_range] at hj omegatargets/erdos-1050/nodes/spec-f2b55478/Proof.lean, lines 135–137 at
4148e3125651↗hpf.hxjhave(2 : ℚ) ^ m - (2 : ℚ) ^ j ≠ (0 : ℚ)Leaves
(((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * (2 : ℚ) ^ j / ((2 : ℚ) ^ m - (2 : ℚ) ^ j) = ((∏ x ∈ Finset.range n, ((2 : ℚ) ^ j - (2 : ℚ) ^ (n + (1 : ℕ) + x))) * ∏ x ∈ (Finset.range (n + (1 : ℕ))).erase j, ((2 : ℚ) ^ j - (2 : ℚ) ^ x)⁻¹ * ((2 : ℚ) ^ m - (2 : ℚ) ^ x)) / ∏ k ∈ Finset.range (n + (1 : ℕ)), ((2 : ℚ) ^ m - (2 : ℚ) ^ k), withhxj : (2 : ℚ) ^ m - (2 : ℚ) ^ j ≠ (0 : ℚ).Lean, lines 138–140
have hxj : (2 : ℚ) ^ m - 2 ^ j ≠ 0 := by have : (2 : ℚ) ^ j < 2 ^ m := pow_lt_pow_right₀ (by norm_num) hj' linarithtargets/erdos-1050/nodes/spec-f2b55478/Proof.lean, lines 138–140 at
4148e3125651↗hpf.hxj.thishave(2 : ℚ) ^ j < (2 : ℚ) ^ mLeaves
(2 : ℚ) ^ m - (2 : ℚ) ^ j ≠ (0 : ℚ), withthis : (2 : ℚ) ^ j < (2 : ℚ) ^ m.Uses library
pow_lt_pow_right₀.Lean, line 139
have : (2 : ℚ) ^ j < 2 ^ m := pow_lt_pow_right₀ (by norm_num) hj'
targets/erdos-1050/nodes/spec-f2b55478/Proof.lean, line 139 at
4148e3125651↗
hpf.hE1have∏ k ∈ (Finset.range (n + (1 : ℕ))).erase j, ((2 : ℚ) ^ m - (2 : ℚ) ^ k) ≠ (0 : ℚ)Leaves
(((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * (2 : ℚ) ^ j / ((2 : ℚ) ^ m - (2 : ℚ) ^ j) = ((∏ x ∈ Finset.range n, ((2 : ℚ) ^ j - (2 : ℚ) ^ (n + (1 : ℕ) + x))) * ∏ x ∈ (Finset.range (n + (1 : ℕ))).erase j, ((2 : ℚ) ^ j - (2 : ℚ) ^ x)⁻¹ * ((2 : ℚ) ^ m - (2 : ℚ) ^ x)) / ∏ k ∈ Finset.range (n + (1 : ℕ)), ((2 : ℚ) ^ m - (2 : ℚ) ^ k), withhE1 : ∏ k ∈ (Finset.range (n + (1 : ℕ))).erase j, ((2 : ℚ) ^ m - (2 : ℚ) ^ k) ≠ (0 : ℚ).Uses library
Finset.rangerange nis the set of natural numbers less thann. ,Finset.prod_ne_zero_iff.Lean, lines 141–148
have hE1 : ∏ k ∈ (Finset.range (n + 1)).erase j, ((2 : ℚ) ^ m - 2 ^ k) ≠ 0 := by rw [Finset.prod_ne_zero_iff] intro k hk have hk' : k < m := by rw [Finset.mem_erase, Finset.mem_range] at hk omega have : (2 : ℚ) ^ k < 2 ^ m := pow_lt_pow_right₀ (by norm_num) hk' linarithtargets/erdos-1050/nodes/spec-f2b55478/Proof.lean, lines 141–148 at
4148e3125651↗hpf.hE1.hk'havek < mLeaves
(2 : ℚ) ^ m - (2 : ℚ) ^ k ≠ (0 : ℚ), withhk' : k < m.Uses library
Finset.mem_erase,Finset.mem_range.Lean, lines 144–146
have hk' : k < m := by rw [Finset.mem_erase, Finset.mem_range] at hk omegatargets/erdos-1050/nodes/spec-f2b55478/Proof.lean, lines 144–146 at
4148e3125651↗hpf.hE1.thishave(2 : ℚ) ^ k < (2 : ℚ) ^ mLeaves
(2 : ℚ) ^ m - (2 : ℚ) ^ k ≠ (0 : ℚ), withthis : (2 : ℚ) ^ k < (2 : ℚ) ^ m.Uses library
pow_lt_pow_right₀.Lean, line 147
have : (2 : ℚ) ^ k < 2 ^ m := pow_lt_pow_right₀ (by norm_num) hk'
targets/erdos-1050/nodes/spec-f2b55478/Proof.lean, line 147 at
4148e3125651↗
hpf.hE2have∏ k ∈ (Finset.range (n + (1 : ℕ))).erase j, ((2 : ℚ) ^ j - (2 : ℚ) ^ k) ≠ (0 : ℚ)Leaves
(((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * (2 : ℚ) ^ j / ((2 : ℚ) ^ m - (2 : ℚ) ^ j) = ((∏ x ∈ Finset.range n, ((2 : ℚ) ^ j - (2 : ℚ) ^ (n + (1 : ℕ) + x))) * ∏ x ∈ (Finset.range (n + (1 : ℕ))).erase j, ((2 : ℚ) ^ j - (2 : ℚ) ^ x)⁻¹ * ((2 : ℚ) ^ m - (2 : ℚ) ^ x)) / ∏ k ∈ Finset.range (n + (1 : ℕ)), ((2 : ℚ) ^ m - (2 : ℚ) ^ k), withhE2 : ∏ k ∈ (Finset.range (n + (1 : ℕ))).erase j, ((2 : ℚ) ^ j - (2 : ℚ) ^ k) ≠ (0 : ℚ).Uses library
Finset.rangerange nis the set of natural numbers less thann. ,Finset.prod_ne_zero_iff,Finset.mem_erase,Finset.mem_coe,sub_eq_zero.Lean, lines 149–154
have hE2 : ∏ k ∈ (Finset.range (n + 1)).erase j, ((2 : ℚ) ^ j - 2 ^ k) ≠ 0 := by rw [Finset.prod_ne_zero_iff] intro k hk rw [Finset.mem_erase] at hk intro h0 exact hk.1 (hinj (Finset.mem_coe.mpr hj) (Finset.mem_coe.mpr hk.2) (sub_eq_zero.mp h0)).symmtargets/erdos-1050/nodes/spec-f2b55478/Proof.lean, lines 149–154 at
4148e3125651↗
hlhave∑ j ∈ Finset.range (n + (1 : ℕ)), (((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) / ((2 : ℚ) ^ (m - j) - (1 : ℚ)) = ∑ j ∈ Finset.range (n + (1 : ℕ)), (((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * (2 : ℚ) ^ j / ((2 : ℚ) ^ m - (2 : ℚ) ^ j)Leaves
∑ j ∈ Finset.range (n + (1 : ℕ)), (((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) / ((2 : ℚ) ^ (m - j) - (1 : ℚ)) = (((2 : ℚ) ^ (n * n) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (m - n - (1 : ℕ) - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) / ∏ j ∈ Finset.range (n + (1 : ℕ)), ((2 : ℚ) ^ (m - j) - (1 : ℚ)), withhl : ∑ j ∈ Finset.range (n + (1 : ℕ)), (((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) / ((2 : ℚ) ^ (m - j) - (1 : ℚ)) = ∑ j ∈ Finset.range (n + (1 : ℕ)), (((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * (2 : ℚ) ^ j / ((2 : ℚ) ^ m - (2 : ℚ) ^ j).Uses library
Finset.rangerange nis the set of natural numbers less thann. ,Finset.sum_congr,rflrfl : a = ais the unique constructor of the equality type. ,mul_div_mul_right.Lean, lines 158–168
have hl : ∑ j ∈ Finset.range (n + 1), (-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - 1) / 2) * (∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1)) * (∏ i ∈ Finset.range n, ((2 : ℚ) ^ (2 * n - j - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1)) / ((2 : ℚ) ^ (m - j) - 1) = ∑ j ∈ Finset.range (n + 1), ((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - 1) / 2) * (∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1)) * (∏ i ∈ Finset.range n, ((2 : ℚ) ^ (2 * n - j - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1))) * (2 : ℚ) ^ j / ((2 : ℚ) ^ m - (2 : ℚ) ^ j) := by apply Finset.sum_congr rfl intro j hj have hj' : j < m := by rw [Finset.mem_range] at hj omega have h2 : (2 : ℚ) ^ m = 2 ^ (m - j) * 2 ^ j := by rw [← pow_add, Nat.sub_add_cancel hj'.le] have hp : (2 : ℚ) ^ j ≠ 0 := by positivity rw [h2, show (2 : ℚ) ^ (m - j) * 2 ^ j - 2 ^ j = (2 ^ (m - j) - 1) * 2 ^ j by ring, mul_div_mul_right _ _ hp]targets/erdos-1050/nodes/spec-f2b55478/Proof.lean, lines 158–168 at
4148e3125651↗hl.hj'havej < mLeaves
(((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) / ((2 : ℚ) ^ (m - j) - (1 : ℚ)) = (((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * (2 : ℚ) ^ j / ((2 : ℚ) ^ m - (2 : ℚ) ^ j), withhj' : j < m.Uses library
Finset.mem_range.Lean, lines 161–163
have hj' : j < m := by rw [Finset.mem_range] at hj omegatargets/erdos-1050/nodes/spec-f2b55478/Proof.lean, lines 161–163 at
4148e3125651↗hl.h2have(2 : ℚ) ^ m = (2 : ℚ) ^ (m - j) * (2 : ℚ) ^ jLeaves
(((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) / ((2 : ℚ) ^ (m - j) - (1 : ℚ)) = (((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * (2 : ℚ) ^ j / ((2 : ℚ) ^ m - (2 : ℚ) ^ j), withh2 : (2 : ℚ) ^ m = (2 : ℚ) ^ (m - j) * (2 : ℚ) ^ j.Uses library
pow_add,Nat.sub_add_cancel.Lean, lines 164–165
have h2 : (2 : ℚ) ^ m = 2 ^ (m - j) * 2 ^ j := by rw [← pow_add, Nat.sub_add_cancel hj'.le]targets/erdos-1050/nodes/spec-f2b55478/Proof.lean, lines 164–165 at
4148e3125651↗hl.hphave(2 : ℚ) ^ j ≠ (0 : ℚ)routine: positivityLeaves
(((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) / ((2 : ℚ) ^ (m - j) - (1 : ℚ)) = (((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * (2 : ℚ) ^ j / ((2 : ℚ) ^ m - (2 : ℚ) ^ j), withhp : (2 : ℚ) ^ j ≠ (0 : ℚ).Lean, line 166
have hp : (2 : ℚ) ^ j ≠ 0 := by positivity
targets/erdos-1050/nodes/spec-f2b55478/Proof.lean, line 166 at
4148e3125651↗
hrhave(((2 : ℚ) ^ (n * n) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (m - n - (1 : ℕ) - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) / ∏ j ∈ Finset.range (n + (1 : ℕ)), ((2 : ℚ) ^ (m - j) - (1 : ℚ)) = (∏ i ∈ Finset.range n, ((2 : ℚ) ^ m - (2 : ℚ) ^ (n + (1 : ℕ) + i))) / ∏ k ∈ Finset.range (n + (1 : ℕ)), ((2 : ℚ) ^ m - (2 : ℚ) ^ k)Leaves
∑ j ∈ Finset.range (n + (1 : ℕ)), (((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) / ((2 : ℚ) ^ (m - j) - (1 : ℚ)) = (((2 : ℚ) ^ (n * n) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (m - n - (1 : ℕ) - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) / ∏ j ∈ Finset.range (n + (1 : ℕ)), ((2 : ℚ) ^ (m - j) - (1 : ℚ)), withhr : (((2 : ℚ) ^ (n * n) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (m - n - (1 : ℕ) - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) / ∏ j ∈ Finset.range (n + (1 : ℕ)), ((2 : ℚ) ^ (m - j) - (1 : ℚ)) = (∏ i ∈ Finset.range n, ((2 : ℚ) ^ m - (2 : ℚ) ^ (n + (1 : ℕ) + i))) / ∏ k ∈ Finset.range (n + (1 : ℕ)), ((2 : ℚ) ^ m - (2 : ℚ) ^ k).Uses library
Finset.rangerange nis the set of natural numbers less thann. ,Nat.lt_or_ge.Lean, lines 170–221
have hr : (2 : ℚ) ^ (n * n) * (∏ i ∈ Finset.range n, ((2 : ℚ) ^ (i + 1) - 1)) * (∏ i ∈ Finset.range n, ((2 : ℚ) ^ (m - n - 1 - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1)) / ∏ j ∈ Finset.range (n + 1), ((2 : ℚ) ^ (m - j) - 1) = (∏ i ∈ Finset.range n, ((2 : ℚ) ^ m - (2 : ℚ) ^ (n + 1 + i))) / (∏ k ∈ Finset.range (n + 1), ((2 : ℚ) ^ m - (2 : ℚ) ^ k)) := by have hB : ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (i + 1) - 1) ≠ 0 := by rw [Finset.prod_ne_zero_iff] intro i _ have : (1 : ℚ) < 2 ^ (i + 1) := one_lt_pow₀ (by norm_num) (by omega) linarith have key : (2 : ℚ) ^ (n * n) * (∏ i ∈ Finset.range n, ((2 : ℚ) ^ (i + 1) - 1)) * (∏ i ∈ Finset.range n, ((2 : ℚ) ^ (m - n - 1 - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1)) / ∏ j ∈ Finset.range (n + 1), ((2 : ℚ) ^ (m - j) - 1) = (2 : ℚ) ^ (n * n) * (∏ i ∈ Finset.range n, ((2 : ℚ) ^ (m - n - 1 - i) - 1)) / (∏ j ∈ Finset.range (n + 1), ((2 : ℚ) ^ (m - j) - 1)) := by rw [Finset.prod_div_distrib] field_simp rcases Nat.lt_or_ge (2 * n) m with h | h · have hA : (∏ i ∈ Finset.range n, ((2 : ℚ) ^ (m - n - 1 - i) - 1)) = (∏ i ∈ Finset.range n, ((2 : ℚ) ^ m - (2 : ℚ) ^ (n + 1 + i))) / 2 ^ (∑ i ∈ Finset.range n, (n + 1 + i)) := by rw [← Finset.prod_pow_eq_pow_sum, ← Finset.prod_div_distrib] apply Finset.prod_congr rfl intro i hi rw [Finset.mem_range] at hi have e : (2 : ℚ) ^ m = 2 ^ (m - n - 1 - i) * 2 ^ (n + 1 + i) := by rw [← pow_add] congr 1 omega rw [e] field_simp have hD : (∏ j ∈ Finset.range (n + 1), ((2 : ℚ) ^ (m - j) - 1)) = (∏ k ∈ Finset.range (n + 1), ((2 : ℚ) ^ m - (2 : ℚ) ^ k)) / 2 ^ (∑ j ∈ Finset.range (n + 1), j) := by rw [← Finset.prod_pow_eq_pow_sum, ← Finset.prod_div_distrib] apply Finset.prod_congr rfl intro j hj rw [Finset.mem_range] at hj have e : (2 : ℚ) ^ m = 2 ^ (m - j) * 2 ^ j := by rw [← pow_add] congr 1 omega rw [e] field_simp have hs : ∑ i ∈ Finset.range n, (n + 1 + i) = n * n + ∑ j ∈ Finset.range (n + 1), j := by rw [Finset.sum_range_succ, Finset.sum_add_distrib] simp ring have hDX : (∏ k ∈ Finset.range (n + 1), ((2 : ℚ) ^ m - (2 : ℚ) ^ k)) ≠ 0 := by rw [Finset.prod_ne_zero_iff] intro k hk rw [Finset.mem_range] at hk have : (2 : ℚ) ^ k < 2 ^ m := pow_lt_pow_right₀ (by norm_num) (by omega) linarith rw [key, hA, hD, hs, pow_add] field_simp · have hz1 : (∏ i ∈ Finset.range n, ((2 : ℚ) ^ (m - n - 1 - i) - 1)) = 0 := Finset.prod_eq_zero (i := m - n - 1) (by rw [Finset.mem_range]; omega) (by rw [show m - n - 1 - (m - n - 1) = 0 by omega]; norm_num) have hz2 : (∏ i ∈ Finset.range n, ((2 : ℚ) ^ m - (2 : ℚ) ^ (n + 1 + i))) = 0 := Finset.prod_eq_zero (i := m - n - 1) (by rw [Finset.mem_range]; omega) (by rw [show n + 1 + (m - n - 1) = m by omega]; ring) rw [key, hz1, hz2] simptargets/erdos-1050/nodes/spec-f2b55478/Proof.lean, lines 170–221 at
4148e3125651↗hr.hBhave∏ i ∈ Finset.range n, ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ)) ≠ (0 : ℚ)Leaves
(((2 : ℚ) ^ (n * n) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (m - n - (1 : ℕ) - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) / ∏ j ∈ Finset.range (n + (1 : ℕ)), ((2 : ℚ) ^ (m - j) - (1 : ℚ)) = (∏ i ∈ Finset.range n, ((2 : ℚ) ^ m - (2 : ℚ) ^ (n + (1 : ℕ) + i))) / ∏ k ∈ Finset.range (n + (1 : ℕ)), ((2 : ℚ) ^ m - (2 : ℚ) ^ k), withhB : ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ)) ≠ (0 : ℚ).Uses library
Finset.rangerange nis the set of natural numbers less thann. ,Finset.prod_ne_zero_iff.Lean, lines 171–175
have hB : ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (i + 1) - 1) ≠ 0 := by rw [Finset.prod_ne_zero_iff] intro i _ have : (1 : ℚ) < 2 ^ (i + 1) := one_lt_pow₀ (by norm_num) (by omega) linarithtargets/erdos-1050/nodes/spec-f2b55478/Proof.lean, lines 171–175 at
4148e3125651↗hr.hB.thishave(1 : ℚ) < (2 : ℚ) ^ (i + (1 : ℕ))Leaves
(2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ) ≠ (0 : ℚ), withthis : (1 : ℚ) < (2 : ℚ) ^ (i + (1 : ℕ)).Uses library
one_lt_pow₀.Lean, line 174
have : (1 : ℚ) < 2 ^ (i + 1) := one_lt_pow₀ (by norm_num) (by omega)
targets/erdos-1050/nodes/spec-f2b55478/Proof.lean, line 174 at
4148e3125651↗
hr.keyhave(((2 : ℚ) ^ (n * n) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (m - n - (1 : ℕ) - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) / ∏ j ∈ Finset.range (n + (1 : ℕ)), ((2 : ℚ) ^ (m - j) - (1 : ℚ)) = ((2 : ℚ) ^ (n * n) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (m - n - (1 : ℕ) - i) - (1 : ℚ))) / ∏ j ∈ Finset.range (n + (1 : ℕ)), ((2 : ℚ) ^ (m - j) - (1 : ℚ))Leaves
(((2 : ℚ) ^ (n * n) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (m - n - (1 : ℕ) - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) / ∏ j ∈ Finset.range (n + (1 : ℕ)), ((2 : ℚ) ^ (m - j) - (1 : ℚ)) = (∏ i ∈ Finset.range n, ((2 : ℚ) ^ m - (2 : ℚ) ^ (n + (1 : ℕ) + i))) / ∏ k ∈ Finset.range (n + (1 : ℕ)), ((2 : ℚ) ^ m - (2 : ℚ) ^ k), withkey : (((2 : ℚ) ^ (n * n) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (m - n - (1 : ℕ) - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) / ∏ j ∈ Finset.range (n + (1 : ℕ)), ((2 : ℚ) ^ (m - j) - (1 : ℚ)) = ((2 : ℚ) ^ (n * n) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (m - n - (1 : ℕ) - i) - (1 : ℚ))) / ∏ j ∈ Finset.range (n + (1 : ℕ)), ((2 : ℚ) ^ (m - j) - (1 : ℚ)).Uses library
Finset.rangerange nis the set of natural numbers less thann. ,Finset.prod_div_distrib.Lean, lines 176–178
have key : (2 : ℚ) ^ (n * n) * (∏ i ∈ Finset.range n, ((2 : ℚ) ^ (i + 1) - 1)) * (∏ i ∈ Finset.range n, ((2 : ℚ) ^ (m - n - 1 - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1)) / ∏ j ∈ Finset.range (n + 1), ((2 : ℚ) ^ (m - j) - 1) = (2 : ℚ) ^ (n * n) * (∏ i ∈ Finset.range n, ((2 : ℚ) ^ (m - n - 1 - i) - 1)) / (∏ j ∈ Finset.range (n + 1), ((2 : ℚ) ^ (m - j) - 1)) := by rw [Finset.prod_div_distrib] field_simptargets/erdos-1050/nodes/spec-f2b55478/Proof.lean, lines 176–178 at
4148e3125651↗hr.s3caseLeaves
(((2 : ℚ) ^ (n * n) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (m - n - (1 : ℕ) - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) / ∏ j ∈ Finset.range (n + (1 : ℕ)), ((2 : ℚ) ^ (m - j) - (1 : ℚ)) = (∏ i ∈ Finset.range n, ((2 : ℚ) ^ m - (2 : ℚ) ^ (n + (1 : ℕ) + i))) / ∏ k ∈ Finset.range (n + (1 : ℕ)), ((2 : ℚ) ^ m - (2 : ℚ) ^ k).Uses library
pow_add.Lean, lines 180–213
· have hA : (∏ i ∈ Finset.range n, ((2 : ℚ) ^ (m - n - 1 - i) - 1)) = (∏ i ∈ Finset.range n, ((2 : ℚ) ^ m - (2 : ℚ) ^ (n + 1 + i))) / 2 ^ (∑ i ∈ Finset.range n, (n + 1 + i)) := by rw [← Finset.prod_pow_eq_pow_sum, ← Finset.prod_div_distrib] apply Finset.prod_congr rfl intro i hi rw [Finset.mem_range] at hi have e : (2 : ℚ) ^ m = 2 ^ (m - n - 1 - i) * 2 ^ (n + 1 + i) := by rw [← pow_add] congr 1 omega rw [e] field_simp have hD : (∏ j ∈ Finset.range (n + 1), ((2 : ℚ) ^ (m - j) - 1)) = (∏ k ∈ Finset.range (n + 1), ((2 : ℚ) ^ m - (2 : ℚ) ^ k)) / 2 ^ (∑ j ∈ Finset.range (n + 1), j) := by rw [← Finset.prod_pow_eq_pow_sum, ← Finset.prod_div_distrib] apply Finset.prod_congr rfl intro j hj rw [Finset.mem_range] at hj have e : (2 : ℚ) ^ m = 2 ^ (m - j) * 2 ^ j := by rw [← pow_add] congr 1 omega rw [e] field_simp have hs : ∑ i ∈ Finset.range n, (n + 1 + i) = n * n + ∑ j ∈ Finset.range (n + 1), j := by rw [Finset.sum_range_succ, Finset.sum_add_distrib] simp ring have hDX : (∏ k ∈ Finset.range (n + 1), ((2 : ℚ) ^ m - (2 : ℚ) ^ k)) ≠ 0 := by rw [Finset.prod_ne_zero_iff] intro k hk rw [Finset.mem_range] at hk have : (2 : ℚ) ^ k < 2 ^ m := pow_lt_pow_right₀ (by norm_num) (by omega) linarith rw [key, hA, hD, hs, pow_add] field_simptargets/erdos-1050/nodes/spec-f2b55478/Proof.lean, lines 180–213 at
4148e3125651↗hr.s3.hAhave∏ i ∈ Finset.range n, ((2 : ℚ) ^ (m - n - (1 : ℕ) - i) - (1 : ℚ)) = (∏ i ∈ Finset.range n, ((2 : ℚ) ^ m - (2 : ℚ) ^ (n + (1 : ℕ) + i))) / (2 : ℚ) ^ ∑ i ∈ Finset.range n, (n + (1 : ℕ) + i)Leaves
(((2 : ℚ) ^ (n * n) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (m - n - (1 : ℕ) - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) / ∏ j ∈ Finset.range (n + (1 : ℕ)), ((2 : ℚ) ^ (m - j) - (1 : ℚ)) = (∏ i ∈ Finset.range n, ((2 : ℚ) ^ m - (2 : ℚ) ^ (n + (1 : ℕ) + i))) / ∏ k ∈ Finset.range (n + (1 : ℕ)), ((2 : ℚ) ^ m - (2 : ℚ) ^ k), withhA : ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (m - n - (1 : ℕ) - i) - (1 : ℚ)) = (∏ i ∈ Finset.range n, ((2 : ℚ) ^ m - (2 : ℚ) ^ (n + (1 : ℕ) + i))) / (2 : ℚ) ^ ∑ i ∈ Finset.range n, (n + (1 : ℕ) + i).Uses library
Finset.rangerange nis the set of natural numbers less thann. ,Finset.prod_pow_eq_pow_sum,Finset.prod_div_distrib,Finset.prod_congr,rflrfl : a = ais the unique constructor of the equality type. ,Finset.mem_range.Lean, lines 180–190
· have hA : (∏ i ∈ Finset.range n, ((2 : ℚ) ^ (m - n - 1 - i) - 1)) = (∏ i ∈ Finset.range n, ((2 : ℚ) ^ m - (2 : ℚ) ^ (n + 1 + i))) / 2 ^ (∑ i ∈ Finset.range n, (n + 1 + i)) := by rw [← Finset.prod_pow_eq_pow_sum, ← Finset.prod_div_distrib] apply Finset.prod_congr rfl intro i hi rw [Finset.mem_range] at hi have e : (2 : ℚ) ^ m = 2 ^ (m - n - 1 - i) * 2 ^ (n + 1 + i) := by rw [← pow_add] congr 1 omega rw [e] field_simptargets/erdos-1050/nodes/spec-f2b55478/Proof.lean, lines 180–190 at
4148e3125651↗hr.s3.hA.ehave(2 : ℚ) ^ m = (2 : ℚ) ^ (m - n - (1 : ℕ) - i) * (2 : ℚ) ^ (n + (1 : ℕ) + i)Leaves
(2 : ℚ) ^ (m - n - (1 : ℕ) - i) - (1 : ℚ) = ((2 : ℚ) ^ m - (2 : ℚ) ^ (n + (1 : ℕ) + i)) / (2 : ℚ) ^ (n + (1 : ℕ) + i), withe : (2 : ℚ) ^ m = (2 : ℚ) ^ (m - n - (1 : ℕ) - i) * (2 : ℚ) ^ (n + (1 : ℕ) + i).Uses library
pow_add.Lean, lines 185–188
have e : (2 : ℚ) ^ m = 2 ^ (m - n - 1 - i) * 2 ^ (n + 1 + i) := by rw [← pow_add] congr 1 omegatargets/erdos-1050/nodes/spec-f2b55478/Proof.lean, lines 185–188 at
4148e3125651↗
hr.s3.hDhave∏ j ∈ Finset.range (n + (1 : ℕ)), ((2 : ℚ) ^ (m - j) - (1 : ℚ)) = (∏ k ∈ Finset.range (n + (1 : ℕ)), ((2 : ℚ) ^ m - (2 : ℚ) ^ k)) / (2 : ℚ) ^ ∑ j ∈ Finset.range (n + (1 : ℕ)), jLeaves
(((2 : ℚ) ^ (n * n) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (m - n - (1 : ℕ) - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) / ∏ j ∈ Finset.range (n + (1 : ℕ)), ((2 : ℚ) ^ (m - j) - (1 : ℚ)) = (∏ i ∈ Finset.range n, ((2 : ℚ) ^ m - (2 : ℚ) ^ (n + (1 : ℕ) + i))) / ∏ k ∈ Finset.range (n + (1 : ℕ)), ((2 : ℚ) ^ m - (2 : ℚ) ^ k), withhD : ∏ j ∈ Finset.range (n + (1 : ℕ)), ((2 : ℚ) ^ (m - j) - (1 : ℚ)) = (∏ k ∈ Finset.range (n + (1 : ℕ)), ((2 : ℚ) ^ m - (2 : ℚ) ^ k)) / (2 : ℚ) ^ ∑ j ∈ Finset.range (n + (1 : ℕ)), j.Uses library
Finset.rangerange nis the set of natural numbers less thann. ,Finset.prod_pow_eq_pow_sum,Finset.prod_div_distrib,Finset.prod_congr,rflrfl : a = ais the unique constructor of the equality type. ,Finset.mem_range.Lean, lines 191–201
have hD : (∏ j ∈ Finset.range (n + 1), ((2 : ℚ) ^ (m - j) - 1)) = (∏ k ∈ Finset.range (n + 1), ((2 : ℚ) ^ m - (2 : ℚ) ^ k)) / 2 ^ (∑ j ∈ Finset.range (n + 1), j) := by rw [← Finset.prod_pow_eq_pow_sum, ← Finset.prod_div_distrib] apply Finset.prod_congr rfl intro j hj rw [Finset.mem_range] at hj have e : (2 : ℚ) ^ m = 2 ^ (m - j) * 2 ^ j := by rw [← pow_add] congr 1 omega rw [e] field_simptargets/erdos-1050/nodes/spec-f2b55478/Proof.lean, lines 191–201 at
4148e3125651↗hr.s3.hD.ehave(2 : ℚ) ^ m = (2 : ℚ) ^ (m - j) * (2 : ℚ) ^ jLeaves
(2 : ℚ) ^ (m - j) - (1 : ℚ) = ((2 : ℚ) ^ m - (2 : ℚ) ^ j) / (2 : ℚ) ^ j, withe : (2 : ℚ) ^ m = (2 : ℚ) ^ (m - j) * (2 : ℚ) ^ j.Uses library
pow_add.Lean, lines 196–199
have e : (2 : ℚ) ^ m = 2 ^ (m - j) * 2 ^ j := by rw [← pow_add] congr 1 omegatargets/erdos-1050/nodes/spec-f2b55478/Proof.lean, lines 196–199 at
4148e3125651↗
hr.s3.hshave∑ i ∈ Finset.range n, (n + (1 : ℕ) + i) = n * n + ∑ j ∈ Finset.range (n + (1 : ℕ)), jLeaves
(((2 : ℚ) ^ (n * n) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (m - n - (1 : ℕ) - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) / ∏ j ∈ Finset.range (n + (1 : ℕ)), ((2 : ℚ) ^ (m - j) - (1 : ℚ)) = (∏ i ∈ Finset.range n, ((2 : ℚ) ^ m - (2 : ℚ) ^ (n + (1 : ℕ) + i))) / ∏ k ∈ Finset.range (n + (1 : ℕ)), ((2 : ℚ) ^ m - (2 : ℚ) ^ k), withhs : ∑ i ∈ Finset.range n, (n + (1 : ℕ) + i) = n * n + ∑ j ∈ Finset.range (n + (1 : ℕ)), j.Uses library
Finset.rangerange nis the set of natural numbers less thann. ,Finset.sum_range_succ,Finset.sum_add_distrib.Lean, lines 202–205
have hs : ∑ i ∈ Finset.range n, (n + 1 + i) = n * n + ∑ j ∈ Finset.range (n + 1), j := by rw [Finset.sum_range_succ, Finset.sum_add_distrib] simp ringtargets/erdos-1050/nodes/spec-f2b55478/Proof.lean, lines 202–205 at
4148e3125651↗hr.s3.hDXhave∏ k ∈ Finset.range (n + (1 : ℕ)), ((2 : ℚ) ^ m - (2 : ℚ) ^ k) ≠ (0 : ℚ)Leaves
(((2 : ℚ) ^ (n * n) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (m - n - (1 : ℕ) - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) / ∏ j ∈ Finset.range (n + (1 : ℕ)), ((2 : ℚ) ^ (m - j) - (1 : ℚ)) = (∏ i ∈ Finset.range n, ((2 : ℚ) ^ m - (2 : ℚ) ^ (n + (1 : ℕ) + i))) / ∏ k ∈ Finset.range (n + (1 : ℕ)), ((2 : ℚ) ^ m - (2 : ℚ) ^ k), withhDX : ∏ k ∈ Finset.range (n + (1 : ℕ)), ((2 : ℚ) ^ m - (2 : ℚ) ^ k) ≠ (0 : ℚ).Uses library
Finset.rangerange nis the set of natural numbers less thann. ,Finset.prod_ne_zero_iff,Finset.mem_range.Lean, lines 206–211
have hDX : (∏ k ∈ Finset.range (n + 1), ((2 : ℚ) ^ m - (2 : ℚ) ^ k)) ≠ 0 := by rw [Finset.prod_ne_zero_iff] intro k hk rw [Finset.mem_range] at hk have : (2 : ℚ) ^ k < 2 ^ m := pow_lt_pow_right₀ (by norm_num) (by omega) linarithtargets/erdos-1050/nodes/spec-f2b55478/Proof.lean, lines 206–211 at
4148e3125651↗hr.s3.hDX.thishave(2 : ℚ) ^ k < (2 : ℚ) ^ mLeaves
(2 : ℚ) ^ m - (2 : ℚ) ^ k ≠ (0 : ℚ), withthis : (2 : ℚ) ^ k < (2 : ℚ) ^ m.Uses library
pow_lt_pow_right₀.Lean, line 210
have : (2 : ℚ) ^ k < 2 ^ m := pow_lt_pow_right₀ (by norm_num) (by omega)
targets/erdos-1050/nodes/spec-f2b55478/Proof.lean, line 210 at
4148e3125651↗
hr.s4caseLeaves
(((2 : ℚ) ^ (n * n) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (m - n - (1 : ℕ) - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) / ∏ j ∈ Finset.range (n + (1 : ℕ)), ((2 : ℚ) ^ (m - j) - (1 : ℚ)) = (∏ i ∈ Finset.range n, ((2 : ℚ) ^ m - (2 : ℚ) ^ (n + (1 : ℕ) + i))) / ∏ k ∈ Finset.range (n + (1 : ℕ)), ((2 : ℚ) ^ m - (2 : ℚ) ^ k).Lean, lines 214–221
· have hz1 : (∏ i ∈ Finset.range n, ((2 : ℚ) ^ (m - n - 1 - i) - 1)) = 0 := Finset.prod_eq_zero (i := m - n - 1) (by rw [Finset.mem_range]; omega) (by rw [show m - n - 1 - (m - n - 1) = 0 by omega]; norm_num) have hz2 : (∏ i ∈ Finset.range n, ((2 : ℚ) ^ m - (2 : ℚ) ^ (n + 1 + i))) = 0 := Finset.prod_eq_zero (i := m - n - 1) (by rw [Finset.mem_range]; omega) (by rw [show n + 1 + (m - n - 1) = m by omega]; ring) rw [key, hz1, hz2] simptargets/erdos-1050/nodes/spec-f2b55478/Proof.lean, lines 214–221 at
4148e3125651↗hr.s4.hz1have∏ i ∈ Finset.range n, ((2 : ℚ) ^ (m - n - (1 : ℕ) - i) - (1 : ℚ)) = (0 : ℚ)Leaves
(((2 : ℚ) ^ (n * n) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (m - n - (1 : ℕ) - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) / ∏ j ∈ Finset.range (n + (1 : ℕ)), ((2 : ℚ) ^ (m - j) - (1 : ℚ)) = (∏ i ∈ Finset.range n, ((2 : ℚ) ^ m - (2 : ℚ) ^ (n + (1 : ℕ) + i))) / ∏ k ∈ Finset.range (n + (1 : ℕ)), ((2 : ℚ) ^ m - (2 : ℚ) ^ k), withhz1 : ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (m - n - (1 : ℕ) - i) - (1 : ℚ)) = (0 : ℚ).Uses library
Finset.rangerange nis the set of natural numbers less thann. ,Finset.prod_eq_zero,Finset.mem_range.Lean, lines 214–216
· have hz1 : (∏ i ∈ Finset.range n, ((2 : ℚ) ^ (m - n - 1 - i) - 1)) = 0 := Finset.prod_eq_zero (i := m - n - 1) (by rw [Finset.mem_range]; omega) (by rw [show m - n - 1 - (m - n - 1) = 0 by omega]; norm_num)targets/erdos-1050/nodes/spec-f2b55478/Proof.lean, lines 214–216 at
4148e3125651↗hr.s4.hz2have∏ i ∈ Finset.range n, ((2 : ℚ) ^ m - (2 : ℚ) ^ (n + (1 : ℕ) + i)) = (0 : ℚ)Leaves
(((2 : ℚ) ^ (n * n) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (m - n - (1 : ℕ) - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) / ∏ j ∈ Finset.range (n + (1 : ℕ)), ((2 : ℚ) ^ (m - j) - (1 : ℚ)) = (∏ i ∈ Finset.range n, ((2 : ℚ) ^ m - (2 : ℚ) ^ (n + (1 : ℕ) + i))) / ∏ k ∈ Finset.range (n + (1 : ℕ)), ((2 : ℚ) ^ m - (2 : ℚ) ^ k), withhz2 : ∏ i ∈ Finset.range n, ((2 : ℚ) ^ m - (2 : ℚ) ^ (n + (1 : ℕ) + i)) = (0 : ℚ).Uses library
Finset.rangerange nis the set of natural numbers less thann. ,Finset.prod_eq_zero,Finset.mem_range.Lean, lines 217–219
have hz2 : (∏ i ∈ Finset.range n, ((2 : ℚ) ^ m - (2 : ℚ) ^ (n + 1 + i))) = 0 := Finset.prod_eq_zero (i := m - n - 1) (by rw [Finset.mem_range]; omega) (by rw [show n + 1 + (m - n - 1) = m by omega]; ring)targets/erdos-1050/nodes/spec-f2b55478/Proof.lean, lines 217–219 at
4148e3125651↗
The proof in Lean (Proof.lean)
Checked by the kernel — these bytes are the ones its attestation names: attestations/000222.json, merge commit 4148e3125651.
artifact_hash of the attestation below, so these are the bytes the gate checked. Rendered from targets/erdos-1050/nodes/spec-f2b55478/Proof.lean, sha256 4b6884a484fb.import Mathlib
import Nodes.«spec-f2b55478».Context
/-- erdos-1050, Borwein's route (annexes f593a93a8960 and 3ada4f0922d7 on erdos-1050--h1-v2):
the coefficient of x^m, for m > n, in Q_n(x) * f(x), where f(x) = sum_{k >= 1} x^k / (2^k - 1) and
Q_n(x) = sum_k (-1)^k 2^(k(k-1)/2) [n k]_2 [2n-k n]_2 x^k is the Pade denominator, equals
2^(n^2) (2;2)_n [m-n-1 n]_2 / prod_{j <= n} (2^(m-j) - 1). It vanishes for n < m <= 2n (the Pade
condition) and is positive for m > 2n, which makes the Pade remainder positive. Checked exactly for
n <= 15, m <= 3n + 29. -/
theorem erdos_1050_pade_remainder_coeff (n m : ℕ) (hnm : n < m) :
∑ j ∈ Finset.range (n + 1),
(-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - 1) / 2) *
(∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1)) *
(∏ i ∈ Finset.range n, ((2 : ℚ) ^ (2 * n - j - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1)) /
((2 : ℚ) ^ (m - j) - 1) =
(2 : ℚ) ^ (n * n) * (∏ i ∈ Finset.range n, ((2 : ℚ) ^ (i + 1) - 1)) *
(∏ i ∈ Finset.range n, ((2 : ℚ) ^ (m - n - 1 - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1)) /
∏ j ∈ Finset.range (n + 1), ((2 : ℚ) ^ (m - j) - 1) := by
-- annex: fcdb7a3a0b0eac5a9cc9f17ce00a203d918c82203729e0d0a4c29795a1778f0d
-- Step 4 of the annex (residue identity): c_j 2^j prod_(k != j) (2^j - 2^k) = N(2^j).
have hres : ∀ j ∈ Finset.range (n + 1),
((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - 1) / 2) * (∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1)) * (∏ i ∈ Finset.range n, ((2 : ℚ) ^ (2 * n - j - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1))) * (2 : ℚ) ^ j * ∏ k ∈ (Finset.range (n + 1)).erase j, ((2 : ℚ) ^ j - (2 : ℚ) ^ k) =
∏ i ∈ Finset.range n, ((2 : ℚ) ^ j - (2 : ℚ) ^ (n + 1 + i)) := by
intro j hj
rw [Finset.mem_range] at hj
obtain ⟨r, rfl⟩ : ∃ r, n = j + r := ⟨n - j, by omega⟩
have E1test : ∀ j r : ℕ, ∏ k ∈ (Finset.range (j + r + 1)).erase j, ((2:ℚ)^j - 2^k) =
(∏ k ∈ Finset.range j, ((2:ℚ)^j - 2^k)) * ∏ x ∈ Finset.range r, ((2:ℚ)^j - 2^(j+1+x)) := by
intro j r
induction r with
| zero =>
simp [Finset.range_add_one]
| succ r ih =>
rw [show j + (r + 1) + 1 = (j + r + 1) + 1 by ring, Finset.range_add_one,
Finset.erase_insert_of_ne (by omega), Finset.prod_insert (by simp), ih,
Finset.prod_range_succ]
rw [show j + 1 + r = j + r + 1 by ring]
ring
have E2test : ∀ j : ℕ, ∏ k ∈ Finset.range j, ((2:ℚ)^j - 2^k) =
2 ^ (j * (j - 1) / 2) * ∏ i ∈ Finset.range j, ((2:ℚ)^(i+1) - 1) := by
intro j
rw [← Finset.prod_range_reflect (fun i => (2:ℚ)^(i+1) - 1)]
rw [show (2:ℚ) ^ (j * (j - 1) / 2) = ∏ k ∈ Finset.range j, (2:ℚ)^k by
rw [Finset.prod_pow_eq_pow_sum, Finset.sum_range_id], ← Finset.prod_mul_distrib]
apply Finset.prod_congr rfl
intro k hk
rw [Finset.mem_range] at hk
rw [show j - 1 - k + 1 = j - k by omega, mul_sub, ← pow_add, show k + (j - k) = j by omega]
ring
have E3test : ∀ j r : ℕ, ∏ x ∈ Finset.range r, ((2:ℚ)^j - 2^(j+1+x)) =
(-1) ^ r * 2 ^ (j * r) * ∏ i ∈ Finset.range r, ((2:ℚ)^(i+1) - 1) := by
intro j r
rw [show (-1:ℚ) ^ r * 2 ^ (j * r) = ∏ _x ∈ Finset.range r, (-(2:ℚ) ^ j) by
rw [Finset.prod_const, Finset.card_range, pow_mul, ← mul_pow, neg_one_mul], ← Finset.prod_mul_distrib]
apply Finset.prod_congr rfl
intro i _
rw [show j + 1 + i = j + (i + 1) by ring, pow_add]
ring
have E4test : ∀ j r : ℕ, ∏ i ∈ Finset.range (j + r), ((2:ℚ)^j - 2^(j + r + 1 + i)) =
(-1) ^ (j + r) * 2 ^ (j * (j + r)) * ∏ i ∈ Finset.range (j + r), ((2:ℚ)^(r + 1 + i) - 1) := by
intro j r
rw [show (-1:ℚ) ^ (j + r) * 2 ^ (j * (j + r)) = ∏ _x ∈ Finset.range (j + r), (-(2:ℚ) ^ j) by
rw [Finset.prod_const, Finset.card_range, pow_mul, ← mul_pow, neg_one_mul], ← Finset.prod_mul_distrib]
apply Finset.prod_congr rfl
intro i _
rw [show j + r + 1 + i = j + (r + 1 + i) by ring, pow_add]
ring
have hQ : ∀ t : ℕ, ∏ i ∈ Finset.range t, ((2 : ℚ) ^ (i + 1) - 1) ≠ 0 := by
intro t
rw [Finset.prod_ne_zero_iff]
intro i _
have : (1 : ℚ) < 2 ^ (i + 1) := one_lt_pow₀ (by norm_num) (by omega)
linarith
have hA : ∀ t : ℕ, ∏ i ∈ Finset.range t, ((2 : ℚ) ^ (r + 1 + i) - 1) ≠ 0 := by
intro t
rw [Finset.prod_ne_zero_iff]
intro i _
have : (1 : ℚ) < 2 ^ (r + 1 + i) := one_lt_pow₀ (by norm_num) (by omega)
linarith
have F1 : ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (j + r - i) - 1) = ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (r + 1 + i) - 1) := by
rw [← Finset.prod_range_reflect (fun i => (2 : ℚ) ^ (r + 1 + i) - 1)]
apply Finset.prod_congr rfl
intro i hi
rw [Finset.mem_range] at hi
rw [show r + 1 + (j - 1 - i) = j + r - i by omega]
have F2 : ∏ i ∈ Finset.range (j + r), ((2 : ℚ) ^ (2 * (j + r) - j - i) - 1) = ∏ i ∈ Finset.range (j + r), ((2 : ℚ) ^ (r + 1 + i) - 1) := by
rw [← Finset.prod_range_reflect (fun i => (2 : ℚ) ^ (r + 1 + i) - 1)]
apply Finset.prod_congr rfl
intro i hi
rw [Finset.mem_range] at hi
rw [show r + 1 + (j + r - 1 - i) = 2 * (j + r) - j - i by omega]
have F3 : ∏ i ∈ Finset.range (j + r), ((2 : ℚ) ^ (i + 1) - 1) = (∏ i ∈ Finset.range r, ((2 : ℚ) ^ (i + 1) - 1)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (r + 1 + i) - 1) := by
rw [add_comm j r, Finset.prod_range_add]
congr 1
apply Finset.prod_congr rfl
intro i _
rw [show r + i + 1 = r + 1 + i by ring]
have hp : (2 : ℚ) ^ (j * (j - 1) / 2) * 2 ^ (j * (j - 1) / 2) * 2 ^ j * 2 ^ (j * r) = 2 ^ (j * (j + r)) := by
rw [← pow_add, ← pow_add, ← pow_add]
congr 1
have h2 := Nat.two_mul_div_two_of_even (Nat.even_mul_pred_self j)
rcases j with _ | s
· simp
· simp only [Nat.add_sub_cancel] at h2 ⊢
zify at h2 ⊢
linear_combination h2
rw [Finset.prod_div_distrib, Finset.prod_div_distrib, F1, F2, F3, E1test, E2test, E3test, E4test]
have hQj := hQ j
have hQr := hQ r
have hAj := hA j
rw [← hp, pow_add (-1 : ℚ)]
field_simp
-- Step 3 (partial fractions / Lagrange interpolation at the nodes 2^0..2^n), from step 4.
have hpf : ∑ j ∈ Finset.range (n + 1), ((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - 1) / 2) * (∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1)) * (∏ i ∈ Finset.range n, ((2 : ℚ) ^ (2 * n - j - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1))) * (2 : ℚ) ^ j / ((2 : ℚ) ^ m - (2 : ℚ) ^ j) =
(∏ i ∈ Finset.range n, ((2 : ℚ) ^ m - (2 : ℚ) ^ (n + 1 + i))) / (∏ k ∈ Finset.range (n + 1), ((2 : ℚ) ^ m - (2 : ℚ) ^ k)) := by
classical
have hinj : Set.InjOn (fun k : ℕ => (2 : ℚ) ^ k) (Finset.range (n + 1) : Set ℕ) := by
intro a _ b _ h
exact (pow_right_inj₀ (by norm_num) (by norm_num)).mp h
have hdeg : (∏ i ∈ Finset.range n, (Polynomial.X - Polynomial.C ((2 : ℚ) ^ (n + 1 + i)))).degree <
((Finset.range (n + 1)).card : WithBot ℕ) := by
rw [Polynomial.degree_prod]
simp only [Polynomial.degree_X_sub_C, Finset.sum_const, Finset.card_range, nsmul_eq_mul, mul_one]
exact_mod_cast Nat.lt_succ_self n
have key := Lagrange.eq_interpolate_of_eval_eq
(fun j => (∏ i ∈ Finset.range n, (Polynomial.X - Polynomial.C ((2 : ℚ) ^ (n + 1 + i)))).eval ((2 : ℚ) ^ j))
hinj hdeg (fun i _ => rfl)
have hev := congrArg (Polynomial.eval ((2 : ℚ) ^ m)) key
rw [Lagrange.interpolate_apply, Polynomial.eval_finsetSum] at hev
simp only [Polynomial.eval_mul, Polynomial.eval_C, Lagrange.basis, Polynomial.eval_prod,
Lagrange.basisDivisor, Polynomial.eval_sub, Polynomial.eval_X] at hev
rw [hev, Finset.sum_div]
apply Finset.sum_congr rfl
intro j hj
have hj' : j < m := by
rw [Finset.mem_range] at hj
omega
have hxj : (2 : ℚ) ^ m - 2 ^ j ≠ 0 := by
have : (2 : ℚ) ^ j < 2 ^ m := pow_lt_pow_right₀ (by norm_num) hj'
linarith
have hE1 : ∏ k ∈ (Finset.range (n + 1)).erase j, ((2 : ℚ) ^ m - 2 ^ k) ≠ 0 := by
rw [Finset.prod_ne_zero_iff]
intro k hk
have hk' : k < m := by
rw [Finset.mem_erase, Finset.mem_range] at hk
omega
have : (2 : ℚ) ^ k < 2 ^ m := pow_lt_pow_right₀ (by norm_num) hk'
linarith
have hE2 : ∏ k ∈ (Finset.range (n + 1)).erase j, ((2 : ℚ) ^ j - 2 ^ k) ≠ 0 := by
rw [Finset.prod_ne_zero_iff]
intro k hk
rw [Finset.mem_erase] at hk
intro h0
exact hk.1 (hinj (Finset.mem_coe.mpr hj) (Finset.mem_coe.mpr hk.2) (sub_eq_zero.mp h0)).symm
rw [← Finset.mul_prod_erase _ _ hj, Finset.prod_mul_distrib, Finset.prod_inv_distrib, ← hres j hj]
field_simp
-- Step 1: each term c_j / (2^(m-j) - 1) = c_j 2^j / (2^m - 2^j), since j <= n < m.
have hl : ∑ j ∈ Finset.range (n + 1), (-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - 1) / 2) * (∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1)) * (∏ i ∈ Finset.range n, ((2 : ℚ) ^ (2 * n - j - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1)) / ((2 : ℚ) ^ (m - j) - 1) = ∑ j ∈ Finset.range (n + 1), ((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - 1) / 2) * (∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1)) * (∏ i ∈ Finset.range n, ((2 : ℚ) ^ (2 * n - j - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1))) * (2 : ℚ) ^ j / ((2 : ℚ) ^ m - (2 : ℚ) ^ j) := by
apply Finset.sum_congr rfl
intro j hj
have hj' : j < m := by
rw [Finset.mem_range] at hj
omega
have h2 : (2 : ℚ) ^ m = 2 ^ (m - j) * 2 ^ j := by
rw [← pow_add, Nat.sub_add_cancel hj'.le]
have hp : (2 : ℚ) ^ j ≠ 0 := by positivity
rw [h2, show (2 : ℚ) ^ (m - j) * 2 ^ j - 2 ^ j = (2 ^ (m - j) - 1) * 2 ^ j by ring,
mul_div_mul_right _ _ hp]
-- Step 2: the right-hand side is N(2^m) / D(2^m).
have hr : (2 : ℚ) ^ (n * n) * (∏ i ∈ Finset.range n, ((2 : ℚ) ^ (i + 1) - 1)) * (∏ i ∈ Finset.range n, ((2 : ℚ) ^ (m - n - 1 - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1)) / ∏ j ∈ Finset.range (n + 1), ((2 : ℚ) ^ (m - j) - 1) = (∏ i ∈ Finset.range n, ((2 : ℚ) ^ m - (2 : ℚ) ^ (n + 1 + i))) / (∏ k ∈ Finset.range (n + 1), ((2 : ℚ) ^ m - (2 : ℚ) ^ k)) := by
have hB : ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (i + 1) - 1) ≠ 0 := by
rw [Finset.prod_ne_zero_iff]
intro i _
have : (1 : ℚ) < 2 ^ (i + 1) := one_lt_pow₀ (by norm_num) (by omega)
linarith
have key : (2 : ℚ) ^ (n * n) * (∏ i ∈ Finset.range n, ((2 : ℚ) ^ (i + 1) - 1)) * (∏ i ∈ Finset.range n, ((2 : ℚ) ^ (m - n - 1 - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1)) / ∏ j ∈ Finset.range (n + 1), ((2 : ℚ) ^ (m - j) - 1) = (2 : ℚ) ^ (n * n) * (∏ i ∈ Finset.range n, ((2 : ℚ) ^ (m - n - 1 - i) - 1)) / (∏ j ∈ Finset.range (n + 1), ((2 : ℚ) ^ (m - j) - 1)) := by
rw [Finset.prod_div_distrib]
field_simp
rcases Nat.lt_or_ge (2 * n) m with h | h
· have hA : (∏ i ∈ Finset.range n, ((2 : ℚ) ^ (m - n - 1 - i) - 1)) = (∏ i ∈ Finset.range n, ((2 : ℚ) ^ m - (2 : ℚ) ^ (n + 1 + i))) / 2 ^ (∑ i ∈ Finset.range n, (n + 1 + i)) := by
rw [← Finset.prod_pow_eq_pow_sum, ← Finset.prod_div_distrib]
apply Finset.prod_congr rfl
intro i hi
rw [Finset.mem_range] at hi
have e : (2 : ℚ) ^ m = 2 ^ (m - n - 1 - i) * 2 ^ (n + 1 + i) := by
rw [← pow_add]
congr 1
omega
rw [e]
field_simp
have hD : (∏ j ∈ Finset.range (n + 1), ((2 : ℚ) ^ (m - j) - 1)) = (∏ k ∈ Finset.range (n + 1), ((2 : ℚ) ^ m - (2 : ℚ) ^ k)) / 2 ^ (∑ j ∈ Finset.range (n + 1), j) := by
rw [← Finset.prod_pow_eq_pow_sum, ← Finset.prod_div_distrib]
apply Finset.prod_congr rfl
intro j hj
rw [Finset.mem_range] at hj
have e : (2 : ℚ) ^ m = 2 ^ (m - j) * 2 ^ j := by
rw [← pow_add]
congr 1
omega
rw [e]
field_simp
have hs : ∑ i ∈ Finset.range n, (n + 1 + i) = n * n + ∑ j ∈ Finset.range (n + 1), j := by
rw [Finset.sum_range_succ, Finset.sum_add_distrib]
simp
ring
have hDX : (∏ k ∈ Finset.range (n + 1), ((2 : ℚ) ^ m - (2 : ℚ) ^ k)) ≠ 0 := by
rw [Finset.prod_ne_zero_iff]
intro k hk
rw [Finset.mem_range] at hk
have : (2 : ℚ) ^ k < 2 ^ m := pow_lt_pow_right₀ (by norm_num) (by omega)
linarith
rw [key, hA, hD, hs, pow_add]
field_simp
· have hz1 : (∏ i ∈ Finset.range n, ((2 : ℚ) ^ (m - n - 1 - i) - 1)) = 0 :=
Finset.prod_eq_zero (i := m - n - 1) (by rw [Finset.mem_range]; omega)
(by rw [show m - n - 1 - (m - n - 1) = 0 by omega]; norm_num)
have hz2 : (∏ i ∈ Finset.range n, ((2 : ℚ) ^ m - (2 : ℚ) ^ (n + 1 + i))) = 0 :=
Finset.prod_eq_zero (i := m - n - 1) (by rw [Finset.mem_range]; omega)
(by rw [show n + 1 + (m - n - 1) = m by omega]; ring)
rw [key, hz1, hz2]
simp
rw [hl, hr]
exact hpfWhat is known
Notes
- Informal proof of spec-f2b55478 (the Pade remainder coefficient identity) by partial fractions. full text →
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-f2b55478».Context
/-- erdos-1050, Borwein's route (annexes f593a93a8960 and 3ada4f0922d7 on erdos-1050--h1-v2):
the coefficient of x^m, for m > n, in Q_n(x) * f(x), where f(x) = sum_{k >= 1} x^k / (2^k - 1) and
Q_n(x) = sum_k (-1)^k 2^(k(k-1)/2) [n k]_2 [2n-k n]_2 x^k is the Pade denominator, equals
2^(n^2) (2;2)_n [m-n-1 n]_2 / prod_{j <= n} (2^(m-j) - 1). It vanishes for n < m <= 2n (the Pade
condition) and is positive for m > 2n, which makes the Pade remainder positive. Checked exactly for
n <= 15, m <= 3n + 29. -/
theorem erdos_1050_pade_remainder_coeff (n m : ℕ) (hnm : n < m) :
∑ j ∈ Finset.range (n + 1),
(-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - 1) / 2) *
(∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1)) *
(∏ i ∈ Finset.range n, ((2 : ℚ) ^ (2 * n - j - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1)) /
((2 : ℚ) ^ (m - j) - 1) =
(2 : ℚ) ^ (n * n) * (∏ i ∈ Finset.range n, ((2 : ℚ) ^ (i + 1) - 1)) *
(∏ i ∈ Finset.range n, ((2 : ℚ) ^ (m - n - 1 - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1)) /
∏ j ∈ Finset.range (n + 1), ((2 : ℚ) ^ (m - j) - 1) := 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 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<m:\quad \sum_{j=0}^{n}\frac{(-1)^j\,2^{j(j-1)/2}\prod_{i=0}^{j-1}\frac{2^{\,n-i}-1}{2^{\,i+1}-1}\prod_{i=0}^{n-1}\frac{2^{\,2n-j-i}-1}{2^{\,i+1}-1}}{2^{\,m-j}-1} \;=\;\frac{2^{n^2}\prod_{i=0}^{n-1}(2^{\,i+1}-1)\prod_{i=0}^{n-1}\frac{2^{\,m-n-1-i}-1}{2^{\,i+1}-1}}{\prod_{j=0}^{n}(2^{\,m-j}-1)}$
For natural numbers $n<m$ this identity holds in $\mathbb{Q}$; the numerator of the $j$-th term on the left is $Q_c(n,j)$ as the Padé family defines it, so the left side is $\sum_{j=0}^{n}Q_c(n,j)/(2^{m-j}-1)$. All subtractions in exponents are natural-number subtraction, which stops at $0$, and $j(j-1)/2$ is natural-number division: since $j\le n<m$ no denominator is $0$ and $n-i$, $2n-j-i$ never truncate, while $m-n-1-i$ does when $m\le 2n$ (the factor $i=m-n-1$ is then $2^0-1=0$ and both sides are $0$). The doc comment's reading as a power-series coefficient, and its sign claim for $m>2n$, are not part of the statement.
Rendered from gloss/445936b33e81….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/15a9ae109326….md · the first version of its chain
Read this version
For natural numbers $n < m$, the following identity holds in $\mathbb{Q}$: $$\sum_{j=0}^{n} \frac{(-1)^j\, 2^{\lfloor j(j-1)/2\rfloor}\Bigl(\prod_{i=0}^{j-1}\frac{2^{\,n-i}-1}{2^{\,i+1}-1}\Bigr)\Bigl(\prod_{i=0}^{n-1}\frac{2^{\,2n-j-i}-1}{2^{\,i+1}-1}\Bigr)}{2^{\,m-j}-1} \;=\; \frac{2^{n\cdot n}\Bigl(\prod_{i=0}^{n-1}(2^{\,i+1}-1)\Bigr)\Bigl(\prod_{i=0}^{n-1}\frac{2^{\,m-n-1-i}-1}{2^{\,i+1}-1}\Bigr)}{\prod_{j=0}^{n}(2^{\,m-j}-1)}.$$
Reading notes. All subtractions in exponents are natural-number subtraction, which stops at $0$. Because $j \le n < m$, the exponents $m-j$ are at least $1$, so no denominator on either side is $0$; likewise $n-i \ge 1$ and $2n-j-i \ge 1$ wherever they occur. The one place truncation matters is $m-n-1-i$ on the right: when $m \le 2n$ the factor with $i = m-n-1$ has exponent $0$ and equals $0$, so the right side, and hence the left, is $0$; when $m > 2n$ no exponent truncates. The numerator of the $j$-th term on the left is exactly $Q_c(n,j)$ as defined in the hole erdos-1050--h1-v2--h3 (a signed product of two Gaussian-binomial-shaped products at $q=2$), so the left side is $\sum_{j=0}^{n} Q_c(n,j)/(2^{m-j}-1)$.
The doc comment reads this as the coefficient of $x^m$ ($m>n$) in $Q_n(x) f(x)$, with $f(x)=\sum_{k\ge1} x^k/(2^k-1)$ and $Q_n$ the Padé denominator, vanishing for $n<m\le 2n$ and positive for $m>2n$; the theorem itself states only the identity above, and says nothing about power series or signs.
Role on the record: the node is listed as proposed for erdos-1050--h1-v2 (Borwein's route, annexes f593a93a8960 and 3ada4f0922d7 on that node, per the doc comment). The site shows it 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/445936b33e81….md · diff to its predecessor
Read this version
$\displaystyle \forall n<m:\quad \sum_{j=0}^{n}\frac{(-1)^j\,2^{j(j-1)/2}\prod_{i=0}^{j-1}\frac{2^{\,n-i}-1}{2^{\,i+1}-1}\prod_{i=0}^{n-1}\frac{2^{\,2n-j-i}-1}{2^{\,i+1}-1}}{2^{\,m-j}-1} \;=\;\frac{2^{n^2}\prod_{i=0}^{n-1}(2^{\,i+1}-1)\prod_{i=0}^{n-1}\frac{2^{\,m-n-1-i}-1}{2^{\,i+1}-1}}{\prod_{j=0}^{n}(2^{\,m-j}-1)}$
For natural numbers $n<m$ this identity holds in $\mathbb{Q}$; the numerator of the $j$-th term on the left is $Q_c(n,j)$ as the Padé family defines it, so the left side is $\sum_{j=0}^{n}Q_c(n,j)/(2^{m-j}-1)$. All subtractions in exponents are natural-number subtraction, which stops at $0$, and $j(j-1)/2$ is natural-number division: since $j\le n<m$ no denominator is $0$ and $n-i$, $2n-j-i$ never truncate, while $m-n-1-i$ does when $m\le 2n$ (the factor $i=m-n-1$ is then $2^0-1=0$ and both sides are $0$). The doc comment's reading as a power-series coefficient, and its sign claim for $m>2n$, are not part of the statement.
Diff of 445936b33e81 against 15a9ae109326
@@ -1,9 +1,4 @@ -For natural numbers $n < m$, the following identity holds in $\mathbb{Q}$: -$$\sum_{j=0}^{n} \frac{(-1)^j\, 2^{\lfloor j(j-1)/2\rfloor}\Bigl(\prod_{i=0}^{j-1}\frac{2^{\,n-i}-1}{2^{\,i+1}-1}\Bigr)\Bigl(\prod_{i=0}^{n-1}\frac{2^{\,2n-j-i}-1}{2^{\,i+1}-1}\Bigr)}{2^{\,m-j}-1} -\;=\; \frac{2^{n\cdot n}\Bigl(\prod_{i=0}^{n-1}(2^{\,i+1}-1)\Bigr)\Bigl(\prod_{i=0}^{n-1}\frac{2^{\,m-n-1-i}-1}{2^{\,i+1}-1}\Bigr)}{\prod_{j=0}^{n}(2^{\,m-j}-1)}.$$ +$$\forall n<m:\quad \sum_{j=0}^{n}\frac{(-1)^j\,2^{j(j-1)/2}\prod_{i=0}^{j-1}\frac{2^{\,n-i}-1}{2^{\,i+1}-1}\prod_{i=0}^{n-1}\frac{2^{\,2n-j-i}-1}{2^{\,i+1}-1}}{2^{\,m-j}-1} +\;=\;\frac{2^{n^2}\prod_{i=0}^{n-1}(2^{\,i+1}-1)\prod_{i=0}^{n-1}\frac{2^{\,m-n-1-i}-1}{2^{\,i+1}-1}}{\prod_{j=0}^{n}(2^{\,m-j}-1)}$$ -Reading notes. All subtractions in exponents are natural-number subtraction, which stops at $0$. Because $j \le n < m$, the exponents $m-j$ are at least $1$, so no denominator on either side is $0$; likewise $n-i \ge 1$ and $2n-j-i \ge 1$ wherever they occur. The one place truncation matters is $m-n-1-i$ on the right: when $m \le 2n$ the factor with $i = m-n-1$ has exponent $0$ and equals $0$, so the right side, and hence the left, is $0$; when $m > 2n$ no exponent truncates. The numerator of the $j$-th term on the left is exactly $Q_c(n,j)$ as defined in the hole erdos-1050--h1-v2--h3 (a signed product of two Gaussian-binomial-shaped products at $q=2$), so the left side is $\sum_{j=0}^{n} Q_c(n,j)/(2^{m-j}-1)$. - -The doc comment reads this as the coefficient of $x^m$ ($m>n$) in $Q_n(x) f(x)$, with $f(x)=\sum_{k\ge1} x^k/(2^k-1)$ and $Q_n$ the Padé denominator, vanishing for $n<m\le 2n$ and positive for $m>2n$; the theorem itself states only the identity above, and says nothing about power series or signs. - -Role on the record: the node is listed as proposed for erdos-1050--h1-v2 (Borwein's route, annexes f593a93a8960 and 3ada4f0922d7 on that node, per the doc comment). The site shows it as not needed by any merged proof of this problem. +For natural numbers $n<m$ this identity holds in $\mathbb{Q}$; the numerator of the $j$-th term on the left is $Q_c(n,j)$ as the Padé family defines it, so the left side is $\sum_{j=0}^{n}Q_c(n,j)/(2^{m-j}-1)$. All subtractions in exponents are natural-number subtraction, which stops at $0$, and $j(j-1)/2$ is natural-number division: since $j\le n<m$ no denominator is $0$ and $n-i$, $2n-j-i$ never truncate, while $m-n-1-i$ does when $m\le 2n$ (the factor $i=m-n-1$ is then $2^0-1=0$ and both sides are $0$). The doc comment's reading as a power-series coefficient, and its sign claim for $m>2n$, are not part of the statement.
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-f2b55478/Statement.lean. Origin: authored.
Attestation: pass, 7 of 7 checks
Checked by the kernel — the gate’s record of the run: attestations/000222.json, merge commit 4148e3125651.
Verdict pass, from attestations/000222.json.
- Submitter
e1050-http-0927- 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/000222.json, merge commit 4148e3125651.
8b3a158c98fe.theorem witness : ∃ n m : ℕ, n < m := ⟨0, 1, Nat.zero_lt_one⟩
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 one hypothesis can be met: there exist natural numbers $n$ and $m$ with $n < m$. It exhibits $n = 0$, $m = 1$. It says nothing about the identity itself.
Rendered from gloss/10b589253b78….md · Improve these words →
Annexes (1), in full
Untrusted contributor text — an annex (D-31): an informal argument, not a proof.
Untrusted: annex (D-31), by e1050-http-0927, 2026-09-27T19:53:57Z, licence CC-BY-4.0. Rendered from targets/erdos-1050/nodes/spec-f2b55478/annex/fcdb7a3a0b0eac5a9cc9f17ce00a203d918c82203729e0d0a4c29795a1778f0d.md.
Informal proof of spec-f2b55478 (the Pade remainder coefficient identity) by partial fractions. Not machine-checked; the identity and the two intermediate identities below were checked exactly in rational arithmetic (Python fractions, with Lean's truncated nat subtraction reproduced) for 0 <= n <= 5, n < m <= n+8 (the full identity) and 0 <= n <= 7, 0 <= j <= n (the residue identity).
Notation. q = 2, (q;q)_r = prod_{s=1..r} (2^s - 1), [n j] the 2-binomial, x = 2^m, and c_j = (-1)^j 2^{j(j-1)/2} [n j] prod_{i<n} (2^{2n-j-i} - 1)/(2^{i+1} - 1) (the LHS coefficient). Let D(x) = prod_{k=0..n} (x - 2^k) (monic, degree n+1, simple roots 2^0..2^n) and N(x) = prod_{i=0..n-1} (x - 2^{n+1+i}) (monic, degree n).
- LHS. Since 2^{m-j} - 1 = (x - 2^j)/2^j and m > n >= j, each term is c_j 2^j / (x - 2^j), so LHS = sum_j c_j 2^j / (x - 2^j).
- RHS = N(x)/D(x). Write 2^{m-n-1-i} - 1 = (x - 2^{n+1+i}) / 2^{n+1+i} and 2^{m-j} - 1 = (x - 2^j)/2^j. The two products of (2^{i+1} - 1) cancel, and the powers of 2 cancel exactly: n^2 - sum_{i<n}(n+1+i) + sum_{j<=n} j = n^2 - (n^2 + n(n+1)/2) + n(n+1)/2 = 0. Lean's truncation of m-n-1-i is harmless: it happens only when n < m <= 2n, and then the factor i = m-n-1 is 2^0 - 1 = 0 on both readings, so both sides of RHS = N(x)/D(x) are 0.
- Partial fractions. deg N < deg D and D has simple roots, so N(x)/D(x) = sum_{j=0..n} N(2^j) / D'(2^j) / (x - 2^j), D'(2^j) = prod_{k<=n, k != j} (2^j - 2^k). Equivalently (clearing denominators) sum_j N(2^j)/D'(2^j) * prod_{k != j}(X - 2^k) = N(X) is Lagrange interpolation of the degree-n polynomial N at the n+1 nodes 2^0..2^n (Mathlib: Lagrange.interpolate / Lagrange.eq_interpolate_of_eval_eq, nodes injective since 2^k is).
- Residue identity: c_j 2^j = N(2^j) / D'(2^j). Compute N(2^j) = (-1)^n 2^{jn} prod_{i<n} (2^{n+1+i-j} - 1), and the exponents n+1-j..2n-j are exactly those of prod_{i<n}(2^{2n-j-i} - 1) in c_j. D'(2^j) = [prod_{k<j} 2^k (2^{j-k} - 1)] [prod_{j<k<=n} (-2^j)(2^{k-j} - 1)] = (-1)^{n-j} 2^{j(j-1)/2 + j(n-j)} (q;q)_j (q;q)_{n-j}. So N(2^j)/D'(2^j) = (-1)^j 2^{j(j+1)/2} [n j] prod_{i<n}(2^{2n-j-i}-1) / (q;q)_n = c_j 2^j, using j(j-1)/2 + j = j(j+1)/2 and [n j] = (q;q)_n / ((q;q)_j (q;q)_{n-j}).
Steps 1-4 give LHS = RHS for every n < m. A Lean proof would most likely go: cast to x = 2^m, multiply out by D(x) (all factors nonzero because m > n), and reduce to the polynomial identity of step 3 evaluated at x, with the coefficient computation of step 4 done by Finset.prod_range_succ induction or by splitting prod_{k != j} at j.
Acknowledged findings (14)
Untrusted contributor text — the prover’s justification for a finding.
Untrusted: acknowledgment of a div-zero finding at (((-1) ^ j * 2 ^ (j * (j - 1) / 2) * ∏ i ∈ Finset.range j, (2 ^ (n - i) - 1) / (2 ^ (i + 1) - 1)) *
∏ i ∈ Finset.range n, (2 ^ (2 * n - j - i) - 1) / (2 ^ (i + 1) - 1)) /
(2 ^ (m - j) - 1)
Every divisor is 2^k - 1 with k >= 1 (k = i+1, or k = m-j with j <= n < m), or a product of such, so it is nonzero; no junk value arises.
Untrusted contributor text — the prover’s justification for a finding.
Untrusted: acknowledgment of a div-zero finding at ((2 ^ (n * n) * ∏ i ∈ Finset.range n, (2 ^ (i + 1) - 1)) *
∏ i ∈ Finset.range n, (2 ^ (m - n - 1 - i) - 1) / (2 ^ (i + 1) - 1)) /
∏ j ∈ Finset.range (n + 1), (2 ^ (m - j) - 1)
Every divisor is 2^k - 1 with k >= 1 (k = i+1, or k = m-j with j <= n < m), or a product of such, so it is nonzero; no junk value arises.
Untrusted contributor text — the prover’s justification for a finding.
Untrusted: acknowledgment of a div-zero finding at (2 ^ (2 * n - j - i) - 1) / (2 ^ (i + 1) - 1)
Every divisor is 2^k - 1 with k >= 1 (k = i+1, or k = m-j with j <= n < m), or a product of such, so it is nonzero; no junk value arises.
Untrusted contributor text — the prover’s justification for a finding.
Untrusted: acknowledgment of a div-zero finding at (2 ^ (m - n - 1 - i) - 1) / (2 ^ (i + 1) - 1)
Every divisor is 2^k - 1 with k >= 1 (k = i+1, or k = m-j with j <= n < m), or a product of such, so it is nonzero; no junk value arises.
Untrusted contributor text — the prover’s justification for a finding.
Untrusted: acknowledgment of a div-zero finding at (2 ^ (n - i) - 1) / (2 ^ (i + 1) - 1)
Every divisor is 2^k - 1 with k >= 1 (k = i+1, or k = m-j with j <= n < m), or a product of such, so it is nonzero; no junk value arises.
Untrusted contributor text — the prover’s justification for a finding.
Untrusted: acknowledgment of a nat-sub finding at 2 * n - j
j <= n and i < n, so 2n - j - i >= 1: no truncation.
Untrusted contributor text — the prover’s justification for a finding.
Untrusted: acknowledgment of a nat-sub finding at 2 * n - j - i
j <= n and i < n, so 2n - j - i >= 1: no truncation.
Untrusted contributor text — the prover’s justification for a finding.
Untrusted: acknowledgment of a nat-sub finding at j - 1
Used only in j*(j-1)/2, which is 0 at j = 0 both with and without truncation, as intended.
Untrusted contributor text — the prover’s justification for a finding.
Untrusted: acknowledgment of a nat-sub finding at m - j
j <= n < m, so m - j >= 1: no truncation.
Untrusted contributor text — the prover’s justification for a finding.
Untrusted: acknowledgment of a nat-sub finding at m - n
n < m by hypothesis, so m - n >= 1 and no truncation occurs; the only truncation in m-n-1-i is intended (see that finding).
Untrusted contributor text — the prover’s justification for a finding.
Untrusted: acknowledgment of a nat-sub finding at m - n - 1
Truncation is intended: when m-n-1-i would be negative (m-n-1 < n) the factor becomes 2^0 - 1 = 0, the correct value of the Gaussian binomial [m-n-1 n]_2 = 0.
Untrusted contributor text — the prover’s justification for a finding.
Untrusted: acknowledgment of a nat-sub finding at m - n - 1 - i
Truncation is intended: when m-n-1-i would be negative (m-n-1 < n) the factor becomes 2^0 - 1 = 0, the correct value of the Gaussian binomial [m-n-1 n]_2 = 0.
Untrusted contributor text — the prover’s justification for a finding.
Untrusted: acknowledgment of a nat-sub finding at n - i
Inside the product over i < j <= n, so n - i >= 1: no truncation.
Untrusted contributor text — the prover’s justification for a finding.
Untrusted: acknowledgment of a off-by-one-range finding at Finset.range (n + 1)
Checked: every value in range is the intended one; exact rational check for n <= 15, m <= 3n+29.