The folding lemma (Erdős 865, §3)

Folds a triple-free set A ⊆ [1,N] onto a FoldedOK set B_h and controls the collisions via the exceptional set, giving the folding lemma folding_lemma.

theorem Erdos865.foldedOK_Bset {A : Finset ℕ} {N h : ℕ} (hA : IsTripleFree A) (hh : h ∈ A) (_hh2 : 2 ≤ h) : FoldedOK h (Bset A N h)

theorem Erdos865.collisions_subset_Eset {A : Finset ℕ} {N h : ℕ} (hA : IsTripleFree A) (hh : h ∈ A) : collisions h (Bset A N h) ⊆ Eset A N h

theorem Erdos865.card_XY_E (A : Finset ℕ) (N h : ℕ) : (Xset A h).card + (Yset A N h).card + (Eset A N h).card = h - 1 + (Bset A N h).card

theorem Erdos865.folding_lemma {A : Finset ℕ} {N h : ℕ} (hA : IsTripleFree A) (hh : h ∈ A) : 4 * ((Xset A h).card + (Yset A N h).card) + 4 * (Eset A N h \ collisions h (Bset A N h)).card ≤ 5 * h + 4