erdos_138.variants.difference.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 348 curated AI-written annotations and 373 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 12 manuscript-grounded curated result annotations were composed from pinned companion PDFs and named source records in a Codex session on 2026-10-14; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. Twelve supporting declarations for the Hilbert-functions result were upgraded on 2026-10-14 from mechanically condensed doc comments to declaration-specific explanations bound to exact page-one terminology in the pinned human-written companion. The other Hilbert challenge statements were deliberately not described as companion-backed results because that manuscript proves P5 specifically. Fifteen previously unannotated declarations along the Hilbert P5 proof spine were annotated on 2026-10-14 from the pinned companion's seven-page argument, covering the two-generator decomposition, finite-difference bounds, critical-case reduction, and final log-concavity step. Each quotation is bound to its exact manuscript page and Lean declaration; no human review is claimed. Twenty-four further declarations along the Hilbert P5 box-count and finite-difference spine were annotated on 2026-10-14, covering the two-dimensional slice count, three-dimensional box formula, first- and second-difference identities, the seven-threshold curvature expression, boundary handling, pointwise transport, sum linearity, and lower-or-upper region classification. Every annotation is bound to an exact quotation on pages 2 or 3 of the pinned human-written companion; Lean-specific boundary and threshold helpers are identified as implementation lemmas rather than separate manuscript claims. No human review is claimed. Twenty-eight further declarations along the Hilbert P5 argument were annotated on 2026-10-14 from pages 2 through 6 of the pinned human-written companion. They expose the shifted residual sequence, exact lower- and upper-region formulas, symmetry by complementary divisors, the curvature-one and curvature-two splits, and the final algebraic reductions. Lean-only transport and integer-arithmetic helpers are labeled as proof infrastructure rather than new manuscript claims; each quotation is page-bound in the source ledger, and no human review is claimed. Twenty high-level declarations completing the Hilbert P5 curvature-one and curvature-two case spine were annotated on 2026-10-14 from pages 3 through 7 of the pinned human-written companion. The explanations separate cases A and B, lower and upper monomial regions, shifted residual evaluation, impossible mixed regions, and the surviving upper-upper estimate; wrapper lemmas are explicitly described as proof structure. Every quotation is page-bound, and no human review is claimed. Twenty-two graph-reconstruction declarations were upgraded or added on 2026-10-14 from the pinned four-page human-written companion, covering the incidence-deletion deck, edge and degree recovery, unique isolated vertices, vertex-type reconstruction, neighboring-type descent, adjacency recovery, and final bipartite isomorphism. The result annotation also records that `G_not_regular` is present in the Lean statement but unused by its proof term and absent from the companion theorem. Exact historical quotations from Paul J. Kelly (1957) and Bondy with Hemminger (1977) are linked separately; no human review is claimed. Eighteen declarations along the Erdős 741(i) strict-natural-density counterexample were added on 2026-10-14, covering the carry-free base-four digit split, full cross-sum coverage, sparse pure self-sums, fixed-factor fat intervals, the lower-scale density deficit, upper-scale sum growth, and the final convergence contradiction. The result annotation was corrected to distinguish the negative strict-natural-density Lean theorem from the compatible affirmative upper-density companion theorem; Ulam AI's written counterexample is explicitly identified as using a different interval length with the same mechanism. The quotations are page- and hash-bound where the PDFs expose text; Paul Erdős's scanned 1994 question was visually checked and is linked separately without a machine-audit claim. No human review is claimed. Twenty-eight additional declaration-level annotations were added on 2026-10-14 for the Erdős 12(i) proof, and its IsGood definition was upgraded from a source-comment condensation. They cover the prime and Chinese-remainder moduli, the actual Lean congruence-block witness, exclusion of cross-block and same-block triples, lower and upper counting bounds, and the positive liminf. The prior result annotation was corrected because the pinned human-written companion proves the same theorem with a different base-2-to-base-3 construction; it is no longer presented as the Lean proof. The original property-P definition from Erdős and Sárközy (1970) is separately linked and page-bound; no human review is claimed. The remaining fifty declarations in the Erdős 12(i) file were annotated on 2026-10-14, completing declaration-level coverage of all eighty definitions, lemmas, and theorems in that file. These additions expose the prime-recursion invariants, divisibility transport, Chinese-remainder witness bounds, numerical density envelopes, injective block coding, and liminf support lemmas instead of leaving the proof spine as raw Lean; no human review is claimed. Eighteen supporting declarations for Erdős 125 were added on 2026-10-14, completing all nineteen declarations in the file. The annotations follow the pinned companion through digit-block decomposition, irrational logarithmic approximation, the explicit Lean contraction factor 11/12, geometric iteration, and the lower-density conclusion. The original 1996 question of Burr, Erdős, Graham, and Li and the 2026 discussion contributions of GTSoukalas, Terence Tao, and Giuseppe Melfi are linked separately; no human review is claimed. Twenty-eight supporting declarations for Erdős 138 were upgraded or added on 2026-10-14, completing all twenty-nine declarations in the file. The annotations separate the greedy difference proof from the Lean-specific representation bridges and ultrafilter compactness proof of existence, and bind quotations from the pinned companion, the AlphaProof Nexus paper, Erdős's 1981 source, van der Waerden's recollection, and the 2026 Erdős Problems discussion. No human review is claimed. The curated Erdős 12(ii), 138, and 152 annotations were further linked on 2026-10-14 to exact quotations from Felix Behrend, Bartel van der Waerden, and Paul Erdős with Pál Turán; the historical quotation sources are labeled separately from the pinned AlphaProof proof companions. The curated Hilbert-functions result, its OrderIdeal and pureOSequence definitions, and the Erdős 846 annotation were further linked on 2026-10-14 to exact quotations from Richard P. Stanley and from Moe Putterman, Mehtaab Sawhney, and Gregory Valiant. The Stanley PDF is hash- and page-bound in the source ledger; these historical sources are labeled separately from the pinned AlphaProof proof companions. Three additional target-specific annotations for Ben Green's Problem 57, exact last-iterate anchored-GDA convergence, and Graffiti.pc Conjecture 2 were composed on 2026-10-14 from the exact pinned Lean statements, quotations from the AlphaProof Nexus paper, and quotations from Green, Ryu with Yuan and Yin, Surina et al., and Wang with Dai and Tong; no human review is claimed. Two additional target-specific quantum-optics annotations for the explicit AME(11,5) construction and the even N >= 4, D = N monochromatic-quantum-graph theorem were composed on 2026-10-14 from the exact pinned Lean statements, page-bound quotations from the AlphaProof Nexus paper, Helwig et al., and Krenn, Gu, and Zeilinger, and Mario Krenn's public priority correction. The AME annotation makes no first-discovery claim; the monochromatic annotation states that the local AlphaProof wrapper contains sorry and links the separate pinned proof-bearing Formal Conjectures artifact without silently treating it as local verification. Twelve declarations that the pinned source repeats verbatim in several files were annotated in only one of the copies, so the build rejected them as differing copies. On 2026-10-16 each curated annotation was copied unchanged to every identical copy: the eleven Hilbert-functions definitions from hilbert_functions_5 to hilbert_functions_1, _2, _3, _4, _7 and _8, and Erdos12.IsGood from erdos_12.parts.i to erdos_12.parts.ii (the better-sourced annotation was kept in each case). Each copy's quotations are bound in the source ledger like the original's; no new text was written and no human review is claimed. The remaining source-derived annotations were generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the source prose.

Credit: Google DeepMind published the AlphaProof Nexus proof artifacts. The pinned repository identifies the mathematical sources and collaborators, including OEIS, Erdős Problems, Gergely Bérczi, and Mario Krenn; those source records remain the authority for individual credit.

Project sources: Pinned AlphaProof Nexus results documentation, AlphaProof Nexus paper, Pinned human-written natural-language proof companions

29 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)

FormalConjectures.Util.ProblemImports

def Erdos138.monoAP_guarantee_set Interval lengths that force a monochromatic arithmetic progression line 51 source
Source documentation
The set of natural numbers that guarantee a monochromatic arithmetic progression.
A number N belongs to this set if, for a given number of colors r and an arithmetic progression length k, any r-coloring of the integers {1, ..., N} must contain a monochromatic arithmetic progression of length k.
L4DEL explanation
contains a monochromatic l-term arithmetic progression.
— Blondal and Jungić, Proof of van der Waerden's Theorem in Nine Figures (2018), p. 162
monoAP_guarantee_set r k contains exactly those natural numbers N for which every r-colouring of {1,...,N} contains a monochromatic arithmetic progression of length k.
1. Membership is the forcing property itself; it does not yet choose the least such interval length.
2. The colouring is represented as a function from Finset.Icc 1 N to Fin r, so the domain and the number of colours are encoded in its type.
Sources and attribution: Pinned Lean source (0647711a7118), Pinned AlphaProof Nexus Lean proof for Erdős 138, Blondal and Jungić, Proof of van der Waerden's Theorem in Nine Figures (2018), p. 162
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Set
Proof uses: setOf, Subtype, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, Fin, ContainsMonoAPofLength
8 instances, coercions and auxiliary constants left out.
```
def monoAP_guarantee_set (r k : ℕ) : Set ℕ :=
…
```
def Erdos138.monoAPNumber The least interval length that forces a monochromatic progression line 59 source
Source documentation
The van der Waerden number, is the smallest integer N such that any r-coloring of {1, ..., N} is guaranteed to contain a monochromatic arithmetic progression of length k. It is defined as the infimum of the (non-empty) set of all such numbers N.
L4DEL explanation
The smallest N guaranteed by the theorem is often denoted by W(l, k) and called a van der Waerden number.
— Blondal and Jungić, Proof of van der Waerden's Theorem in Nine Figures (2018), p. 163
monoAPNumber r k is the infimum of the forcing set, hence the formal van der Waerden number for r colours and progression length k once that set is known to be nonempty.
1. The definition is noncomputable: it specifies the least forcing length mathematically rather than giving an algorithm for calculating it.
2. Nonemptiness is not hidden in this definition; W_is_nonempty proves it later from van der Waerden's theorem through an ultrafilter compactness argument.
Sources and attribution: Pinned Lean source (0647711a7118), Pinned AlphaProof Nexus Lean proof for Erdős 138, Blondal and Jungić, Proof of van der Waerden's Theorem in Nine Figures (2018), p. 163
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: InfSet.sInf, Erdos138.monoAP_guarantee_set
1 instances, coercions and auxiliary constants left out.
```
noncomputable def monoAPNumber (r k : ℕ) : ℕ := sInf (monoAP_guarantee_set r k)
```
Mentions: Erdos138.monoAP_guarantee_set
abbrev Erdos138.W The two-colour van der Waerden number W(k) line 66 source
Source documentation
An abbreviation for the van der Waerden number for 2 colors, commonly written as W(k). This represents the smallest integer N such that any 2-coloring of {1, ..., N} must contain a monochromatic arithmetic progression of length k.
L4DEL explanation
W abbreviates monoAPNumber 2, so W k is the least interval length that forces a monochromatic k-term arithmetic progression under every red-blue colouring.
1. This is an abbreviation, not a new theorem: Lean unfolds it to the two-colour specialization of monoAPNumber whenever needed.
Sources and attribution: Pinned Lean source (0647711a7118), Pinned AlphaProof Nexus Lean proof for Erdős 138, Blondal and Jungić, Proof of van der Waerden's Theorem in Nine Figures (2018), p. 163
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Erdos138.monoAPNumber, OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
```
noncomputable abbrev W : ℕ → ℕ := monoAPNumber 2
…
```
Mentions: Erdos138.monoAPNumber
def Erdos138.HasMonoAP An explicit monochromatic arithmetic progression inside [1,N] line 103 source
L4DEL explanation
An l-term arithmetic progression is a set of the form {a, a + d,..., a + (l − 1)d}.
— Blondal and Jungić, Proof of van der Waerden's Theorem in Nine Figures (2018), p. 163
HasMonoAP c N k supplies a first term a and positive step d such that all k terms a+m*d have colour c a, start at or above 1, and end at or before N.
1. The endpoint bound is written a+(k-1)*d≤N; the colour condition quantifies over every index m<k.
2. This whole-number formulation is convenient for extending a colouring one integer at a time; two later bridge lemmas connect it to Mathlib's set-valued ContainsMonoAPofLength predicate.
Sources and attribution: Pinned Lean source (0647711a7118), Pinned AlphaProof Nexus Lean proof for Erdős 138, Blondal and Jungić, Proof of van der Waerden's Theorem in Nine Figures (2018), p. 163
no axioms what this means
Statement uses: Nat, Fin, OfNat.ofNat
Proof uses: Exists, And, GT.gt, GE.ge, LE.le, HAdd.hAdd, HMul.hMul, HSub.hSub, LT.lt, Eq
10 instances, coercions and auxiliary constants left out.
```
def HasMonoAP (c : ℕ → Fin 2) (N k : ℕ) : Prop :=
…
```
lemma Erdos138.ap_must_end Any newly created (k+1)-progression must end at the new point line 111 source
L4DEL explanation
the (k + 1)-th element for both progressions lands exactly on M + 1
— Human-written proof companion for Erdős 138
If the old colouring has no (k+1)-term progression through N+i, but assigning a colour at N+i+1 creates one, that progression must use N+i+1 as its last term.
1. If its endpoint were at most N+i, every one of its terms would retain the old colour, contradicting the hypothesis that the old interval had no such progression.
2. Removing the final term leaves k old points of the newly assigned colour, a structure used to compare the two blocked colour choices.
Sources and attribution: Pinned Lean source (0647711a7118), Pinned AlphaProof Nexus Lean proof for Erdős 138, Human-written proof companion for Erdős 138
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Fin, OfNat.ofNat, Not, Erdos138.HasMonoAP, HAdd.hAdd, ite, Eq, Exists, And, GT.gt, GE.ge, HMul.hMul, LT.lt
Proof uses: LE.le, HSub.hSub, Decidable.byContradiction, Eq.mp, congrArg, Exists.intro, Eq.mpr, id, Ne, Nat.mul_le_mul_right, Nat.le_add_right, if_neg, And.intro, Nat.mul_lt_mul_of_pos_right, Nat.mul_pos, if_pos, Eq.refl
32 instances, coercions and auxiliary constants left out.

Tactic trace: 50 steps
Open to load the checked before-and-after goal states.
```
lemma ap_must_end (k i N : ℕ) (c : ℕ → Fin 2) (color : Fin 2)
  (h_no_ap_k1 : ¬ HasMonoAP c (N + i) (k + 1))
  (h_has : HasMonoAP (fun x => if x = N + i + 1 then color else c x) (N + i + 1) (k + 1)) :
  ∃ a d, d > 0 ∧ a ≥ 1 ∧ a + k * d = N + i + 1 ∧
         (∀ m < k, c (a + m * d) = color) := by
…
```
Mentions: Erdos138.HasMonoAP
lemma Erdos138.extend_one_step At least one colour safely extends the progression-free interval line 161 source
L4DEL explanation
both calculations land exactly on the positive integer M + 1 − dR dB
— Human-written proof companion for Erdős 138
The only way this algorithm could result in an invalid coloring is if both choices are blocked
— George Tsoukalas et al., AlphaProof Nexus paper, Erdős 138 appendix
any two arithmetic progressions of length k and step size <k with the same start/end point must have at least one other point in common
— Erdős Problems 138 discussion (Adam Zsolt Wagner and Thomas Bloom)
While fewer than k new points have been appended, a two-colouring with no old k-progression and no current (k+1)-progression can always colour the next point without creating a (k+1)-progression.
1. If both colours were blocked, ap_must_end would produce a red and a blue k-term prefix ending at the same new point.
2. Each step size is at most i; a larger step would put the entire k-term prefix inside the original interval and contradict the absence of an old k-progression.
3. Stepping back d₁ places along the colour-0 progression and d₀ places along the colour-1 progression reaches the same integer N+i+1-d₀d₁, forcing it to have both colours.
Sources and attribution: Pinned Lean source (0647711a7118), Pinned AlphaProof Nexus Lean proof for Erdős 138, Human-written proof companion for Erdős 138, George Tsoukalas et al., AlphaProof Nexus paper, Erdős 138 appendix, Erdős Problems 138 discussion (Adam Zsolt Wagner and Thomas Bloom)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, OfNat.ofNat, GT.gt, LT.lt, Not, Erdos138.HasMonoAP, HAdd.hAdd, Exists, ite, Eq
Proof uses: Decidable.byContradiction, Eq.mp, Eq.trans, binderNameHint, forall_congr, And, GE.ge, HMul.hMul, Erdos138.ap_must_end, False, LE.le, HSub.hSub, Nat.sub_mul, Nat.one_mul, congrArg, Eq.mpr, id, Nat.mul_le_mul_right, Exists.intro, Eq.refl and 6 more
46 instances, coercions and auxiliary constants left out.

Tactic trace: 94 steps
Open to load the checked before-and-after goal states.
```
lemma extend_one_step (k i N : ℕ) (c : ℕ → Fin 2)
  (hk : k > 0)
  (hi : i < k)
  (h_no_ap_k : ¬ HasMonoAP c N k)
  (h_no_ap_k1 : ¬ HasMonoAP c (N + i) (k + 1)) :
  ∃ color : Fin 2, ¬ HasMonoAP (fun x => if x = N + i + 1 then color else c x) (N + i + 1) (k + 1) := by
…
```
Mentions: Erdos138.HasMonoAP
lemma Erdos138.has_mono_ap_ext The progression predicate depends only on colours inside [1,N] line 258 source
L4DEL explanation
a k-colouring of a set A is any function c : A → B
— Blondal and Jungić, Proof of van der Waerden's Theorem in Nine Figures (2018), p. 162
If two total colourings agree at every positive integer at most N, then either both contain a monochromatic k-term progression inside that interval or neither does.
1. The endpoint inequality places the first term and every indexed term within the agreement range, so the same witnesses a,d transfer in both directions.
Sources and attribution: Pinned Lean source (0647711a7118), Pinned AlphaProof Nexus Lean proof for Erdős 138, Blondal and Jungić, Proof of van der Waerden's Theorem in Nine Figures (2018), p. 162
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Fin, OfNat.ofNat, LE.le, GE.ge, Eq, Iff, Erdos138.HasMonoAP
Proof uses: Iff.intro, Exists, And, GT.gt, HAdd.hAdd, HMul.hMul, HSub.hSub, LT.lt, Exists.intro, And.intro, Decidable.byContradiction, Not, Nat.mul_le_mul_right, Eq.mpr, id, congrArg, Eq.symm
18 instances, coercions and auxiliary constants left out.

Tactic trace: 33 steps
Open to load the checked before-and-after goal states.
```
lemma has_mono_ap_ext (c1 c2 : ℕ → Fin 2) (N k : ℕ)
  (h_eq : ∀ x ≤ N, x ≥ 1 → c1 x = c2 x) :
  HasMonoAP c1 N k ↔ HasMonoAP c2 N k := by
…
```
Mentions: Erdos138.HasMonoAP
lemma Erdos138.extend_j_steps Iterating the safe extension for up to k new points line 287 source
L4DEL explanation
we can extend it by k further elements without creating a monochromatic (k + 1)-AP
— Human-written proof companion for Erdős 138
From a colouring of [1,N] with no monochromatic k-term progression, the lemma constructs a colouring through N+j, for every j≤k, with no monochromatic (k+1)-term progression and with all original colours preserved.
1. At j=0, any (k+1)-progression would already contain a forbidden k-term prefix.
2. The successor case first transfers the old k-progression-free property to the current extension, then invokes extend_one_step and proves the new assignment does not alter positions at most N.
Sources and attribution: Pinned Lean source (0647711a7118), Pinned AlphaProof Nexus Lean proof for Erdős 138, Human-written proof companion for Erdős 138
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, OfNat.ofNat, GT.gt, LE.le, Not, Erdos138.HasMonoAP, Exists, And, Eq, HAdd.hAdd
Proof uses: Nat.recAux, Exists.intro, And.intro, rfl, id, GE.ge, HMul.hMul, HSub.hSub, LT.lt, False, Decidable.byContradiction, Nat.mul_le_mul_right, Eq.mp, congrArg, Eq.mpr, Eq.symm, propext, Erdos138.has_mono_ap_ext, ite, Erdos138.extend_one_step and 2 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 50 steps
Open to load the checked before-and-after goal states.
```
lemma extend_j_steps (k N j : ℕ) (c : ℕ → Fin 2) (hk : k > 0)
  (hj : j ≤ k)
  (h_no_ap_k : ¬ HasMonoAP c N k) :
  ∃ c' : ℕ → Fin 2, (∀ x ≤ N, c' x = c x) ∧ ¬ HasMonoAP c' (N + j) (k + 1) := by
…
```
Mentions: Erdos138.HasMonoAP
def Erdos138.extend_coloring Extend a finite interval colouring to every natural number line 335 source
L4DEL explanation
extend_coloring N c agrees with the subtype-valued colouring c on {1,...,N} and assigns colour 0 everywhere outside that interval.
1. The arbitrary outside value is bookkeeping only: every later use proves that the progression under discussion lies in the original interval.
Sources and attribution: Pinned Lean source (0647711a7118), Pinned AlphaProof Nexus Lean proof for Erdős 138, Blondal and Jungić, Proof of van der Waerden's Theorem in Nine Figures (2018), p. 162
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Subtype, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, Fin
Proof uses: dite, Subtype.mk, Not
15 instances, coercions and auxiliary constants left out.
```
def extend_coloring (N : ℕ) (c : Finset.Icc 1 N → Fin 2) : ℕ → Fin 2 :=
…
```
def Erdos138.ap_equiv Indexing a positive-step arithmetic progression by Fin k line 338 source
L4DEL explanation
For d>0, the map m ↦ a+m*d is an equivalence from the k indices to the set of the first k terms of the arithmetic progression.
1. The inverse recovers the index as (x-a)/d; positivity of d makes multiplication injective and validates the division identities.
Sources and attribution: Pinned Lean source (0647711a7118), Pinned AlphaProof Nexus Lean proof for Erdős 138, Blondal and Jungić, Proof of van der Waerden's Theorem in Nine Figures (2018), p. 163
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, GT.gt, OfNat.ofNat, Equiv, Fin, setOf, Exists, And, LT.lt, Eq, HAdd.hAdd, HMul.hMul
Proof uses: Equiv.mk, Subtype.mk, Membership.mem, Set, Fin.mk, HDiv.hDiv, HSub.hSub
25 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
```
def ap_equiv (a d k : ℕ) (hd : d > 0) : Fin k ≃ { x : ℕ | ∃ m < k, x = a + m * d } where
…
```
lemma Erdos138.card_ap_eq_k A positive-step k-term progression has exactly k elements line 365 source
L4DEL explanation
The underlying set {a+m*d | m<k} has extended-natural cardinality k whenever d>0 and k>0.
1. The proof transports the known cardinality of Fin k across ap_equiv; no separate counting or no-duplication argument is needed.
Sources and attribution: Pinned Lean source (0647711a7118), Pinned AlphaProof Nexus Lean proof for Erdős 138
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GT.gt, OfNat.ofNat, Eq, ENat, ENat.card, setOf, Exists, And, LT.lt, HAdd.hAdd, HMul.hMul
Proof uses: Equiv, Fin, Erdos138.ap_equiv, Eq.mpr, id, congrArg, Eq.symm, ENat.card_congr, Eq.trans, Fintype.card, ENat.card_eq_coe_fintype_card, of_eq_true, True, Fintype.card_fin, eq_self
19 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma card_ap_eq_k (a d k : ℕ) (hd : d > 0) (hk : k > 0) :
  ENat.card ↑{ x : ℕ | ∃ m < k, x = a + m * d } = k := by
…
```
lemma Erdos138.card_ap_pos_d More than one progression term forces a positive step line 371 source
L4DEL explanation
If k>1 and the set {a+m*d | m<k} really has cardinality k, then d cannot be zero.
1. With d=0 every indexed term collapses to a, making the set a singleton and contradicting k>1.
Sources and attribution: Pinned Lean source (0647711a7118), Pinned AlphaProof Nexus Lean proof for Erdős 138, Blondal and Jungić, Proof of van der Waerden's Theorem in Nine Figures (2018), p. 163
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GT.gt, OfNat.ofNat, Eq, ENat, ENat.card, setOf, Exists, And, LT.lt, HAdd.hAdd, HMul.hMul
Proof uses: Decidable.byContradiction, Not, Set, Singleton.singleton, Set.ext, Eq.mpr, Iff, Membership.mem, id, congrArg, Iff.intro, Eq.symm, Exists.intro, And.intro, Set.encard_singleton, Eq.refl, Iff.mp, WithTop, WithTop.coe_inj
39 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
```
lemma card_ap_pos_d (a d k : ℕ) (hk : k > 1) (h_card : ENat.card ↑{ x : ℕ | ∃ m < k, x = a + m * d } = k) :
  d > 0 := by
…
```
lemma Erdos138.contains_mono_ap_imp Convert Mathlib's set-valued progression witness to HasMonoAP line 395 source
L4DEL explanation
A monochromatic arithmetic-progression subset of Finset.Icc 1 N yields explicit natural-number witnesses a,d satisfying HasMonoAP for the extended colouring.
1. The proof identifies the coerced subtype set with {a+m*d | m<k} and transports its cardinality.
2. For k=1 it may choose step 1; for k>1, card_ap_pos_d recovers the strictly positive step required by HasMonoAP.
Sources and attribution: Pinned Lean source (0647711a7118), Pinned AlphaProof Nexus Lean proof for Erdős 138
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GT.gt, OfNat.ofNat, Subtype, Membership.mem, Finset, Finset.Icc, Fin, ContainsMonoAPofLength, Erdos138.HasMonoAP, Erdos138.extend_coloring
Proof uses: Exists, Set, And, Set.IsAPOfLength, Set.image, ENat, Eq, Set.IsAPOfLengthWith, ENat.card, setOf, LT.lt, HAdd.hAdd, HSMul.hSMul, HMul.hMul, rfl, Eq.mpr, id, congrArg, Set.ext, Iff and 25 more
88 instances, coercions and auxiliary constants left out.

Tactic trace: 124 steps
Open to load the checked before-and-after goal states.
```
lemma contains_mono_ap_imp (N k : ℕ) (hk : k > 0) (c : Finset.Icc 1 N → Fin 2)
  (h : ContainsMonoAPofLength c k) :
  HasMonoAP (extend_coloring N c) N k := by
…
```
Mentions: Erdos138.HasMonoAP, Erdos138.extend_coloring
lemma Erdos138.imp_contains_mono_ap Convert HasMonoAP back to Mathlib's interval predicate line 507 source
L4DEL explanation
Explicit witnesses a,d for a monochromatic progression inside [1,N] define the required progression subset of the interval subtype.
1. The endpoint bound proves every term lies in Finset.Icc 1 N; card_ap_eq_k supplies the exact size, and the original colour equation supplies monochromaticity.
Sources and attribution: Pinned Lean source (0647711a7118), Pinned AlphaProof Nexus Lean proof for Erdős 138
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GT.gt, OfNat.ofNat, Fin, Erdos138.HasMonoAP, ContainsMonoAPofLength, Finset, Finset.Icc, Subtype, Membership.mem
Proof uses: Exists, And, GE.ge, LE.le, HAdd.hAdd, HMul.hMul, HSub.hSub, LT.lt, Eq, id, Exists.intro, Set, Set.IsAPOfLength, Set.image, ENat, setOf, HasSubset.Subset, Eq.mpr, congrArg, propext and 28 more
70 instances, coercions and auxiliary constants left out.

Tactic trace: 68 steps
Open to load the checked before-and-after goal states.
```
lemma imp_contains_mono_ap (N k : ℕ) (hk : k > 0) (c : ℕ → Fin 2)
  (h : HasMonoAP c N k) :
  ContainsMonoAPofLength (fun (x : Finset.Icc 1 N) => c x.1) k := by
…
```
Mentions: Erdos138.HasMonoAP
lemma Erdos138.not_guarantee_extend A countercolouring for k extends to one for k+1 line 566 source
L4DEL explanation
Given a 2-coloring of the first W(k) − 1 integers without a monochromatic k-AP
— Human-written proof companion for Erdős 138
If some two-colouring of {1,...,N} avoids every k-term progression, then some two-colouring of {1,...,N+k} avoids every (k+1)-term progression.
1. Extend the finite colouring to all naturals, apply extend_j_steps with j=k, and translate the resulting explicit predicate back to ContainsMonoAPofLength only to contradict it.
Sources and attribution: Pinned Lean source (0647711a7118), Pinned AlphaProof Nexus Lean proof for Erdős 138, Human-written proof companion for Erdős 138
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GT.gt, OfNat.ofNat, Not, Membership.mem, Set, Erdos138.monoAP_guarantee_set, HAdd.hAdd
Proof uses: Subtype, Finset, Finset.Icc, Fin, ContainsMonoAPofLength, Exists, Eq.mp, setOf, Erdos138.HasMonoAP, Erdos138.extend_coloring, Erdos138.imp_contains_mono_ap, Eq, funext, Fin.ext, id, Subtype.property, Eq.mpr, dite, Subtype.mk, congrArg and 14 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 34 steps
Open to load the checked before-and-after goal states.
```
lemma not_guarantee_extend (k N : ℕ) (hk : k > 0) :
    N ∉ monoAP_guarantee_set 2 k → (N + k) ∉ monoAP_guarantee_set 2 (k + 1) := by
…
```
Mentions: Erdos138.monoAP_guarantee_set
lemma Erdos138.not_in_set_of_lt_sInf Nothing below a natural-number infimum belongs to the set line 601 source
L4DEL explanation
For any set of naturals s, if n<sInf s, then n∉s.
1. Membership would imply sInf s≤n by the defining lower-bound property of the infimum, contradicting the strict inequality.
Sources and attribution: Pinned Lean source (0647711a7118), Pinned AlphaProof Nexus Lean proof for Erdős 138
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, LT.lt, InfSet.sInf, Not, Membership.mem
Proof uses: LE.le, csInf_le, OrderBot.bddBelow
13 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma not_in_set_of_lt_sInf {s : Set ℕ} {n : ℕ} (h : n < sInf s) : n ∉ s := by
…
```
def Erdos138.U_limit_color The ultrafilter-limit colour at one integer line 607 source
L4DEL explanation
Given a sequence of two-colourings C n, U_limit_color C U x chooses colour 0 when the indices assigning 0 to x are large in U, and otherwise chooses colour 1.
1. This is a proof-oriented compactness construction in the Lean file, not a step stated in the one-page human-written companion.
Sources and attribution: Pinned Lean source (0647711a7118), Pinned AlphaProof Nexus Lean proof for Erdős 138
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, OfNat.ofNat, Ultrafilter
Proof uses: ite, Membership.mem, Set, setOf, Eq
6 instances, coercions and auxiliary constants left out.
```
noncomputable def U_limit_color (C : ℕ → ℕ → Fin 2) (U : Ultrafilter ℕ) (x : ℕ) : Fin 2 :=
…
```
lemma Erdos138.U_limit_color_mem The chosen limit colour occurs on a U-large set of indices line 610 source
L4DEL explanation
For each position x, the indices n satisfying C n x = U_limit_color C U x belong to the ultrafilter.
1. If the colour-0 fibre is not in U, ultrafilter maximality puts its complement in U; because Fin 2 has only two values, that complement is exactly the colour-1 fibre.
Sources and attribution: Pinned Lean source (0647711a7118), Pinned AlphaProof Nexus Lean proof for Erdős 138
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, OfNat.ofNat, Ultrafilter, Membership.mem, Set, setOf, Eq, Erdos138.U_limit_color
Proof uses: id, dite, ite, Eq.mpr, congrArg, if_pos, Not, if_neg, Compl.compl, Union.union, Set.univ, Set.union_compl_self, Filter.univ_mem, Or, Iff.mp, Ultrafilter.union_mem_iff, Eq.mp, Eq.symm, Or.inl, False.elim and 14 more
22 instances, coercions and auxiliary constants left out.

Tactic trace: 45 steps
Open to load the checked before-and-after goal states.
```
lemma U_limit_color_mem (C : ℕ → ℕ → Fin 2) (U : Ultrafilter ℕ) (x : ℕ) :
  {n | C n x = U_limit_color C U x} ∈ U := by
…
```
Mentions: Erdos138.U_limit_color
lemma Erdos138.U_inter_mem Finitely many progression positions agree with the limit colouring together line 645 source
L4DEL explanation
For fixed a,b,k, the indices whose colourings agree with the ultrafilter-limit colouring at every point a*s+b for s<k form a set in U.
1. Induction on k reduces the claim to closure of a filter under finite intersections.
Sources and attribution: Pinned Lean source (0647711a7118), Pinned AlphaProof Nexus Lean proof for Erdős 138
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, OfNat.ofNat, Ultrafilter, Membership.mem, Set, setOf, LT.lt, Eq, HAdd.hAdd, HMul.hMul, Erdos138.U_limit_color
Proof uses: Nat.recAux, Set.univ, Set.ext, Eq.mpr, Iff, id, Eq.trans, True, congrArg, iff_true, Decidable.byContradiction, Not, Filter.univ_mem, Erdos138.U_limit_color_mem, Filter, Inter.inter, Filter.inter_mem, And, Iff.intro, Or and 2 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 35 steps
Open to load the checked before-and-after goal states.
```
lemma U_inter_mem (C : ℕ → ℕ → Fin 2) (U : Ultrafilter ℕ) (a b k : ℕ) :
  {n | ∀ s < k, C n (a * s + b) = U_limit_color C U (a * s + b)} ∈ U := by
…
```
Mentions: Erdos138.U_limit_color
lemma Erdos138.U_atTop_mem_large A U-large set contains arbitrarily large indices line 676 source
L4DEL explanation
When the ultrafilter lies above atTop, every set in it meets every tail {n | n≥M}.
1. Intersect the given set with the tail inside U; a member of an ultrafilter is nonempty, so the intersection supplies an index at least M.
Sources and attribution: Pinned Lean source (0647711a7118), Pinned AlphaProof Nexus Lean proof for Erdős 138
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ultrafilter, Nat, LE.le, Filter, Filter.atTop, Set, Membership.mem, Exists, And, GE.ge
Proof uses: setOf, Iff.mpr, Filter.mem_atTop_sets, Exists.intro, Inter.inter, Filter.inter_mem, Set.Nonempty, Ultrafilter.nonempty_of_mem, And.intro, And.left, And.right
29 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma U_atTop_mem_large (U : Ultrafilter ℕ) (h_le : ↑U ≤ (Filter.atTop : Filter ℕ))
  (s : Set ℕ) (hs : s ∈ U) (M : ℕ) : ∃ n ∈ s, n ≥ M := by
…
```
lemma Erdos138.W_is_nonempty Van der Waerden forcing lengths exist for every progression length line 685 source
L4DEL explanation
follows van der Waerden’s original idea to establish the existence of W(l, k) by using double induction.
— Blondal and Jungić, Proof of van der Waerden's Theorem in Nine Figures (2018), p. 163
proved that there is a smallest integer f (n)
— Paul Erdős, On the combinatorial problems which I would most like to see solved (1981), p. 5
For every k, some finite N forces a monochromatic k-term progression under every two-colouring, so the set whose infimum defines W k is nonempty.
1. For k=0 the empty progression is immediate. Otherwise, assume countercolourings exist for every finite N, extend them to all naturals, and take an ultrafilter-limit colouring.
2. Mathlib's infinite van der Waerden theorem gives a monochromatic homothetic copy in the limit colouring. Finite intersection and an arbitrarily large matching index transfer that progression back to one of the alleged countercolourings.
3. Blondal and Jungić describe van der Waerden's original double-induction proof of existence; the Lean declaration instead uses this ultrafilter compactness route. The sources support the theorem, not an identity of proofs.
Sources and attribution: Pinned Lean source (0647711a7118), Pinned AlphaProof Nexus Lean proof for Erdős 138, Blondal and Jungić, Proof of van der Waerden's Theorem in Nine Figures (2018), p. 163, Paul Erdős, On the combinatorial problems which I would most like to see solved (1981), p. 5
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Set.Nonempty, Erdos138.monoAP_guarantee_set, OfNat.ofNat
Proof uses: dite, Eq, Exists.intro, Membership.mem, Set, Subtype, Finset, Finset.Icc, Fin, id, ContainsMonoAPofLength, Exists, And, Set.IsAPOfLength, Set.image, ENat, Set.IsAPOfLengthWith, ENat.card, setOf, LT.lt and 66 more
105 instances, coercions and auxiliary constants left out.

Tactic trace: 102 steps
Open to load the checked before-and-after goal states.
```
lemma W_is_nonempty (k : ℕ) : (monoAP_guarantee_set 2 k).Nonempty := by
…
```
Mentions: Erdos138.monoAP_guarantee_set
lemma Erdos138.Icc_subset_succ The interval [1,N] sits inside [1,N+1] line 787 source
L4DEL explanation
Any natural number between 1 and N is also between 1 and N+1.
1. This small coercion lemma lets the proof restrict a colouring of the larger interval to the smaller subtype without changing its values.
Sources and attribution: Pinned Lean source (0647711a7118), Pinned AlphaProof Nexus Lean proof for Erdős 138
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, HAdd.hAdd
Proof uses: Eq.mpr, And, LE.le, id, Eq, congrArg, propext, Finset.mem_Icc, Decidable.byContradiction, Not, Eq.mp
16 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma Icc_subset_succ (N x : ℕ) (hx : x ∈ Finset.Icc 1 N) : x ∈ Finset.Icc 1 (N + 1) := by
…
```
lemma Erdos138.guarantee_upward_closed Once an interval length guarantees a progression, every larger one does line 791 source
L4DEL explanation
If every r-colouring of {1,...,N} contains a monochromatic k-term progression, then the same is true for {1,...,N+1}.
1. Restrict an arbitrary colouring of the larger interval to the first N points, obtain the progression there, and lift its subtype-valued set back into the larger interval.
Sources and attribution: Pinned Lean source (0647711a7118), Pinned AlphaProof Nexus Lean proof for Erdős 138
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Membership.mem, Set, Erdos138.monoAP_guarantee_set, HAdd.hAdd, OfNat.ofNat
Proof uses: Subtype, Finset, Finset.Icc, Fin, Subtype.mk, Erdos138.Icc_subset_succ, Subtype.property, ContainsMonoAPofLength, id, Exists, And, Set.IsAPOfLength, Set.image, ENat, Eq, setOf, Exists.intro, And.intro, Set.IsAPOfLengthWith, ENat.card and 11 more
40 instances, coercions and auxiliary constants left out.

Tactic trace: 55 steps
Open to load the checked before-and-after goal states.
```
lemma guarantee_upward_closed (k r N : ℕ) :
    N ∈ monoAP_guarantee_set r k → (N + 1) ∈ monoAP_guarantee_set r k := by
…
```
Mentions: Erdos138.monoAP_guarantee_set
lemma Erdos138.not_in_guarantee_lt_sInf A non-guaranteeing length lies below the van der Waerden number line 841 source
L4DEL explanation
If N does not force a two-colour k-term progression, then N<W k.
1. W_is_nonempty makes the infimum a genuine minimum, while guarantee_upward_closed shows every number at or above that minimum belongs to the forcing set.
Sources and attribution: Pinned Lean source (0647711a7118), Pinned AlphaProof Nexus Lean proof for Erdős 138, Blondal and Jungić, Proof of van der Waerden's Theorem in Nine Figures (2018), p. 163
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Not, Membership.mem, Set, Erdos138.monoAP_guarantee_set, OfNat.ofNat, LT.lt, Erdos138.W
Proof uses: Set.Nonempty, Erdos138.W_is_nonempty, Nat.sInf_mem, Decidable.byContradiction, Exists, Eq, HAdd.hAdd, Exists.intro, HSub.hSub, Eq.symm, Nat.add_sub_of_le, Eq.mp, LE.le, False, Nat.recAux, Nat.succ, Eq.mpr, id, congrArg, Erdos138.guarantee_upward_closed
20 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
lemma not_in_guarantee_lt_sInf (k N : ℕ) (hN : N ∉ monoAP_guarantee_set 2 k) :
    N < W k := by
…
```
Mentions: Erdos138.monoAP_guarantee_set, Erdos138.W
lemma Erdos138.W_not_guarantee One less than a positive van der Waerden number is a counterexample length line 859 source
L4DEL explanation
When W k≠0, minimality gives W k-1∉monoAP_guarantee_set 2 k.
1. Natural-number arithmetic gives W k-1<W k; not_in_set_of_lt_sInf then excludes membership in the forcing set.
Sources and attribution: Pinned Lean source (0647711a7118), Pinned AlphaProof Nexus Lean proof for Erdős 138
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Ne, Erdos138.W, OfNat.ofNat, Not, Membership.mem, Set, Erdos138.monoAP_guarantee_set, HSub.hSub
Proof uses: Erdos138.not_in_set_of_lt_sInf, id, LT.lt, InfSet.sInf, Decidable.byContradiction
11 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma W_not_guarantee (k : ℕ) (hW : W k ≠ 0) : W k - 1 ∉ monoAP_guarantee_set 2 k := by
…
```
Mentions: Erdos138.W, Erdos138.monoAP_guarantee_set
lemma Erdos138.W_diff_bound_gt0 The quantitative gap bound when W(k) is positive line 864 source
L4DEL explanation
We will show that W(k + 1) ≥ W(k) + k
— Human-written proof companion for Erdős 138
For k>0 and W k≠0, the proof establishes W(k+1)-W(k)≥k.
1. Minimality supplies a k-progression-free colouring through W k-1; not_guarantee_extend extends it through (W k-1)+k without a (k+1)-progression.
2. That extended counterexample lies strictly below W(k+1), and natural-number arithmetic rearranges the inequality into the desired difference bound.
Sources and attribution: Pinned Lean source (0647711a7118), Pinned AlphaProof Nexus Lean proof for Erdős 138, Human-written proof companion for Erdős 138
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GT.gt, OfNat.ofNat, Ne, Erdos138.W, GE.ge, HSub.hSub, HAdd.hAdd
Proof uses: Not, Membership.mem, Set, Erdos138.monoAP_guarantee_set, Erdos138.W_not_guarantee, Erdos138.not_guarantee_extend, LT.lt, Erdos138.not_in_guarantee_lt_sInf, Decidable.byContradiction
17 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma W_diff_bound_gt0 (k : ℕ) (hk : k > 0) (hW : W k ≠ 0) : W (k + 1) - W k ≥ k := by
…
```
Mentions: Erdos138.W
lemma Erdos138.W_diff_ge_k The gap bound for every natural k line 870 source
L4DEL explanation
For all natural numbers k, W(k+1)-W(k)≥k, including the edge cases introduced by the natural-number encoding.
1. The case k=0 is immediate. If k>0 but W k=0, the proof first shows that the empty interval cannot force a positive-length progression and extends that counterexample.
2. When W k≠0, the result is exactly W_diff_bound_gt0.
Sources and attribution: Pinned Lean source (0647711a7118), Pinned AlphaProof Nexus Lean proof for Erdős 138, Human-written proof companion for Erdős 138
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, HSub.hSub, Erdos138.W, HAdd.hAdd, OfNat.ofNat
Proof uses: dite, Eq, Decidable.byContradiction, Not, Eq.symm, Membership.mem, Set, Erdos138.monoAP_guarantee_set, Subtype, Finset, Finset.Icc, Fin, ContainsMonoAPofLength, Exists, And, Set.IsAPOfLength, Set.image, ENat, False, Set.IsAPOfLengthWith and 19 more
58 instances, coercions and auxiliary constants left out.

Tactic trace: 32 steps
Open to load the checked before-and-after goal states.
```
lemma W_diff_ge_k (k : ℕ) : W (k + 1) - W k ≥ k := by
…
```
Mentions: Erdos138.W
lemma Erdos138.W_diff_ge_k_all The pointwise lower bound used to prove divergence line 898 source
L4DEL explanation
the obvious generalization of this argument gives W(k + 1, l + 1) ≥ W(k, l) + min(k, l)
— George Tsoukalas et al., AlphaProof Nexus paper, Erdős 138 appendix
This wrapper presents the uniform inequality k≤W(k+1)-W(k) in the orientation expected by Filter.tendsto_atTop_mono.
1. At zero the bound is trivial; at a successor it invokes W_diff_ge_k with the positive index.
2. The AlphaProof Nexus paper also records Thomas Bloom's off-diagonal generalization; that is linked as context, not claimed by this Lean declaration.
Sources and attribution: Pinned Lean source (0647711a7118), Pinned AlphaProof Nexus Lean proof for Erdős 138, George Tsoukalas et al., AlphaProof Nexus paper, Erdős 138 appendix
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, HSub.hSub, Erdos138.W, HAdd.hAdd, OfNat.ofNat
Proof uses: Nat.casesAuxOn, Eq, Nat.zero_le, Eq.symm, Erdos138.W_diff_ge_k, Eq.refl
13 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma W_diff_ge_k_all (k : ℕ) : W (k + 1) - W k ≥ k := by
…
```
Mentions: Erdos138.W
theorem Erdos138.target_theorem_0 Erdős problem 138: consecutive van der Waerden numbers separate without bound line 906 source
L4DEL explanation
We will show that W(k + 1) ≥ W(k) + k
— Human-written proof companion for Erdős 138
We will show that W(k + 1) ≥ W(k) + k
— George Tsoukalas et al., AlphaProof Nexus paper, Erdős 138 appendix
Can one at least prove that f(n + 1) − f(n) → ∞?
— Paul Erdős, On the combinatorial problems which I would most like to see solved (1981), p. 6
Whatever one makes explicit and draws is much easier to remember and to reproduce than mere thoughts
— Bartel van der Waerden's 1971 recollection, reproduced by Blondal and Jungić (2018), p. 162
The argument is rather simple, once one knows what the right thing to prove is.
— Erdős Problems 138 discussion (Adam Zsolt Wagner and Thomas Bloom)
For the two-colour van der Waerden number W(k), the difference W(k+1)-W(k) tends to infinity. The proof establishes the explicit lower bound W(k+1) ≥ W(k)+k, which immediately forces the differences upward.
1. Begin with a two-colouring of [1,W(k)-1] containing no monochromatic k-term arithmetic progression.
2. Greedily colour k more integers; if both colours were blocked at one step, two terminal progressions would force one earlier point to have both colours.
3. Hence a colouring without a monochromatic (k+1)-term progression exists through W(k)+k-1, proving the bound.
4. The Lean file separately proves that every W(k) exists, using an ultrafilter limit and Mathlib's infinite van der Waerden theorem; the one-page companion states the greedy difference argument rather than that compactness implementation.
5. Erdős's 1981 source asks both a quotient question and this weaker difference question. This theorem resolves only the difference variant; it does not claim that W(k+1)/W(k)→∞ or settle the stronger growth problem.
6. Formally the statement is answer(True) ↔ Tendsto ...; the reverse implication is trivial because the recorded answer is already True, while the forward implication uses the quantitative bound.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written proof companion for Erdős 138, Erdős Problems 138 source record, George Tsoukalas et al., AlphaProof Nexus paper, Erdős 138 appendix, Paul Erdős, On the combinatorial problems which I would most like to see solved (1981), p. 6, Bartel van der Waerden's 1971 recollection, reproduced by Blondal and Jungić (2018), p. 162, Erdős Problems 138 discussion (Adam Zsolt Wagner and Thomas Bloom)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Iff, True, Filter.Tendsto, Nat, HSub.hSub, Erdos138.W, HAdd.hAdd, OfNat.ofNat, Filter.atTop
Proof uses: Iff.intro, Filter.tendsto_atTop_mono, Erdos138.W_diff_ge_k_all, Filter.tendsto_id, True.intro
12 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
theorem target_theorem_0
  : answer(
  -- EVOLVE-VALUE-START
  True
  -- EVOLVE-VALUE-END
  ) ↔ atTop.Tendsto (fun k => (W (k + 1) - W k)) atTop := by
…
```
Mentions: Erdos138.W