From 0cd0647e4242e3342438c5229fe65b0748db53da Mon Sep 17 00:00:00 2001 From: Fred Date: Tue, 16 Jun 2026 13:27:49 +0200 Subject: [PATCH 1/2] ErdosProblems/349: integer characterization and dyadic fiber (partial results) Adds six partial results assembling a complete characterization on positive integer pairs. Statements only; proofs recorded via the `formal_proof using formal_conjectures` mechanism (commit on the author's fork) per the proof-length guideline. Docstrings use LaTeX markdown. --- FormalConjectures/ErdosProblems/349.lean | 64 ++++++++++++++++++++++++ 1 file changed, 64 insertions(+) diff --git a/FormalConjectures/ErdosProblems/349.lean b/FormalConjectures/ErdosProblems/349.lean index 7625e0a4bd..5bfa267342 100644 --- a/FormalConjectures/ErdosProblems/349.lean +++ b/FormalConjectures/ErdosProblems/349.lean @@ -92,4 +92,68 @@ the repository's proof-length guideline. -/ theorem alpha_gt_two_not_isGoodPair (t α : ℝ) (ht : 0 < t) (hα : 2 < α) : ¬ IsGoodPair t α := by sorry +/-- For $0 < \alpha \le 1$ and any $t > 0$, $(t, \alpha)$ is not a good pair: every term +$\lfloor t\alpha^n\rfloor$ lies in the finite interval $[0, \lfloor t\rfloor]$ (since +$\alpha^n \le 1$), so every subset sum is bounded by the constant $\sum_{i \in [0,\lfloor t\rfloor]} i$, +and no large integer can be a subset sum. A partial result on the open Erdős Problem 349, +complementing the $2 < \alpha$ and integer-coefficient cases. -/ +@[category research solved, AMS 11, + formal_proof using formal_conjectures at + "https://github.com/cepadugato/formal-conjectures/blob/erdos-349-integer-characterization-proof/FormalConjectures/ErdosProblems/349.lean"] +theorem alpha_le_one_not_isGoodPair (t α : ℝ) (ht : 0 < t) (hα0 : 0 < α) (hα1 : α ≤ 1) : + ¬ IsGoodPair t α := by + sorry + +/-- **Binary expansion.** Every natural number $k$ is a sum of distinct powers of two: there is +a finite set $E$ of exponents with $k = \sum_{i \in E} 2^i$. Proved by strong induction: +subtract the largest power $2^m \le k$, recurse on the remainder. -/ +@[category research solved, AMS 11, + formal_proof using formal_conjectures at + "https://github.com/cepadugato/formal-conjectures/blob/erdos-349-integer-characterization-proof/FormalConjectures/ErdosProblems/349.lean"] +theorem exists_finset_sum_two_pow (k : ℕ) : + ∃ E : Finset ℕ, k = ∑ i ∈ E, 2 ^ i := by + sorry + +/-- **The pair $(1, 2)$ is good.** The powers of two $\lfloor 1\cdot 2^n\rfloor = 2^n$ form an +additively complete set: every $k \ge 1$ is a finite sum of distinct powers of two. -/ +@[category research solved, AMS 11, + formal_proof using formal_conjectures at + "https://github.com/cepadugato/formal-conjectures/blob/erdos-349-integer-characterization-proof/FormalConjectures/ErdosProblems/349.lean"] +theorem one_two_isGoodPair : IsGoodPair 1 2 := by + sorry + +/-- **The dyadic fiber at $\alpha = 2$.** For every $k$, the pair $(1/2^k, 2)$ is good: the +sequence $\lfloor 2^n / 2^k\rfloor$ is additively complete because at index $n = m + k$ it equals +the exact power $2^m$, so its range contains all powers of two, which already form an additively +complete set. Uses monotonicity `IsAddComplete.mono`. -/ +@[category research solved, AMS 11, + formal_proof using formal_conjectures at + "https://github.com/cepadugato/formal-conjectures/blob/erdos-349-integer-characterization-proof/FormalConjectures/ErdosProblems/349.lean"] +theorem dyadic_two_isGoodPair (k : ℕ) : IsGoodPair (1 / 2 ^ k) 2 := by + sorry + +/-- **Integer leading coefficient $t \ge 2$ blocks completeness.** For every integer base +$\alpha$, the pair $(t, \alpha)$ with integer $t \ge 2$ is not good: $\lfloor t\alpha^n\rfloor = +t\alpha^n$ is a multiple of $t$, so every subset sum is too, but two consecutive large integers +cannot both be multiples of $t$. Generalizes the parity obstruction ($t = 2$). A partial result +on Erdős Problem 349. -/ +@[category research solved, AMS 11, + formal_proof using formal_conjectures at + "https://github.com/cepadugato/formal-conjectures/blob/erdos-349-integer-characterization-proof/FormalConjectures/ErdosProblems/349.lean"] +theorem int_coeff_ge_two_not_isGoodPair (t : ℤ) (ht : 2 ≤ t) (α : ℤ) : + ¬ IsGoodPair (t : ℝ) (α : ℝ) := by + sorry + +/-- **Erdős Problem 349, complete characterization on positive integer pairs.** For integers +$t \ge 1$, $\alpha \ge 1$, the pair $(t, \alpha)$ is good (i.e. $\lfloor t\alpha^n\rfloor$ is +additively complete) iff $(t, \alpha) = (1, 2)$. Assembles the four partial results: $(1,2)$ is +good, $\alpha \le 1$ fails, $2 < \alpha$ fails (`alpha_gt_two_not_isGoodPair`), and integer +$t \ge 2$ fails. -/ +@[category research solved, AMS 11, + formal_proof using formal_conjectures at + "https://github.com/cepadugato/formal-conjectures/blob/erdos-349-integer-characterization-proof/FormalConjectures/ErdosProblems/349.lean"] +theorem integer_isGoodPair_iff (t α : ℤ) (ht : 1 ≤ t) (hα : 1 ≤ α) : + IsGoodPair (t : ℝ) (α : ℝ) ↔ t = 1 ∧ α = 2 := by + sorry + end Erdos349 From 8c0b7da46f9fff6d1b120a74593867441a972bbe Mon Sep 17 00:00:00 2001 From: Fred Date: Tue, 16 Jun 2026 13:31:57 +0200 Subject: [PATCH 2/2] ErdosProblems/349: (3/2, 2) is not a good pair (mod-3 obstruction) Statement only; proof recorded via the `formal_proof using formal_conjectures` mechanism (commit on the author's fork) per the proof-length guideline. Docstring uses LaTeX markdown. --- FormalConjectures/ErdosProblems/349.lean | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/FormalConjectures/ErdosProblems/349.lean b/FormalConjectures/ErdosProblems/349.lean index 5bfa267342..2eb04d25bc 100644 --- a/FormalConjectures/ErdosProblems/349.lean +++ b/FormalConjectures/ErdosProblems/349.lean @@ -156,4 +156,18 @@ theorem integer_isGoodPair_iff (t α : ℤ) (ht : 1 ≤ t) (hα : 1 ≤ α) : IsGoodPair (t : ℝ) (α : ℝ) ↔ t = 1 ∧ α = 2 := by sorry +/-- **The pair $(3/2, 2)$ is NOT good.** The negative companion of `dyadic_two_isGoodPair`: +while every dyadic coefficient $1/2^k$ gives a good pair at $\alpha = 2$, the non-dyadic rational +$t = 3/2$ does not. The sequence $\lfloor (3/2)\cdot 2^n\rfloor = 1, 3, 6, 12, 24, \ldots$ is not +additively complete because every term but the first $\lfloor 3/2\rfloor = 1$ is a multiple of +$3$ (namely $\lfloor (3/2)\cdot 2^{n+1}\rfloor = 3\cdot 2^n$), so every subset sum is +$\equiv 0$ or $1 \pmod 3$; the infinitely many integers $\equiv 2 \pmod 3$ are never reached. +A partial result on Erdős Problem 349 in the same divisibility family as +`int_coeff_ge_two_not_isGoodPair` (here the modulus is $3$). -/ +@[category research solved, AMS 11, + formal_proof using formal_conjectures at + "https://github.com/cepadugato/formal-conjectures/blob/erdos-349-three-halves-fiber-proof/FormalConjectures/ErdosProblems/349.lean"] +theorem three_halves_two_not_isGoodPair : ¬ IsGoodPair (3 / 2) 2 := by + sorry + end Erdos349