The even-N upper bound (Erdős 865, §4)

Strong induction on N proving even_bound: every triple-free A ⊆ [1, 2e] satisfies the 5/8 counting bound, split into the cases even_bound_case1 and even_bound_case2.

theorem Erdos865.card_A_bound {A : Finset ℕ} {N : ℕ} (hsub : A ⊆ Finset.Icc 1 N) (h : ℕ) : A.card ≤ (Xset A h).card + (Yset A N h).card + 2 + (N - 2 * h)

theorem Erdos865.gap_empty {A : Finset ℕ} {H p q : ℕ} (_hqlo : H ≤ q) (hqmin : ∀ a ∈ A, H ≤ a → q ≤ a) (hpmax : ∀ a ∈ A, a ≤ H → a ≤ p) (a : ℕ) : a ∈ A → ¬(p < a ∧ a < q)

theorem Erdos865.case1_I_sub {A : Finset ℕ} {H p q : ℕ} (_hqlo : H ≤ q) (hqmin : ∀ a ∈ A, H ≤ a → q ≤ a) (hpmax : ∀ a ∈ A, a ≤ H → a ≤ p) : Finset.Ico (max p (2 * H - q) + 1) q ⊆ Eset A (2 * H) q \ collisions q (Bset A (2 * H) q)

theorem Erdos865.even_bound_case1 {H p q : ℕ} {A : Finset ℕ} (hsub : A ⊆ Finset.Icc 1 (2 * H)) (hA : IsTripleFree A) (hq : q ∈ A) (hqlo : H ≤ q) (hqhi : q ≤ 2 * H) (hqmin : ∀ a ∈ A, H ≤ a → q ≤ a) (_hp : p ∈ A) (_hplo : 1 ≤ p) (hphi : p ≤ H) (hpmax : ∀ a ∈ A, a ≤ H → a ≤ p) (hcase : q - H ≤ 4 * (H - p)) : 4 * A.card ≤ 5 * H + 24

theorem Erdos865.case2_Bset_disjoint {A : Finset ℕ} {H p q : ℕ} (hqmin : ∀ a ∈ A, H ≤ a → q ≤ a) (hpmax : ∀ a ∈ A, a ≤ H → a ≤ p) : Bset A (2 * H) p ∩ Finset.Ico 1 (q - p) = ∅

theorem Erdos865.case2_I_sub {A : Finset ℕ} {H p q : ℕ} (hple : q - p ≤ p) (hqmin : ∀ a ∈ A, H ≤ a → q ≤ a) (hpmax : ∀ a ∈ A, a ≤ H → a ≤ p) : Finset.Ico 1 (q - p) \ A ⊆ Eset A (2 * H) p \ collisions p (Bset A (2 * H) p)

theorem Erdos865.tripleFree_subset {A B : Finset ℕ} (hA : IsTripleFree A) (h : B ⊆ A) : IsTripleFree B

A subset of a triple-free set is triple-free.

theorem Erdos865.even_bound_case2 {H p q : ℕ} {A : Finset ℕ} (hsub : A ⊆ Finset.Icc 1 (2 * H)) (hA : IsTripleFree A) (hqlo : H ≤ q) (hqhi : q ≤ 2 * H) (hqmin : ∀ a ∈ A, H ≤ a → q ≤ a) (hp : p ∈ A) (hplo : 1 ≤ p) (hphi : p ≤ H) (hpmax : ∀ a ∈ A, a ≤ H → a ≤ p) (hcase : 4 * (H - p) < q - H) (IH : ∀ (H' : ℕ) (A' : Finset ℕ), H' < H → A' ⊆ Finset.Icc 1 (2 * H') → IsTripleFree A' → 4 * A'.card ≤ 5 * H' + 24) : 4 * A.card ≤ 5 * H + 24

theorem Erdos865.even_bound (H : ℕ) (A : Finset ℕ) (hsub : A ⊆ Finset.Icc 1 (2 * H)) (hA : IsTripleFree A) : 4 * A.card ≤ 5 * H + 24