Erdős Problem 346, limit-exists interpretation

This file formalizes an attempted Lean 4 proof of the limit-exists interpretation of Erdős Problem 346.

Original problem: T. F. Bloom, Erdős Problem #346, https://www.erdosproblems.com/346

Background references:

• P. Erdős and R. L. Graham, Old and New Problems and Results in Combinatorial Number Theory, Monographie No. 28 de L'Enseignement Mathématique, 1980.
• R. L. Graham, "A Property of Fibonacci Numbers", Fibonacci Quarterly 2 (1964), 1-10.

Forum relation: In the Erdős Problems discussion thread for Problem #346, Liam Price submitted an answer for the convergence-from-hypotheses interpretation. Dogmachine then proposed the limit-exists interpretation, citing ambiguity in the Erdős-Graham phrasing and Graham's earlier formulation. This file formalizes that limit-exists interpretation:

if the two deletion hypotheses hold, the sequence has a uniform ratio gap, and a (n+1) / a n tends to a real number L > 1, then the quotient sequence tends to the golden ratio.

AI usage disclosure: The Lean formalization and accompanying writeup were prepared with assistance from Codex and ChatGPT. The final mathematical claims and public presentation remain the author's responsibility.

def Erdos346.subsetSums (a : ℕ → ℕ) (I : Set ℕ) : Set ℕ

Finite subset sums using only terms with indices in I.

Equations

• Erdos346.subsetSums a I = {t : ℕ | ∃ (F : Finset ℕ), ↑F ⊆ I ∧ ∑ i ∈ F, a i = t}

def Erdos346.IsCompleteOn (a : ℕ → ℕ) (I : Set ℕ) : Prop

Completeness of the subsequence with index set I: every sufficiently large natural number is a finite subset sum of terms indexed by I.

Equations

• Erdos346.IsCompleteOn a I = ∃ (H : ℕ), ∀ (n : ℕ), H ≤ n → n ∈ Erdos346.subsetSums a I

noncomputable def Erdos346.leastCompleteThreshold (a : ℕ → ℕ) (I : Set ℕ) (hcomplete : IsCompleteOn a I) : ℕ

The least threshold from which a complete subsequence is complete, once a proof of completeness is supplied.

Equations

• Erdos346.leastCompleteThreshold a I hcomplete = Nat.find hcomplete

theorem Erdos346.leastCompleteThreshold_spec {a : ℕ → ℕ} {I : Set ℕ} (hcomplete : IsCompleteOn a I) (t : ℕ) : leastCompleteThreshold a I hcomplete ≤ t → t ∈ subsetSums a I

theorem Erdos346.leastCompleteThreshold_le_of_complete_from {a : ℕ → ℕ} {I : Set ℕ} (hcomplete : IsCompleteOn a I) {H : ℕ} (hH : ∀ (t : ℕ), H ≤ t → t ∈ subsetSums a I) : leastCompleteThreshold a I hcomplete ≤ H

theorem Erdos346.exists_hole_of_lt_leastCompleteThreshold {a : ℕ → ℕ} {I : Set ℕ} (hcomplete : IsCompleteOn a I) {B : ℕ} (hB : B < leastCompleteThreshold a I hcomplete) : ∃ (t : ℕ), B ≤ t ∧ t ∉ subsetSums a I

theorem Erdos346.lt_leastCompleteThreshold_of_exists_hole {a : ℕ → ℕ} {I : Set ℕ} (hcomplete : IsCompleteOn a I) {B : ℕ} (hhole : ∃ (t : ℕ), B ≤ t ∧ t ∉ subsetSums a I) : B < leastCompleteThreshold a I hcomplete

theorem Erdos346.lt_leastCompleteThreshold_iff_exists_hole {a : ℕ → ℕ} {I : Set ℕ} (hcomplete : IsCompleteOn a I) {B : ℕ} : B < leastCompleteThreshold a I hcomplete ↔ ∃ (t : ℕ), B ≤ t ∧ t ∉ subsetSums a I

theorem Erdos346.pred_leastCompleteThreshold_not_mem {a : ℕ → ℕ} {I : Set ℕ} (hcomplete : IsCompleteOn a I) (hpos : 0 < leastCompleteThreshold a I hcomplete) : leastCompleteThreshold a I hcomplete - 1 ∉ subsetSums a I

theorem Erdos346.exists_hole_at_pred_leastCompleteThreshold {a : ℕ → ℕ} {I : Set ℕ} (hcomplete : IsCompleteOn a I) (hpos : 0 < leastCompleteThreshold a I hcomplete) : ∃ (t : ℕ), t = leastCompleteThreshold a I hcomplete - 1 ∧ t ∉ subsetSums a I

def Erdos346.prefixSubsetSums (a : ℕ → ℕ) (I : Set ℕ) (n : ℕ) : Set ℕ

Finite subset sums using only terms in I up to index n.

Equations

• Erdos346.prefixSubsetSums a I n = Erdos346.subsetSums a (I ∩ Set.Iic n)

def Erdos346.CoversInterval (a : ℕ → ℕ) (I : Set ℕ) (n H T : ℕ) : Prop

The finite subset sums up to n cover the whole interval [H, T].

Equations

• Erdos346.CoversInterval a I n H T = ∀ (t : ℕ), H ≤ t → t ≤ T → t ∈ Erdos346.prefixSubsetSums a I n

theorem Erdos346.exists_prefixCoverThreshold_vacuous {a : ℕ → ℕ} {I : Set ℕ} {n T : ℕ} : ∃ (H : ℕ), CoversInterval a I n H T

noncomputable def Erdos346.leastPrefixCoverThreshold (a : ℕ → ℕ) (I : Set ℕ) (n T : ℕ) : ℕ

The least lower endpoint H from which the prefix through n covers [H, T]. This is always defined: H = T + 1 gives a vacuous cover.

Equations

• Erdos346.leastPrefixCoverThreshold a I n T = Nat.find ⋯

theorem Erdos346.leastPrefixCoverThreshold_cover {a : ℕ → ℕ} {I : Set ℕ} {n T : ℕ} : CoversInterval a I n (leastPrefixCoverThreshold a I n T) T

The least prefix-cover threshold really covers from itself.

theorem Erdos346.leastPrefixCoverThreshold_le_of_cover {a : ℕ → ℕ} {I : Set ℕ} {n T H : ℕ} (hcover : CoversInterval a I n H T) : leastPrefixCoverThreshold a I n T ≤ H

Any prefix-cover threshold bounds the least such threshold.

theorem Erdos346.CoversInterval.mono_lower {a : ℕ → ℕ} {I : Set ℕ} {n H H' T : ℕ} (hcover : CoversInterval a I n H T) (hHH' : H ≤ H') : CoversInterval a I n H' T

theorem Erdos346.not_coversInterval_iff_exists_prefix_hole {a : ℕ → ℕ} {I : Set ℕ} {n H T : ℕ} : ¬CoversInterval a I n H T ↔ ∃ (t : ℕ), H ≤ t ∧ t ≤ T ∧ t ∉ prefixSubsetSums a I n

theorem Erdos346.exists_prefix_hole_of_lt_leastPrefixCoverThreshold {a : ℕ → ℕ} {I : Set ℕ} {n T B : ℕ} (hB : B < leastPrefixCoverThreshold a I n T) : ∃ (t : ℕ), B ≤ t ∧ t ≤ T ∧ t ∉ prefixSubsetSums a I n

theorem Erdos346.lt_leastPrefixCoverThreshold_of_exists_prefix_hole {a : ℕ → ℕ} {I : Set ℕ} {n T B : ℕ} (hhole : ∃ (t : ℕ), B ≤ t ∧ t ≤ T ∧ t ∉ prefixSubsetSums a I n) : B < leastPrefixCoverThreshold a I n T

theorem Erdos346.lt_leastPrefixCoverThreshold_iff_exists_prefix_hole {a : ℕ → ℕ} {I : Set ℕ} {n T B : ℕ} : B < leastPrefixCoverThreshold a I n T ↔ ∃ (t : ℕ), B ≤ t ∧ t ≤ T ∧ t ∉ prefixSubsetSums a I n

def Erdos346.nextSeedMargin (a : ℕ → ℕ) (M : ℕ) : ℕ

The first finite margin in the start = M + 2 seed.

Equations

• Erdos346.nextSeedMargin a M = a (M + 2) - a (M + 1)

def Erdos346.pairSeedMargin (a : ℕ → ℕ) (M : ℕ) : ℕ

The second finite margin in the start = M + 2 seed.

Equations

• Erdos346.pairSeedMargin a M = a (M + 1) + a (M + 2) - a (M + 3)

theorem Erdos346.nextSeedMargin_lt_least_of_not_seed_keep {a : ℕ → ℕ} {I : Set ℕ} {M : ℕ} (hnext : a (M + 1) ≤ a (M + 2)) (hnot : ¬leastPrefixCoverThreshold a I M (a (M + 2) - 1) + a (M + 1) ≤ a (M + 2)) : nextSeedMargin a M < leastPrefixCoverThreshold a I M (a (M + 2) - 1)

theorem Erdos346.pairSeedMargin_lt_least_of_not_seed_margin {a : ℕ → ℕ} {I : Set ℕ} {M : ℕ} (hpair : a (M + 3) ≤ a (M + 1) + a (M + 2)) (hnot : ¬leastPrefixCoverThreshold a I M (a (M + 2) - 1) + a (M + 3) ≤ a (M + 1) + a (M + 2)) : pairSeedMargin a M < leastPrefixCoverThreshold a I M (a (M + 2) - 1)

theorem Erdos346.exists_prefix_hole_of_not_seed_keep {a : ℕ → ℕ} {I : Set ℕ} {M : ℕ} (hnext : a (M + 1) ≤ a (M + 2)) (hnot : ¬leastPrefixCoverThreshold a I M (a (M + 2) - 1) + a (M + 1) ≤ a (M + 2)) : ∃ (t : ℕ), nextSeedMargin a M ≤ t ∧ t ≤ a (M + 2) - 1 ∧ t ∉ prefixSubsetSums a I M

theorem Erdos346.exists_prefix_hole_of_not_seed_margin {a : ℕ → ℕ} {I : Set ℕ} {M : ℕ} (hpair : a (M + 3) ≤ a (M + 1) + a (M + 2)) (hnot : ¬leastPrefixCoverThreshold a I M (a (M + 2) - 1) + a (M + 3) ≤ a (M + 1) + a (M + 2)) : ∃ (t : ℕ), pairSeedMargin a M ≤ t ∧ t ≤ a (M + 2) - 1 ∧ t ∉ prefixSubsetSums a I M

noncomputable def Erdos346.keptPrefixSum (a : ℕ → ℕ) (D : Set ℕ) (n : ℕ) : ℕ

Sum of the non-deleted terms up to index n.

Equations

• Erdos346.keptPrefixSum a D n = ∑ i ∈ Finset.range (n + 1) with i ∉ D, a i

def Erdos346.fullPrefixSum (a : ℕ → ℕ) (n : ℕ) : ℕ

Sum of all terms up to index n.

Equations

• Erdos346.fullPrefixSum a n = ∑ i ∈ Finset.range (n + 1), a i

def Erdos346.budgetBase (a : ℕ → ℕ) (H M T : ℕ) : ℕ

The fixed numerical slack needed to convert a full-prefix surplus into the Brown budget inequality for an initial covered interval [H, T] at index M.

Equations

• Erdos346.budgetBase a H M T = Erdos346.fullPrefixSum a M + H - (T + 1)

def Erdos346.beforeBudgetNeed (a : ℕ → ℕ) (H start : ℕ) : ℕ

A simple finite upper bound sufficient for all before-budget inequalities between M and the first deleted index start. This is deliberately coarse: it packages the finite obstruction into one number.

Equations

• Erdos346.beforeBudgetNeed a H start = (Finset.range start).sup fun (n : ℕ) => H + a (n + 1)

noncomputable def Erdos346.deletedPrefixSum (a : ℕ → ℕ) (D : Set ℕ) (n : ℕ) : ℕ

Sum of the deleted terms up to index n.

Equations

• Erdos346.deletedPrefixSum a D n = ∑ i ∈ Finset.range (n + 1) with i ∈ D, a i

def Erdos346.indexedDeletedSum (a b : ℕ → ℕ) (k : ℕ) : ℕ

Sum of the first k deleted terms in an indexed deletion sequence.

Equations

• Erdos346.indexedDeletedSum a b k = ∑ j ∈ Finset.range k, a (b j)

theorem Erdos346.indexedDeletedSum_zero {a b : ℕ → ℕ} : indexedDeletedSum a b 0 = 0

theorem Erdos346.indexedDeletedSum_succ {a b : ℕ → ℕ} {k : ℕ} : indexedDeletedSum a b (k + 1) = indexedDeletedSum a b k + a (b k)

def Erdos346.recursiveBudgetState (a threshold : ℕ → ℕ) (C start : ℕ) : ℕ → ℕ × ℕ

State for the recursive sparse-deletion construction. The first component is the current deleted index, and the second component is the sum of all deleted terms chosen so far.

Equations

• One or more equations did not get rendered due to their size.
• Erdos346.recursiveBudgetState a threshold C start 0 = (start, a start)

def Erdos346.recursiveBudgetSeq (a threshold : ℕ → ℕ) (C start k : ℕ) : ℕ

The indexed deletion sequence associated to recursiveBudgetState.

Equations

• Erdos346.recursiveBudgetSeq a threshold C start k = (Erdos346.recursiveBudgetState a threshold C start k).1

theorem Erdos346.recursiveBudgetSeq_zero {a threshold : ℕ → ℕ} {C start : ℕ} : recursiveBudgetSeq a threshold C start 0 = start

theorem Erdos346.recursiveBudgetState_sum {a threshold : ℕ → ℕ} {C start : ℕ} (k : ℕ) : (recursiveBudgetState a threshold C start k).2 = indexedDeletedSum a (recursiveBudgetSeq a threshold C start) (k + 1)

theorem Erdos346.recursiveBudgetSeq_succ {a threshold : ℕ → ℕ} {C start k : ℕ} : recursiveBudgetSeq a threshold C start (k + 1) = max (recursiveBudgetSeq a threshold C start k + 2) (threshold (C + indexedDeletedSum a (recursiveBudgetSeq a threshold C start) (k + 1)))

theorem Erdos346.recursiveBudgetSeq_gap {a threshold : ℕ → ℕ} {C start : ℕ} (k : ℕ) : recursiveBudgetSeq a threshold C start k + 1 < recursiveBudgetSeq a threshold C start (k + 1)

theorem Erdos346.recursiveBudgetSeq_threshold_le_succ {a threshold : ℕ → ℕ} {C start k : ℕ} : threshold (C + indexedDeletedSum a (recursiveBudgetSeq a threshold C start) (k + 1)) ≤ recursiveBudgetSeq a threshold C start (k + 1)

def Erdos346.blockDeletionSet (b e : ℕ → ℕ) : Set ℕ

Deletion set obtained from an indexed family of finite blocks [b k, e k].

Equations

• Erdos346.blockDeletionSet b e = {n : ℕ | ∃ (k : ℕ), b k ≤ n ∧ n ≤ e k}

def Erdos346.initialTailDeletionSet (F : Set ℕ) (b : ℕ → ℕ) : Set ℕ

Deletion set obtained by combining a finite initial deletion set with an indexed sparse tail.

Equations

• Erdos346.initialTailDeletionSet F b = F ∪ Set.range b

def Erdos346.periodicDeletionSeq (start period k : ℕ) : ℕ

Arithmetic-progression deletion indices. In the global-budget route these are used to delete one term every fixed block.

Equations

• Erdos346.periodicDeletionSeq start period k = start + k * period

def Erdos346.periodicDeletionSet (start period : ℕ) : Set ℕ

The set of indices deleted by the periodic deletion scheme with the given start and period, i.e. the range of periodicDeletionSeq start period.

Equations

• Erdos346.periodicDeletionSet start period = Set.range (Erdos346.periodicDeletionSeq start period)

def Erdos346.previousBlockSum (a : ℕ → ℕ) (m n : ℕ) : ℕ

Sum of the m terms immediately preceding index n. For m ≤ n, this is a (n-m) + ... + a (n-1).

Equations

• Erdos346.previousBlockSum a m n = ∑ i ∈ Finset.Icc (n - m) (n - 1), a i

def Erdos346.FixedLengthBlockSurplusFrom (a : ℕ → ℕ) (m N : ℕ) : Prop

From index N on, every term a (n + 1) is strictly dominated by the sum of the previous m terms (previousBlockSum a m n). This is the fixed-length block surplus property used to force completeness.

Equations

• Erdos346.FixedLengthBlockSurplusFrom a m N = ∀ (n : ℕ), N ≤ n → m ≤ n → a (n + 1) < Erdos346.previousBlockSum a m n

theorem Erdos346.FixedLengthBlockSurplusFrom.mono {a : ℕ → ℕ} {m N N' : ℕ} (hsurplus : FixedLengthBlockSurplusFrom a m N) (hNN' : N ≤ N') : FixedLengthBlockSurplusFrom a m N'

def Erdos346.GeometricBlockSurplus (ρ : ℝ) (m : ℕ) : Prop

The geometric block-surplus condition at ratio ρ and block length m: for every n ≥ m, the inverse geometric weights of the previous m terms sum to more than one. This drives the surplus needed for the golden-ratio bound.

Equations

• Erdos346.GeometricBlockSurplus ρ m = ∀ (n : ℕ), m ≤ n → 1 < ∑ i ∈ Finset.Icc (n - m) (n - 1), (ρ ^ (n + 1 - i))⁻¹

theorem Erdos346.periodicDeletionSeq_succ {start period k : ℕ} : periodicDeletionSeq start period (k + 1) = periodicDeletionSeq start period k + period

theorem Erdos346.periodicDeletionSeq_gap_of_two_le_period {start period : ℕ} (hperiod : 2 ≤ period) (k : ℕ) : periodicDeletionSeq start period k + 1 < periodicDeletionSeq start period (k + 1)

theorem Erdos346.strictMono_periodicDeletionSeq_of_pos {start period : ℕ} (hperiod : 0 < period) : StrictMono (periodicDeletionSeq start period)

theorem Erdos346.periodicDeletionSet_infinite {start period : ℕ} (hperiod : 0 < period) : (periodicDeletionSet start period).Infinite

theorem Erdos346.periodicDeletionSet_coinfinite_of_two_le_period {start period : ℕ} (hperiod : 2 ≤ period) : (periodicDeletionSet start period)ᶜ.Infinite

theorem Erdos346.periodicDeletionSet_avoids_initial {M start period : ℕ} (hMstart : M < start) : Set.Iic M ⊆ (periodicDeletionSet start period)ᶜ

theorem Erdos346.periodicDeletionSeq_add_period_le_of_lt {start period j k : ℕ} (hperiod : 0 < period) (hjk : j < k) : periodicDeletionSeq start period j + period ≤ periodicDeletionSeq start period k

theorem Erdos346.periodicDeletionSet_not_mem_of_current_window {start period k i : ℕ} (hperiod : 0 < period) (hleft : periodicDeletionSeq start period k < i + period) (hright : i < periodicDeletionSeq start period k) : i ∉ periodicDeletionSet start period

theorem Erdos346.periodicDeletionSet_not_mem_previousBlock_of_period_m_add_two {start m k i : ℕ} (hmpos : 0 < m) (hmd : m ≤ periodicDeletionSeq start (m + 2) k) (hlo : periodicDeletionSeq start (m + 2) k - m ≤ i) (hhi : i ≤ periodicDeletionSeq start (m + 2) k - 1) : i ∉ periodicDeletionSet start (m + 2)

theorem Erdos346.periodicDeletionSet_not_mem_previousBlock_of_mem_period_m_add_two {start m d i : ℕ} (hmpos : 0 < m) (hmem : d ∈ periodicDeletionSet start (m + 2)) (hmd : m ≤ d) (hlo : d - m ≤ i) (hhi : i ≤ d - 1) : i ∉ periodicDeletionSet start (m + 2)

theorem Erdos346.periodicDeletionSet_start_le_of_mem {start period d : ℕ} (hmem : d ∈ periodicDeletionSet start period) : start ≤ d

theorem Erdos346.periodicDeletionSet_mem_period_m_add_two_bounds {M m d : ℕ} (hmem : d ∈ periodicDeletionSet (M + m + 1) (m + 2)) : M < d - m ∧ m ≤ d ∧ M + m + 1 ≤ d

noncomputable def Erdos346.quotient (a : ℕ → ℕ) (n : ℕ) : ℝ

The quotient a (n+1) / a n, viewed in ℝ.

Equations

• Erdos346.quotient a n = ↑(a (n + 1)) / ↑(a n)

def Erdos346.HasUniformRatioGap (a : ℕ → ℕ) : Prop

The original lacunarity lower bound, expressed for index sequences.

Equations

• Erdos346.HasUniformRatioGap a = ∃ (ε : ℝ), 0 < ε ∧ ∀ (n : ℕ), 1 + ε ≤ Erdos346.quotient a n

def Erdos346.FiniteDeletionComplete (a : ℕ → ℕ) : Prop

Deleting any finite set of indices leaves a complete subsequence.

Equations

• Erdos346.FiniteDeletionComplete a = ∀ (D : Set ℕ), D.Finite → Erdos346.IsCompleteOn a Dᶜ

def Erdos346.UniformFinSingletonComplete (a : ℕ → ℕ) : Prop

Uniform finite-base singleton completeness. This is the remaining uniformity needed by the finite-initial-tail lower-bound route: after deleting one fixed finite base set F, deleting any sufficiently late single extra index still leaves a complete subsequence with one common threshold.

Equations

• Erdos346.UniformFinSingletonComplete a = ∃ (F : Set ℕ), F.Finite ∧ ∃ (H : ℕ), ∀ᶠ (M : ℕ) in Filter.atTop, ∀ (t : ℕ), H ≤ t → t ∈ Erdos346.subsetSums a (F ∪ {M + 1})ᶜ

def Erdos346.UniformFinSingletonPrefixCover (a : ℕ → ℕ) : Prop

The weaker uniform condition actually needed by the start = M + 2 finite-initial-tail seed route. Instead of asking for full completeness after deleting F ∪ {M + 1}, it asks only for the finite prefix cover window used by the seed constructor.

Equations

• Erdos346.UniformFinSingletonPrefixCover a = ∃ (F : Set ℕ), F.Finite ∧ ∃ (H : ℕ), ∀ᶠ (M : ℕ) in Filter.atTop, F ⊆ Set.Iic M ∧ Erdos346.CoversInterval a Fᶜ M H (a (M + 2) - 1)

def Erdos346.EventualFinSingletonSmallPrefixCover (a : ℕ → ℕ) : Prop

A still weaker seed-window condition: the threshold may depend on M, but for eventually all M there is a prefix-cover threshold small enough for the two finite numeric inequalities used by the start = M + 2 seed constructor.

Equations

• One or more equations did not get rendered due to their size.

def Erdos346.ArbitrarilyLargeFinSingletonSmallPrefixCover (a : ℕ → ℕ) : Prop

The seed construction only needs one sufficiently late good singleton window, not a good window at every sufficiently late index. This formulation asks for good finite-singleton windows arbitrarily far out.

Equations

• One or more equations did not get rendered due to their size.

def Erdos346.EventualFinSingletonLeastSmallPrefixCover (a : ℕ → ℕ) : Prop

The same small-window target phrased using the least possible prefix-cover threshold. This turns the remaining finite-deletion problem into bounding one explicit finite combinatorial quantity.

Equations

• One or more equations did not get rendered due to their size.

def Erdos346.ArbitrarilyLargeFinSingletonLeastSmallPrefixCover (a : ℕ → ℕ) : Prop

Least-threshold form of ArbitrarilyLargeFinSingletonSmallPrefixCover.

Equations

• One or more equations did not get rendered due to their size.

def Erdos346.ArbitrarilyLargeFinSingletonFirstSmallPrefixCover (a : ℕ → ℕ) : Prop

The weakest current finite-window target for the lower-bound route. It only asks, arbitrarily far out, for the first finite seed inequality. Under the eventual upper ratio bound quotient a n < ρ < φ, finite-deletion completeness upgrades this to the full least-small target below.

Equations

• One or more equations did not get rendered due to their size.

def Erdos346.ArbitrarilyLargeFinSingletonFirstPrefixCover (a : ℕ → ℕ) : Prop

Equivalent cover form of the current first-seed target. Instead of speaking about the canonical least threshold, it asks directly that the finite prefix through M cover the whole first seed window [nextSeedMargin a M, a (M + 2) - 1].

Equations

• One or more equations did not get rendered due to their size.

def Erdos346.FirstWindowShiftClosed (a : ℕ → ℕ) (F : Set ℕ) (M : ℕ) : Prop

Local closure condition that rules out the first-window shift gap. Every prefix sum below the first seed margin remains a prefix sum after adding a (M + 1), even though index M + 1 itself is not allowed in the prefix through M.

Equations

• Erdos346.FirstWindowShiftClosed a F M = ∀ s ∈ Erdos346.prefixSubsetSums a Fᶜ M, s < Erdos346.nextSeedMargin a M → a (M + 1) + s ∈ Erdos346.prefixSubsetSums a Fᶜ M

def Erdos346.ArbitrarilyLargeFinSingletonFirstWindowShiftClosed (a : ℕ → ℕ) : Prop

Arbitrarily late occurrences of the local first-window shift closure for one fixed finite base set.

Equations

• Erdos346.ArbitrarilyLargeFinSingletonFirstWindowShiftClosed a = ∃ (F : Set ℕ), F.Finite ∧ ∀ (N : ℕ), ∃ (M : ℕ), N ≤ M ∧ F ⊆ Set.Iic M ∧ Erdos346.FirstWindowShiftClosed a F M

def Erdos346.FinSingletonCompleteBelowPrev (a : ℕ → ℕ) (F : Set ℕ) (M : ℕ) : Prop

The moving singleton-deletion threshold condition sufficient for FirstWindowShiftClosed: after deleting F ∪ {M + 1}, completeness has already started by the previous term a (M + 1).

Equations

• Erdos346.FinSingletonCompleteBelowPrev a F M = ∃ H ≤ a (M + 1), ∀ (t : ℕ), H ≤ t → t ∈ Erdos346.subsetSums a (F ∪ {M + 1})ᶜ

def Erdos346.ArbitrarilyLargeFinSingletonCompleteBelowPrev (a : ℕ → ℕ) : Prop

Arbitrarily late occurrences of the moving singleton-deletion threshold condition for one fixed finite base set.

Equations

• Erdos346.ArbitrarilyLargeFinSingletonCompleteBelowPrev a = ∃ (F : Set ℕ), F.Finite ∧ ∀ (N : ℕ), ∃ (M : ℕ), N ≤ M ∧ F ⊆ Set.Iic M ∧ Erdos346.FinSingletonCompleteBelowPrev a F M

def Erdos346.InfiniteDeletionIncomplete (a : ℕ → ℕ) : Prop

Deleting any infinite set of indices leaves an incomplete subsequence.

Equations

• Erdos346.InfiniteDeletionIncomplete a = ∀ (D : Set ℕ), D.Infinite → ¬Erdos346.IsCompleteOn a Dᶜ

def Erdos346.IsCompleteAfterDeletingValues (a : ℕ → ℕ) (B : Set ℕ) : Prop

Completeness after deleting a set of values rather than a set of indices. The remaining terms are those indices i whose value a i is not in B.

Equations

• Erdos346.IsCompleteAfterDeletingValues a B = Erdos346.IsCompleteOn a {i : ℕ | a i ∉ B}

def Erdos346.ValueFiniteDeletionComplete (a : ℕ → ℕ) : Prop

Deleting any finite set of values leaves a complete subsequence.

Equations

• Erdos346.ValueFiniteDeletionComplete a = ∀ (B : Set ℕ), B.Finite → Erdos346.IsCompleteAfterDeletingValues a B

def Erdos346.ValueInfiniteDeletionIncomplete (a : ℕ → ℕ) : Prop

Deleting any infinite subset of the sequence values leaves an incomplete subsequence. The side condition B ⊆ Set.range a says that B really consists of values from the sequence.

Equations

• Erdos346.ValueInfiniteDeletionIncomplete a = ∀ (B : Set ℕ), B.Infinite → B ⊆ Set.range a → ¬Erdos346.IsCompleteAfterDeletingValues a B

theorem Erdos346.index_compl_eq_value_kept_image {a : ℕ → ℕ} (hmono : StrictMono a) (D : Set ℕ) : Dᶜ = {i : ℕ | a i ∉ a '' D}

theorem Erdos346.finiteDeletionComplete_of_valueFiniteDeletionComplete {a : ℕ → ℕ} (hmono : StrictMono a) (hvalue : ValueFiniteDeletionComplete a) : FiniteDeletionComplete a

theorem Erdos346.valueFiniteDeletionComplete_of_finiteDeletionComplete {a : ℕ → ℕ} (hmono : StrictMono a) (hindex : FiniteDeletionComplete a) : ValueFiniteDeletionComplete a

theorem Erdos346.finiteDeletionComplete_iff_valueFiniteDeletionComplete {a : ℕ → ℕ} (hmono : StrictMono a) : FiniteDeletionComplete a ↔ ValueFiniteDeletionComplete a

theorem Erdos346.infiniteDeletionIncomplete_of_valueInfiniteDeletionIncomplete {a : ℕ → ℕ} (hmono : StrictMono a) (hvalue : ValueInfiniteDeletionIncomplete a) : InfiniteDeletionIncomplete a

theorem Erdos346.valueInfiniteDeletionIncomplete_of_infiniteDeletionIncomplete {a : ℕ → ℕ} (hindex : InfiniteDeletionIncomplete a) : ValueInfiniteDeletionIncomplete a

theorem Erdos346.infiniteDeletionIncomplete_iff_valueInfiniteDeletionIncomplete {a : ℕ → ℕ} (hmono : StrictMono a) : InfiniteDeletionIncomplete a ↔ ValueInfiniteDeletionIncomplete a

theorem Erdos346.term_ge_succ_of_strictMono_pos {a : ℕ → ℕ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (n : ℕ) : n + 1 ≤ a n

theorem Erdos346.evt_const_add_self_le_next_of_uniformRatioGap {a : ℕ → ℕ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hgap : HasUniformRatioGap a) (C : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, C + a n ≤ a (n + 1)

theorem Erdos346.evt_const_add_next_le_next_next_of_uniformRatioGap {a : ℕ → ℕ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hgap : HasUniformRatioGap a) (C : ℕ) : ∀ᶠ (M : ℕ) in Filter.atTop, C + a (M + 1) ≤ a (M + 2)

theorem Erdos346.complete_univ_of_finiteDeletionComplete {a : ℕ → ℕ} (hfinite : FiniteDeletionComplete a) : IsCompleteOn a Set.univ

theorem Erdos346.tail_complete_of_finiteDeletionComplete {a : ℕ → ℕ} (hfinite : FiniteDeletionComplete a) (N : ℕ) : IsCompleteOn a (Set.Ici N)

theorem Erdos346.finite_singleton_complete_of_finiteDeletionComplete {a : ℕ → ℕ} {F : Set ℕ} (hfinite : FiniteDeletionComplete a) (hF : F.Finite) (M : ℕ) : IsCompleteOn a (F ∪ {M + 1})ᶜ

noncomputable def Erdos346.finSingletonCompleteThreshold (a : ℕ → ℕ) (hfinite : FiniteDeletionComplete a) {F : Set ℕ} (hF : F.Finite) (M : ℕ) : ℕ

The canonical completeness threshold obtained from finite deletion after deleting a fixed finite base set F and the moving singleton M + 1.

Equations

• Erdos346.finSingletonCompleteThreshold a hfinite hF M = Erdos346.leastCompleteThreshold a (F ∪ {M + 1})ᶜ ⋯

theorem Erdos346.finSingletonCompleteThreshold_spec {a : ℕ → ℕ} (hfinite : FiniteDeletionComplete a) {F : Set ℕ} (hF : F.Finite) {M t : ℕ} (ht : finSingletonCompleteThreshold a hfinite hF M ≤ t) : t ∈ subsetSums a (F ∪ {M + 1})ᶜ

theorem Erdos346.finSingletonCompleteThreshold_le_of_complete_from {a : ℕ → ℕ} (hfinite : FiniteDeletionComplete a) {F : Set ℕ} (hF : F.Finite) {M H : ℕ} (hH : ∀ (t : ℕ), H ≤ t → t ∈ subsetSums a (F ∪ {M + 1})ᶜ) : finSingletonCompleteThreshold a hfinite hF M ≤ H

theorem Erdos346.finSingletonCompleteBelowPrev_iff_threshold_le {a : ℕ → ℕ} (hfinite : FiniteDeletionComplete a) {F : Set ℕ} (hF : F.Finite) {M : ℕ} : FinSingletonCompleteBelowPrev a F M ↔ finSingletonCompleteThreshold a hfinite hF M ≤ a (M + 1)

theorem Erdos346.not_finSingletonCompleteBelowPrev_iff_prev_lt_threshold {a : ℕ → ℕ} (hfinite : FiniteDeletionComplete a) {F : Set ℕ} (hF : F.Finite) {M : ℕ} : ¬FinSingletonCompleteBelowPrev a F M ↔ a (M + 1) < finSingletonCompleteThreshold a hfinite hF M

theorem Erdos346.exists_finSingletonCompleteThreshold_hole_of_prev_lt {a : ℕ → ℕ} (hfinite : FiniteDeletionComplete a) {F : Set ℕ} (hF : F.Finite) {M : ℕ} (hlt : a (M + 1) < finSingletonCompleteThreshold a hfinite hF M) : ∃ (t : ℕ), a (M + 1) ≤ t ∧ t ∉ subsetSums a (F ∪ {M + 1})ᶜ

theorem Erdos346.pred_finSingletonCompleteThreshold_hole_of_prev_lt {a : ℕ → ℕ} (hfinite : FiniteDeletionComplete a) {F : Set ℕ} (hF : F.Finite) {M : ℕ} (hlt : a (M + 1) < finSingletonCompleteThreshold a hfinite hF M) : finSingletonCompleteThreshold a hfinite hF M - 1 ∉ subsetSums a (F ∪ {M + 1})ᶜ

theorem Erdos346.pred_finSingletonCompleteThreshold_ge_prev_of_prev_lt {a : ℕ → ℕ} (hfinite : FiniteDeletionComplete a) {F : Set ℕ} (hF : F.Finite) {M : ℕ} (hlt : a (M + 1) < finSingletonCompleteThreshold a hfinite hF M) : a (M + 1) ≤ finSingletonCompleteThreshold a hfinite hF M - 1

theorem Erdos346.exists_pred_finSingletonCompleteThreshold_hole_of_prev_lt {a : ℕ → ℕ} (hfinite : FiniteDeletionComplete a) {F : Set ℕ} (hF : F.Finite) {M : ℕ} (hlt : a (M + 1) < finSingletonCompleteThreshold a hfinite hF M) : ∃ (t : ℕ), t = finSingletonCompleteThreshold a hfinite hF M - 1 ∧ a (M + 1) ≤ t ∧ t ∉ subsetSums a (F ∪ {M + 1})ᶜ

theorem Erdos346.arbLargeFinSingletonCompleteBelowPrev_iff_threshold_le {a : ℕ → ℕ} (hfinite : FiniteDeletionComplete a) : ArbitrarilyLargeFinSingletonCompleteBelowPrev a ↔ ∃ (F : Set ℕ) (hF : F.Finite), ∀ (N : ℕ), ∃ (M : ℕ), N ≤ M ∧ F ⊆ Set.Iic M ∧ finSingletonCompleteThreshold a hfinite hF M ≤ a (M + 1)

theorem Erdos346.uniformFinSingletonComplete_of_eventual_singleton_complete {a : ℕ → ℕ} (hsingleton : ∃ (H : ℕ), ∀ᶠ (M : ℕ) in Filter.atTop, ∀ (t : ℕ), H ≤ t → t ∈ subsetSums a {M + 1}ᶜ) : UniformFinSingletonComplete a

theorem Erdos346.one_add_lt_mul_of_goldenRatio_lt {x y : ℝ} (hx : Real.goldenRatio < x) (hy : Real.goldenRatio < y) : 1 + x < x * y

theorem Erdos346.two_step_gap_of_quotient_gt_goldenRatio {a : ℕ → ℕ} {n : ℕ} (hpos : ∀ (n : ℕ), 0 < a n) (hn : Real.goldenRatio < quotient a n) (hn1 : Real.goldenRatio < quotient a (n + 1)) : a n + a (n + 1) < a (n + 2)

theorem Erdos346.goldenRatio_lt_two : Real.goldenRatio < 2

theorem Erdos346.rho_mul_sub_one_lt_one {ρ : ℝ} (hρ1 : 1 < ρ) (hρφ : ρ < Real.goldenRatio) : ρ * (ρ - 1) < 1

theorem Erdos346.exists_range_geometricBlockWeightSum_gt_one {ρ : ℝ} (hρ1 : 1 < ρ) (hρφ : ρ < Real.goldenRatio) : ∃ (m : ℕ), 0 < m ∧ 1 < ∑ j ∈ Finset.range m, (ρ ^ (j + 2))⁻¹

theorem Erdos346.geometricBlockSurplus_of_range_geometricBlockWeightSum_gt_one {ρ : ℝ} {m : ℕ} (hmpos : 0 < m) (hrange : 1 < ∑ j ∈ Finset.range m, (ρ ^ (j + 2))⁻¹) : GeometricBlockSurplus ρ m

theorem Erdos346.exists_geometricBlockSurplus_of_lt_goldenRatio {ρ : ℝ} (hρ1 : 1 < ρ) (hρφ : ρ < Real.goldenRatio) : ∃ (m : ℕ), 0 < m ∧ GeometricBlockSurplus ρ m

theorem Erdos346.two_mul_of_quotient_succ_lt_two {a : ℕ → ℕ} {n : ℕ} (hpos : ∀ (n : ℕ), 0 < a n) (h : quotient a (n + 1) < 2) : a (n + 2) < 2 * a (n + 1)

theorem Erdos346.evt_two_mul_of_eventual_quotient_lt_of_lt_two {a : ℕ → ℕ} {ρ : ℝ} (hpos : ∀ (n : ℕ), 0 < a n) (hρ2 : ρ < 2) (hupper : ∀ᶠ (n : ℕ) in Filter.atTop, quotient a n < ρ) : ∀ᶠ (n : ℕ) in Filter.atTop, a (n + 2) < 2 * a (n + 1)

theorem Erdos346.two_step_sum_gt_of_quotient_lt_rho {a : ℕ → ℕ} {ρ : ℝ} {n : ℕ} (hpos : ∀ (n : ℕ), 0 < a n) (hρ1 : 1 < ρ) (hρφ : ρ < Real.goldenRatio) (hn : quotient a n < ρ) (hn1 : quotient a (n + 1) < ρ) : a (n + 2) < a n + a (n + 1)

theorem Erdos346.evt_two_step_sum_gt_of_eventual_quotient_lt_rho {a : ℕ → ℕ} {ρ : ℝ} (hpos : ∀ (n : ℕ), 0 < a n) (hρ1 : 1 < ρ) (hρφ : ρ < Real.goldenRatio) (hupper : ∀ᶠ (n : ℕ) in Filter.atTop, quotient a n < ρ) : ∀ᶠ (n : ℕ) in Filter.atTop, a (n + 2) < a n + a (n + 1)

theorem Erdos346.evt_two_step_le_of_eventual_quotient_lt_rho {a : ℕ → ℕ} {ρ : ℝ} (hpos : ∀ (n : ℕ), 0 < a n) (hρ1 : 1 < ρ) (hρφ : ρ < Real.goldenRatio) (hupper : ∀ᶠ (n : ℕ) in Filter.atTop, quotient a n < ρ) : ∀ᶠ (n : ℕ) in Filter.atTop, a (n + 2) ≤ a n + a (n + 1)

theorem Erdos346.const_add_two_step_le_of_quotient_lt_rho_of_const_le {a : ℕ → ℕ} {ρ : ℝ} {C n : ℕ} (hpos : ∀ (n : ℕ), 0 < a n) (hρ1 : 1 < ρ) (hC : ↑C ≤ (1 - ρ * (ρ - 1)) * ↑(a n)) (hn : quotient a n < ρ) (hn1 : quotient a (n + 1) < ρ) : C + a (n + 2) ≤ a n + a (n + 1)

theorem Erdos346.evt_const_add_two_step_le_of_eventual_quotient_lt_rho {a : ℕ → ℕ} {ρ : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hρ1 : 1 < ρ) (hρφ : ρ < Real.goldenRatio) (hupper : ∀ᶠ (n : ℕ) in Filter.atTop, quotient a n < ρ) (C : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, C + a (n + 2) ≤ a n + a (n + 1)

theorem Erdos346.term_le_pow_mul_of_quotient_lt_on_range {a : ℕ → ℕ} {ρ : ℝ} {s k : ℕ} (hpos : ∀ (n : ℕ), 0 < a n) (hρpos : 0 < ρ) (hquot : ∀ j < k, quotient a (s + j) < ρ) : ↑(a (s + k)) ≤ ρ ^ k * ↑(a s)

theorem Erdos346.term_div_pow_le_of_quotient_lt_between {a : ℕ → ℕ} {ρ : ℝ} {i n : ℕ} (hpos : ∀ (n : ℕ), 0 < a n) (hρpos : 0 < ρ) (hin : i ≤ n + 1) (hquot : ∀ (t : ℕ), i ≤ t → t < n + 1 → quotient a t < ρ) : ↑(a (n + 1)) / ρ ^ (n + 1 - i) ≤ ↑(a i)

theorem Erdos346.fixedLengthBlockSurplusFrom_of_geometricBlockSurplus_of_eventual_quotient_lt {a : ℕ → ℕ} {ρ : ℝ} {m : ℕ} (hpos : ∀ (n : ℕ), 0 < a n) (hρpos : 0 < ρ) (hgeom : GeometricBlockSurplus ρ m) (hupper : ∀ᶠ (n : ℕ) in Filter.atTop, quotient a n < ρ) : ∃ (N : ℕ), FixedLengthBlockSurplusFrom a m N

def Erdos346.propagatedGap (a : ℕ → ℕ) (N : ℕ) : ℕ → ℕ

A moving hole in a tail. Starting from a N - 1, it is propagated two steps at a time by adding the intervening odd-indexed tail term.

Equations

• Erdos346.propagatedGap a N 0 = a N - 1
• Erdos346.propagatedGap a N k.succ = Erdos346.propagatedGap a N k + a (N + 2 * k + 1)

theorem Erdos346.finset_sum_le_Icc_sum_of_subset_Ici_of_forall_le {a : ℕ → ℕ} {F : Finset ℕ} {N m : ℕ} (hFN : ↑F ⊆ Set.Ici N) (hm : ∀ i ∈ F, i ≤ m) : ∑ i ∈ F, a i ≤ ∑ i ∈ Finset.Icc N m, a i

theorem Erdos346.propagatedGap_ge_self {a : ℕ → ℕ} {N : ℕ} (hpos : ∀ (n : ℕ), 0 < a n) (k : ℕ) : k ≤ propagatedGap a N k

theorem Erdos346.prefixSubsetSums_mono_index {a : ℕ → ℕ} {I : Set ℕ} {m n : ℕ} (hmn : m ≤ n) : prefixSubsetSums a I m ⊆ prefixSubsetSums a I n

theorem Erdos346.prefixSubsetSums_subset {a : ℕ → ℕ} {I : Set ℕ} {n : ℕ} : prefixSubsetSums a I n ⊆ subsetSums a I

theorem Erdos346.prefixSubsetSums_succ_iff {a : ℕ → ℕ} {I : Set ℕ} {M t : ℕ} : t ∈ prefixSubsetSums a I (M + 1) ↔ t ∈ prefixSubsetSums a I M ∨ M + 1 ∈ I ∧ a (M + 1) ≤ t ∧ t - a (M + 1) ∈ prefixSubsetSums a I M

theorem Erdos346.CoversInterval.mono_index {a : ℕ → ℕ} {I : Set ℕ} {m n H T : ℕ} (hcover : CoversInterval a I m H T) (hmn : m ≤ n) : CoversInterval a I n H T

theorem Erdos346.CoversInterval.mono_set {a : ℕ → ℕ} {I J : Set ℕ} {n H T : ℕ} (hcover : CoversInterval a I n H T) (hIJ : I ∩ Set.Iic n ⊆ J ∩ Set.Iic n) : CoversInterval a J n H T

theorem Erdos346.cover_compl_of_cover_univ_of_avoid {a : ℕ → ℕ} {D : Set ℕ} {n H T : ℕ} (hcover : CoversInterval a Set.univ n H T) (havoid : Set.Iic n ⊆ Dᶜ) : CoversInterval a Dᶜ n H T

theorem Erdos346.prefixSubsetSum_le_fullPrefixSum {a : ℕ → ℕ} {I : Set ℕ} {n t : ℕ} (ht : t ∈ prefixSubsetSums a I n) : t ≤ fullPrefixSum a n

theorem Erdos346.wide_prefix_cover_forces_zero_left {a : ℕ → ℕ} {M H T : ℕ} (hcover : CoversInterval a Set.univ M H T) (hHT : H ≤ T) (hwide : fullPrefixSum a M + H ≤ T) : H = 0

theorem Erdos346.exists_prefix_cover_univ_of_complete {a : ℕ → ℕ} (hcomplete : IsCompleteOn a Set.univ) : ∃ (H : ℕ), ∀ (T : ℕ), H ≤ T → ∃ (M : ℕ), CoversInterval a Set.univ M H T

theorem Erdos346.exists_prefix_cover_of_complete {a : ℕ → ℕ} {I : Set ℕ} (hcomplete : IsCompleteOn a I) : ∃ (H : ℕ), ∀ (T : ℕ), H ≤ T → ∃ (M : ℕ), CoversInterval a I M H T

theorem Erdos346.finite_subset_iic {F : Set ℕ} (hF : F.Finite) : ∃ (M : ℕ), F ⊆ Set.Iic M

theorem Erdos346.exists_prefix_cover_compl_of_finiteDeletionComplete {a : ℕ → ℕ} {F : Set ℕ} (hfinite : FiniteDeletionComplete a) (hF : F.Finite) : ∃ (H : ℕ), ∀ (T : ℕ), H ≤ T → ∃ (M : ℕ), F ⊆ Set.Iic M ∧ CoversInterval a Fᶜ M H T

theorem Erdos346.finset_term_le_sum_of_mem {a : ℕ → ℕ} {F : Finset ℕ} {i : ℕ} (hi : i ∈ F) : a i ≤ ∑ j ∈ F, a j

theorem Erdos346.subset_sum_eq_lt_next_uses_only_prefix {a : ℕ → ℕ} {F : Finset ℕ} {n t : ℕ} (hmono : StrictMono a) (hsum : ∑ i ∈ F, a i = t) (hlt : t < a (n + 1)) : ↑F ⊆ Set.Iic n

theorem Erdos346.subsetSums_lt_next_subset_prefixSubsetSums {a : ℕ → ℕ} {I : Set ℕ} {n t : ℕ} (hmono : StrictMono a) (ht : t ∈ subsetSums a I) (hlt : t < a (n + 1)) : t ∈ prefixSubsetSums a I n

theorem Erdos346.complete_prefix_cover_two_mul_sub_one {a : ℕ → ℕ} {H q : ℕ} (hmono : StrictMono a) (hprev_pos : 0 < a (q + 1)) (hcompleteH : ∀ (t : ℕ), H ≤ t → t ∈ subsetSums a Set.univ) (hnext : a (q + 1) + H ≤ a (q + 2)) : CoversInterval a Set.univ (q + 1) H (2 * a (q + 1) - 1)

theorem Erdos346.exists_initial_global_budget_seed_of_complete_of_evtQuotientLtGold {a : ℕ → ℕ} {ρ : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hgap : HasUniformRatioGap a) (hcomplete : IsCompleteOn a Set.univ) (hρ1 : 1 < ρ) (hρφ : ρ < Real.goldenRatio) (hupper : ∀ᶠ (n : ℕ) in Filter.atTop, quotient a n < ρ) : ∃ (H : ℕ) (q : ℕ), H ≤ 2 * a (q + 1) - 1 ∧ CoversInterval a Set.univ (q + 1) H (2 * a (q + 1) - 1) ∧ a (q + 2) ≤ 2 * a (q + 1) - H

theorem Erdos346.exists_initial_global_budget_seed_after_of_complete_of_evtQuotientLtGold {a : ℕ → ℕ} {ρ : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hgap : HasUniformRatioGap a) (hcomplete : IsCompleteOn a Set.univ) (hρ1 : 1 < ρ) (hρφ : ρ < Real.goldenRatio) (hupper : ∀ᶠ (n : ℕ) in Filter.atTop, quotient a n < ρ) (B : ℕ) : ∃ (H : ℕ) (q : ℕ), B ≤ q ∧ H ≤ 2 * a (q + 1) - 1 ∧ CoversInterval a Set.univ (q + 1) H (2 * a (q + 1) - 1) ∧ a (q + 2) ≤ 2 * a (q + 1) - H

theorem Erdos346.not_subsetSums_of_not_prefixSubsetSums_of_lt_next {a : ℕ → ℕ} {I : Set ℕ} {n t : ℕ} (hmono : StrictMono a) (hmiss : t ∉ prefixSubsetSums a I n) (hlt : t < a (n + 1)) : t ∉ subsetSums a I

theorem Erdos346.subsetSums_avoiding_finite_singleton_lt_next_next_subset_prefix {a : ℕ → ℕ} {F : Set ℕ} {M t : ℕ} (hmono : StrictMono a) (ht : t ∈ subsetSums a (F ∪ {M + 1})ᶜ) (hlt : t < a (M + 2)) : t ∈ prefixSubsetSums a Fᶜ M

theorem Erdos346.prefixSubsetSums_subset_subsetSums_avoiding_finite_singleton {a : ℕ → ℕ} {F : Set ℕ} {M t : ℕ} (ht : t ∈ prefixSubsetSums a Fᶜ M) : t ∈ subsetSums a (F ∪ {M + 1})ᶜ

theorem Erdos346.subsetSums_avoiding_finite_singleton_lt_next_next_iff_prefix {a : ℕ → ℕ} {F : Set ℕ} {M t : ℕ} (hmono : StrictMono a) (hlt : t < a (M + 2)) : t ∈ subsetSums a (F ∪ {M + 1})ᶜ ↔ t ∈ prefixSubsetSums a Fᶜ M

theorem Erdos346.not_prefixSubsetSums_of_not_subsetSums_avoiding_finite_singleton {a : ℕ → ℕ} {F : Set ℕ} {M t : ℕ} (hmiss : t ∉ subsetSums a (F ∪ {M + 1})ᶜ) : t ∉ prefixSubsetSums a Fᶜ M

theorem Erdos346.not_subsetSums_avoiding_finite_singleton_of_prefix_hole {a : ℕ → ℕ} {F : Set ℕ} {M t : ℕ} (hmono : StrictMono a) (hmiss : t ∉ prefixSubsetSums a Fᶜ M) (hlt : t < a (M + 2)) : t ∉ subsetSums a (F ∪ {M + 1})ᶜ

theorem Erdos346.exists_finite_singleton_hole_of_not_seed_margins {a : ℕ → ℕ} {F : Set ℕ} {M : ℕ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hnext : a (M + 1) ≤ a (M + 2)) (hpair : a (M + 3) ≤ a (M + 1) + a (M + 2)) (hnot : ¬(leastPrefixCoverThreshold a Fᶜ M (a (M + 2) - 1) + a (M + 1) ≤ a (M + 2) ∧ leastPrefixCoverThreshold a Fᶜ M (a (M + 2) - 1) + a (M + 3) ≤ a (M + 1) + a (M + 2))) : ∃ t ≤ a (M + 2) - 1, t < a (M + 2) ∧ t ∉ subsetSums a (F ∪ {M + 1})ᶜ ∧ (nextSeedMargin a M ≤ t ∨ pairSeedMargin a M ≤ t)

theorem Erdos346.finite_singleton_hole_mem_base_compl_forces_shifted_prefix {a : ℕ → ℕ} {F : Set ℕ} {H M t : ℕ} (hmono : StrictMono a) (hcompleteF : ∀ (u : ℕ), H ≤ u → u ∈ subsetSums a Fᶜ) (hHt : H ≤ t) (hmiss : t ∉ subsetSums a (F ∪ {M + 1})ᶜ) (hlt : t < a (M + 2)) : a (M + 1) ≤ t ∧ t - a (M + 1) ∈ prefixSubsetSums a Fᶜ M

theorem Erdos346.finite_singleton_hole_lt_next_forces_shifted_prefix {a : ℕ → ℕ} {F : Set ℕ} {H M R t : ℕ} (hmono : StrictMono a) (hcompleteF : ∀ (u : ℕ), H ≤ u → u ∈ subsetSums a Fᶜ) (hHt : H ≤ t) (hmiss : t ∉ subsetSums a (F ∪ {M + 1})ᶜ) (hlt : t < a (R + 1)) : a (M + 1) ≤ t ∧ t - a (M + 1) ∈ prefixSubsetSums a (F ∪ {M + 1})ᶜ R

theorem Erdos346.finite_singleton_hole_lt_next3_forces_shifted_prefix {a : ℕ → ℕ} {F : Set ℕ} {H M t : ℕ} (hmono : StrictMono a) (hcompleteF : ∀ (u : ℕ), H ≤ u → u ∈ subsetSums a Fᶜ) (hHt : H ≤ t) (hmiss : t ∉ subsetSums a (F ∪ {M + 1})ᶜ) (hlt : t < a (M + 3)) : a (M + 1) ≤ t ∧ t - a (M + 1) ∈ prefixSubsetSums a (F ∪ {M + 1})ᶜ (M + 2)

theorem Erdos346.finite_singleton_hole_ge_base_threshold_forces_shifted_prefix_of_finiteDeletionComplete {a : ℕ → ℕ} {F : Set ℕ} (hmono : StrictMono a) (hfinite : FiniteDeletionComplete a) (hFfinite : F.Finite) : ∃ (H : ℕ), ∀ (M t : ℕ), H ≤ t → t ∉ subsetSums a (F ∪ {M + 1})ᶜ → t < a (M + 2) → a (M + 1) ≤ t ∧ t - a (M + 1) ∈ prefixSubsetSums a Fᶜ M

theorem Erdos346.shifted_prefix_source_lt_nextSeedMargin {a : ℕ → ℕ} {M t : ℕ} (ha : a (M + 1) ≤ t) (hlt : t < a (M + 2)) : t - a (M + 1) < nextSeedMargin a M

theorem Erdos346.shifted_prefix_hole_gives_prefix_shift_gap {a : ℕ → ℕ} {F : Set ℕ} {M t : ℕ} (ha : a (M + 1) ≤ t) (hsource : t - a (M + 1) ∈ prefixSubsetSums a Fᶜ M) (hmiss : t ∉ subsetSums a (F ∪ {M + 1})ᶜ) (hlt : t < a (M + 2)) : ∃ s ∈ prefixSubsetSums a Fᶜ M, s < nextSeedMargin a M ∧ a (M + 1) + s < a (M + 2) ∧ a (M + 1) + s ∉ prefixSubsetSums a Fᶜ M

theorem Erdos346.pred_finSingletonCompleteThreshold_small_forces_prefix_shift_gap {a : ℕ → ℕ} (hfinite : FiniteDeletionComplete a) {F : Set ℕ} (hF : F.Finite) {H M : ℕ} (hmono : StrictMono a) (hcompleteF : ∀ (u : ℕ), H ≤ u → u ∈ subsetSums a Fᶜ) (hHprev : H ≤ a (M + 1)) (hprevlt : a (M + 1) < finSingletonCompleteThreshold a hfinite hF M) (hthreshold_le : finSingletonCompleteThreshold a hfinite hF M ≤ a (M + 2)) : ∃ s ∈ prefixSubsetSums a Fᶜ M, s < nextSeedMargin a M ∧ a (M + 1) + s < a (M + 2) ∧ a (M + 1) + s ∉ prefixSubsetSums a Fᶜ M

theorem Erdos346.pred_finSingletonCompleteThreshold_next_forces_shifted_prefix {a : ℕ → ℕ} (hfinite : FiniteDeletionComplete a) {F : Set ℕ} (hF : F.Finite) {H M R : ℕ} (hmono : StrictMono a) (hcompleteF : ∀ (u : ℕ), H ≤ u → u ∈ subsetSums a Fᶜ) (hM1R : M + 1 < R) (hHR : H ≤ a R) (hRlt : a R < finSingletonCompleteThreshold a hfinite hF M) (hthreshold_le : finSingletonCompleteThreshold a hfinite hF M ≤ a (R + 1)) : ∃ (t : ℕ) (s : ℕ), t = finSingletonCompleteThreshold a hfinite hF M - 1 ∧ a R ≤ t ∧ t < a (R + 1) ∧ t ∉ subsetSums a (F ∪ {M + 1})ᶜ ∧ s = t - a (M + 1) ∧ s ∈ prefixSubsetSums a (F ∪ {M + 1})ᶜ R

theorem Erdos346.pred_finSingletonCompleteThreshold_next3_forces_shifted_prefix {a : ℕ → ℕ} (hfinite : FiniteDeletionComplete a) {F : Set ℕ} (hF : F.Finite) {H M : ℕ} (hmono : StrictMono a) (hcompleteF : ∀ (u : ℕ), H ≤ u → u ∈ subsetSums a Fᶜ) (hHnext : H ≤ a (M + 2)) (hnextlt : a (M + 2) < finSingletonCompleteThreshold a hfinite hF M) (hthreshold_le : finSingletonCompleteThreshold a hfinite hF M ≤ a (M + 3)) : ∃ (t : ℕ) (s : ℕ), t = finSingletonCompleteThreshold a hfinite hF M - 1 ∧ a (M + 2) ≤ t ∧ t < a (M + 3) ∧ t ∉ subsetSums a (F ∪ {M + 1})ᶜ ∧ s = t - a (M + 1) ∧ s ∈ prefixSubsetSums a (F ∪ {M + 1})ᶜ (M + 2)

theorem Erdos346.first_prefix_cover_of_succ_cover_and_shiftClosed {a : ℕ → ℕ} {F : Set ℕ} {M : ℕ} (hpos : 0 < a (M + 2)) (hcoverSucc : CoversInterval a Fᶜ (M + 1) (nextSeedMargin a M) (a (M + 2) - 1)) (hclosed : FirstWindowShiftClosed a F M) : CoversInterval a Fᶜ M (nextSeedMargin a M) (a (M + 2) - 1)

theorem Erdos346.firstWindowShiftClosed_of_first_prefix_cover_of_nextSeedMargin_le_prev {a : ℕ → ℕ} {F : Set ℕ} {M : ℕ} (hnext_le : nextSeedMargin a M ≤ a (M + 1)) (hcover : CoversInterval a Fᶜ M (nextSeedMargin a M) (a (M + 2) - 1)) : FirstWindowShiftClosed a F M

theorem Erdos346.firstWindowShiftClosed_of_finSingletonCompleteBelowPrev {a : ℕ → ℕ} {F : Set ℕ} {M : ℕ} (hmono : StrictMono a) (hbelow : FinSingletonCompleteBelowPrev a F M) : FirstWindowShiftClosed a F M

theorem Erdos346.prefix_shift_gap_forces_nextSeedMargin_lt_least {a : ℕ → ℕ} {F : Set ℕ} {M s : ℕ} (hnext_le : nextSeedMargin a M ≤ a (M + 1)) (hgap : s ∈ prefixSubsetSums a Fᶜ M ∧ s < nextSeedMargin a M ∧ a (M + 1) + s < a (M + 2) ∧ a (M + 1) + s ∉ prefixSubsetSums a Fᶜ M) : nextSeedMargin a M < leastPrefixCoverThreshold a Fᶜ M (a (M + 2) - 1)

theorem Erdos346.complete_forces_next_le_fullPrefixSum_add_one {a : ℕ → ℕ} {H n : ℕ} (hmono : StrictMono a) (hcomplete : ∀ (t : ℕ), H ≤ t → t ∈ subsetSums a Set.univ) (hH : H ≤ fullPrefixSum a n + 1) : a (n + 1) ≤ fullPrefixSum a n + 1

theorem Erdos346.complete_prefix_cover_of_lt_next {a : ℕ → ℕ} {H n T : ℕ} (hmono : StrictMono a) (hcomplete : ∀ (t : ℕ), H ≤ t → t ∈ subsetSums a Set.univ) (hTlt : T < a (n + 1)) : CoversInterval a Set.univ n H T

theorem Erdos346.complete_prefix_cover_of_lt_next_on {a : ℕ → ℕ} {I : Set ℕ} {H n T : ℕ} (hmono : StrictMono a) (hcomplete : ∀ (t : ℕ), H ≤ t → t ∈ subsetSums a I) (hTlt : T < a (n + 1)) : CoversInterval a I n H T

theorem Erdos346.exists_prefix_cover_compl_lt_next_of_finiteDeletionComplete {a : ℕ → ℕ} {F : Set ℕ} (hmono : StrictMono a) (hfinite : FiniteDeletionComplete a) (hF : F.Finite) : ∃ (H : ℕ), ∀ (n T : ℕ), T < a (n + 1) → CoversInterval a Fᶜ n H T

theorem Erdos346.keptPrefixSum_add_deletedPrefixSum {a : ℕ → ℕ} {D : Set ℕ} {n : ℕ} : keptPrefixSum a D n + deletedPrefixSum a D n = fullPrefixSum a n

theorem Erdos346.keptPrefixSum_eq_fullPrefixSum_sub_deletedPrefixSum {a : ℕ → ℕ} {D : Set ℕ} {n : ℕ} : keptPrefixSum a D n = fullPrefixSum a n - deletedPrefixSum a D n

theorem Erdos346.deletedPrefixSum_eq_zero_of_avoid {a : ℕ → ℕ} {D : Set ℕ} {n : ℕ} (havoid : Set.Iic n ⊆ Dᶜ) : deletedPrefixSum a D n = 0

theorem Erdos346.deletedPrefixSum_mono_set {a : ℕ → ℕ} {D E : Set ℕ} {n : ℕ} (hDE : D ∩ Set.Iic n ⊆ E ∩ Set.Iic n) : deletedPrefixSum a D n ≤ deletedPrefixSum a E n

theorem Erdos346.finset_sum_union_le_add {a : ℕ → ℕ} {s t : Finset ℕ} : ∑ i ∈ s ∪ t, a i ≤ ∑ i ∈ s, a i + ∑ i ∈ t, a i

theorem Erdos346.fullPrefixSum_succ {a : ℕ → ℕ} {n : ℕ} : fullPrefixSum a (n + 1) = fullPrefixSum a n + a (n + 1)

theorem Erdos346.fullPrefixSum_mono {a : ℕ → ℕ} : Monotone (fullPrefixSum a)

theorem Erdos346.succ_le_fullPrefixSum_of_pos {a : ℕ → ℕ} (hpos : ∀ (n : ℕ), 0 < a n) (n : ℕ) : n + 1 ≤ fullPrefixSum a n

theorem Erdos346.evt_next_le_fullPrefixSum_add_one_of_complete {a : ℕ → ℕ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hcomplete : IsCompleteOn a Set.univ) : ∀ᶠ (n : ℕ) in Filter.atTop, a (n + 1) ≤ fullPrefixSum a n + 1

theorem Erdos346.next_add_fullPrefixSum_ge_add_next_of_evt_two_mul_aux {a : ℕ → ℕ} {N : ℕ} (hsmall : ∀ (n : ℕ), N ≤ n → a (n + 2) < 2 * a (n + 1)) (k : ℕ) : a (N + 1) + fullPrefixSum a (N + k) ≥ k + a (N + k + 1)

theorem Erdos346.evt_const_add_next_le_fullPrefixSum_of_evt_two_mul {a : ℕ → ℕ} (hsmall : ∀ᶠ (n : ℕ) in Filter.atTop, a (n + 2) < 2 * a (n + 1)) (C : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, C + a (n + 1) ≤ fullPrefixSum a n

theorem Erdos346.two_initial_add_fullPrefixSum_ge_add_pair_aux {a : ℕ → ℕ} {N : ℕ} (hsmall : ∀ (n : ℕ), N ≤ n → a (n + 2) < a n + a (n + 1)) (k : ℕ) : a N + a (N + 1) + fullPrefixSum a (N + k) ≥ k + (a (N + k) + a (N + k + 1))

theorem Erdos346.evt_const_add_pair_le_fullPrefixSum_of_evt_pair_gap {a : ℕ → ℕ} (hsmall : ∀ᶠ (n : ℕ) in Filter.atTop, a (n + 2) < a n + a (n + 1)) (C : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, C + a n + a (n + 1) ≤ fullPrefixSum a n

theorem Erdos346.evt_pair_prefix_surplus_of_evtQuotientLtGold {a : ℕ → ℕ} {ρ : ℝ} (hpos : ∀ (n : ℕ), 0 < a n) (hρ1 : 1 < ρ) (hρφ : ρ < Real.goldenRatio) (hupper : ∀ᶠ (n : ℕ) in Filter.atTop, quotient a n < ρ) (C : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, C + a n + a (n + 1) ≤ fullPrefixSum a n

theorem Erdos346.evt_next_next_seed_tail_conditions_of_evtQuotientLtGold {a : ℕ → ℕ} {ρ : ℝ} (hpos : ∀ (n : ℕ), 0 < a n) (hρ1 : 1 < ρ) (hρφ : ρ < Real.goldenRatio) (hupper : ∀ᶠ (n : ℕ) in Filter.atTop, quotient a n < ρ) : ∀ᶠ (M : ℕ) in Filter.atTop, a (M + 2) + a (M + 3) ≤ fullPrefixSum a (M + 2) ∧ ∀ (n : ℕ), M + 2 ≤ n → a (n + 2) ≤ a n + a (n + 1)

theorem Erdos346.evt_next_next_seed_numeric_conditions {a : ℕ → ℕ} {ρ : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hratioGap : HasUniformRatioGap a) (hρ1 : 1 < ρ) (hρφ : ρ < Real.goldenRatio) (hupper : ∀ᶠ (n : ℕ) in Filter.atTop, quotient a n < ρ) (H : ℕ) : ∀ᶠ (M : ℕ) in Filter.atTop, H + a (M + 1) ≤ a (M + 2) ∧ a (M + 2) + a (M + 3) ≤ fullPrefixSum a (M + 2) ∧ ∀ (n : ℕ), M + 2 ≤ n → a (n + 2) ≤ a n + a (n + 1)

theorem Erdos346.evt_next_next_seed_numeric_conditions_with_margin {a : ℕ → ℕ} {ρ : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hratioGap : HasUniformRatioGap a) (hρ1 : 1 < ρ) (hρφ : ρ < Real.goldenRatio) (hupper : ∀ᶠ (n : ℕ) in Filter.atTop, quotient a n < ρ) (H : ℕ) : ∀ᶠ (M : ℕ) in Filter.atTop, H + a (M + 1) ≤ a (M + 2) ∧ a (M + 2) + a (M + 3) ≤ fullPrefixSum a (M + 2) ∧ H + a (M + 3) ≤ a (M + 1) + a (M + 2) ∧ ∀ (n : ℕ), M + 2 ≤ n → a (n + 2) ≤ a n + a (n + 1)

theorem Erdos346.range_infinite_of_strictMono_nat {b : ℕ → ℕ} (hb : StrictMono b) : (Set.range b).Infinite

theorem Erdos346.strictMono_nat_add_le {b : ℕ → ℕ} (hb : StrictMono b) (k : ℕ) : b 0 + k ≤ b k

theorem Erdos346.strictMono_of_gap_one {b : ℕ → ℕ} (hgap : ∀ (k : ℕ), b k + 1 < b (k + 1)) : StrictMono b

theorem Erdos346.deletedPrefixSum_range_le_indexedDeletedSum_of_lt {a b : ℕ → ℕ} {n k : ℕ} (hb : StrictMono b) (hnk : n < b k) : deletedPrefixSum a (Set.range b) n ≤ indexedDeletedSum a b k

theorem Erdos346.deletedPrefixSum_range_le_indexedDeletedSum_between {a b : ℕ → ℕ} {n k : ℕ} (hb : StrictMono b) (_hleft : b k ≤ n) (hright : n < b (k + 1)) : deletedPrefixSum a (Set.range b) n ≤ indexedDeletedSum a b (k + 1)

theorem Erdos346.deletedPrefixSum_initialTail_le_initial_add_range {a b : ℕ → ℕ} {F : Set ℕ} {M n : ℕ} (hF : F ⊆ Set.Iic M) : deletedPrefixSum a (initialTailDeletionSet F b) n ≤ deletedPrefixSum a (initialTailDeletionSet F b) M + deletedPrefixSum a (Set.range b) n

theorem Erdos346.deletedPrefixSum_initialTail_le_initial_add_indexedDeletedSum_of_lt {a b : ℕ → ℕ} {F : Set ℕ} {M n k : ℕ} (hF : F ⊆ Set.Iic M) (hb : StrictMono b) (hnk : n < b k) : deletedPrefixSum a (initialTailDeletionSet F b) n ≤ deletedPrefixSum a (initialTailDeletionSet F b) M + indexedDeletedSum a b k

theorem Erdos346.deletedPrefixSum_initialTail_le_initial_of_lt_first {a b : ℕ → ℕ} {F : Set ℕ} {M n : ℕ} (hF : F ⊆ Set.Iic M) (hb : StrictMono b) (hn : n < b 0) : deletedPrefixSum a (initialTailDeletionSet F b) n ≤ deletedPrefixSum a (initialTailDeletionSet F b) M

theorem Erdos346.succ_range_subset_compl_of_gap {b : ℕ → ℕ} (hgap : ∀ (k : ℕ), b k + 1 < b (k + 1)) : (Set.range fun (k : ℕ) => b k + 1) ⊆ (Set.range b)ᶜ

theorem Erdos346.range_succ_infinite_of_gap {b : ℕ → ℕ} (hgap : ∀ (k : ℕ), b k + 1 < b (k + 1)) : (Set.range fun (k : ℕ) => b k + 1).Infinite

theorem Erdos346.coinfinite_range_of_gap {b : ℕ → ℕ} (hgap : ∀ (k : ℕ), b k + 1 < b (k + 1)) : (Set.range b)ᶜ.Infinite

theorem Erdos346.initialTailDeletionSet_infinite {F : Set ℕ} {b : ℕ → ℕ} (hgap : ∀ (k : ℕ), b k + 1 < b (k + 1)) : (initialTailDeletionSet F b).Infinite

theorem Erdos346.gap_points_subset_compl_initialTailDeletionSet {F : Set ℕ} {b : ℕ → ℕ} {M : ℕ} (hF : F ⊆ Set.Iic M) (hgap : ∀ (k : ℕ), b k + 1 < b (k + 1)) (havoid : ∀ (k : ℕ), M < b k) : (Set.range fun (k : ℕ) => b k + 1) ⊆ (initialTailDeletionSet F b)ᶜ

theorem Erdos346.initialTailDeletionSet_coinfinite {F : Set ℕ} {b : ℕ → ℕ} {M : ℕ} (hF : F ⊆ Set.Iic M) (hgap : ∀ (k : ℕ), b k + 1 < b (k + 1)) (havoid : ∀ (k : ℕ), M < b k) : (initialTailDeletionSet F b)ᶜ.Infinite

theorem Erdos346.cover_initialTailDeletionSet_of_cover_initial {a : ℕ → ℕ} {F : Set ℕ} {b : ℕ → ℕ} {H M T : ℕ} (hcover : CoversInterval a Fᶜ M H T) (havoid : ∀ (k : ℕ), M < b k) : CoversInterval a (initialTailDeletionSet F b)ᶜ M H T

theorem Erdos346.strictMono_block_left {b e : ℕ → ℕ} (hnonempty : ∀ (k : ℕ), b k ≤ e k) (hgap : ∀ (k : ℕ), e k + 1 < b (k + 1)) : StrictMono b

theorem Erdos346.strictMono_block_right {b e : ℕ → ℕ} (hnonempty : ∀ (k : ℕ), b k ≤ e k) (hgap : ∀ (k : ℕ), e k + 1 < b (k + 1)) : StrictMono e

theorem Erdos346.blockDeletionSet_infinite {b e : ℕ → ℕ} (hnonempty : ∀ (k : ℕ), b k ≤ e k) (hgap : ∀ (k : ℕ), e k + 1 < b (k + 1)) : (blockDeletionSet b e).Infinite

theorem Erdos346.block_gap_points_subset_compl {b e : ℕ → ℕ} (hnonempty : ∀ (k : ℕ), b k ≤ e k) (hgap : ∀ (k : ℕ), e k + 1 < b (k + 1)) : (Set.range fun (k : ℕ) => e k + 1) ⊆ (blockDeletionSet b e)ᶜ

theorem Erdos346.block_gap_points_infinite {b e : ℕ → ℕ} (hnonempty : ∀ (k : ℕ), b k ≤ e k) (hgap : ∀ (k : ℕ), e k + 1 < b (k + 1)) : (Set.range fun (k : ℕ) => e k + 1).Infinite

theorem Erdos346.blockDeletionSet_coinfinite {b e : ℕ → ℕ} (hnonempty : ∀ (k : ℕ), b k ≤ e k) (hgap : ∀ (k : ℕ), e k + 1 < b (k + 1)) : (blockDeletionSet b e)ᶜ.Infinite

theorem Erdos346.keptPrefixSum_succ_of_mem {a : ℕ → ℕ} {D : Set ℕ} {n : ℕ} (hmem : n + 1 ∈ D) : keptPrefixSum a D (n + 1) = keptPrefixSum a D n

theorem Erdos346.keptPrefixSum_succ_of_not_mem {a : ℕ → ℕ} {D : Set ℕ} {n : ℕ} (hmem : n + 1 ∉ D) : keptPrefixSum a D (n + 1) = keptPrefixSum a D n + a (n + 1)

theorem Erdos346.keptPrefixSum_mono {a : ℕ → ℕ} {D : Set ℕ} : Monotone (keptPrefixSum a D)

theorem Erdos346.keptPrefixSum_add_term_le_of_lt_of_not_mem {a : ℕ → ℕ} {D : Set ℕ} {n m : ℕ} (hnm : n < m) (hm : m ∉ D) : keptPrefixSum a D n + a m ≤ keptPrefixSum a D m

theorem Erdos346.brown_tail_budget_nonempty_of_initial {a : ℕ → ℕ} {D : Set ℕ} {H M T n : ℕ} (hMn : M ≤ n) (hnonempty : H ≤ T) : H ≤ T + (keptPrefixSum a D n - keptPrefixSum a D M)

theorem Erdos346.brown_tail_budget_propagates_of_two_mul {a : ℕ → ℕ} {D : Set ℕ} {H M T n : ℕ} (hMn : M ≤ n) (hnonempty : H ≤ T + (keptPrefixSum a D n - keptPrefixSum a D M)) (hkeep : n + 1 ∉ D) (hcurrent : a (n + 1) ≤ T + (keptPrefixSum a D n - keptPrefixSum a D M) - H + 1) (htwo : a (n + 2) ≤ 2 * a (n + 1)) : a (n + 2) ≤ T + (keptPrefixSum a D (n + 1) - keptPrefixSum a D M) - H + 1

theorem Erdos346.brown_tail_budget_unchanged_of_deleted {a : ℕ → ℕ} {D : Set ℕ} {H M T n : ℕ} (hdel : n + 1 ∈ D) : T + (keptPrefixSum a D (n + 1) - keptPrefixSum a D M) - H + 1 = T + (keptPrefixSum a D n - keptPrefixSum a D M) - H + 1

theorem Erdos346.keptPrefixSum_add_sum_Icc_le_of_not_mem {a : ℕ → ℕ} {D : Set ℕ} {M lo hi : ℕ} (hMlo : M < lo) (hlohi : lo ≤ hi) (hkeep : ∀ (i : ℕ), lo ≤ i → i ≤ hi → i ∉ D) : keptPrefixSum a D M + ∑ i ∈ Finset.Icc lo hi, a i ≤ keptPrefixSum a D hi

theorem Erdos346.previousBlockSum_le_brown_tail_budget_of_not_mem {a : ℕ → ℕ} {D : Set ℕ} {H M T m n : ℕ} (hnonempty : H ≤ T) (hmpos : 0 < m) (hmn : m ≤ n) (hMlo : M < n - m) (hkeep : ∀ (i : ℕ), n - m ≤ i → i ≤ n - 1 → i ∉ D) : previousBlockSum a m n ≤ T + (keptPrefixSum a D (n - 1) - keptPrefixSum a D M) - H + 1

theorem Erdos346.brown_tail_budget_after_deleted_of_previousBlockSurplus {a : ℕ → ℕ} {D : Set ℕ} {H M T m d : ℕ} (hnonempty : H ≤ T) (hmpos : 0 < m) (hmd : m ≤ d) (hMlo : M < d - m) (hkeep : ∀ (i : ℕ), d - m ≤ i → i ≤ d - 1 → i ∉ D) (hdel : d ∈ D) (hsurplus : a (d + 1) < previousBlockSum a m d) : a (d + 1) ≤ T + (keptPrefixSum a D d - keptPrefixSum a D M) - H + 1

theorem Erdos346.periodicDeletion_step_of_fixedBlockSurplus {a : ℕ → ℕ} {H M T m : ℕ} (hmpos : 0 < m) (hnonempty : H ≤ T) (hbase : a (M + 1) ≤ T - H + 1) (htwo : ∀ (n : ℕ), M ≤ n → a (n + 2) ≤ 2 * a (n + 1)) (hsurplus : FixedLengthBlockSurplusFrom a m (M + m + 1)) (n : ℕ) : M ≤ n → n + 1 ∉ periodicDeletionSet (M + m + 1) (m + 2) → a (n + 1) ≤ T + (keptPrefixSum a (periodicDeletionSet (M + m + 1) (m + 2)) n - keptPrefixSum a (periodicDeletionSet (M + m + 1) (m + 2)) M) - H + 1

theorem Erdos346.exists_keptPrefixSum_ge_of_infinite_compl {a : ℕ → ℕ} {D : Set ℕ} (hpos : ∀ (n : ℕ), 0 < a n) (hinf : Dᶜ.Infinite) (k start : ℕ) : ∃ (n : ℕ), start ≤ n ∧ k ≤ keptPrefixSum a D n

theorem Erdos346.coversInterval_step_of_kept {a : ℕ → ℕ} {D : Set ℕ} {n H T : ℕ} (hcover : CoversInterval a Dᶜ n H T) (hHT : H ≤ T) (hkeep : n + 1 ∉ D) (hnext : a (n + 1) ≤ T - H + 1) : CoversInterval a Dᶜ (n + 1) H (T + a (n + 1))

structure Erdos346.BrownDeletionData (a : ℕ → ℕ) (D : Set ℕ) (H M : ℕ) : Prop

Brown-style data guaranteeing that deleting D preserves eventual completeness. The initial interval [H, keptPrefixSum M] is covered, every kept next term is small enough to extend the covered interval, and the kept prefix sums are unbounded.

• infinite : D.Infinite
• initial_nonempty : H ≤ keptPrefixSum a D M
• initial_cover : CoversInterval a Dᶜ M H (keptPrefixSum a D M)
• step (n : ℕ) : M ≤ n → n + 1 ∉ D → a (n + 1) ≤ keptPrefixSum a D n - H + 1
• unbounded (t : ℕ) : H ≤ t → ∃ (n : ℕ), M ≤ n ∧ t ≤ keptPrefixSum a D n

structure Erdos346.BrownStepData (a : ℕ → ℕ) (D : Set ℕ) (H M : ℕ) : Prop

Brown-style data before proving unboundedness of the kept prefix sums. Coinfiniteness of the kept set plus positivity implies the unbounded field of BrownDeletionData.

• infinite : D.Infinite
• coinfinite : Dᶜ.Infinite
• initial_nonempty : H ≤ keptPrefixSum a D M
• initial_cover : CoversInterval a Dᶜ M H (keptPrefixSum a D M)
• step (n : ℕ) : M ≤ n → n + 1 ∉ D → a (n + 1) ≤ keptPrefixSum a D n - H + 1

structure Erdos346.BrownSeedData (a : ℕ → ℕ) (D : Set ℕ) (H M C : ℕ) : Prop

Brown-style seed data with a fixed initial slack C. This is weaker than BrownStepData: the propagated covered interval is allowed to be [H, C + keptPrefixSum n] rather than [H, keptPrefixSum n].

• infinite : D.Infinite
• coinfinite : Dᶜ.Infinite
• initial_nonempty : H ≤ C + keptPrefixSum a D M
• initial_cover : CoversInterval a Dᶜ M H (C + keptPrefixSum a D M)
• step (n : ℕ) : M ≤ n → n + 1 ∉ D → a (n + 1) ≤ C + keptPrefixSum a D n - H + 1

structure Erdos346.BrownTailData (a : ℕ → ℕ) (D : Set ℕ) (H M T : ℕ) : Prop

Brown-style tail data with an explicit initial covered interval [H, T]. The construction only has to avoid deleting the initial prefix. Lean then transfers the Set.univ prefix cover to Dᶜ and propagates the covered upper endpoint by the kept-prefix growth after M.

• infinite : D.Infinite
• coinfinite : Dᶜ.Infinite
• avoids_initial : Set.Iic M ⊆ Dᶜ
• initial_nonempty : H ≤ T
• step (n : ℕ) : M ≤ n → n + 1 ∉ D → a (n + 1) ≤ T + (keptPrefixSum a D n - keptPrefixSum a D M) - H + 1

structure Erdos346.BrownTailCoverData (a : ℕ → ℕ) (D : Set ℕ) (H M T : ℕ) : Prop

Brown-style tail data when the initial cover has already been proved in the kept set. This removes the avoids_initial requirement and is useful for starting after a finite batch of deletions.

• infinite : D.Infinite
• coinfinite : Dᶜ.Infinite
• initial_nonempty : H ≤ T
• initial_cover : CoversInterval a Dᶜ M H T
• step (n : ℕ) : M ≤ n → n + 1 ∉ D → a (n + 1) ≤ T + (keptPrefixSum a D n - keptPrefixSum a D M) - H + 1

structure Erdos346.BrownBudgetData (a : ℕ → ℕ) (D : Set ℕ) (H M T : ℕ) : Prop

A purely numerical sufficient condition for BrownTailData. It controls the total deleted mass up to n, rather than mentioning the kept prefix sum in the step inequality.

• infinite : D.Infinite
• coinfinite : Dᶜ.Infinite
• avoids_initial : Set.Iic M ⊆ Dᶜ
• initial_nonempty : H ≤ T
• budget (n : ℕ) : M ≤ n → n + 1 ∉ D → deletedPrefixSum a D n + a (n + 1) ≤ T + (fullPrefixSum a n - fullPrefixSum a M) - H + 1

structure Erdos346.BrownBudgetCoverData (a : ℕ → ℕ) (D : Set ℕ) (H M T : ℕ) : Prop

Numerical sufficient condition for BrownTailCoverData. Unlike BrownBudgetData, this permits a finite batch of deletions at or before M, provided the initial cover is already in the kept set.

• infinite : D.Infinite
• coinfinite : Dᶜ.Infinite
• initial_nonempty : H ≤ T
• initial_cover : CoversInterval a Dᶜ M H T
• budget (n : ℕ) : M ≤ n → n + 1 ∉ D → deletedPrefixSum a D n + a (n + 1) + fullPrefixSum a M + H ≤ T + fullPrefixSum a n + deletedPrefixSum a D M + 1

structure Erdos346.IndexedBudgetInitialTailData (a : ℕ → ℕ) (F : Set ℕ) (b : ℕ → ℕ) (H M T : ℕ) : Prop

Indexed sparse-tail data after a finite initial deletion set F. The initial interval is covered in Fᶜ; the indexed tail starts after M, so the initial cover also lives in the full kept set (F ∪ range b)ᶜ.

• initial_subset : F ⊆ Set.Iic M
• gap (k : ℕ) : b k + 1 < b (k + 1)
• avoids_initial (k : ℕ) : M < b k
• initial_nonempty : H ≤ T
• initial_cover : CoversInterval a Fᶜ M H T
• budget (n : ℕ) : M ≤ n → n + 1 ∉ initialTailDeletionSet F b → deletedPrefixSum a (initialTailDeletionSet F b) n + a (n + 1) + fullPrefixSum a M + H ≤ T + fullPrefixSum a n + deletedPrefixSum a (initialTailDeletionSet F b) M + 1

structure Erdos346.IndexedPartialBudgetInitialTailData (a : ℕ → ℕ) (F : Set ℕ) (b : ℕ → ℕ) (H M T : ℕ) : Prop

Constructive version of IndexedBudgetInitialTailData. It only asks for the budget inequality before the first tail deletion and between consecutive tail deletions.

• initial_subset : F ⊆ Set.Iic M
• gap (k : ℕ) : b k + 1 < b (k + 1)
• avoids_initial (k : ℕ) : M < b k
• initial_nonempty : H ≤ T
• initial_cover : CoversInterval a Fᶜ M H T
• budget_before (n : ℕ) : M ≤ n → n < b 0 → n + 1 ∉ initialTailDeletionSet F b → deletedPrefixSum a (initialTailDeletionSet F b) n + a (n + 1) + fullPrefixSum a M + H ≤ T + fullPrefixSum a n + deletedPrefixSum a (initialTailDeletionSet F b) M + 1
• budget_between (k n : ℕ) : b k ≤ n → n < b (k + 1) → n + 1 ∉ initialTailDeletionSet F b → indexedDeletedSum a b (k + 1) + a (n + 1) + fullPrefixSum a M + H ≤ T + fullPrefixSum a n + 1

structure Erdos346.IndexedBudgetData (a b : ℕ → ℕ) (H M T : ℕ) : Prop

Indexed sparse-deletion budget data. Unlike the discarded block-control condition below, this asks for the Brown budget inequality itself at the kept extension steps.

• gap (k : ℕ) : b k + 1 < b (k + 1)
• avoids_initial (k : ℕ) : M < b k
• initial_nonempty : H ≤ T
• budget (n : ℕ) : M ≤ n → n + 1 ∉ Set.range b → deletedPrefixSum a (Set.range b) n + a (n + 1) ≤ T + (fullPrefixSum a n - fullPrefixSum a M) - H + 1

structure Erdos346.IndexedPartialBudgetData (a b : ℕ → ℕ) (H M T : ℕ) : Prop

A more constructive form of indexed sparse-deletion budget data. It only mentions the finite sum of the first k chosen deleted terms on the interval before the next deletion.

• gap (k : ℕ) : b k + 1 < b (k + 1)
• avoids_initial (k : ℕ) : M < b k
• initial_nonempty : H ≤ T
• budget_before (n : ℕ) : M ≤ n → n < b 0 → n + 1 ∉ Set.range b → a (n + 1) ≤ T + (fullPrefixSum a n - fullPrefixSum a M) - H + 1
• budget_between (k n : ℕ) : b k ≤ n → n < b (k + 1) → n + 1 ∉ Set.range b → indexedDeletedSum a b (k + 1) + a (n + 1) ≤ T + (fullPrefixSum a n - fullPrefixSum a M) - H + 1

structure Erdos346.IndexedPartialBudgetSeed (a : ℕ → ℕ) (H M T start : ℕ) : Prop

Finite seed data for the remaining recursive sparse-deletion construction. After start, the global pair-prefix surplus handles all later intervals; the finite interval before start is recorded explicitly.

• initial_cover : CoversInterval a Set.univ M H T
• initial_nonempty : H ≤ T
• avoids_initial : M < start
• surplus_from (n : ℕ) : start ≤ n → budgetBase a H M T + a n + a (n + 1) ≤ fullPrefixSum a n
• budget_before (n : ℕ) : M ≤ n → n < start → n + 1 ≠ start → a (n + 1) ≤ T + (fullPrefixSum a n - fullPrefixSum a M) - H + 1

structure Erdos346.IndexedInitialTailSeed (a : ℕ → ℕ) (F : Set ℕ) (H M T start : ℕ) : Prop

Seed data for the finite-initial-deletion route. The initial covered interval is already proved after deleting a finite set F ⊆ Iic M; after start, the usual pair-prefix surplus controls the recursive sparse tail.

• initial_subset : F ⊆ Set.Iic M
• initial_cover : CoversInterval a Fᶜ M H T
• initial_nonempty : H ≤ T
• avoids_initial : M < start
• surplus_from (n : ℕ) : start ≤ n → budgetBase a H M T + a n + a (n + 1) ≤ fullPrefixSum a n
• budget_before (n : ℕ) : M ≤ n → n < start → n + 1 ≠ start → a (n + 1) + fullPrefixSum a M + H ≤ T + fullPrefixSum a n + 1

theorem Erdos346.indexedPartialBudgetSeed_of_wide_prefix_cover {a : ℕ → ℕ} {H M T start : ℕ} (hcover : CoversInterval a Set.univ M H T) (hHT : H ≤ T) (hwide : fullPrefixSum a M + H ≤ T) (hMstart : M < start) (hnext : ∀ (n : ℕ), M ≤ n → a (n + 1) ≤ fullPrefixSum a n + 1) (hsurplus0 : ∀ (n : ℕ), start ≤ n → a n + a (n + 1) ≤ fullPrefixSum a n) : IndexedPartialBudgetSeed a H M T start

theorem Erdos346.indexedPartialBudgetSeed_of_prefix_cover_and_tail_surplus {a : ℕ → ℕ} {H M T : ℕ} (hcover : CoversInterval a Set.univ M H T) (hHT : H ≤ T) (hsurplus_from : ∀ (n : ℕ), M + 1 ≤ n → budgetBase a H M T + a n + a (n + 1) ≤ fullPrefixSum a n) : IndexedPartialBudgetSeed a H M T (M + 1)

theorem Erdos346.before_budget_of_large_T {a : ℕ → ℕ} {H M T start : ℕ} (hmono : StrictMono a) (hTlarge : H + a start ≤ T) (n : ℕ) : M ≤ n → n < start → n + 1 ≠ start → a (n + 1) ≤ T + (fullPrefixSum a n - fullPrefixSum a M) - H + 1

theorem Erdos346.beforeBudgetNeed_ge {a : ℕ → ℕ} {H start n : ℕ} (hnstart : n < start) : H + a (n + 1) ≤ beforeBudgetNeed a H start

theorem Erdos346.before_budget_of_T_ge_beforeBudgetNeed {a : ℕ → ℕ} {H M T start : ℕ} (hT : beforeBudgetNeed a H start ≤ T) (n : ℕ) : M ≤ n → n < start → n + 1 ≠ start → a (n + 1) ≤ T + (fullPrefixSum a n - fullPrefixSum a M) - H + 1

theorem Erdos346.indexedInitialTailSeed_of_cover_ge_beforeBudgetNeed_and_tail_surplus {a : ℕ → ℕ} {F : Set ℕ} {H M T start : ℕ} (hF : F ⊆ Set.Iic M) (hcover : CoversInterval a Fᶜ M H T) (hHT : H ≤ T) (hMstart : M < start) (hT : beforeBudgetNeed a H start ≤ T) (hsurplus_from : ∀ (n : ℕ), start ≤ n → budgetBase a H M T + a n + a (n + 1) ≤ fullPrefixSum a n) : IndexedInitialTailSeed a F H M T start

theorem Erdos346.indexedPartialBudgetSeed_of_large_cover_and_tail_surplus {a : ℕ → ℕ} {H M T start : ℕ} (hmono : StrictMono a) (hcover : CoversInterval a Set.univ M H T) (hHT : H ≤ T) (hMstart : M < start) (hTlarge : H + a start ≤ T) (hsurplus_from : ∀ (n : ℕ), start ≤ n → budgetBase a H M T + a n + a (n + 1) ≤ fullPrefixSum a n) : IndexedPartialBudgetSeed a H M T start

theorem Erdos346.indexedPartialBudgetSeed_of_cover_ge_beforeBudgetNeed_and_tail_surplus {a : ℕ → ℕ} {H M T start : ℕ} (hcover : CoversInterval a Set.univ M H T) (hHT : H ≤ T) (hMstart : M < start) (hT : beforeBudgetNeed a H start ≤ T) (hsurplus_from : ∀ (n : ℕ), start ≤ n → budgetBase a H M T + a n + a (n + 1) ≤ fullPrefixSum a n) : IndexedPartialBudgetSeed a H M T start

theorem Erdos346.prefix_cover_of_complete_avoiding_singleton_of_lt_next_next {a : ℕ → ℕ} {H M T : ℕ} (hmono : StrictMono a) (hcomplete : ∀ (t : ℕ), H ≤ t → t ∈ subsetSums a {M + 1}ᶜ) (hTlt : T < a (M + 2)) : CoversInterval a Set.univ M H T

theorem Erdos346.exists_prefix_cover_of_finiteDeletionComplete_avoiding_singleton {a : ℕ → ℕ} (hmono : StrictMono a) (hfinite : FiniteDeletionComplete a) (M : ℕ) : ∃ (H : ℕ), ∀ (T : ℕ), H ≤ T → T < a (M + 2) → CoversInterval a Set.univ M H T

theorem Erdos346.tail_pair_surplus_of_initial_and_two_step_le {a : ℕ → ℕ} {C start : ℕ} (hinit : C + a start + a (start + 1) ≤ fullPrefixSum a start) (hstep : ∀ (n : ℕ), start ≤ n → a (n + 2) ≤ a n + a (n + 1)) (n : ℕ) : start ≤ n → C + a n + a (n + 1) ≤ fullPrefixSum a n

theorem Erdos346.indexedPartialBudgetSeed_of_next_next_cover {a : ℕ → ℕ} {H M : ℕ} (hcover : CoversInterval a Set.univ M H (a (M + 2) - 1)) (hHT : H ≤ a (M + 2) - 1) (hkeep : H + a (M + 1) ≤ a (M + 2)) (hsurplus_from : ∀ (n : ℕ), M + 2 ≤ n → budgetBase a H M (a (M + 2) - 1) + a n + a (n + 1) ≤ fullPrefixSum a n) : IndexedPartialBudgetSeed a H M (a (M + 2) - 1) (M + 2)

theorem Erdos346.indexedPartialBudgetSeed_of_next_next_cover_and_two_step_tail {a : ℕ → ℕ} {H M : ℕ} (hcover : CoversInterval a Set.univ M H (a (M + 2) - 1)) (hHT : H ≤ a (M + 2) - 1) (hkeep : H + a (M + 1) ≤ a (M + 2)) (hinit : budgetBase a H M (a (M + 2) - 1) + a (M + 2) + a (M + 3) ≤ fullPrefixSum a (M + 2)) (hstep : ∀ (n : ℕ), M + 2 ≤ n → a (n + 2) ≤ a n + a (n + 1)) : IndexedPartialBudgetSeed a H M (a (M + 2) - 1) (M + 2)

theorem Erdos346.budgetBase_next_next_initial_surplus_of_pair_and_margin {a : ℕ → ℕ} {H M : ℕ} (hA2pos : 0 < a (M + 2)) (hpair : a (M + 2) + a (M + 3) ≤ fullPrefixSum a (M + 2)) (hmargin : H + a (M + 3) ≤ a (M + 1) + a (M + 2)) : budgetBase a H M (a (M + 2) - 1) + a (M + 2) + a (M + 3) ≤ fullPrefixSum a (M + 2)

theorem Erdos346.indexedPartialBudgetSeed_of_next_next_cover_and_margin_tail {a : ℕ → ℕ} {H M : ℕ} (hpos : ∀ (n : ℕ), 0 < a n) (hcover : CoversInterval a Set.univ M H (a (M + 2) - 1)) (hHT : H ≤ a (M + 2) - 1) (hkeep : H + a (M + 1) ≤ a (M + 2)) (hpair : a (M + 2) + a (M + 3) ≤ fullPrefixSum a (M + 2)) (hmargin : H + a (M + 3) ≤ a (M + 1) + a (M + 2)) (hstep : ∀ (n : ℕ), M + 2 ≤ n → a (n + 2) ≤ a n + a (n + 1)) : IndexedPartialBudgetSeed a H M (a (M + 2) - 1) (M + 2)

theorem Erdos346.indexedPartialBudgetSeed_of_next_next_cover_and_numeric_conditions {a : ℕ → ℕ} {H M : ℕ} (hpos : ∀ (n : ℕ), 0 < a n) (hcover : CoversInterval a Set.univ M H (a (M + 2) - 1)) (hHT : H ≤ a (M + 2) - 1) (hnum : H + a (M + 1) ≤ a (M + 2) ∧ a (M + 2) + a (M + 3) ≤ fullPrefixSum a (M + 2) ∧ H + a (M + 3) ≤ a (M + 1) + a (M + 2) ∧ ∀ (n : ℕ), M + 2 ≤ n → a (n + 2) ≤ a n + a (n + 1)) : IndexedPartialBudgetSeed a H M (a (M + 2) - 1) (M + 2)

theorem Erdos346.indexedInitialTailSeed_of_next_next_cover {a : ℕ → ℕ} {F : Set ℕ} {H M : ℕ} (hF : F ⊆ Set.Iic M) (hcover : CoversInterval a Fᶜ M H (a (M + 2) - 1)) (hHT : H ≤ a (M + 2) - 1) (hkeep : H + a (M + 1) ≤ a (M + 2)) (hsurplus_from : ∀ (n : ℕ), M + 2 ≤ n → budgetBase a H M (a (M + 2) - 1) + a n + a (n + 1) ≤ fullPrefixSum a n) : IndexedInitialTailSeed a F H M (a (M + 2) - 1) (M + 2)

theorem Erdos346.indexedInitialTailSeed_of_next_next_cover_and_two_step_tail {a : ℕ → ℕ} {F : Set ℕ} {H M : ℕ} (hF : F ⊆ Set.Iic M) (hcover : CoversInterval a Fᶜ M H (a (M + 2) - 1)) (hHT : H ≤ a (M + 2) - 1) (hkeep : H + a (M + 1) ≤ a (M + 2)) (hinit : budgetBase a H M (a (M + 2) - 1) + a (M + 2) + a (M + 3) ≤ fullPrefixSum a (M + 2)) (hstep : ∀ (n : ℕ), M + 2 ≤ n → a (n + 2) ≤ a n + a (n + 1)) : IndexedInitialTailSeed a F H M (a (M + 2) - 1) (M + 2)

theorem Erdos346.indexedInitialTailSeed_of_next_next_cover_and_margin_tail {a : ℕ → ℕ} {F : Set ℕ} {H M : ℕ} (hpos : ∀ (n : ℕ), 0 < a n) (hF : F ⊆ Set.Iic M) (hcover : CoversInterval a Fᶜ M H (a (M + 2) - 1)) (hHT : H ≤ a (M + 2) - 1) (hkeep : H + a (M + 1) ≤ a (M + 2)) (hpair : a (M + 2) + a (M + 3) ≤ fullPrefixSum a (M + 2)) (hmargin : H + a (M + 3) ≤ a (M + 1) + a (M + 2)) (hstep : ∀ (n : ℕ), M + 2 ≤ n → a (n + 2) ≤ a n + a (n + 1)) : IndexedInitialTailSeed a F H M (a (M + 2) - 1) (M + 2)

theorem Erdos346.indexedInitialTailSeed_of_next_next_cover_and_numeric_conditions {a : ℕ → ℕ} {F : Set ℕ} {H M : ℕ} (hpos : ∀ (n : ℕ), 0 < a n) (hF : F ⊆ Set.Iic M) (hcover : CoversInterval a Fᶜ M H (a (M + 2) - 1)) (hHT : H ≤ a (M + 2) - 1) (hnum : H + a (M + 1) ≤ a (M + 2) ∧ a (M + 2) + a (M + 3) ≤ fullPrefixSum a (M + 2) ∧ H + a (M + 3) ≤ a (M + 1) + a (M + 2) ∧ ∀ (n : ℕ), M + 2 ≤ n → a (n + 2) ≤ a n + a (n + 1)) : IndexedInitialTailSeed a F H M (a (M + 2) - 1) (M + 2)

theorem Erdos346.prefix_cover_of_complete_avoiding_finite_singleton_of_lt_next_next {a : ℕ → ℕ} {F : Set ℕ} {H M T : ℕ} (hmono : StrictMono a) (hcomplete : ∀ (t : ℕ), H ≤ t → t ∈ subsetSums a (F ∪ {M + 1})ᶜ) (hTlt : T < a (M + 2)) : CoversInterval a Fᶜ M H T

theorem Erdos346.indexedInitialTailSeed_of_finite_singleton_complete_and_numeric_conditions {a : ℕ → ℕ} {F : Set ℕ} {H M : ℕ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hF : F ⊆ Set.Iic M) (hcomplete : ∀ (t : ℕ), H ≤ t → t ∈ subsetSums a (F ∪ {M + 1})ᶜ) (hnum : H + a (M + 1) ≤ a (M + 2) ∧ a (M + 2) + a (M + 3) ≤ fullPrefixSum a (M + 2) ∧ H + a (M + 3) ≤ a (M + 1) + a (M + 2) ∧ ∀ (n : ℕ), M + 2 ≤ n → a (n + 2) ≤ a n + a (n + 1)) : IndexedInitialTailSeed a F H M (a (M + 2) - 1) (M + 2)

theorem Erdos346.uniformFinSingletonPrefixCover_of_uniformFinSingletonComplete {a : ℕ → ℕ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (huniform : UniformFinSingletonComplete a) : UniformFinSingletonPrefixCover a

theorem Erdos346.exists_prefix_cover_avoiding_finite_singleton_of_finiteDeletionComplete {a : ℕ → ℕ} {F : Set ℕ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hfinite : FiniteDeletionComplete a) (hFfinite : F.Finite) (M : ℕ) : ∃ (H : ℕ), CoversInterval a Fᶜ M H (a (M + 2) - 1)

theorem Erdos346.eventualFinSingletonSmallPrefixCover_of_uniformFinSingletonPrefixCover {a : ℕ → ℕ} {ρ : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hratioGap : HasUniformRatioGap a) (hρ1 : 1 < ρ) (hρφ : ρ < Real.goldenRatio) (hupper : ∀ᶠ (n : ℕ) in Filter.atTop, quotient a n < ρ) (hprefix : UniformFinSingletonPrefixCover a) : EventualFinSingletonSmallPrefixCover a

theorem Erdos346.eventualFinSingletonSmallPrefixCover_of_leastSmall {a : ℕ → ℕ} (hleast : EventualFinSingletonLeastSmallPrefixCover a) : EventualFinSingletonSmallPrefixCover a

theorem Erdos346.leastSmall_of_eventualFinSingletonSmallPrefixCover {a : ℕ → ℕ} (hsmall : EventualFinSingletonSmallPrefixCover a) : EventualFinSingletonLeastSmallPrefixCover a

theorem Erdos346.eventualFinSingletonSmallPrefixCover_iff_leastSmall {a : ℕ → ℕ} : EventualFinSingletonSmallPrefixCover a ↔ EventualFinSingletonLeastSmallPrefixCover a

theorem Erdos346.arbLargeFinSingletonSmallPrefixCover_of_eventual {a : ℕ → ℕ} (hsmall : EventualFinSingletonSmallPrefixCover a) : ArbitrarilyLargeFinSingletonSmallPrefixCover a

theorem Erdos346.arbLargeFinSingletonSmallPrefixCover_of_leastLarge {a : ℕ → ℕ} (hleast : ArbitrarilyLargeFinSingletonLeastSmallPrefixCover a) : ArbitrarilyLargeFinSingletonSmallPrefixCover a

theorem Erdos346.leastLarge_of_arbLargeFinSingletonSmallPrefixCover {a : ℕ → ℕ} (hsmall : ArbitrarilyLargeFinSingletonSmallPrefixCover a) : ArbitrarilyLargeFinSingletonLeastSmallPrefixCover a

theorem Erdos346.arbLargeFinSingletonSmallPrefixCover_iff_leastLarge {a : ℕ → ℕ} : ArbitrarilyLargeFinSingletonSmallPrefixCover a ↔ ArbitrarilyLargeFinSingletonLeastSmallPrefixCover a

theorem Erdos346.first_seed_keep_iff_leastPrefixCoverThreshold_le_nextSeedMargin {a : ℕ → ℕ} {I : Set ℕ} {M : ℕ} (hnext : a (M + 1) ≤ a (M + 2)) : leastPrefixCoverThreshold a I M (a (M + 2) - 1) + a (M + 1) ≤ a (M + 2) ↔ leastPrefixCoverThreshold a I M (a (M + 2) - 1) ≤ nextSeedMargin a M

theorem Erdos346.first_prefix_cover_of_first_seed_keep {a : ℕ → ℕ} {I : Set ℕ} {M : ℕ} (hnext : a (M + 1) ≤ a (M + 2)) (hkeep : leastPrefixCoverThreshold a I M (a (M + 2) - 1) + a (M + 1) ≤ a (M + 2)) : CoversInterval a I M (nextSeedMargin a M) (a (M + 2) - 1)

theorem Erdos346.first_seed_keep_of_first_prefix_cover {a : ℕ → ℕ} {I : Set ℕ} {M : ℕ} (hnext : a (M + 1) ≤ a (M + 2)) (hcover : CoversInterval a I M (nextSeedMargin a M) (a (M + 2) - 1)) : leastPrefixCoverThreshold a I M (a (M + 2) - 1) + a (M + 1) ≤ a (M + 2)

theorem Erdos346.arbLargeFinSingletonFirstPrefixCover_of_firstSmall {a : ℕ → ℕ} (hmono : StrictMono a) (hfirst : ArbitrarilyLargeFinSingletonFirstSmallPrefixCover a) : ArbitrarilyLargeFinSingletonFirstPrefixCover a

theorem Erdos346.arbLargeFinSingletonFirstSmallPrefixCover_of_firstPrefixCover {a : ℕ → ℕ} (hmono : StrictMono a) (hcover : ArbitrarilyLargeFinSingletonFirstPrefixCover a) : ArbitrarilyLargeFinSingletonFirstSmallPrefixCover a

theorem Erdos346.arbLargeFinSingletonFirstPrefixCover_iff_firstSmall {a : ℕ → ℕ} (hmono : StrictMono a) : ArbitrarilyLargeFinSingletonFirstPrefixCover a ↔ ArbitrarilyLargeFinSingletonFirstSmallPrefixCover a

theorem Erdos346.eventual_first_prefix_cover_failure_of_not_arbLarge_fixedBase {a : ℕ → ℕ} {F : Set ℕ} (hnot : ¬∀ (N : ℕ), ∃ (M : ℕ), N ≤ M ∧ F ⊆ Set.Iic M ∧ CoversInterval a Fᶜ M (nextSeedMargin a M) (a (M + 2) - 1)) : ∃ (N : ℕ), ∀ (M : ℕ), N ≤ M → F ⊆ Set.Iic M → ¬CoversInterval a Fᶜ M (nextSeedMargin a M) (a (M + 2) - 1)

theorem Erdos346.evt_prefix_holes_of_not_arbLargeFirstPrefixCover_fixedBase {a : ℕ → ℕ} {F : Set ℕ} (hFfinite : F.Finite) (hnot : ¬∀ (N : ℕ), ∃ (M : ℕ), N ≤ M ∧ F ⊆ Set.Iic M ∧ CoversInterval a Fᶜ M (nextSeedMargin a M) (a (M + 2) - 1)) : ∀ᶠ (M : ℕ) in Filter.atTop, ∃ (t : ℕ), nextSeedMargin a M ≤ t ∧ t ≤ a (M + 2) - 1 ∧ t ∉ prefixSubsetSums a Fᶜ M

theorem Erdos346.evt_finite_singleton_holes_of_not_arbLargeFirstPrefixCover_fixedBase {a : ℕ → ℕ} {F : Set ℕ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hFfinite : F.Finite) (hnot : ¬∀ (N : ℕ), ∃ (M : ℕ), N ≤ M ∧ F ⊆ Set.Iic M ∧ CoversInterval a Fᶜ M (nextSeedMargin a M) (a (M + 2) - 1)) : ∀ᶠ (M : ℕ) in Filter.atTop, ∃ t ≤ a (M + 2) - 1, t < a (M + 2) ∧ t ∉ subsetSums a (F ∪ {M + 1})ᶜ ∧ nextSeedMargin a M ≤ t

theorem Erdos346.arbLargeFinSingletonFirstPrefixCover_of_arbLargeFinSingletonSmallPrefixCover {a : ℕ → ℕ} (hmono : StrictMono a) (hsmall : ArbitrarilyLargeFinSingletonSmallPrefixCover a) : ArbitrarilyLargeFinSingletonFirstPrefixCover a

theorem Erdos346.arbLargeFinSingletonFirstPrefixCover_of_uniformFinSingletonPrefixCover {a : ℕ → ℕ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hgap : HasUniformRatioGap a) (hprefix : UniformFinSingletonPrefixCover a) : ArbitrarilyLargeFinSingletonFirstPrefixCover a

theorem Erdos346.arbLargeFinSingletonFirstPrefixCover_of_firstWindowShiftClosed {a : ℕ → ℕ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hgap : HasUniformRatioGap a) (hfinite : FiniteDeletionComplete a) (hclosed : ArbitrarilyLargeFinSingletonFirstWindowShiftClosed a) : ArbitrarilyLargeFinSingletonFirstPrefixCover a

theorem Erdos346.evt_pair_seed_margin_of_evtQuotientLtGold {a : ℕ → ℕ} {ρ : ℝ} (hpos : ∀ (n : ℕ), 0 < a n) (hρ1 : 1 < ρ) (hρφ : ρ < Real.goldenRatio) (hupper : ∀ᶠ (n : ℕ) in Filter.atTop, quotient a n < ρ) : ∀ᶠ (M : ℕ) in Filter.atTop, a (M + 3) ≤ a (M + 1) + a (M + 2)

theorem Erdos346.evt_nextSeedMargin_ge_of_uniformRatioGap {a : ℕ → ℕ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hgap : HasUniformRatioGap a) (C : ℕ) : ∀ᶠ (M : ℕ) in Filter.atTop, C ≤ nextSeedMargin a M

theorem Erdos346.evt_pairSeedMargin_ge_of_evtQuotientLtGold {a : ℕ → ℕ} {ρ : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hρ1 : 1 < ρ) (hρφ : ρ < Real.goldenRatio) (hupper : ∀ᶠ (n : ℕ) in Filter.atTop, quotient a n < ρ) (C : ℕ) : ∀ᶠ (M : ℕ) in Filter.atTop, C ≤ pairSeedMargin a M

theorem Erdos346.evt_prefix_shift_gaps_of_not_arbLargeFirstPrefixCover_fixedBase {a : ℕ → ℕ} {F : Set ℕ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hgap : HasUniformRatioGap a) (hfinite : FiniteDeletionComplete a) (hFfinite : F.Finite) (hnot : ¬∀ (N : ℕ), ∃ (M : ℕ), N ≤ M ∧ F ⊆ Set.Iic M ∧ CoversInterval a Fᶜ M (nextSeedMargin a M) (a (M + 2) - 1)) : ∀ᶠ (M : ℕ) in Filter.atTop, ∃ s ∈ prefixSubsetSums a Fᶜ M, s < nextSeedMargin a M ∧ a (M + 1) + s < a (M + 2) ∧ a (M + 1) + s ∉ prefixSubsetSums a Fᶜ M

theorem Erdos346.evt_not_firstWindowShiftClosed_of_not_arbLargeFirstPrefixCover_fixedBase {a : ℕ → ℕ} {F : Set ℕ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hgap : HasUniformRatioGap a) (hfinite : FiniteDeletionComplete a) (hFfinite : F.Finite) (hnot : ¬∀ (N : ℕ), ∃ (M : ℕ), N ≤ M ∧ F ⊆ Set.Iic M ∧ CoversInterval a Fᶜ M (nextSeedMargin a M) (a (M + 2) - 1)) : ∀ᶠ (M : ℕ) in Filter.atTop, ¬FirstWindowShiftClosed a F M

theorem Erdos346.evt_not_finSingletonCompleteBelowPrev_of_not_arbLargeFirstPrefixCover_fixedBase {a : ℕ → ℕ} {F : Set ℕ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hgap : HasUniformRatioGap a) (hfinite : FiniteDeletionComplete a) (hFfinite : F.Finite) (hnot : ¬∀ (N : ℕ), ∃ (M : ℕ), N ≤ M ∧ F ⊆ Set.Iic M ∧ CoversInterval a Fᶜ M (nextSeedMargin a M) (a (M + 2) - 1)) : ∀ᶠ (M : ℕ) in Filter.atTop, ¬FinSingletonCompleteBelowPrev a F M

theorem Erdos346.evt_prev_lt_finSingletonCompleteThreshold_of_not_arbLargeFirstPrefixCover_fixedBase {a : ℕ → ℕ} {F : Set ℕ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hgap : HasUniformRatioGap a) (hfinite : FiniteDeletionComplete a) (hFfinite : F.Finite) (hnot : ¬∀ (N : ℕ), ∃ (M : ℕ), N ≤ M ∧ F ⊆ Set.Iic M ∧ CoversInterval a Fᶜ M (nextSeedMargin a M) (a (M + 2) - 1)) : ∀ᶠ (M : ℕ) in Filter.atTop, a (M + 1) < finSingletonCompleteThreshold a hfinite hFfinite M

theorem Erdos346.evt_finSingletonCompleteThreshold_holes_of_not_arbLargeFirstPrefixCover_fixedBase {a : ℕ → ℕ} {F : Set ℕ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hgap : HasUniformRatioGap a) (hfinite : FiniteDeletionComplete a) (hFfinite : F.Finite) (hnot : ¬∀ (N : ℕ), ∃ (M : ℕ), N ≤ M ∧ F ⊆ Set.Iic M ∧ CoversInterval a Fᶜ M (nextSeedMargin a M) (a (M + 2) - 1)) : ∀ᶠ (M : ℕ) in Filter.atTop, ∃ (t : ℕ), a (M + 1) ≤ t ∧ t ∉ subsetSums a (F ∪ {M + 1})ᶜ

theorem Erdos346.evt_pred_finSingletonCompleteThreshold_holes_of_not_arbLargeFirstPrefixCover_fixedBase {a : ℕ → ℕ} {F : Set ℕ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hgap : HasUniformRatioGap a) (hfinite : FiniteDeletionComplete a) (hFfinite : F.Finite) (hnot : ¬∀ (N : ℕ), ∃ (M : ℕ), N ≤ M ∧ F ⊆ Set.Iic M ∧ CoversInterval a Fᶜ M (nextSeedMargin a M) (a (M + 2) - 1)) : ∀ᶠ (M : ℕ) in Filter.atTop, ∃ (t : ℕ), t = finSingletonCompleteThreshold a hfinite hFfinite M - 1 ∧ a (M + 1) ≤ t ∧ t ∉ subsetSums a (F ∪ {M + 1})ᶜ

theorem Erdos346.evt_predThreshold_small_forces_prefix_shift_gap_of_not_arbLargeFirstPrefixCover_fixedBase {a : ℕ → ℕ} {F : Set ℕ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hgap : HasUniformRatioGap a) (hfinite : FiniteDeletionComplete a) (hFfinite : F.Finite) (hnot : ¬∀ (N : ℕ), ∃ (M : ℕ), N ≤ M ∧ F ⊆ Set.Iic M ∧ CoversInterval a Fᶜ M (nextSeedMargin a M) (a (M + 2) - 1)) : ∀ᶠ (M : ℕ) in Filter.atTop, finSingletonCompleteThreshold a hfinite hFfinite M ≤ a (M + 2) → ∃ s ∈ prefixSubsetSums a Fᶜ M, s < nextSeedMargin a M ∧ a (M + 1) + s < a (M + 2) ∧ a (M + 1) + s ∉ prefixSubsetSums a Fᶜ M

theorem Erdos346.evt_threshold_large_or_prefix_shift_gap_of_not_arbLargeFirstPrefixCover_fixedBase {a : ℕ → ℕ} {F : Set ℕ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hgap : HasUniformRatioGap a) (hfinite : FiniteDeletionComplete a) (hFfinite : F.Finite) (hnot : ¬∀ (N : ℕ), ∃ (M : ℕ), N ≤ M ∧ F ⊆ Set.Iic M ∧ CoversInterval a Fᶜ M (nextSeedMargin a M) (a (M + 2) - 1)) : ∀ᶠ (M : ℕ) in Filter.atTop, a (M + 2) < finSingletonCompleteThreshold a hfinite hFfinite M ∨ ∃ s ∈ prefixSubsetSums a Fᶜ M, s < nextSeedMargin a M ∧ a (M + 1) + s < a (M + 2) ∧ a (M + 1) + s ∉ prefixSubsetSums a Fᶜ M

theorem Erdos346.evt_offset_threshold_or_shifted_prefix_of_threshold_escape {a : ℕ → ℕ} {F : Set ℕ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hfinite : FiniteDeletionComplete a) (hFfinite : F.Finite) (k : ℕ) (hk : 2 ≤ k) (hescape : ∀ᶠ (M : ℕ) in Filter.atTop, a (M + k) < finSingletonCompleteThreshold a hfinite hFfinite M) : ∀ᶠ (M : ℕ) in Filter.atTop, a (M + k + 1) < finSingletonCompleteThreshold a hfinite hFfinite M ∨ ∃ (t : ℕ) (s : ℕ), t = finSingletonCompleteThreshold a hfinite hFfinite M - 1 ∧ a (M + k) ≤ t ∧ t < a (M + k + 1) ∧ t ∉ subsetSums a (F ∪ {M + 1})ᶜ ∧ s = t - a (M + 1) ∧ s ∈ prefixSubsetSums a (F ∪ {M + 1})ᶜ (M + k)

theorem Erdos346.evt_next3_threshold_or_shifted_prefix_of_threshold_escape {a : ℕ → ℕ} {F : Set ℕ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hfinite : FiniteDeletionComplete a) (hFfinite : F.Finite) (hescape : ∀ᶠ (M : ℕ) in Filter.atTop, a (M + 2) < finSingletonCompleteThreshold a hfinite hFfinite M) : ∀ᶠ (M : ℕ) in Filter.atTop, a (M + 3) < finSingletonCompleteThreshold a hfinite hFfinite M ∨ ∃ (t : ℕ) (s : ℕ), t = finSingletonCompleteThreshold a hfinite hFfinite M - 1 ∧ a (M + 2) ≤ t ∧ t < a (M + 3) ∧ t ∉ subsetSums a (F ∪ {M + 1})ᶜ ∧ s = t - a (M + 1) ∧ s ∈ prefixSubsetSums a (F ∪ {M + 1})ᶜ (M + 2)

theorem Erdos346.not_arbLargeFinSingletonCompleteBelowPrev_fixedBase_of_not_arbLargeFirstPrefixCover_fixedBase {a : ℕ → ℕ} {F : Set ℕ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hgap : HasUniformRatioGap a) (hfinite : FiniteDeletionComplete a) (hFfinite : F.Finite) (hnot : ¬∀ (N : ℕ), ∃ (M : ℕ), N ≤ M ∧ F ⊆ Set.Iic M ∧ CoversInterval a Fᶜ M (nextSeedMargin a M) (a (M + 2) - 1)) : ¬∀ (N : ℕ), ∃ (M : ℕ), N ≤ M ∧ F ⊆ Set.Iic M ∧ FinSingletonCompleteBelowPrev a F M

theorem Erdos346.nextSeedMargin_le_prev_of_two_step_le {a : ℕ → ℕ} {M : ℕ} (hmono : StrictMono a) (htwo : a (M + 2) ≤ a M + a (M + 1)) : nextSeedMargin a M ≤ a (M + 1)

theorem Erdos346.evt_nextSeedMargin_le_prev_of_evtQuotientLtGold {a : ℕ → ℕ} {ρ : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hρ1 : 1 < ρ) (hρφ : ρ < Real.goldenRatio) (hupper : ∀ᶠ (n : ℕ) in Filter.atTop, quotient a n < ρ) : ∀ᶠ (M : ℕ) in Filter.atTop, nextSeedMargin a M ≤ a (M + 1)

theorem Erdos346.arbLargeFinSingletonFirstWindowShiftClosed_of_firstPrefixCover_of_evtQuotientLtGold {a : ℕ → ℕ} {ρ : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hρ1 : 1 < ρ) (hρφ : ρ < Real.goldenRatio) (hupper : ∀ᶠ (n : ℕ) in Filter.atTop, quotient a n < ρ) (hcover : ArbitrarilyLargeFinSingletonFirstPrefixCover a) : ArbitrarilyLargeFinSingletonFirstWindowShiftClosed a

theorem Erdos346.arbLargeFinSingletonFirstPrefixCover_iff_firstWindowShiftClosed_of_evtQuotientLtGold {a : ℕ → ℕ} {ρ : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hgap : HasUniformRatioGap a) (hfinite : FiniteDeletionComplete a) (hρ1 : 1 < ρ) (hρφ : ρ < Real.goldenRatio) (hupper : ∀ᶠ (n : ℕ) in Filter.atTop, quotient a n < ρ) : ArbitrarilyLargeFinSingletonFirstPrefixCover a ↔ ArbitrarilyLargeFinSingletonFirstWindowShiftClosed a

theorem Erdos346.arbLargeFinSingletonFirstWindowShiftClosed_of_completeBelowPrev {a : ℕ → ℕ} (hmono : StrictMono a) (hbelow : ArbitrarilyLargeFinSingletonCompleteBelowPrev a) : ArbitrarilyLargeFinSingletonFirstWindowShiftClosed a

theorem Erdos346.arbLargeFinSingletonFirstPrefixCover_of_completeBelowPrev {a : ℕ → ℕ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hgap : HasUniformRatioGap a) (hfinite : FiniteDeletionComplete a) (hbelow : ArbitrarilyLargeFinSingletonCompleteBelowPrev a) : ArbitrarilyLargeFinSingletonFirstPrefixCover a

theorem Erdos346.not_seed_keep_of_nextSeedMargin_lt_least {a : ℕ → ℕ} {F : Set ℕ} {M : ℕ} (hnext : a (M + 1) ≤ a (M + 2)) (hlt : nextSeedMargin a M < leastPrefixCoverThreshold a Fᶜ M (a (M + 2) - 1)) : ¬leastPrefixCoverThreshold a Fᶜ M (a (M + 2) - 1) + a (M + 1) ≤ a (M + 2)

theorem Erdos346.evt_finite_singleton_holes_of_eventual_seed_margin_failure {a : ℕ → ℕ} {F : Set ℕ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hFfinite : F.Finite) (hbad : ∃ (N : ℕ), ∀ (M : ℕ), N ≤ M → F ⊆ Set.Iic M → ¬(leastPrefixCoverThreshold a Fᶜ M (a (M + 2) - 1) + a (M + 1) ≤ a (M + 2) ∧ leastPrefixCoverThreshold a Fᶜ M (a (M + 2) - 1) + a (M + 3) ≤ a (M + 1) + a (M + 2))) (hnext : ∀ᶠ (M : ℕ) in Filter.atTop, a (M + 1) ≤ a (M + 2)) (hpair : ∀ᶠ (M : ℕ) in Filter.atTop, a (M + 3) ≤ a (M + 1) + a (M + 2)) : ∀ᶠ (M : ℕ) in Filter.atTop, ∃ t ≤ a (M + 2) - 1, t < a (M + 2) ∧ t ∉ subsetSums a (F ∪ {M + 1})ᶜ ∧ (nextSeedMargin a M ≤ t ∨ pairSeedMargin a M ≤ t)

theorem Erdos346.evt_finite_singleton_holes_of_eventual_seed_margin_failure_of_evtQuotientLtGold {a : ℕ → ℕ} {F : Set ℕ} {ρ : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hFfinite : F.Finite) (hρ1 : 1 < ρ) (hρφ : ρ < Real.goldenRatio) (hupper : ∀ᶠ (n : ℕ) in Filter.atTop, quotient a n < ρ) (hbad : ∃ (N : ℕ), ∀ (M : ℕ), N ≤ M → F ⊆ Set.Iic M → ¬(leastPrefixCoverThreshold a Fᶜ M (a (M + 2) - 1) + a (M + 1) ≤ a (M + 2) ∧ leastPrefixCoverThreshold a Fᶜ M (a (M + 2) - 1) + a (M + 3) ≤ a (M + 1) + a (M + 2))) : ∀ᶠ (M : ℕ) in Filter.atTop, ∃ t ≤ a (M + 2) - 1, t < a (M + 2) ∧ t ∉ subsetSums a (F ∪ {M + 1})ᶜ ∧ (nextSeedMargin a M ≤ t ∨ pairSeedMargin a M ≤ t)

theorem Erdos346.eventual_seed_margin_failure_of_not_arbLargeLeastSmall_fixedBase {a : ℕ → ℕ} {F : Set ℕ} (hnot : ¬∀ (N : ℕ), ∃ (M : ℕ), N ≤ M ∧ F ⊆ Set.Iic M ∧ leastPrefixCoverThreshold a Fᶜ M (a (M + 2) - 1) + a (M + 1) ≤ a (M + 2) ∧ leastPrefixCoverThreshold a Fᶜ M (a (M + 2) - 1) + a (M + 3) ≤ a (M + 1) + a (M + 2)) : ∃ (N : ℕ), ∀ (M : ℕ), N ≤ M → F ⊆ Set.Iic M → ¬(leastPrefixCoverThreshold a Fᶜ M (a (M + 2) - 1) + a (M + 1) ≤ a (M + 2) ∧ leastPrefixCoverThreshold a Fᶜ M (a (M + 2) - 1) + a (M + 3) ≤ a (M + 1) + a (M + 2))

theorem Erdos346.evt_finite_singleton_holes_of_not_arbLargeLeastSmall_fixedBase_of_evtQuotientLtGold {a : ℕ → ℕ} {F : Set ℕ} {ρ : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hFfinite : F.Finite) (hρ1 : 1 < ρ) (hρφ : ρ < Real.goldenRatio) (hupper : ∀ᶠ (n : ℕ) in Filter.atTop, quotient a n < ρ) (hnot : ¬∀ (N : ℕ), ∃ (M : ℕ), N ≤ M ∧ F ⊆ Set.Iic M ∧ leastPrefixCoverThreshold a Fᶜ M (a (M + 2) - 1) + a (M + 1) ≤ a (M + 2) ∧ leastPrefixCoverThreshold a Fᶜ M (a (M + 2) - 1) + a (M + 3) ≤ a (M + 1) + a (M + 2)) : ∀ᶠ (M : ℕ) in Filter.atTop, ∃ t ≤ a (M + 2) - 1, t < a (M + 2) ∧ t ∉ subsetSums a (F ∪ {M + 1})ᶜ ∧ (nextSeedMargin a M ≤ t ∨ pairSeedMargin a M ≤ t)

theorem Erdos346.evt_shifted_prefix_holes_of_not_arbLargeLeastSmall_fixedBase {a : ℕ → ℕ} {F : Set ℕ} {ρ : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hgap : HasUniformRatioGap a) (hfinite : FiniteDeletionComplete a) (hFfinite : F.Finite) (hρ1 : 1 < ρ) (hρφ : ρ < Real.goldenRatio) (hupper : ∀ᶠ (n : ℕ) in Filter.atTop, quotient a n < ρ) (hnot : ¬∀ (N : ℕ), ∃ (M : ℕ), N ≤ M ∧ F ⊆ Set.Iic M ∧ leastPrefixCoverThreshold a Fᶜ M (a (M + 2) - 1) + a (M + 1) ≤ a (M + 2) ∧ leastPrefixCoverThreshold a Fᶜ M (a (M + 2) - 1) + a (M + 3) ≤ a (M + 1) + a (M + 2)) : ∀ᶠ (M : ℕ) in Filter.atTop, ∃ t ≤ a (M + 2) - 1, t < a (M + 2) ∧ t ∉ subsetSums a (F ∪ {M + 1})ᶜ ∧ a (M + 1) ≤ t ∧ t - a (M + 1) ∈ prefixSubsetSums a Fᶜ M ∧ (nextSeedMargin a M ≤ t ∨ pairSeedMargin a M ≤ t)

theorem Erdos346.evt_prefix_shift_gaps_of_not_arbLargeLeastSmall_fixedBase {a : ℕ → ℕ} {F : Set ℕ} {ρ : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hgap : HasUniformRatioGap a) (hfinite : FiniteDeletionComplete a) (hFfinite : F.Finite) (hρ1 : 1 < ρ) (hρφ : ρ < Real.goldenRatio) (hupper : ∀ᶠ (n : ℕ) in Filter.atTop, quotient a n < ρ) (hnot : ¬∀ (N : ℕ), ∃ (M : ℕ), N ≤ M ∧ F ⊆ Set.Iic M ∧ leastPrefixCoverThreshold a Fᶜ M (a (M + 2) - 1) + a (M + 1) ≤ a (M + 2) ∧ leastPrefixCoverThreshold a Fᶜ M (a (M + 2) - 1) + a (M + 3) ≤ a (M + 1) + a (M + 2)) : ∀ᶠ (M : ℕ) in Filter.atTop, ∃ s ∈ prefixSubsetSums a Fᶜ M, s < nextSeedMargin a M ∧ a (M + 1) + s < a (M + 2) ∧ a (M + 1) + s ∉ prefixSubsetSums a Fᶜ M

theorem Erdos346.evt_nextSeedMargin_lt_least_of_not_arbLargeLeastSmall_fixedBase {a : ℕ → ℕ} {F : Set ℕ} {ρ : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hgap : HasUniformRatioGap a) (hfinite : FiniteDeletionComplete a) (hFfinite : F.Finite) (hρ1 : 1 < ρ) (hρφ : ρ < Real.goldenRatio) (hupper : ∀ᶠ (n : ℕ) in Filter.atTop, quotient a n < ρ) (hnot : ¬∀ (N : ℕ), ∃ (M : ℕ), N ≤ M ∧ F ⊆ Set.Iic M ∧ leastPrefixCoverThreshold a Fᶜ M (a (M + 2) - 1) + a (M + 1) ≤ a (M + 2) ∧ leastPrefixCoverThreshold a Fᶜ M (a (M + 2) - 1) + a (M + 3) ≤ a (M + 1) + a (M + 2)) : ∀ᶠ (M : ℕ) in Filter.atTop, nextSeedMargin a M < leastPrefixCoverThreshold a Fᶜ M (a (M + 2) - 1)

theorem Erdos346.evt_not_seed_keep_of_not_arbLargeLeastSmall_fixedBase {a : ℕ → ℕ} {F : Set ℕ} {ρ : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hgap : HasUniformRatioGap a) (hfinite : FiniteDeletionComplete a) (hFfinite : F.Finite) (hρ1 : 1 < ρ) (hρφ : ρ < Real.goldenRatio) (hupper : ∀ᶠ (n : ℕ) in Filter.atTop, quotient a n < ρ) (hnot : ¬∀ (N : ℕ), ∃ (M : ℕ), N ≤ M ∧ F ⊆ Set.Iic M ∧ leastPrefixCoverThreshold a Fᶜ M (a (M + 2) - 1) + a (M + 1) ≤ a (M + 2) ∧ leastPrefixCoverThreshold a Fᶜ M (a (M + 2) - 1) + a (M + 3) ≤ a (M + 1) + a (M + 2)) : ∀ᶠ (M : ℕ) in Filter.atTop, ¬leastPrefixCoverThreshold a Fᶜ M (a (M + 2) - 1) + a (M + 1) ≤ a (M + 2)

theorem Erdos346.arbLargeLeastSmall_of_firstSmall_of_evtQuotientLtGold {a : ℕ → ℕ} {ρ : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hgap : HasUniformRatioGap a) (hfinite : FiniteDeletionComplete a) (hρ1 : 1 < ρ) (hρφ : ρ < Real.goldenRatio) (hupper : ∀ᶠ (n : ℕ) in Filter.atTop, quotient a n < ρ) (hfirst : ArbitrarilyLargeFinSingletonFirstSmallPrefixCover a) : ArbitrarilyLargeFinSingletonLeastSmallPrefixCover a

theorem Erdos346.indexedPartialBudgetSeed_of_singleton_complete_and_numeric_conditions {a : ℕ → ℕ} {H M : ℕ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hcomplete : ∀ (t : ℕ), H ≤ t → t ∈ subsetSums a {M + 1}ᶜ) (hnum : H + a (M + 1) ≤ a (M + 2) ∧ a (M + 2) + a (M + 3) ≤ fullPrefixSum a (M + 2) ∧ H + a (M + 3) ≤ a (M + 1) + a (M + 2) ∧ ∀ (n : ℕ), M + 2 ≤ n → a (n + 2) ≤ a n + a (n + 1)) : IndexedPartialBudgetSeed a H M (a (M + 2) - 1) (M + 2)

theorem Erdos346.exists_indexedPartialBudgetSeed_of_eventual_singleton_complete {a : ℕ → ℕ} {ρ : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hratioGap : HasUniformRatioGap a) (hρ1 : 1 < ρ) (hρφ : ρ < Real.goldenRatio) (hupper : ∀ᶠ (n : ℕ) in Filter.atTop, quotient a n < ρ) (hsingleton : ∃ (H : ℕ), ∀ᶠ (M : ℕ) in Filter.atTop, ∀ (t : ℕ), H ≤ t → t ∈ subsetSums a {M + 1}ᶜ) : ∃ (H : ℕ) (M : ℕ) (T : ℕ) (start : ℕ), IndexedPartialBudgetSeed a H M T start

theorem Erdos346.exists_indexedInitialTailSeed_of_eventual_finite_singleton_complete {a : ℕ → ℕ} {ρ : ℝ} {F : Set ℕ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hratioGap : HasUniformRatioGap a) (hρ1 : 1 < ρ) (hρφ : ρ < Real.goldenRatio) (hupper : ∀ᶠ (n : ℕ) in Filter.atTop, quotient a n < ρ) (hFfinite : F.Finite) (hfiniteSingleton : ∃ (H : ℕ), ∀ᶠ (M : ℕ) in Filter.atTop, ∀ (t : ℕ), H ≤ t → t ∈ subsetSums a (F ∪ {M + 1})ᶜ) : ∃ (H : ℕ) (M : ℕ) (T : ℕ) (start : ℕ), IndexedInitialTailSeed a F H M T start

theorem Erdos346.exists_indexedInitialTailSeed_of_uniformFinSingletonPrefixCover {a : ℕ → ℕ} {ρ : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hratioGap : HasUniformRatioGap a) (hρ1 : 1 < ρ) (hρφ : ρ < Real.goldenRatio) (hupper : ∀ᶠ (n : ℕ) in Filter.atTop, quotient a n < ρ) (hprefix : UniformFinSingletonPrefixCover a) : ∃ (F : Set ℕ) (H : ℕ) (M : ℕ) (T : ℕ) (start : ℕ), IndexedInitialTailSeed a F H M T start

theorem Erdos346.exists_indexedInitialTailSeed_of_arbLargeFinSingletonSmallPrefixCover {a : ℕ → ℕ} {ρ : ℝ} (hpos : ∀ (n : ℕ), 0 < a n) (hρ1 : 1 < ρ) (hρφ : ρ < Real.goldenRatio) (hupper : ∀ᶠ (n : ℕ) in Filter.atTop, quotient a n < ρ) (hsmall : ArbitrarilyLargeFinSingletonSmallPrefixCover a) : ∃ (F : Set ℕ) (H : ℕ) (M : ℕ) (T : ℕ) (start : ℕ), IndexedInitialTailSeed a F H M T start

theorem Erdos346.exists_indexedInitialTailSeed_of_eventualFinSingletonSmallPrefixCover {a : ℕ → ℕ} {ρ : ℝ} (hpos : ∀ (n : ℕ), 0 < a n) (hρ1 : 1 < ρ) (hρφ : ρ < Real.goldenRatio) (hupper : ∀ᶠ (n : ℕ) in Filter.atTop, quotient a n < ρ) (hsmall : EventualFinSingletonSmallPrefixCover a) : ∃ (F : Set ℕ) (H : ℕ) (M : ℕ) (T : ℕ) (start : ℕ), IndexedInitialTailSeed a F H M T start

theorem Erdos346.budgetBase_next_next_eq_zero_of_le {a : ℕ → ℕ} {H M : ℕ} (hpos : 0 < a (M + 2)) (hbase : fullPrefixSum a M + H ≤ a (M + 2)) : budgetBase a H M (a (M + 2) - 1) = 0

theorem Erdos346.indexedPartialBudgetSeed_of_next_next_cover_and_zero_base_tail {a : ℕ → ℕ} {H M : ℕ} (hpos : ∀ (n : ℕ), 0 < a n) (hcover : CoversInterval a Set.univ M H (a (M + 2) - 1)) (hHT : H ≤ a (M + 2) - 1) (hkeep : H + a (M + 1) ≤ a (M + 2)) (hbase : fullPrefixSum a M + H ≤ a (M + 2)) (hpair : a (M + 2) + a (M + 3) ≤ fullPrefixSum a (M + 2)) (hstep : ∀ (n : ℕ), M + 2 ≤ n → a (n + 2) ≤ a n + a (n + 1)) : IndexedPartialBudgetSeed a H M (a (M + 2) - 1) (M + 2)

structure Erdos346.IndexedPartialBudgetSeedParameters (a : ℕ → ℕ) (H M T start : ℕ) : Prop

The explicit finite/tail conditions that are sufficient to produce an IndexedPartialBudgetSeed. This packages the remaining fixed-point choice: find a prefix cover whose upper endpoint is large enough for the finite before-budget, and whose budgetBase surplus starts before start.

• cover : CoversInterval a Set.univ M H T
• nonempty : H ≤ T
• start_after : M < start
• before_bound : beforeBudgetNeed a H start ≤ T
• tail_surplus (n : ℕ) : start ≤ n → budgetBase a H M T + a n + a (n + 1) ≤ fullPrefixSum a n

theorem Erdos346.indexedPartialBudgetSeed_of_parameters {a : ℕ → ℕ} {H M T start : ℕ} (hparams : IndexedPartialBudgetSeedParameters a H M T start) : IndexedPartialBudgetSeed a H M T start

theorem Erdos346.indexedPartialBudgetSeedParameters_upper_le_fullPrefixSum {a : ℕ → ℕ} {H M T start : ℕ} (hparams : IndexedPartialBudgetSeedParameters a H M T start) : T ≤ fullPrefixSum a M

theorem Erdos346.indexedPartialBudgetSeedParameters_need_le_fullPrefixSum {a : ℕ → ℕ} {H M T start : ℕ} (hparams : IndexedPartialBudgetSeedParameters a H M T start) : beforeBudgetNeed a H start ≤ fullPrefixSum a M

theorem Erdos346.exists_indexedPartialBudgetData_of_seed {a : ℕ → ℕ} {H M T start : ℕ} (hmono : StrictMono a) (hsurplus : ∀ (R : ℕ), ∀ᶠ (n : ℕ) in Filter.atTop, R + a n + a (n + 1) ≤ fullPrefixSum a n) (hseed : IndexedPartialBudgetSeed a H M T start) : ∃ (b : ℕ → ℕ), CoversInterval a Set.univ M H T ∧ IndexedPartialBudgetData a b H M T

theorem Erdos346.exists_indexedPartialBudgetInitialTailData_of_seed {a : ℕ → ℕ} {F : Set ℕ} {H M T start : ℕ} (hmono : StrictMono a) (hsurplus : ∀ (R : ℕ), ∀ᶠ (n : ℕ) in Filter.atTop, R + a n + a (n + 1) ≤ fullPrefixSum a n) (hseed : IndexedInitialTailSeed a F H M T start) : ∃ (b : ℕ → ℕ), IndexedPartialBudgetInitialTailData a F b H M T

theorem Erdos346.indexedBudgetData_of_indexedPartialBudgetData {a b : ℕ → ℕ} {H M T : ℕ} (hdata : IndexedPartialBudgetData a b H M T) : IndexedBudgetData a b H M T

theorem Erdos346.indexedBudgetInitialTailData_of_indexedPartialBudgetInitialTailData {a b : ℕ → ℕ} {F : Set ℕ} {H M T : ℕ} (hdata : IndexedPartialBudgetInitialTailData a F b H M T) : IndexedBudgetInitialTailData a F b H M T

theorem Erdos346.brownBudgetData_of_indexedBudgetData {a b : ℕ → ℕ} {H M T : ℕ} (hdata : IndexedBudgetData a b H M T) : BrownBudgetData a (Set.range b) H M T

theorem Erdos346.brownBudgetCoverData_of_indexedBudgetInitialTailData {a b : ℕ → ℕ} {F : Set ℕ} {H M T : ℕ} (hdata : IndexedBudgetInitialTailData a F b H M T) : BrownBudgetCoverData a (initialTailDeletionSet F b) H M T

structure Erdos346.IndexedBlockControlData (a b e : ℕ → ℕ) (H M T C : ℕ) : Prop

Block version of the remaining deletion-control data. Blocks allow the construction to delete a term and wait until the current term is large enough before the next kept-extension step.

• nonempty (k : ℕ) : b k ≤ e k
• gap (k : ℕ) : e k + 1 < b (k + 1)
• avoids_initial (k : ℕ) : M < b k
• initial_nonempty : H ≤ T
• margin : fullPrefixSum a M + H ≤ T + C + 1
• surplus_from (n : ℕ) : M ≤ n → C + a n + a (n + 1) ≤ fullPrefixSum a n
• deleted_bound (n : ℕ) : M ≤ n → n + 1 ∉ blockDeletionSet b e → deletedPrefixSum a (blockDeletionSet b e) n ≤ a n

theorem Erdos346.deletedPrefixSum_ge_add_of_two_mem {a : ℕ → ℕ} {D : Set ℕ} {n i j : ℕ} (hi_le : i ≤ n) (hj_le : j ≤ n) (hij : i ≠ j) (hiD : i ∈ D) (hjD : j ∈ D) : a i + a j ≤ deletedPrefixSum a D n

theorem Erdos346.not_indexedBlockControlData_of_pos {a b e : ℕ → ℕ} {H M T C : ℕ} (hpos : ∀ (n : ℕ), 0 < a n) : ¬IndexedBlockControlData a b e H M T C

The earlier block-control condition is too strong: at the end of the second deleted block the deleted prefix already contains a positive earlier deleted term plus the current block endpoint.

theorem Erdos346.brownBudgetData_of_indexedBlockControlData {a b e : ℕ → ℕ} {H M T C : ℕ} (hdata : IndexedBlockControlData a b e H M T C) : BrownBudgetData a (blockDeletionSet b e) H M T

theorem Erdos346.brownTailData_of_brownBudgetData {a : ℕ → ℕ} {D : Set ℕ} {H M T : ℕ} (hdata : BrownBudgetData a D H M T) : BrownTailData a D H M T

theorem Erdos346.brownTailCoverData_of_brownBudgetCoverData {a : ℕ → ℕ} {D : Set ℕ} {H M T : ℕ} (hdata : BrownBudgetCoverData a D H M T) : BrownTailCoverData a D H M T

theorem Erdos346.brownDeletionData_of_brownStepData {a : ℕ → ℕ} {D : Set ℕ} {H M : ℕ} (hpos : ∀ (n : ℕ), 0 < a n) (hdata : BrownStepData a D H M) : BrownDeletionData a D H M

theorem Erdos346.coversInterval_keptPrefixSum_of_brown {a : ℕ → ℕ} {D : Set ℕ} {H M n : ℕ} (hdata : BrownDeletionData a D H M) (hn : M ≤ n) : CoversInterval a Dᶜ n H (keptPrefixSum a D n) ∧ H ≤ keptPrefixSum a D n

theorem Erdos346.complete_of_brownDeletionData {a : ℕ → ℕ} {D : Set ℕ} {H M : ℕ} (hdata : BrownDeletionData a D H M) : D.Infinite ∧ IsCompleteOn a Dᶜ

theorem Erdos346.coversInterval_seedBound_of_brownSeed {a : ℕ → ℕ} {D : Set ℕ} {H M C n : ℕ} (hdata : BrownSeedData a D H M C) (hn : M ≤ n) : CoversInterval a Dᶜ n H (C + keptPrefixSum a D n) ∧ H ≤ C + keptPrefixSum a D n

theorem Erdos346.complete_of_brownSeedData {a : ℕ → ℕ} {D : Set ℕ} {H M C : ℕ} (hpos : ∀ (n : ℕ), 0 < a n) (hdata : BrownSeedData a D H M C) : D.Infinite ∧ IsCompleteOn a Dᶜ

theorem Erdos346.coversInterval_tailBound_of_brownTail {a : ℕ → ℕ} {D : Set ℕ} {H M T n : ℕ} (hcover0 : CoversInterval a Set.univ M H T) (hdata : BrownTailData a D H M T) (hn : M ≤ n) : CoversInterval a Dᶜ n H (T + (keptPrefixSum a D n - keptPrefixSum a D M)) ∧ H ≤ T + (keptPrefixSum a D n - keptPrefixSum a D M)

theorem Erdos346.complete_of_brownTailData {a : ℕ → ℕ} {D : Set ℕ} {H M T : ℕ} (hpos : ∀ (n : ℕ), 0 < a n) (hcover0 : CoversInterval a Set.univ M H T) (hdata : BrownTailData a D H M T) : D.Infinite ∧ IsCompleteOn a Dᶜ

theorem Erdos346.coversInterval_tailBound_of_brownTailCover {a : ℕ → ℕ} {D : Set ℕ} {H M T n : ℕ} (hdata : BrownTailCoverData a D H M T) (hn : M ≤ n) : CoversInterval a Dᶜ n H (T + (keptPrefixSum a D n - keptPrefixSum a D M)) ∧ H ≤ T + (keptPrefixSum a D n - keptPrefixSum a D M)

theorem Erdos346.complete_of_brownTailCoverData {a : ℕ → ℕ} {D : Set ℕ} {H M T : ℕ} (hpos : ∀ (n : ℕ), 0 < a n) (hdata : BrownTailCoverData a D H M T) : D.Infinite ∧ IsCompleteOn a Dᶜ

theorem Erdos346.complete_of_brownBudgetCoverData {a : ℕ → ℕ} {D : Set ℕ} {H M T : ℕ} (hpos : ∀ (n : ℕ), 0 < a n) (hdata : BrownBudgetCoverData a D H M T) : D.Infinite ∧ IsCompleteOn a Dᶜ

theorem Erdos346.complete_of_periodicDeletion_budget {a : ℕ → ℕ} {H M T start period : ℕ} (hpos : ∀ (n : ℕ), 0 < a n) (hperiod : 2 ≤ period) (hMstart : M < start) (hnonempty : H ≤ T) (hcover : CoversInterval a Set.univ M H T) (hbudget : ∀ (n : ℕ), M ≤ n → n + 1 ∉ periodicDeletionSet start period → deletedPrefixSum a (periodicDeletionSet start period) n + a (n + 1) ≤ T + (fullPrefixSum a n - fullPrefixSum a M) - H + 1) : ∃ (D : Set ℕ), D.Infinite ∧ IsCompleteOn a Dᶜ

theorem Erdos346.complete_of_periodicDeletion_step {a : ℕ → ℕ} {H M T start period : ℕ} (hpos : ∀ (n : ℕ), 0 < a n) (hperiod : 2 ≤ period) (hMstart : M < start) (hnonempty : H ≤ T) (hcover : CoversInterval a Set.univ M H T) (hstep : ∀ (n : ℕ), M ≤ n → n + 1 ∉ periodicDeletionSet start period → a (n + 1) ≤ T + (keptPrefixSum a (periodicDeletionSet start period) n - keptPrefixSum a (periodicDeletionSet start period) M) - H + 1) : ∃ (D : Set ℕ), D.Infinite ∧ IsCompleteOn a Dᶜ

theorem Erdos346.complete_of_periodicDeletion_fixedBlockSurplus {a : ℕ → ℕ} {H M T m : ℕ} (hpos : ∀ (n : ℕ), 0 < a n) (hmpos : 0 < m) (hnonempty : H ≤ T) (hcover : CoversInterval a Set.univ M H T) (hbase : a (M + 1) ≤ T - H + 1) (htwo : ∀ (n : ℕ), M ≤ n → a (n + 2) ≤ 2 * a (n + 1)) (hsurplus : FixedLengthBlockSurplusFrom a m (M + m + 1)) : ∃ (D : Set ℕ), D.Infinite ∧ IsCompleteOn a Dᶜ

theorem Erdos346.infCompleteDeletion_of_evtRatioLtGold_of_geometricBlockSurplus {a : ℕ → ℕ} {ρ : ℝ} {m : ℕ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hratioGap : HasUniformRatioGap a) (hcomplete : IsCompleteOn a Set.univ) (hmpos : 0 < m) (hρ1 : 1 < ρ) (hρφ : ρ < Real.goldenRatio) (hgeom : GeometricBlockSurplus ρ m) (hupper : ∀ᶠ (n : ℕ) in Filter.atTop, quotient a n < ρ) : ∃ (D : Set ℕ), D.Infinite ∧ IsCompleteOn a Dᶜ

theorem Erdos346.complete_of_indexedBudgetInitialTailData {a b : ℕ → ℕ} {F : Set ℕ} {H M T : ℕ} (hpos : ∀ (n : ℕ), 0 < a n) (hdata : IndexedBudgetInitialTailData a F b H M T) : (initialTailDeletionSet F b).Infinite ∧ IsCompleteOn a (initialTailDeletionSet F b)ᶜ

theorem Erdos346.complete_of_indexedPartialBudgetInitialTailData {a b : ℕ → ℕ} {F : Set ℕ} {H M T : ℕ} (hpos : ∀ (n : ℕ), 0 < a n) (hdata : IndexedPartialBudgetInitialTailData a F b H M T) : (initialTailDeletionSet F b).Infinite ∧ IsCompleteOn a (initialTailDeletionSet F b)ᶜ

theorem Erdos346.complete_of_indexedInitialTailSeed {a : ℕ → ℕ} {F : Set ℕ} {H M T start : ℕ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hsurplus : ∀ (R : ℕ), ∀ᶠ (n : ℕ) in Filter.atTop, R + a n + a (n + 1) ≤ fullPrefixSum a n) (hseed : IndexedInitialTailSeed a F H M T start) : ∃ (D : Set ℕ), D.Infinite ∧ IsCompleteOn a Dᶜ

theorem Erdos346.propagated_hole_step {a : ℕ → ℕ} {N m y : ℕ} (hmono : StrictMono a) (hgap : a m + a (m + 1) < a (m + 2)) (hnot : y ∉ subsetSums a (Set.Ici N)) (hylt : y < a m) (hsumlt : ∑ i ∈ Finset.Icc N m, a i < y + a (m + 1)) : y + a (m + 1) ∉ subsetSums a (Set.Ici N)

theorem Erdos346.propagatedGap_invariants {a : ℕ → ℕ} {N : ℕ} (hmono : StrictMono a) (hgap : ∀ (n : ℕ), N ≤ n → a n + a (n + 1) < a (n + 2)) (hNgt : 1 < a N) (k : ℕ) : propagatedGap a N k ∉ subsetSums a (Set.Ici N) ∧ propagatedGap a N k < a (N + 2 * k) ∧ ∑ i ∈ Finset.Icc N (N + 2 * k), a i < propagatedGap a N k + a (N + 2 * k + 1)

Proved analytic steps

The first theorem below turns L > φ into the eventual two-step gap. The gap-propagation theorem after it is also proved in Lean. The lower-bound L < φ side is handled later by the axiom-free global-budget periodic deletion construction.

theorem Erdos346.evt_two_step_gap_of_goldenRatio_lt_limit {a : ℕ → ℕ} {L : ℝ} (hpos : ∀ (n : ℕ), 0 < a n) (hlim : Filter.Tendsto (quotient a) Filter.atTop (nhds L)) (hgt : Real.goldenRatio < L) : ∀ᶠ (n : ℕ) in Filter.atTop, a n + a (n + 1) < a (n + 2)

If the ratio limit is larger than the golden ratio, then eventually there is a two-step gap.

theorem Erdos346.noncomplete_tail_of_evt_two_step_gap {a : ℕ → ℕ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hgap : ∀ᶠ (n : ℕ) in Filter.atTop, a n + a (n + 1) < a (n + 2)) : ∃ (N : ℕ), ¬IsCompleteOn a (Set.Ici N)

A tail satisfying the eventual two-step gap cannot be complete.

theorem Erdos346.exists_indexedBudgetData_of_eventual_singleton_complete {a : ℕ → ℕ} {ρ : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hratioGap : HasUniformRatioGap a) (hρ1 : 1 < ρ) (hρφ : ρ < Real.goldenRatio) (hupper : ∀ᶠ (n : ℕ) in Filter.atTop, quotient a n < ρ) (hsingleton : ∃ (H : ℕ), ∀ᶠ (M : ℕ) in Filter.atTop, ∀ (t : ℕ), H ≤ t → t ∈ subsetSums a {M + 1}ᶜ) : ∃ (b : ℕ → ℕ) (H : ℕ) (M : ℕ) (T : ℕ), CoversInterval a Set.univ M H T ∧ IndexedBudgetData a b H M T

theorem Erdos346.exists_brownBudgetData_of_evtRatioLtGold_of_eventual_singleton_complete {a : ℕ → ℕ} {ρ : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hratioGap : HasUniformRatioGap a) (hρ1 : 1 < ρ) (hρφ : ρ < Real.goldenRatio) (hupper : ∀ᶠ (n : ℕ) in Filter.atTop, quotient a n < ρ) (hsingleton : ∃ (H : ℕ), ∀ᶠ (M : ℕ) in Filter.atTop, ∀ (t : ℕ), H ≤ t → t ∈ subsetSums a {M + 1}ᶜ) : ∃ (D : Set ℕ) (H : ℕ) (M : ℕ) (T : ℕ), CoversInterval a Set.univ M H T ∧ BrownBudgetData a D H M T

theorem Erdos346.infCompleteDeletion_of_evtRatioLtGold {a : ℕ → ℕ} {ρ : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hgap : HasUniformRatioGap a) (hcomplete : IsCompleteOn a Set.univ) (hρ1 : 1 < ρ) (hρφ : ρ < Real.goldenRatio) (hupper : ∀ᶠ (n : ℕ) in Filter.atTop, quotient a n < ρ) : ∃ (D : Set ℕ), D.Infinite ∧ IsCompleteOn a Dᶜ

The Brown-style sparse deletion data gives the lower-bound deletion counterexample needed in the main proof.

theorem Erdos346.infCompleteDeletion_of_evtRatioLtGold_of_eventual_singleton_complete {a : ℕ → ℕ} {ρ : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hratioGap : HasUniformRatioGap a) (hρ1 : 1 < ρ) (hρφ : ρ < Real.goldenRatio) (hupper : ∀ᶠ (n : ℕ) in Filter.atTop, quotient a n < ρ) (hsingleton : ∃ (H : ℕ), ∀ᶠ (M : ℕ) in Filter.atTop, ∀ (t : ℕ), H ≤ t → t ∈ subsetSums a {M + 1}ᶜ) : ∃ (D : Set ℕ), D.Infinite ∧ IsCompleteOn a Dᶜ

theorem Erdos346.infCompleteDeletion_of_evtRatioLtGold_of_eventual_finite_singleton_complete {a : ℕ → ℕ} {ρ : ℝ} {F : Set ℕ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hratioGap : HasUniformRatioGap a) (hρ1 : 1 < ρ) (hρφ : ρ < Real.goldenRatio) (hupper : ∀ᶠ (n : ℕ) in Filter.atTop, quotient a n < ρ) (hFfinite : F.Finite) (hfiniteSingleton : ∃ (H : ℕ), ∀ᶠ (M : ℕ) in Filter.atTop, ∀ (t : ℕ), H ≤ t → t ∈ subsetSums a (F ∪ {M + 1})ᶜ) : ∃ (D : Set ℕ), D.Infinite ∧ IsCompleteOn a Dᶜ

theorem Erdos346.infCompleteDeletion_of_evtRatioLtGold_of_uniformFinSingletonPrefixCover {a : ℕ → ℕ} {ρ : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hratioGap : HasUniformRatioGap a) (hρ1 : 1 < ρ) (hρφ : ρ < Real.goldenRatio) (hupper : ∀ᶠ (n : ℕ) in Filter.atTop, quotient a n < ρ) (hprefix : UniformFinSingletonPrefixCover a) : ∃ (D : Set ℕ), D.Infinite ∧ IsCompleteOn a Dᶜ

theorem Erdos346.infCompleteDeletion_of_evtRatioLtGold_of_eventualFinSingletonSmallPrefixCover {a : ℕ → ℕ} {ρ : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hρ1 : 1 < ρ) (hρφ : ρ < Real.goldenRatio) (hupper : ∀ᶠ (n : ℕ) in Filter.atTop, quotient a n < ρ) (hsmall : EventualFinSingletonSmallPrefixCover a) : ∃ (D : Set ℕ), D.Infinite ∧ IsCompleteOn a Dᶜ

theorem Erdos346.infCompleteDeletion_of_evtRatioLtGold_of_arbLargeFinSingletonSmallPrefixCover {a : ℕ → ℕ} {ρ : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hρ1 : 1 < ρ) (hρφ : ρ < Real.goldenRatio) (hupper : ∀ᶠ (n : ℕ) in Filter.atTop, quotient a n < ρ) (hsmall : ArbitrarilyLargeFinSingletonSmallPrefixCover a) : ∃ (D : Set ℕ), D.Infinite ∧ IsCompleteOn a Dᶜ

theorem Erdos346.infCompleteDeletion_of_evtRatioLtGold_of_arbLargeFinSingletonFirstSmallPrefixCover {a : ℕ → ℕ} {ρ : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hgap : HasUniformRatioGap a) (hfinite : FiniteDeletionComplete a) (hρ1 : 1 < ρ) (hρφ : ρ < Real.goldenRatio) (hupper : ∀ᶠ (n : ℕ) in Filter.atTop, quotient a n < ρ) (hfirst : ArbitrarilyLargeFinSingletonFirstSmallPrefixCover a) : ∃ (D : Set ℕ), D.Infinite ∧ IsCompleteOn a Dᶜ

theorem Erdos346.infCompleteDeletion_of_evtRatioLtGold_of_arbLargeFinSingletonFirstPrefixCover {a : ℕ → ℕ} {ρ : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hgap : HasUniformRatioGap a) (hfinite : FiniteDeletionComplete a) (hρ1 : 1 < ρ) (hρφ : ρ < Real.goldenRatio) (hupper : ∀ᶠ (n : ℕ) in Filter.atTop, quotient a n < ρ) (hcover : ArbitrarilyLargeFinSingletonFirstPrefixCover a) : ∃ (D : Set ℕ), D.Infinite ∧ IsCompleteOn a Dᶜ

theorem Erdos346.infCompleteDeletion_of_limit_lt_goldenRatio_of_eventual_finite_singleton_complete {a : ℕ → ℕ} {L : ℝ} {F : Set ℕ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hratioGap : HasUniformRatioGap a) (hlim : Filter.Tendsto (quotient a) Filter.atTop (nhds L)) (hL1 : 1 < L) (hlt : L < Real.goldenRatio) (hFfinite : F.Finite) (hfiniteSingleton : ∃ (H : ℕ), ∀ᶠ (M : ℕ) in Filter.atTop, ∀ (t : ℕ), H ≤ t → t ∈ subsetSums a (F ∪ {M + 1})ᶜ) : ∃ (D : Set ℕ), D.Infinite ∧ IsCompleteOn a Dᶜ

theorem Erdos346.infCompleteDeletion_of_limit_lt_goldenRatio_of_uniformFinSingletonPrefixCover {a : ℕ → ℕ} {L : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hratioGap : HasUniformRatioGap a) (hlim : Filter.Tendsto (quotient a) Filter.atTop (nhds L)) (hL1 : 1 < L) (hlt : L < Real.goldenRatio) (hprefix : UniformFinSingletonPrefixCover a) : ∃ (D : Set ℕ), D.Infinite ∧ IsCompleteOn a Dᶜ

theorem Erdos346.infCompleteDeletion_of_limit_lt_goldenRatio_of_eventualFinSingletonSmallPrefixCover {a : ℕ → ℕ} {L : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hlim : Filter.Tendsto (quotient a) Filter.atTop (nhds L)) (hL1 : 1 < L) (hlt : L < Real.goldenRatio) (hsmall : EventualFinSingletonSmallPrefixCover a) : ∃ (D : Set ℕ), D.Infinite ∧ IsCompleteOn a Dᶜ

theorem Erdos346.infCompleteDeletion_of_limit_lt_goldenRatio_of_arbLargeFinSingletonSmallPrefixCover {a : ℕ → ℕ} {L : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hlim : Filter.Tendsto (quotient a) Filter.atTop (nhds L)) (hL1 : 1 < L) (hlt : L < Real.goldenRatio) (hsmall : ArbitrarilyLargeFinSingletonSmallPrefixCover a) : ∃ (D : Set ℕ), D.Infinite ∧ IsCompleteOn a Dᶜ

theorem Erdos346.infCompleteDeletion_of_limit_lt_goldenRatio_of_arbLargeFinSingletonFirstSmallPrefixCover {a : ℕ → ℕ} {L : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hgap : HasUniformRatioGap a) (hfinite : FiniteDeletionComplete a) (hlim : Filter.Tendsto (quotient a) Filter.atTop (nhds L)) (hL1 : 1 < L) (hlt : L < Real.goldenRatio) (hfirst : ArbitrarilyLargeFinSingletonFirstSmallPrefixCover a) : ∃ (D : Set ℕ), D.Infinite ∧ IsCompleteOn a Dᶜ

theorem Erdos346.infCompleteDeletion_of_limit_lt_goldenRatio_of_arbLargeFinSingletonFirstPrefixCover {a : ℕ → ℕ} {L : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hgap : HasUniformRatioGap a) (hfinite : FiniteDeletionComplete a) (hlim : Filter.Tendsto (quotient a) Filter.atTop (nhds L)) (hL1 : 1 < L) (hlt : L < Real.goldenRatio) (hcover : ArbitrarilyLargeFinSingletonFirstPrefixCover a) : ∃ (D : Set ℕ), D.Infinite ∧ IsCompleteOn a Dᶜ

theorem Erdos346.infCompleteDeletion_of_limit_lt_goldenRatio {a : ℕ → ℕ} {L : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hgap : HasUniformRatioGap a) (hcomplete : IsCompleteOn a Set.univ) (hlim : Filter.Tendsto (quotient a) Filter.atTop (nhds L)) (hL1 : 1 < L) (hlt : L < Real.goldenRatio) : ∃ (D : Set ℕ), D.Infinite ∧ IsCompleteOn a Dᶜ

If the ratio limit lies strictly between 1 and φ, then one can delete an infinite, sufficiently sparse set of indices and still remain complete. The limit-to-eventual-bound part is proved here; the remaining sparse-deletion construction is isolated above.

Consequences of the inputs

theorem Erdos346.limit_le_goldenRatio {a : ℕ → ℕ} {L : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hfinite : FiniteDeletionComplete a) (hlim : Filter.Tendsto (quotient a) Filter.atTop (nhds L)) : L ≤ Real.goldenRatio

theorem Erdos346.goldenRatio_le_limit_of_eventual_finite_singleton_complete {a : ℕ → ℕ} {L : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hratioGap : HasUniformRatioGap a) (hinfinite : InfiniteDeletionIncomplete a) (hlim : Filter.Tendsto (quotient a) Filter.atTop (nhds L)) (hL1 : 1 < L) (hfiniteSingleton : ∃ (F : Set ℕ), F.Finite ∧ ∃ (H : ℕ), ∀ᶠ (M : ℕ) in Filter.atTop, ∀ (t : ℕ), H ≤ t → t ∈ subsetSums a (F ∪ {M + 1})ᶜ) : Real.goldenRatio ≤ L

theorem Erdos346.goldenRatio_le_limit_of_uniformFinSingletonPrefixCover {a : ℕ → ℕ} {L : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hratioGap : HasUniformRatioGap a) (hinfinite : InfiniteDeletionIncomplete a) (hlim : Filter.Tendsto (quotient a) Filter.atTop (nhds L)) (hL1 : 1 < L) (hprefix : UniformFinSingletonPrefixCover a) : Real.goldenRatio ≤ L

theorem Erdos346.goldenRatio_le_limit_of_eventualFinSingletonSmallPrefixCover {a : ℕ → ℕ} {L : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hinfinite : InfiniteDeletionIncomplete a) (hlim : Filter.Tendsto (quotient a) Filter.atTop (nhds L)) (hL1 : 1 < L) (hsmall : EventualFinSingletonSmallPrefixCover a) : Real.goldenRatio ≤ L

theorem Erdos346.goldenRatio_le_limit_of_arbLargeFinSingletonSmallPrefixCover {a : ℕ → ℕ} {L : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hinfinite : InfiniteDeletionIncomplete a) (hlim : Filter.Tendsto (quotient a) Filter.atTop (nhds L)) (hL1 : 1 < L) (hsmall : ArbitrarilyLargeFinSingletonSmallPrefixCover a) : Real.goldenRatio ≤ L

theorem Erdos346.goldenRatio_le_limit_of_arbLargeFinSingletonFirstSmallPrefixCover {a : ℕ → ℕ} {L : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hgap : HasUniformRatioGap a) (hfinite : FiniteDeletionComplete a) (hinfinite : InfiniteDeletionIncomplete a) (hlim : Filter.Tendsto (quotient a) Filter.atTop (nhds L)) (hL1 : 1 < L) (hfirst : ArbitrarilyLargeFinSingletonFirstSmallPrefixCover a) : Real.goldenRatio ≤ L

theorem Erdos346.goldenRatio_le_limit_of_arbLargeFinSingletonFirstPrefixCover {a : ℕ → ℕ} {L : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hgap : HasUniformRatioGap a) (hfinite : FiniteDeletionComplete a) (hinfinite : InfiniteDeletionIncomplete a) (hlim : Filter.Tendsto (quotient a) Filter.atTop (nhds L)) (hL1 : 1 < L) (hcover : ArbitrarilyLargeFinSingletonFirstPrefixCover a) : Real.goldenRatio ≤ L

theorem Erdos346.goldenRatio_le_limit_of_uniformFinSingletonComplete {a : ℕ → ℕ} {L : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hratioGap : HasUniformRatioGap a) (hinfinite : InfiniteDeletionIncomplete a) (hlim : Filter.Tendsto (quotient a) Filter.atTop (nhds L)) (hL1 : 1 < L) (huniform : UniformFinSingletonComplete a) : Real.goldenRatio ≤ L

theorem Erdos346.goldenRatio_le_limit {a : ℕ → ℕ} {L : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hratioGap : HasUniformRatioGap a) (hfinite : FiniteDeletionComplete a) (hinfinite : InfiniteDeletionIncomplete a) (hlim : Filter.Tendsto (quotient a) Filter.atTop (nhds L)) (hL1 : 1 < L) : Real.goldenRatio ≤ L

theorem Erdos346.ratio_limit_eq_goldenRatio {a : ℕ → ℕ} {L : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hratioGap : HasUniformRatioGap a) (hfinite : FiniteDeletionComplete a) (hinfinite : InfiniteDeletionIncomplete a) (hlim : Filter.Tendsto (quotient a) Filter.atTop (nhds L)) (hL1 : 1 < L) : L = Real.goldenRatio

Conditional value theorem for the interpretation where the ratio limit is assumed to exist and to be greater than one.

theorem Erdos346.ratio_limit_eq_goldenRatio_of_uniformFinSingletonComplete {a : ℕ → ℕ} {L : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hratioGap : HasUniformRatioGap a) (hfinite : FiniteDeletionComplete a) (hinfinite : InfiniteDeletionIncomplete a) (huniform : UniformFinSingletonComplete a) (hlim : Filter.Tendsto (quotient a) Filter.atTop (nhds L)) (hL1 : 1 < L) : L = Real.goldenRatio

Legacy conditional value theorem under the explicit uniform finite-base singleton completeness condition. The main theorem no longer needs this route, but it remains as a named sufficient condition for the older singleton-threshold approach.

theorem Erdos346.ratio_limit_eq_goldenRatio_of_uniformFinSingletonPrefixCover {a : ℕ → ℕ} {L : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hratioGap : HasUniformRatioGap a) (hfinite : FiniteDeletionComplete a) (hinfinite : InfiniteDeletionIncomplete a) (hprefix : UniformFinSingletonPrefixCover a) (hlim : Filter.Tendsto (quotient a) Filter.atTop (nhds L)) (hL1 : 1 < L) : L = Real.goldenRatio

A fully proved variant of the value theorem under the weaker uniform prefix cover condition used by the finite-initial-tail seed.

theorem Erdos346.ratio_limit_eq_goldenRatio_of_eventualFinSingletonSmallPrefixCover {a : ℕ → ℕ} {L : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hfinite : FiniteDeletionComplete a) (hinfinite : InfiniteDeletionIncomplete a) (hsmall : EventualFinSingletonSmallPrefixCover a) (hlim : Filter.Tendsto (quotient a) Filter.atTop (nhds L)) (hL1 : 1 < L) : L = Real.goldenRatio

Value theorem under the small, M-dependent prefix-cover window condition. This is weaker than the uniform prefix-cover condition: the threshold can vary with M, provided it is small enough for that M.

theorem Erdos346.ratio_limit_eq_goldenRatio_of_arbLargeFinSingletonSmallPrefixCover {a : ℕ → ℕ} {L : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hfinite : FiniteDeletionComplete a) (hinfinite : InfiniteDeletionIncomplete a) (hsmall : ArbitrarilyLargeFinSingletonSmallPrefixCover a) (hlim : Filter.Tendsto (quotient a) Filter.atTop (nhds L)) (hL1 : 1 < L) : L = Real.goldenRatio

Value theorem under the still weaker condition that suitable small finite-singleton windows occur arbitrarily far out.

theorem Erdos346.ratio_limit_eq_goldenRatio_of_arbLargeFinSingletonFirstSmallPrefixCover {a : ℕ → ℕ} {L : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hgap : HasUniformRatioGap a) (hfinite : FiniteDeletionComplete a) (hinfinite : InfiniteDeletionIncomplete a) (hfirst : ArbitrarilyLargeFinSingletonFirstSmallPrefixCover a) (hlim : Filter.Tendsto (quotient a) Filter.atTop (nhds L)) (hL1 : 1 < L) : L = Real.goldenRatio

Value theorem under the current weakest finite-window condition: arbitrarily far out, only the first seed inequality is assumed.

theorem Erdos346.ratio_limit_eq_goldenRatio_of_arbLargeFinSingletonFirstPrefixCover {a : ℕ → ℕ} {L : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hgap : HasUniformRatioGap a) (hfinite : FiniteDeletionComplete a) (hinfinite : InfiniteDeletionIncomplete a) (hcover : ArbitrarilyLargeFinSingletonFirstPrefixCover a) (hlim : Filter.Tendsto (quotient a) Filter.atTop (nhds L)) (hL1 : 1 < L) : L = Real.goldenRatio

Value theorem under the equivalent direct-cover form of the current weakest finite-window condition.

theorem Erdos346.ratio_tendsto_goldenRatio_of_limit_exists {a : ℕ → ℕ} {L : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hratioGap : HasUniformRatioGap a) (hfinite : FiniteDeletionComplete a) (hinfinite : InfiniteDeletionIncomplete a) (hlim : Filter.Tendsto (quotient a) Filter.atTop (nhds L)) (hL1 : 1 < L) : Filter.Tendsto (quotient a) Filter.atTop (nhds Real.goldenRatio)

Same theorem phrased as convergence to the golden ratio.

theorem Erdos346.ratio_tendsto_goldenRatio_of_limit_exists_of_uniformFinSingletonComplete {a : ℕ → ℕ} {L : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hratioGap : HasUniformRatioGap a) (hfinite : FiniteDeletionComplete a) (hinfinite : InfiniteDeletionIncomplete a) (huniform : UniformFinSingletonComplete a) (hlim : Filter.Tendsto (quotient a) Filter.atTop (nhds L)) (hL1 : 1 < L) : Filter.Tendsto (quotient a) Filter.atTop (nhds Real.goldenRatio)

Convergence form of ratio_limit_eq_goldenRatio_of_uniformFinSingletonComplete.

theorem Erdos346.ratio_tendsto_goldenRatio_of_limit_exists_of_uniformFinSingletonPrefixCover {a : ℕ → ℕ} {L : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hratioGap : HasUniformRatioGap a) (hfinite : FiniteDeletionComplete a) (hinfinite : InfiniteDeletionIncomplete a) (hprefix : UniformFinSingletonPrefixCover a) (hlim : Filter.Tendsto (quotient a) Filter.atTop (nhds L)) (hL1 : 1 < L) : Filter.Tendsto (quotient a) Filter.atTop (nhds Real.goldenRatio)

Convergence form of ratio_limit_eq_goldenRatio_of_uniformFinSingletonPrefixCover.

theorem Erdos346.ratio_tendsto_goldenRatio_of_limit_exists_of_eventualFinSingletonSmallPrefixCover {a : ℕ → ℕ} {L : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hfinite : FiniteDeletionComplete a) (hinfinite : InfiniteDeletionIncomplete a) (hsmall : EventualFinSingletonSmallPrefixCover a) (hlim : Filter.Tendsto (quotient a) Filter.atTop (nhds L)) (hL1 : 1 < L) : Filter.Tendsto (quotient a) Filter.atTop (nhds Real.goldenRatio)

Convergence form of ratio_limit_eq_goldenRatio_of_eventualFinSingletonSmallPrefixCover.

theorem Erdos346.ratio_tendsto_goldenRatio_of_limit_exists_of_arbLargeFinSingletonSmallPrefixCover {a : ℕ → ℕ} {L : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hfinite : FiniteDeletionComplete a) (hinfinite : InfiniteDeletionIncomplete a) (hsmall : ArbitrarilyLargeFinSingletonSmallPrefixCover a) (hlim : Filter.Tendsto (quotient a) Filter.atTop (nhds L)) (hL1 : 1 < L) : Filter.Tendsto (quotient a) Filter.atTop (nhds Real.goldenRatio)

Convergence form of ratio_limit_eq_goldenRatio_of_arbLargeFinSingletonSmallPrefixCover.

theorem Erdos346.ratio_tendsto_goldenRatio_of_limit_exists_of_arbLargeFinSingletonFirstSmallPrefixCover {a : ℕ → ℕ} {L : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hgap : HasUniformRatioGap a) (hfinite : FiniteDeletionComplete a) (hinfinite : InfiniteDeletionIncomplete a) (hfirst : ArbitrarilyLargeFinSingletonFirstSmallPrefixCover a) (hlim : Filter.Tendsto (quotient a) Filter.atTop (nhds L)) (hL1 : 1 < L) : Filter.Tendsto (quotient a) Filter.atTop (nhds Real.goldenRatio)

Convergence form of ratio_limit_eq_goldenRatio_of_arbLargeFinSingletonFirstSmallPrefixCover.

theorem Erdos346.ratio_tendsto_goldenRatio_of_limit_exists_of_arbLargeFinSingletonFirstPrefixCover {a : ℕ → ℕ} {L : ℝ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hgap : HasUniformRatioGap a) (hfinite : FiniteDeletionComplete a) (hinfinite : InfiniteDeletionIncomplete a) (hcover : ArbitrarilyLargeFinSingletonFirstPrefixCover a) (hlim : Filter.Tendsto (quotient a) Filter.atTop (nhds L)) (hL1 : 1 < L) : Filter.Tendsto (quotient a) Filter.atTop (nhds Real.goldenRatio)

Convergence form of ratio_limit_eq_goldenRatio_of_arbLargeFinSingletonFirstPrefixCover.

theorem Erdos346.intended_problem_if_limit_exists {a : ℕ → ℕ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hratioGap : HasUniformRatioGap a) (hfinite : FiniteDeletionComplete a) (hinfinite : InfiniteDeletionIncomplete a) (hexists : ∃ (L : ℝ), 1 < L ∧ Filter.Tendsto (quotient a) Filter.atTop (nhds L)) : Filter.Tendsto (quotient a) Filter.atTop (nhds Real.goldenRatio)

Compact formulation: if a ratio limit L > 1 exists, then it is φ.

theorem Erdos346.intended_problem_if_limit_exists_of_uniformFinSingletonComplete {a : ℕ → ℕ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hratioGap : HasUniformRatioGap a) (hfinite : FiniteDeletionComplete a) (hinfinite : InfiniteDeletionIncomplete a) (huniform : UniformFinSingletonComplete a) (hexists : ∃ (L : ℝ), 1 < L ∧ Filter.Tendsto (quotient a) Filter.atTop (nhds L)) : Filter.Tendsto (quotient a) Filter.atTop (nhds Real.goldenRatio)

Compact formulation of the axiom-free conditional route using the explicit uniform finite-base singleton completeness hypothesis.

theorem Erdos346.intended_problem_if_limit_exists_of_uniformFinSingletonPrefixCover {a : ℕ → ℕ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hratioGap : HasUniformRatioGap a) (hfinite : FiniteDeletionComplete a) (hinfinite : InfiniteDeletionIncomplete a) (hprefix : UniformFinSingletonPrefixCover a) (hexists : ∃ (L : ℝ), 1 < L ∧ Filter.Tendsto (quotient a) Filter.atTop (nhds L)) : Filter.Tendsto (quotient a) Filter.atTop (nhds Real.goldenRatio)

Compact formulation of the axiom-free conditional route using only the weaker uniform finite-base prefix-cover hypothesis.

theorem Erdos346.intended_problem_if_limit_exists_of_eventualFinSingletonSmallPrefixCover {a : ℕ → ℕ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hfinite : FiniteDeletionComplete a) (hinfinite : InfiniteDeletionIncomplete a) (hsmall : EventualFinSingletonSmallPrefixCover a) (hexists : ∃ (L : ℝ), 1 < L ∧ Filter.Tendsto (quotient a) Filter.atTop (nhds L)) : Filter.Tendsto (quotient a) Filter.atTop (nhds Real.goldenRatio)

Compact formulation of the axiom-free conditional route using the M-dependent small prefix-cover window condition.

theorem Erdos346.intended_problem_if_limit_exists_of_arbLargeFinSingletonSmallPrefixCover {a : ℕ → ℕ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hfinite : FiniteDeletionComplete a) (hinfinite : InfiniteDeletionIncomplete a) (hsmall : ArbitrarilyLargeFinSingletonSmallPrefixCover a) (hexists : ∃ (L : ℝ), 1 < L ∧ Filter.Tendsto (quotient a) Filter.atTop (nhds L)) : Filter.Tendsto (quotient a) Filter.atTop (nhds Real.goldenRatio)

Compact formulation using only arbitrarily late good finite-singleton prefix-cover windows.

theorem Erdos346.intended_problem_if_limit_exists_of_arbLargeFinSingletonFirstSmallPrefixCover {a : ℕ → ℕ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hgap : HasUniformRatioGap a) (hfinite : FiniteDeletionComplete a) (hinfinite : InfiniteDeletionIncomplete a) (hfirst : ArbitrarilyLargeFinSingletonFirstSmallPrefixCover a) (hexists : ∃ (L : ℝ), 1 < L ∧ Filter.Tendsto (quotient a) Filter.atTop (nhds L)) : Filter.Tendsto (quotient a) Filter.atTop (nhds Real.goldenRatio)

Compact formulation using only arbitrarily late first seed inequalities.

theorem Erdos346.intended_problem_if_limit_exists_of_arbLargeFinSingletonFirstPrefixCover {a : ℕ → ℕ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hgap : HasUniformRatioGap a) (hfinite : FiniteDeletionComplete a) (hinfinite : InfiniteDeletionIncomplete a) (hcover : ArbitrarilyLargeFinSingletonFirstPrefixCover a) (hexists : ∃ (L : ℝ), 1 < L ∧ Filter.Tendsto (quotient a) Filter.atTop (nhds L)) : Filter.Tendsto (quotient a) Filter.atTop (nhds Real.goldenRatio)

Compact formulation using the direct finite-prefix cover of the first seed window [nextSeedMargin a M, a (M + 2) - 1].

theorem Erdos346.intended_problem_if_limit_exists_of_arbLargeFinSingletonFirstWindowShiftClosed {a : ℕ → ℕ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hgap : HasUniformRatioGap a) (hfinite : FiniteDeletionComplete a) (hinfinite : InfiniteDeletionIncomplete a) (hclosed : ArbitrarilyLargeFinSingletonFirstWindowShiftClosed a) (hexists : ∃ (L : ℝ), 1 < L ∧ Filter.Tendsto (quotient a) Filter.atTop (nhds L)) : Filter.Tendsto (quotient a) Filter.atTop (nhds Real.goldenRatio)

Compact formulation using the local first-window shift-closure condition. Finite-deletion completeness supplies the prefix cover through M + 1; the shift-closure condition is exactly what lowers that cover to the prefix through M.

theorem Erdos346.intended_problem_if_limit_exists_of_arbLargeFinSingletonCompleteBelowPrev {a : ℕ → ℕ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hgap : HasUniformRatioGap a) (hfinite : FiniteDeletionComplete a) (hinfinite : InfiniteDeletionIncomplete a) (hbelow : ArbitrarilyLargeFinSingletonCompleteBelowPrev a) (hexists : ∃ (L : ℝ), 1 < L ∧ Filter.Tendsto (quotient a) Filter.atTop (nhds L)) : Filter.Tendsto (quotient a) Filter.atTop (nhds Real.goldenRatio)

Compact formulation using the moving singleton-deletion threshold condition: arbitrarily far out, after deleting F ∪ {M + 1}, completeness starts no later than a (M + 1).

theorem Erdos346.intended_problem_if_limit_exists_of_eventualFinSingletonLeastSmallPrefixCover {a : ℕ → ℕ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hfinite : FiniteDeletionComplete a) (hinfinite : InfiniteDeletionIncomplete a) (hleast : EventualFinSingletonLeastSmallPrefixCover a) (hexists : ∃ (L : ℝ), 1 < L ∧ Filter.Tendsto (quotient a) Filter.atTop (nhds L)) : Filter.Tendsto (quotient a) Filter.atTop (nhds Real.goldenRatio)

Compact formulation using the least-threshold phrasing of the small finite-window condition.

theorem Erdos346.intended_problem_if_limit_exists_of_arbLargeFinSingletonLeastSmallPrefixCover {a : ℕ → ℕ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hfinite : FiniteDeletionComplete a) (hinfinite : InfiniteDeletionIncomplete a) (hleast : ArbitrarilyLargeFinSingletonLeastSmallPrefixCover a) (hexists : ∃ (L : ℝ), 1 < L ∧ Filter.Tendsto (quotient a) Filter.atTop (nhds L)) : Filter.Tendsto (quotient a) Filter.atTop (nhds Real.goldenRatio)

Compact formulation using the least-threshold phrasing of the arbitrarily late small finite-window condition.

theorem Erdos346.main {a : ℕ → ℕ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hratioGap : HasUniformRatioGap a) (hfinite : FiniteDeletionComplete a) (hinfinite : InfiniteDeletionIncomplete a) (hexists : ∃ (L : ℝ), 1 < L ∧ Filter.Tendsto (quotient a) Filter.atTop (nhds L)) : Filter.Tendsto (quotient a) Filter.atTop (nhds Real.goldenRatio)

Short public-facing name for the main theorem.

theorem Erdos346.main_expanded {a : ℕ → ℕ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hratioGap : ∃ (ε : ℝ), 0 < ε ∧ ∀ (n : ℕ), 1 + ε ≤ quotient a n) (hfinite : ∀ (D : Set ℕ), D.Finite → ∃ (H : ℕ), ∀ (n : ℕ), H ≤ n → n ∈ subsetSums a Dᶜ) (hinfinite : ∀ (D : Set ℕ), D.Infinite → ¬∃ (H : ℕ), ∀ (n : ℕ), H ≤ n → n ∈ subsetSums a Dᶜ) (hexists : ∃ (L : ℝ), 1 < L ∧ Filter.Tendsto (quotient a) Filter.atTop (nhds L)) : Filter.Tendsto (quotient a) Filter.atTop (nhds Real.goldenRatio)

Expanded statement for human inspection.

This is definitionally the same theorem as main, but the three compact hypotheses HasUniformRatioGap, FiniteDeletionComplete, and InfiniteDeletionIncomplete are expanded in the theorem statement.

theorem Erdos346.main_valueDeletion {a : ℕ → ℕ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hratioGap : HasUniformRatioGap a) (hfinite : ValueFiniteDeletionComplete a) (hinfinite : ValueInfiniteDeletionIncomplete a) (hexists : ∃ (L : ℝ), 1 < L ∧ Filter.Tendsto (quotient a) Filter.atTop (nhds L)) : Filter.Tendsto (quotient a) Filter.atTop (nhds Real.goldenRatio)

Public-facing theorem using value deletion rather than index deletion. Finite and infinite deletion hypotheses are stated for sets B : Set ℕ of sequence values.

theorem Erdos346.main_valueDeletion_expanded {a : ℕ → ℕ} (hmono : StrictMono a) (hpos : ∀ (n : ℕ), 0 < a n) (hratioGap : ∃ (ε : ℝ), 0 < ε ∧ ∀ (n : ℕ), 1 + ε ≤ quotient a n) (hfinite : ∀ (B : Set ℕ), B.Finite → ∃ (H : ℕ), ∀ (n : ℕ), H ≤ n → n ∈ subsetSums a {i : ℕ | a i ∉ B}) (hinfinite : ∀ (B : Set ℕ), B.Infinite → B ⊆ Set.range a → ¬∃ (H : ℕ), ∀ (n : ℕ), H ≤ n → n ∈ subsetSums a {i : ℕ | a i ∉ B}) (hexists : ∃ (L : ℝ), 1 < L ∧ Filter.Tendsto (quotient a) Filter.atTop (nhds L)) : Filter.Tendsto (quotient a) Filter.atTop (nhds Real.goldenRatio)

Expanded value-deletion statement for human inspection.