diff --git a/LeanPool.lean b/LeanPool.lean
index c42ffb54..3af8424a 100644
--- a/LeanPool.lean
+++ b/LeanPool.lean
@@ -795,6 +795,14 @@ import LeanPool.Erdos403
 import LeanPool.Erdos403.Basic
 import LeanPool.Erdos403.FactBase
 import LeanPool.Erdos403.Sharp
+import LeanPool.Erdos865
+import LeanPool.Erdos865.Defs
+import LeanPool.Erdos865.FoldedAux
+import LeanPool.Erdos865.FoldedMain
+import LeanPool.Erdos865.Folding
+import LeanPool.Erdos865.Main
+import LeanPool.Erdos865.Sharpness
+import LeanPool.Erdos865.UpperBound
 import LeanPool.ErdosMoser
 import LeanPool.ErdosMoser.Basic
 import LeanPool.ErdosMoser.Bounds
diff --git a/LeanPool/Erdos865.lean b/LeanPool/Erdos865.lean
new file mode 100644
index 00000000..cc9088c2
--- /dev/null
+++ b/LeanPool/Erdos865.lean
@@ -0,0 +1,24 @@
+/-
+Copyright (c) 2026 Ricky Cipollini. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Ricky Cipollini
+-/
+
+import LeanPool.Erdos865.Defs
+import LeanPool.Erdos865.FoldedAux
+import LeanPool.Erdos865.FoldedMain
+import LeanPool.Erdos865.Folding
+import LeanPool.Erdos865.Sharpness
+import LeanPool.Erdos865.UpperBound
+import LeanPool.Erdos865.Main
+
+/-!
+# A sharp 5/8 bound for Erdős Problem 865
+
+Source: url:https://github.com/mrricky22/erdos-865-lean
+Authors: Ricky Cipollini
+Status: verified
+Main declarations: `Erdos865.erdos865_upper_bound`, `Erdos865.sharpness`
+Tags: additive-combinatorics, erdos-problems, sum-free-sets, combinatorics
+MSC: 11B75, 11B13
+-/
diff --git a/LeanPool/Erdos865/Defs.lean b/LeanPool/Erdos865/Defs.lean
new file mode 100644
index 00000000..14ea29c1
--- /dev/null
+++ b/LeanPool/Erdos865/Defs.lean
@@ -0,0 +1,66 @@
+/-
+Copyright (c) 2026 Ricky Cipollini. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Ricky Cipollini
+-/
+import Mathlib.Order.Interval.Finset.Nat
+
+/-!
+# Definitions for the sharp 5/8 bound (Erdős 865)
+
+Basic objects for the pairwise-sums problem: pairwise-sum triples and triple-free sets
+(`HasTriple`, `IsTripleFree`), the folded sum sets `lowSums`/`highSums`/`collisions`, the
+hypothesis `FoldedOK`, and the folding sets `Xset`/`Yset`/`Bset`/`Eset`.
+-/
+
+open Finset
+
+namespace Erdos865
+
+/-- `A` contains a *pairwise-sum triple*: distinct `a, b, c ∈ A` with
+`a+b, a+c, b+c ∈ A`. -/
+def HasTriple (A : Finset ℕ) : Prop :=
+  ∃ a ∈ A, ∃ b ∈ A, ∃ c ∈ A,
+    a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ a + b ∈ A ∧ a + c ∈ A ∧ b + c ∈ A
+
+/-- `A` is *triple-free* if it contains no pairwise-sum triple. -/
+def IsTripleFree (A : Finset ℕ) : Prop := ¬ HasTriple A
+
+/-! ### Folded additive lemma definitions -/
+
+/-- Non-wrapped pair sums `x + y` (`x ≠ y`, both in `B`, `x + y < m`). -/
+def lowSums (m : ℕ) (B : Finset ℕ) : Finset ℕ :=
+  ((B ×ˢ B).filter (fun p => p.1 ≠ p.2 ∧ p.1 + p.2 < m)).image (fun p => p.1 + p.2)
+
+/-- Wrapped pair sums `x + y - m` (`x ≠ y`, both in `B`, `x + y > m`). -/
+def highSums (m : ℕ) (B : Finset ℕ) : Finset ℕ :=
+  ((B ×ˢ B).filter (fun p => p.1 ≠ p.2 ∧ m < p.1 + p.2)).image (fun p => p.1 + p.2 - m)
+
+/-- Residues arising both as a non-wrapped and as a wrapped pair sum. -/
+def collisions (m : ℕ) (B : Finset ℕ) : Finset ℕ := lowSums m B ∩ highSums m B
+
+/-- The hypothesis `(1.1)` of the folded additive lemma: `B ⊆ {1,…,m-1}` and for
+all distinct `x, y ∈ B`, `x + y ≠ m` and the residue of `x + y` mod `m` is not in
+`B`. -/
+def FoldedOK (m : ℕ) (B : Finset ℕ) : Prop :=
+  (∀ b ∈ B, 1 ≤ b ∧ b < m) ∧
+  (∀ x ∈ B, ∀ y ∈ B, x ≠ y → x + y ≠ m ∧ (x + y) % m ∉ B)
+
+/-! ### Folding definitions -/
+
+/-- `X = {r : 1 ≤ r < h, r ∈ A}`. -/
+def Xset (A : Finset ℕ) (h : ℕ) : Finset ℕ :=
+  (Finset.Ico 1 h).filter (fun r => r ∈ A)
+
+/-- `Y = {r : 1 ≤ r < h, h + r ≤ N, h + r ∈ A}`. -/
+def Yset (A : Finset ℕ) (N h : ℕ) : Finset ℕ :=
+  (Finset.Ico 1 h).filter (fun r => h + r ≤ N ∧ h + r ∈ A)
+
+/-- `B_h = X ∩ Y`. -/
+def Bset (A : Finset ℕ) (N h : ℕ) : Finset ℕ := Xset A h ∩ Yset A N h
+
+/-- `E = [1, h-1] \ (X ∪ Y)`. -/
+def Eset (A : Finset ℕ) (N h : ℕ) : Finset ℕ :=
+  (Finset.Ico 1 h) \ (Xset A h ∪ Yset A N h)
+
+end Erdos865
diff --git a/LeanPool/Erdos865/FoldedAux.lean b/LeanPool/Erdos865/FoldedAux.lean
new file mode 100644
index 00000000..3db3d39f
--- /dev/null
+++ b/LeanPool/Erdos865/FoldedAux.lean
@@ -0,0 +1,365 @@
+/-
+Copyright (c) 2026 Ricky Cipollini. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Ricky Cipollini
+-/
+import LeanPool.Erdos865.Defs
+import Mathlib.Data.ZMod.Basic
+import Mathlib.Tactic.IntervalCases
+import Mathlib.Tactic.LinearCombinationPrime
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum
+import Mathlib.Tactic.Ring
+
+/-!
+# The four sets `T₁,…,T₄` and their pairwise intersections
+
+Supporting material for the folded additive lemma: the images `T₁,…,T₄` of `B` inside
+`ZMod m`, their cardinalities, and the pairwise-intersection bounds culminating in the
+four-set union bound `case2_bound`.
+-/
+
+open Finset
+
+namespace Erdos865
+
+/-! ### Generic helpers -/
+
+/-
+Inclusion–exclusion upper bound for four finite sets.
+-/
+theorem four_card_le {X : Type*} [DecidableEq X] (s1 s2 s3 s4 : Finset X) :
+    s1.card + s2.card + s3.card + s4.card ≤
+      (s1 ∪ s2 ∪ s3 ∪ s4).card +
+        ((s1 ∩ s2).card + (s1 ∩ s3).card + (s1 ∩ s4).card +
+          (s2 ∩ s3).card + (s2 ∩ s4).card + (s3 ∩ s4).card) := by
+  have h1 := Finset.card_union_add_card_inter s1 ( s2 ∪ s3 ∪ s4 );
+  have h2 := Finset.card_union_add_card_inter s2 ( s3 ∪ s4 )
+  have h3 := Finset.card_union_add_card_inter s3 s4
+  simp_all +decide [ Finset.inter_union_distrib_left ]
+  linarith [ Finset.card_union_add_card_inter ( s1 ∩ s2 ) ( s1 ∩ s3 ∪ s1 ∩ s4 ),
+    Finset.card_union_add_card_inter ( s1 ∩ s3 ) ( s1 ∩ s4 ),
+    Finset.card_union_add_card_inter ( s2 ∩ s3 ) ( s2 ∩ s4 ) ]
+
+/-
+In `ZMod m` the equation `2 * x = c` has at most two solutions.
+-/
+theorem card_two_sol (m : ℕ) [NeZero m] (c : ZMod m) :
+    (Finset.univ.filter (fun x : ZMod m => 2 * x = c)).card ≤ 2 := by
+  by_contra! h_contra;
+  -- Let S = univ.filter (fun x : ZMod m => 2*x = c). Show S ⊆ {a, b} where
+  -- a = ((c.val/2 : ℕ) : ZMod m) and b = (((c.val+m)/2 : ℕ) : ZMod m);
+  -- then card S ≤ card {a,b} ≤ 2 (Finset.card_le_card and Finset.card_le_two,
+  -- or card_insert_le / card_pair).
+  obtain ⟨a, b, hab⟩ : ∃ a b : ZMod m, ∀ x : ZMod m, 2 * x = c → x = a ∨ x = b := by
+    use ((c.val / 2 : ℕ) : ZMod m), (((c.val + m) / 2 : ℕ) : ZMod m);
+    intro x hx
+    have h_eq : (2 * x.val : ℕ) % m = c.val % m := by
+      simp +decide [ ← ZMod.natCast_eq_natCast_iff', hx ];
+    -- Since $2 * x.val \equiv c.val \pmod{m}$, we have $2 * x.val = c.val + k * m$ for some
+    -- integer $k$.
+    obtain ⟨k, hk⟩ : ∃ k : ℕ, 2 * x.val = c.val + k * m := by
+      exact ⟨ ( 2 * x.val ) / m,
+        by linarith [ Nat.mod_add_div ( 2 * x.val ) m,
+          Nat.mod_eq_of_lt ( show c.val < m from ZMod.val_lt c ) ] ⟩;
+    rcases k with ( _ | _ | k ) <;> norm_num at *;
+    · norm_num [ ← hk, mul_comm ];
+    · norm_num [ ← hk, Nat.add_div ];
+    · nlinarith [ x.val_lt, c.val_lt ];
+  exact h_contra.not_ge ( le_trans ( Finset.card_le_card
+    ( show Finset.filter ( fun x : ZMod m => 2 * x = c ) Finset.univ ⊆ { a, b }
+      by intros x hx; aesop ) ) ( Finset.card_insert_le _ _ ) )
+
+/-! ### The four sets `T₁,…,T₄` in `ZMod m` -/
+
+/-- `T₁ = B` inside `ZMod m`. -/
+def T1 (m : ℕ) (B : Finset ℕ) : Finset (ZMod m) := B.image (fun b : ℕ => (b : ZMod m))
+
+/-- `T₂ = -B` inside `ZMod m`. -/
+def T2 (m : ℕ) (B : Finset ℕ) : Finset (ZMod m) := B.image (fun b : ℕ => -(b : ZMod m))
+
+/-- `T₃ = (B - α) \ {0}` inside `ZMod m`. -/
+def T3 (m : ℕ) (B : Finset ℕ) (α : ℕ) : Finset (ZMod m) :=
+  (B.image (fun b : ℕ => (b : ZMod m) - (α : ZMod m))).erase 0
+
+/-- `T₄ = (β - B) \ {0}` inside `ZMod m`. -/
+def T4 (m : ℕ) (B : Finset ℕ) (β : ℕ) : Finset (ZMod m) :=
+  (B.image (fun b : ℕ => (β : ZMod m) - (b : ZMod m))).erase 0
+
+/-
+The cast `ℕ → ZMod m` is injective on `B` when `B ⊆ {1,…,m-1}`.
+-/
+theorem cast_injOn {m : ℕ} {B : Finset ℕ} (hB : FoldedOK m B) :
+    Set.InjOn (fun b : ℕ => (b : ZMod m)) (B : Set ℕ) := by
+  intro x hx y hy; have := hB.1 x hx; have := hB.1 y hy;
+  simp_all +decide only [SetLike.mem_coe, ZMod.natCast_eq_natCast_iff'];
+  exact fun h =>
+    Nat.mod_eq_of_lt ( by linarith : x < m ) ▸ Nat.mod_eq_of_lt ( by linarith : y < m ) ▸ h
+
+theorem card_T1 {m : ℕ} {B : Finset ℕ} (hB : FoldedOK m B) : (T1 m B).card = B.card := by
+  exact Finset.card_image_of_injOn (cast_injOn hB)
+
+theorem card_T2 {m : ℕ} {B : Finset ℕ} (hB : FoldedOK m B) : (T2 m B).card = B.card := by
+  apply Finset.card_image_of_injOn;
+  intro x hx y hy; have := cast_injOn hB; aesop;
+
+theorem card_T3 {m : ℕ} {B : Finset ℕ} (hB : FoldedOK m B) {α : ℕ} (hα : α ∈ B) :
+    (T3 m B α).card = B.card - 1 := by
+  rw [ Erdos865.T3, Finset.card_erase_of_mem ];
+  · rw [ Finset.card_image_of_injOn ];
+    intro x hx y hy; have := hB.1 x hx; have := hB.1 y hy;
+    simp_all +decide only [SetLike.mem_coe, sub_eq_iff_eq_add, sub_add_cancel];
+    exact fun h => Nat.mod_eq_of_lt ( by linarith : x < m ) ▸
+      Nat.mod_eq_of_lt ( by linarith : y < m ) ▸
+        by simpa [ ZMod.natCast_eq_natCast_iff' ] using h;
+  · aesop
+
+theorem card_T4 {m : ℕ} {B : Finset ℕ} (hB : FoldedOK m B) {β : ℕ} (hβ : β ∈ B) :
+    (T4 m B β).card = B.card - 1 := by
+  have h_inj : Set.InjOn (fun b : ℕ => (β : ZMod m) - (b : ZMod m)) (B : Set ℕ) := by
+    intro x hx y hy; have := hB.1 x hx; have := hB.1 y hy;
+    simp_all +decide only [SetLike.mem_coe, sub_right_inj, ZMod.natCast_eq_natCast_iff'];
+    exact fun h =>
+      Nat.mod_eq_of_lt ( by linarith : x < m ) ▸ Nat.mod_eq_of_lt ( by linarith : y < m ) ▸ h;
+  rw [Erdos865.T4,
+    Finset.card_erase_of_mem (Finset.mem_image.mpr ⟨β, hβ, by simp⟩),
+    Finset.card_image_of_injOn h_inj]
+
+/-
+None of the four sets contain `0`, so their union misses `0`.
+-/
+theorem union_card_le {m : ℕ} (hm : 2 ≤ m) {B : Finset ℕ} (hB : FoldedOK m B) (α β : ℕ) :
+    haveI : NeZero m := ⟨by omega⟩
+    (T1 m B ∪ T2 m B ∪ T3 m B α ∪ T4 m B β).card ≤ m - 1 := by
+  haveI : NeZero m := ⟨by omega⟩
+  have hsub : T1 m B ∪ T2 m B ∪ T3 m B α ∪ T4 m B β ⊆ Finset.univ.erase (0 : ZMod m) := by
+    intro x hx
+    rw [Finset.mem_erase]
+    refine ⟨?_, Finset.mem_univ x⟩
+    simp only [Finset.mem_union] at hx
+    rcases hx with ((hx | hx) | hx) | hx
+    · rw [T1, Finset.mem_image] at hx
+      obtain ⟨a, ha, rfl⟩ := hx
+      obtain ⟨ha1, ha2⟩ := hB.1 a ha
+      simpa [ZMod.natCast_eq_zero_iff] using Nat.not_dvd_of_pos_of_lt (by omega) ha2
+    · rw [T2, Finset.mem_image] at hx
+      obtain ⟨a, ha, rfl⟩ := hx
+      obtain ⟨ha1, ha2⟩ := hB.1 a ha
+      simpa [neg_eq_zero, ZMod.natCast_eq_zero_iff] using Nat.not_dvd_of_pos_of_lt (by omega) ha2
+    · rw [T3] at hx; exact (Finset.mem_erase.mp hx).1
+    · rw [T4] at hx; exact (Finset.mem_erase.mp hx).1
+  calc (T1 m B ∪ T2 m B ∪ T3 m B α ∪ T4 m B β).card
+      ≤ (Finset.univ.erase (0 : ZMod m)).card := Finset.card_le_card hsub
+    _ = m - 1 := by
+        rw [Finset.card_erase_of_mem (Finset.mem_univ _), Finset.card_univ, ZMod.card]
+
+/-! ### The pairwise intersection bounds -/
+
+theorem inter_T1_T2_le {m : ℕ} {B : Finset ℕ} (hB : FoldedOK m B) :
+    (T1 m B ∩ T2 m B).card ≤ 1 := by
+  -- Take an arbitrary element z ∈ T1 m B ∩ T2 m B.
+  have h_eq : ∀ z ∈ T1 m B ∩ T2 m B, ∃ b ∈ B, z = (b : ZMod m) ∧ 2 * b = m := by
+    intro z hz
+    obtain ⟨b, hbB, hbz⟩ : ∃ b ∈ B, (b : ZMod m) = z := by
+      unfold T1 at hz; aesop;
+    obtain ⟨b', hb'B, hb'z⟩ : ∃ b' ∈ B, -(b' : ZMod m) = z := by
+      unfold T2 at hz; aesop;
+    have h_eq : m ∣ (b + b') := by
+      simp_all +decide only [mem_inter, ← ZMod.natCast_eq_zero_iff, Nat.cast_add];
+      rw [ ← hb'z, neg_add_cancel ];
+    have h_eq : b + b' = m := by
+      have := hB.1 b hbB; have := hB.1 b' hb'B; obtain ⟨ k, hk ⟩ := h_eq;
+      nlinarith [ show k = 1 by nlinarith ];
+    have := hB.2 b hbB b' hb'B; simp_all +decide [ two_mul ] ;
+    grind;
+  exact Finset.card_le_one.mpr fun x hx y hy => by
+    obtain ⟨ b₁, hb₁, rfl, hb₁' ⟩ := h_eq x hx; obtain ⟨ b₂, hb₂, rfl, hb₂' ⟩ := h_eq y hy; aesop;
+
+theorem inter_T1_T2_odd {m : ℕ} (hodd : ¬ 2 ∣ m) {B : Finset ℕ} (hB : FoldedOK m B) :
+    T1 m B ∩ T2 m B = ∅ := by
+  simp +decide only [Nat.two_dvd_ne_zero, T1, T2, Finset.ext_iff, mem_inter, mem_image,
+    notMem_empty, iff_false, not_and, not_exists, forall_exists_index, and_imp,
+    forall_apply_eq_imp_iff₂] at *;
+  intro a ha b hb; rw [ neg_eq_iff_add_eq_zero ] ; have := hB.1 a ha; have := hB.1 b hb;
+  simp_all +decide only [ne_eq];
+  by_contra h_contra
+  have h_div : m ∣ (a + b) := by
+    simp_all +decide [ ← ZMod.natCast_eq_zero_iff, add_comm ]
+  have h_eq : a + b = m := by
+    obtain ⟨ k, hk ⟩ := h_div; nlinarith [ show k = 1 by nlinarith ] ;
+  have h_contra' : a ≠ b := by
+    omega
+  have h_contra'' : a + b ≠ m := by
+    exact hB.2 a ha b hb h_contra' |>.1
+  contradiction
+
+theorem inter_T1_T3_le {m : ℕ} {B : Finset ℕ} (hB : FoldedOK m B) {α : ℕ} (hα : α ∈ B) :
+    (T1 m B ∩ T3 m B α).card ≤ 1 := by
+  by_contra h_contra;
+  obtain ⟨x, hx⟩ : ∃ x ∈ T1 m B ∩ T3 m B α, x ≠ (α : ZMod m) := by
+    exact Exists.elim ( Finset.exists_mem_ne ( lt_of_not_ge h_contra ) _ )
+      fun x hx => ⟨ x, hx.1, hx.2 ⟩;
+  obtain ⟨b, hb, hb_eq⟩ : ∃ b ∈ B, x = (b : ZMod m) := by
+    unfold T1 at hx; aesop;
+  obtain ⟨c, hc, hc_eq⟩ : ∃ c ∈ B, x = (c : ZMod m) - (α : ZMod m) ∧ c ≠ α := by
+    unfold T3 at hx; aesop;
+  have h_mod : (b + α) % m = c % m := by
+    simp_all +decide only [not_le, mem_inter, ne_eq, ← ZMod.natCast_eq_natCast_iff', Nat.cast_add];
+    linear_combination' -hb_eq;
+  have := hB.2 b hb α hα; simp_all +decide only [not_le, mem_inter, ne_eq] ;
+  exact this ( by aesop ) |>.2
+    ( by simpa [ Nat.mod_eq_of_lt ( show c < m from hB.1 c hc |>.2 ) ] using hc )
+
+theorem inter_T2_T3_le {m : ℕ} {B : Finset ℕ} (hB : FoldedOK m B) {α : ℕ} (hα : α ∈ B)
+    (hmin : ∀ x ∈ B, α ≤ x) : (T2 m B ∩ T3 m B α).card ≤ 1 := by
+  -- Since $z \in T2 \cap T3$, we have $z = -(u : ZMod m)$ and $u \in B$, and
+  -- $z = (b : ZMod m) - (α : ZMod m)$ and $b \in B$. Thus,
+  have h_eq : ∀ z ∈ T2 m B ∩ T3 m B α, ∃ u ∈ B, z = -(u : ZMod m) ∧ ∃ b ∈ B,
+      z = (b : ZMod m) - (α : ZMod m) ∧ u = b ∧ 2 * u = α + m := by
+    intro z hz
+    obtain ⟨u, huB, hu⟩ : ∃ u ∈ B, z = -(u : ZMod m) := by
+      unfold T2 at hz; aesop;
+    obtain ⟨b, hbB, hb⟩ : ∃ b ∈ B, z = (b : ZMod m) - (α : ZMod m) := by
+      grind +locals
+    have h_eq : (u + b : ℕ) % m = α % m := by
+      simp_all +decide only [mem_inter, ← ZMod.natCast_eq_natCast_iff', Nat.cast_add];
+      linear_combination' hu
+    have h_eq' : (u + b : ℕ) = α ∨ (u + b : ℕ) = α + m := by
+      have h_eq' : (u + b : ℕ) < 2 * m := by
+        linarith [ hB.1 u huB, hB.1 b hbB ];
+      have h_eq' : (u + b : ℕ) = α + m * ((u + b) / m) := by
+        linarith [ Nat.mod_add_div ( u + b ) m,
+          Nat.mod_eq_of_lt ( show α < m from hB.1 α hα |>.2 ) ];
+      have : ( u + b ) / m ≤ 1 := Nat.le_of_lt_succ ( Nat.div_lt_of_lt_mul <| by linarith )
+      interval_cases ( u + b ) / m <;>
+        simp +decide only [mul_zero, add_zero, mul_one] at h_eq' ⊢;
+      · exact Or.inl h_eq';
+      · exact Or.inr h_eq'
+    have h_eq'' : u = b := by
+      cases h_eq' <;> have := hB.2 u huB b hbB <;> simp_all +decide;
+      · grind +qlia;
+      · have := hB.1 α hα; simp_all +decide [ Nat.mod_eq_of_lt ] ;
+    have h_eq''' : 2 * u = α + m := by
+      cases h_eq' <;> simp_all +decide [ two_mul ];
+      linarith [ hmin _ hbB, show α > 0 from hB.1 _ hα |>.1 ]
+    use u, huB, hu, b, hbB, hb, h_eq'', h_eq''';
+  -- Since $2u = α + m$, and $u$ is uniquely determined, the set $T2 \cap T3$ can contain at
+  -- most one element.
+  have h_unique : ∀ z ∈ T2 m B ∩ T3 m B α, ∀ z' ∈ T2 m B ∩ T3 m B α, z = z' := by
+    grind;
+  exact Finset.card_le_one.mpr h_unique
+
+theorem inter_T2_T4_le {m : ℕ} {B : Finset ℕ} (hB : FoldedOK m B) {β : ℕ} (hβ : β ∈ B) :
+    (T2 m B ∩ T4 m B β).card ≤ 1 := by
+  rw [ Finset.card_le_one_iff ];
+  intros a b ha hb
+  have h_eq : ∀ z ∈ T2 m B ∩ T4 m B β, z = -(β : ZMod m) := by
+    intros z hz
+    obtain ⟨u, hu⟩ : ∃ u ∈ B, z = -(u : ZMod m) := by
+      unfold T2 at hz; aesop;
+    obtain ⟨b, hb⟩ : ∃ b ∈ B, z = (β : ZMod m) - (b : ZMod m) := by
+      unfold T4 at hz; aesop;
+    have h_eq : (b : ZMod m) = (β : ZMod m) + (u : ZMod m) := by
+      grind;
+    have h_eq_mod : (β + u) % m = b % m := by
+      simp_all +decide [ ← ZMod.natCast_eq_natCast_iff' ];
+    have h_eq_mod : (β + u) % m ∈ B := by
+      have := hB.1 b hb.1; simp_all +decide [ Nat.mod_eq_of_lt ] ;
+    have := hB.2 β hβ u hu.1; simp_all +decide ;
+  rw [ h_eq a ha, h_eq b hb ]
+
+theorem inter_T1_T4_le {m : ℕ} (hm : 2 ≤ m) {B : Finset ℕ} (hB : FoldedOK m B) {β : ℕ}
+    (hβ : β ∈ B) : (T1 m B ∩ T4 m B β).card ≤ 2 := by
+  have := @card_two_sol m ⟨ by omega ⟩ ( β : ZMod m );
+  refine le_trans ( Finset.card_le_card ?_ ) this;
+  intro x hx; simp_all +decide [ T1, T4 ] ;
+  obtain ⟨ ⟨ a, ha, rfl ⟩, hx, ⟨ b, hb, hx' ⟩ ⟩ := hx; simp_all +decide [ sub_eq_iff_eq_add ] ;
+  by_cases hab : a = b <;> simp_all +decide [ two_mul ];
+  have := hB.2 a ha b hb hab; simp_all +decide [ ZMod.natCast_eq_natCast_iff' ] ;
+  have := hB.1 β hβ; simp_all +decide [ ZMod.natCast_eq_zero_iff ] ;
+  have := Nat.mod_eq_of_lt this.2; simp_all +decide [ ← ZMod.val_natCast ] ;
+
+theorem inter_T3_T4_le {m : ℕ} {B : Finset ℕ} (hB : FoldedOK m B) {α β : ℕ}
+    (hα : α ∈ B) (hβ : β ∈ B) (hαβ : α < β) (hmin : ∀ x ∈ B, α ≤ x)
+    (hmin2 : ∀ x ∈ B, x ≠ α → β ≤ x) (hsum : α + β < m)
+    (hnc : α + β ∉ collisions m B) : (T3 m B α ∩ T4 m B β).card ≤ 2 := by
+  have h_inter_T3_T4_le : ∀ z ∈ T3 m B α ∩ T4 m B β, ∀ b ∈ B, ∀ b' ∈ B,
+      z = (b : ZMod m) - (α : ZMod m) ∧ z = (β : ZMod m) - (b' : ZMod m) →
+        b = β ∨ ∃ c ∈ B, 2 * c = α + β + m ∧ z = (c : ZMod m) - (α : ZMod m) := by
+    intros z hz b hb b' hb' h_eq
+    have h_sum : (b + b') % m = (α + β) % m := by
+      simp_all +decide [ ← ZMod.natCast_eq_natCast_iff' ];
+      grind
+    have h_cases : b + b' = α + β ∨ b + b' = α + β + m := by
+      obtain ⟨ k, hk ⟩ := Nat.modEq_iff_dvd.mp h_sum.symm;
+      rcases lt_trichotomy k 0 with hk' | rfl | hk' <;> norm_num at hk ⊢ <;>
+        try (left; nlinarith [ hB.1 b hb, hB.1 b' hb' ]);
+      exact Or.inr ( by nlinarith [ show k = 1 by nlinarith [ hB.1 b hb, hB.1 b' hb' ] ] )
+    obtain h_case1 | h_case2 := h_cases
+    · generalize_proofs at *
+      by_cases hb_eq_α : b = α <;> by_cases hb'_eq_β : b' = β <;> simp_all +decide [ add_comm ]
+      · unfold T3 T4 at hz; aesop
+      · omega
+      · grind +splitImp
+    · by_cases hbb' : b = b' <;>
+        simp_all +decide only [ne_eq, collisions, mem_inter, not_and, sub_left_inj,
+          Nat.add_mod_right]
+      · exact Or.inr ⟨ b', hb', by linarith, rfl ⟩
+      · contrapose! hnc
+        simp_all +decide only [ne_eq, lowSums, mem_image, mem_filter, mem_product, Prod.exists,
+          highSums]
+        exact ⟨ ⟨ α, β, ⟨ ⟨ hα, hβ ⟩, by linarith, by linarith ⟩, rfl ⟩,
+          ⟨ b, b', ⟨ ⟨ hb, hb' ⟩, hbb', by linarith ⟩, Nat.sub_eq_of_eq_add <| by linarith ⟩ ⟩
+  have h_inter_T3_T4_le : ∀ z ∈ T3 m B α ∩ T4 m B β, z = (β : ZMod m) - (α : ZMod m) ∨
+      ∃ c ∈ B, 2 * c = α + β + m ∧ z = (c : ZMod m) - (α : ZMod m) := by
+    grind +locals;
+  have h_inter_T3_T4_le : ∀ c1 c2 : ℕ, c1 ∈ B → c2 ∈ B → 2 * c1 = α + β + m →
+      2 * c2 = α + β + m → c1 = c2 := by
+    intros c1 c2 hc1 hc2 hc1_eq hc2_eq
+    linarith;
+  have h_inter_T3_T4_le : ∀ z1 z2 : ZMod m, z1 ∈ T3 m B α ∩ T4 m B β →
+      z2 ∈ T3 m B α ∩ T4 m B β →
+        z1 = (β : ZMod m) - (α : ZMod m) ∨ z2 = (β : ZMod m) - (α : ZMod m) ∨ z1 = z2 := by
+    grind;
+  contrapose! h_inter_T3_T4_le;
+  obtain ⟨ z1, hz1, z2, hz2, hne ⟩ := Finset.two_lt_card.mp h_inter_T3_T4_le;
+  grind
+
+/-! ### The Case 2 bound -/
+
+/-
+The four-set union bound of Case 2 of the folded additive lemma.
+-/
+theorem case2_bound {m : ℕ} (hm : 2 ≤ m) {B : Finset ℕ} (hB : FoldedOK m B) {α β : ℕ}
+    (hα : α ∈ B) (hβ : β ∈ B) (hαβ : α < β) (hmin : ∀ x ∈ B, α ≤ x)
+    (hmin2 : ∀ x ∈ B, x ≠ α → β ≤ x) (hsum : α + β < m)
+    (hnc : α + β ∉ collisions m B) : 4 * B.card ≤ m + 8 := by
+  by_cases h_even : 2 ∣ m
+  · have := ( four_card_le ( T1 m B ) ( T2 m B ) ( T3 m B α ) ( T4 m B β ) )
+    rw [ card_T1 hB, card_T2 hB, card_T3 hB hα, card_T4 hB hβ ] at this
+    have := union_card_le hm hB α β
+    have := inter_T1_T2_le hB
+    have := inter_T1_T3_le hB hα
+    have := inter_T1_T4_le hm hB hβ
+    have := inter_T2_T3_le hB hα hmin
+    have := inter_T2_T4_le hB hβ
+    have := inter_T3_T4_le hB hα hβ hαβ hmin hmin2 hsum hnc
+    omega
+  · have h_union_card : (T1 m B ∪ T2 m B ∪ T3 m B α ∪ T4 m B β).card ≤ m - 1 := by
+      convert union_card_le hm hB α β using 1
+    have h_four_card_le : (T1 m B).card + (T2 m B).card + (T3 m B α).card + (T4 m B β).card ≤
+        (T1 m B ∪ T2 m B ∪ T3 m B α ∪ T4 m B β).card +
+          ((T1 m B ∩ T2 m B).card + (T1 m B ∩ T3 m B α).card + (T1 m B ∩ T4 m B β).card +
+            (T2 m B ∩ T3 m B α).card + (T2 m B ∩ T4 m B β).card + (T3 m B α ∩ T4 m B β).card) := by
+      convert four_card_le ( T1 m B ) ( T2 m B ) ( T3 m B α ) ( T4 m B β ) using 1
+    have := inter_T1_T3_le hB hα
+    have := inter_T2_T3_le hB hα hmin
+    have := inter_T2_T4_le hB hβ
+    have := inter_T1_T4_le hm hB hβ
+    have := inter_T3_T4_le hB hα hβ hαβ hmin hmin2 hsum hnc
+    simp_all +decide [ card_T1, card_T2, card_T3, card_T4 ]
+    have := inter_T1_T2_odd ( show ¬2 ∣ m from by omega ) hB
+    simp_all +decide [ Finset.ext_iff ]
+    omega
+
+end Erdos865
diff --git a/LeanPool/Erdos865/FoldedMain.lean b/LeanPool/Erdos865/FoldedMain.lean
new file mode 100644
index 00000000..d5bf6069
--- /dev/null
+++ b/LeanPool/Erdos865/FoldedMain.lean
@@ -0,0 +1,264 @@
+/-
+Copyright (c) 2026 Ricky Cipollini. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Ricky Cipollini
+-/
+import LeanPool.Erdos865.FoldedAux
+
+/-!
+# The folded additive lemma
+
+Monotonicity of the sum sets, the reflection `-B = {m - b}` and its effect on
+`lowSums`/`highSums`/`collisions`, and the inductive `core_step` that proves the folded
+additive lemma `folded_additive`.
+-/
+
+open Finset
+
+namespace Erdos865
+
+/-! ### Monotonicity of the sum sets -/
+
+theorem foldedOK_subset {m : ℕ} {B C : Finset ℕ} (hB : FoldedOK m B) (h : C ⊆ B) :
+    FoldedOK m C := by
+  constructor;
+  · exact fun x hx => hB.1 x ( h hx );
+  · exact fun x hx y hy hxy =>
+      ⟨ hB.2 x ( h hx ) y ( h hy ) hxy |>.1,
+        fun hxy' => hB.2 x ( h hx ) y ( h hy ) hxy |>.2 <| h hxy' ⟩
+
+theorem lowSums_mono {m : ℕ} {B C : Finset ℕ} (h : B ⊆ C) : lowSums m B ⊆ lowSums m C := by
+  exact Finset.image_subset_image
+    ( Finset.filter_subset_filter _ ( Finset.product_subset_product h h ) )
+
+theorem highSums_mono {m : ℕ} {B C : Finset ℕ} (h : B ⊆ C) : highSums m B ⊆ highSums m C := by
+  exact Finset.image_subset_iff.mpr fun p hp => Finset.mem_image.mpr
+    ⟨ p, Finset.mem_filter.mpr
+      ⟨ Finset.mem_product.mpr
+        ⟨ h <| Finset.mem_filter.mp hp |>.1 |> Finset.mem_product.mp |>.1,
+          h <| Finset.mem_filter.mp hp |>.1 |> Finset.mem_product.mp |>.2 ⟩,
+        Finset.mem_filter.mp hp |>.2 ⟩, rfl ⟩
+
+theorem collisions_mono {m : ℕ} {B C : Finset ℕ} (h : B ⊆ C) :
+    collisions m B ⊆ collisions m C :=
+  Finset.inter_subset_inter (lowSums_mono h) (highSums_mono h)
+
+theorem mem_lowSums_lt {m : ℕ} {B : Finset ℕ} {v : ℕ} (hv : v ∈ lowSums m B) : v < m := by
+  unfold lowSums at hv;
+  grind
+
+theorem mem_highSums_lt {m : ℕ} (_hm : 2 ≤ m) {B : Finset ℕ} (hB : FoldedOK m B) {v : ℕ}
+    (hv : v ∈ highSums m B) : v < m := by
+  obtain ⟨ p, hp, rfl ⟩ := Finset.mem_image.mp hv;
+  rw [ tsub_lt_iff_left ] <;>
+    linarith [ Finset.mem_filter.mp hp,
+      hB.1 p.1 ( Finset.mem_product.mp ( Finset.mem_filter.mp hp |>.1 ) |>.1 ),
+      hB.1 p.2 ( Finset.mem_product.mp ( Finset.mem_filter.mp hp |>.1 ) |>.2 ) ]
+
+/-
+After deleting the minimum `α`, the value `α + β` is no longer a low pair sum, because
+every remaining pair of distinct elements has both entries `≥ β > α`, so sum `> α + β`.
+-/
+theorem sum_not_lowSums_erase {m : ℕ} {S : Finset ℕ} {α β : ℕ} (hαβ : α < β)
+    (hmin2 : ∀ x ∈ S, x ≠ α → β ≤ x) : α + β ∉ lowSums m (S.erase α) := by
+  simp [lowSums];
+  grind
+
+/-! ### Reflection `-B = {m - b}` -/
+
+/-- The reflected set `-B = {m - b : b ∈ B}`. -/
+def reflB (m : ℕ) (B : Finset ℕ) : Finset ℕ := B.image (fun b : ℕ => m - b)
+
+theorem card_reflB {m : ℕ} {B : Finset ℕ} (hB : FoldedOK m B) : (reflB m B).card = B.card := by
+  rw [ reflB, Finset.card_image_of_injOn ];
+  exact fun x hx y hy hxy => by rw [ tsub_right_inj ] at hxy <;> linarith [ hB.1 x hx, hB.1 y hy ] ;
+
+theorem foldedOK_reflB {m : ℕ} (hm : 2 ≤ m) {B : Finset ℕ} (hB : FoldedOK m B) :
+    FoldedOK m (reflB m B) := by
+  constructor;
+  · intro b hb; obtain ⟨ x, hx, rfl ⟩ := Finset.mem_image.mp hb;
+    exact ⟨ Nat.sub_pos_of_lt ( hB.1 x hx |>.2 ), Nat.sub_lt ( by linarith ) ( hB.1 x hx |>.1 ) ⟩;
+  · intro x hx y hy hxy;
+    constructor;
+    · obtain ⟨ a, ha, rfl ⟩ := Finset.mem_image.mp hx;
+      obtain ⟨ b, hb, rfl ⟩ := Finset.mem_image.mp hy;
+      simp_all +decide [ FoldedOK ];
+      grind +ring;
+    · simp_all +decide only [reflB, mem_image, ne_eq, not_exists, not_and];
+      intro z hz;
+      obtain ⟨ a, ha, rfl ⟩ := hx; obtain ⟨ b, hb, rfl ⟩ := hy; have := hB.2 a ha b hb;
+      simp_all +decide only [ne_eq];
+      contrapose! this;
+      have h_eq : (a + b) % m = z := by
+        have h_eq : (a + b) % m = (m - (m - a + (m - b)) % m) % m := by
+          simp +decide only [← ZMod.natCast_eq_natCast_iff', Nat.cast_add];
+          rw [ Nat.cast_sub ( Nat.le_of_lt ( Nat.mod_lt _ ( by linarith ) ) ) ];
+          simp +decide [ Nat.cast_sub ( show a ≤ m from by linarith [ hB.1 a ha ] ),
+            Nat.cast_sub ( show b ≤ m from by linarith [ hB.1 b hb ] ) ];
+          ring;
+        rw [ h_eq, ← this, Nat.sub_sub_self ( show z ≤ m from by linarith [ hB.1 z hz ] ) ];
+        exact Nat.mod_eq_of_lt ( hB.1 z hz |>.2 );
+      exact ⟨ by aesop, fun _ => h_eq.symm ▸ hz ⟩
+
+theorem lowSums_reflB {m : ℕ} (_hm : 2 ≤ m) {B : Finset ℕ} (hB : FoldedOK m B) :
+    lowSums m (reflB m B) = (highSums m B).image (fun v : ℕ => m - v) := by
+  ext z;
+  constructor;
+  · unfold lowSums highSums;
+    simp +zetaDelta only [ne_eq, mem_image, mem_filter, mem_product, Prod.exists, ↓existsAndEq,
+      and_true, forall_exists_index, and_imp] at *;
+    rintro x y hx hy hxy hxy' rfl; rcases Finset.mem_image.mp hx with ⟨ a, ha, rfl ⟩;
+    rcases Finset.mem_image.mp hy with ⟨ b, hb, rfl ⟩; use a, b; simp_all +decide ;
+    have := hB.1 a ha; have := hB.1 b hb; omega;
+  · simp +zetaDelta only [mem_image, forall_exists_index, and_imp] at *;
+    rintro x hx rfl;
+    unfold highSums lowSums reflB at *;
+    simp +zetaDelta only [ne_eq, mem_image, mem_filter, mem_product, Prod.exists, ↓existsAndEq,
+      and_true] at *;
+    obtain ⟨ a, b, ⟨ ⟨ ha, hb ⟩, hab, h ⟩, rfl ⟩ := hx; use a, b;
+    simp_all +decide [ add_comm ];
+    have := hB.1 a ha; have := hB.1 b hb; omega;
+
+theorem highSums_reflB {m : ℕ} (hm : 2 ≤ m) {B : Finset ℕ} :
+    highSums m (reflB m B) = (lowSums m B).image (fun v : ℕ => m - v) := by
+  ext z;
+  simp only [highSums, ne_eq, reflB, mem_image, mem_filter, mem_product, Prod.exists, ↓existsAndEq,
+    and_true, lowSums];
+  constructor <;> intro h; all_goals grind
+
+theorem collisions_reflB_card {m : ℕ} (hm : 2 ≤ m) {B : Finset ℕ} (hB : FoldedOK m B) :
+    (collisions m (reflB m B)).card = (collisions m B).card := by
+  -- By definition of `collisions`, we know that
+  -- `collisions m (reflB m B) = coll highSums m B ∩ lowSums m B|
+  have h_collisions_refl : collisions m (reflB m B) =
+      ((highSums m B) ∩ (lowSums m B)).image (fun v => m - v) := by
+    unfold collisions
+    rw [lowSums_reflB hm hB, highSums_reflB (B := B) hm]
+    ext z
+    simp only [Finset.mem_inter, Finset.mem_image]
+    constructor
+    · rintro ⟨⟨a, ha, rfl⟩, b, hb, hb'⟩
+      have ha_lt := mem_highSums_lt hm hB ha
+      have hb_lt := mem_lowSums_lt hb
+      have hab : a = b := by omega
+      exact ⟨a, ⟨ha, by rw [hab]; exact hb⟩, rfl⟩
+    · rintro ⟨v, ⟨hv1, hv2⟩, rfl⟩
+      exact ⟨⟨v, hv1, rfl⟩, v, hv2, rfl⟩
+  rw [ h_collisions_refl, collisions ];
+  rw [ Finset.inter_comm, Finset.card_image_of_injOn ];
+  exact fun x hx y hy hxy => by
+    rw [ tsub_right_inj ] at hxy <;>
+      linarith [ mem_lowSums_lt ( Finset.mem_of_mem_inter_left hx ),
+        mem_highSums_lt hm hB ( Finset.mem_of_mem_inter_right hy ) ];
+
+/-! ### The core inductive step -/
+
+theorem core_step {m : ℕ} (hm : 2 ≤ m) {S : Finset ℕ} (hS : FoldedOK m S) {α β : ℕ}
+    (hα : α ∈ S) (hβ : β ∈ S) (hαβ : α < β) (hmin : ∀ x ∈ S, α ≤ x)
+    (hmin2 : ∀ x ∈ S, x ≠ α → β ≤ x) (hsum : α + β < m)
+    (IH : ∀ S', FoldedOK m S' → S'.card < S.card →
+      4 * S'.card ≤ 4 * (collisions m S').card + m + 8) :
+    4 * S.card ≤ 4 * (collisions m S).card + m + 8 := by
+  by_cases hnc : α + β ∈ collisions m S;
+  · obtain ⟨S', hS', hS'_card⟩ :
+        ∃ S' : Finset ℕ, S' = S.erase α ∧ FoldedOK m S' ∧ S'.card < S.card ∧
+          (collisions m S').card + 1 ≤ (collisions m S).card := by
+      refine ⟨ S.erase α, rfl, foldedOK_subset hS ( Finset.erase_subset α S ), ?_, ?_ ⟩;
+      · exact Finset.card_lt_card ( Finset.erase_ssubset hα );
+      · refine Nat.succ_le_of_lt ( Finset.card_lt_card ?_ );
+        refine ⟨ ?_, ?_ ⟩;
+        · exact collisions_mono ( Finset.erase_subset _ _ );
+        · rw [ Finset.not_subset ];
+          refine ⟨ α + β, hnc, ?_ ⟩;
+          exact fun h => sum_not_lowSums_erase hαβ hmin2 <| Finset.mem_of_mem_inter_left h;
+    grind;
+  · linarith [ case2_bound hm hS hα hβ hαβ hmin hmin2 hsum hnc ]
+
+/-! ### The folded additive lemma -/
+
+/-
+**Folded additive lemma.** For `m ≥ 2` and `B` satisfying `FoldedOK`,
+`4 * |B| ≤ 4 * |C(B)| + m + 8`, i.e. `|B| - |C(B)| ≤ m/4 + 2`.
+-/
+theorem folded_additive {m : ℕ} (hm : 2 ≤ m) {B : Finset ℕ} (hB : FoldedOK m B) :
+    4 * B.card ≤ 4 * (collisions m B).card + m + 8 := by
+  by_contra! h_contra;
+  -- By strong induction on B.card, we can assume the statement holds for all sets with
+  -- cardinality less than B.card.
+  induction k : B.card using Nat.strong_induction_on generalizing B m
+  rename_i ih
+  by_cases h_card : B.card ≤ 1;
+  · grind;
+  · -- Let α := B.min' (nonempty proof from card ≥ 2). Then hα : α ∈ B (Finset.min'_mem) and
+    -- hmin : ∀ x ∈ B, α ≤ x (Finset.min'_le).
+    obtain ⟨α, hα⟩ : ∃ α ∈ B, ∀ x ∈ B, α ≤ x := by
+      exact ⟨ Nat.find <| Finset.card_pos.mp <| by linarith,
+        Nat.find_spec <| Finset.card_pos.mp <| by linarith, fun x hx => Nat.find_min' _ hx ⟩
+    obtain ⟨β, hβ⟩ : ∃ β ∈ B.erase α, ∀ x ∈ B.erase α, β ≤ x := by
+      exact ⟨ Finset.min' _
+        ⟨ Classical.choose ( Finset.exists_mem_ne ( by linarith ) α ),
+          Finset.mem_erase_of_ne_of_mem
+            ( Classical.choose_spec ( Finset.exists_mem_ne ( by linarith ) α ) |>.2 )
+            ( Classical.choose_spec ( Finset.exists_mem_ne ( by linarith ) α ) |>.1 ) ⟩,
+        Finset.min'_mem _ _, fun x hx => Finset.min'_le _ _ hx ⟩
+    have hαβ : α < β := by
+      exact lt_of_le_of_ne ( hα.2 β ( Finset.mem_of_mem_erase hβ.1 ) ) ( by aesop )
+    have hmin2 : ∀ x ∈ B, x ≠ α → β ≤ x := by
+      exact fun x hx hx' => hβ.2 x ( Finset.mem_erase_of_ne_of_mem hx' hx )
+    have hsum : α + β < m ∨ β + α > m := by
+      have := hB.2 α hα.1 β ( Finset.mem_of_mem_erase hβ.1 ) ( by linarith ); omega;
+    obtain hsum | hsum := hsum;
+    · exact absurd ( core_step hm hB hα.1 ( Finset.mem_of_mem_erase hβ.1 ) hαβ hα.2 hmin2 hsum
+        fun S' hS' hS'_card => by
+          specialize ih ( S'.card ) ( by linarith [ Finset.card_erase_lt_of_mem hα.1 ] ) hm hS';
+          aesop ) ( by linarith );
+    · -- Let u := B.max' (nonempty), v := (B.erase u).max'. Then:
+      obtain ⟨u, hu⟩ : ∃ u ∈ B, ∀ x ∈ B, x ≤ u := by
+        exact ⟨ Finset.max' B ⟨ α, hα.1 ⟩, Finset.max'_mem _ _, fun x hx => Finset.le_max' _ _ hx ⟩
+      obtain ⟨v, hv⟩ : ∃ v ∈ B.erase u, ∀ x ∈ B.erase u, x ≤ v := by
+        exact ⟨ Finset.max' _ <| Finset.card_pos.mp <|
+            by rw [ Finset.card_erase_of_mem hu.1 ]; omega,
+          Finset.max'_mem _ _, fun x hx => Finset.le_max' _ _ hx ⟩
+      have hu_gt_v : u > v := by
+        grind
+      have huv_gt_m : u + v > m := by
+        grind
+      have huv_ne_m : u + v ≠ m := by
+        grind
+      generalize_proofs at *; (
+      -- Let S := reflB m B, and consider α' := m - u, β' := m - v. Verify the core_step
+      -- hypotheses for S with α', β':
+      set S := reflB m B
+      set α' := m - u
+      set β' := m - v
+      have hS : FoldedOK m S := by
+        exact foldedOK_reflB hm hB
+      have hα' : α' ∈ S := by
+        exact Finset.mem_image.mpr ⟨ u, hu.1, rfl ⟩
+      have hβ' : β' ∈ S := by
+        exact Finset.mem_image.mpr ⟨ v, Finset.mem_of_mem_erase hv.1, rfl ⟩
+      have hα'β' : α' < β' := by
+        exact Nat.sub_lt_sub_left
+          ( by linarith [ hB.1 u hu.1, hB.1 v ( Finset.mem_of_mem_erase hv.1 ) ] ) hu_gt_v
+      have hmin' : ∀ z ∈ S, α' ≤ z := by
+        simp +zetaDelta at *;
+        simp +decide [ reflB ];
+        grind
+      have hmin2' : ∀ z ∈ S, z ≠ α' → β' ≤ z := by
+        simp +zetaDelta at *;
+        simp_all +decide [ reflB ];
+        grind +qlia
+      have hsum' : α' + β' < m := by
+        rw [ tsub_add_tsub_comm ] <;>
+          try linarith [ hB.1 u hu.1, hB.1 v ( Finset.mem_of_mem_erase hv.1 ) ];
+        grind
+      generalize_proofs at *; (
+      -- Apply the core_step lemma to S with α' and β'.
+      have h_core_step : 4 * S.card ≤ 4 * (collisions m S).card + m + 8 := by
+        apply core_step hm hS hα' hβ' hα'β' hmin' hmin2' hsum' (fun S' hS' hS'_card => by
+          exact le_of_not_gt fun h =>
+            ih _ ( by linarith [ show #S = #B from card_reflB hB ] ) hm hS' h rfl)
+      generalize_proofs at *; (
+      grind +suggestions)))
+
+end Erdos865
diff --git a/LeanPool/Erdos865/Folding.lean b/LeanPool/Erdos865/Folding.lean
new file mode 100644
index 00000000..4bbdcc49
--- /dev/null
+++ b/LeanPool/Erdos865/Folding.lean
@@ -0,0 +1,106 @@
+/-
+Copyright (c) 2026 Ricky Cipollini. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Ricky Cipollini
+-/
+import LeanPool.Erdos865.FoldedMain
+
+/-!
+# 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`.
+-/
+
+open Finset
+
+namespace Erdos865
+
+/-
+For a triple-free set `A` with pivot `h ∈ A` and `h ≥ 2`, the folded coordinate set
+`B_h` satisfies the hypothesis of the folded additive lemma modulo `h`.
+-/
+theorem foldedOK_Bset {A : Finset ℕ} {N h : ℕ} (hA : IsTripleFree A) (hh : h ∈ A)
+    (_hh2 : 2 ≤ h) : FoldedOK h (Bset A N h) := by
+  constructor;
+  · exact fun x hx => by unfold Bset at hx; unfold Xset at hx; unfold Yset at hx; aesop;
+  · intro x hx y hy hxy;
+    refine ⟨ ?_, ?_ ⟩ <;> contrapose! hxy <;>
+      simp_all +decide only [Bset, Xset, Yset, mem_inter, mem_filter, mem_Ico];
+    · unfold IsTripleFree at hA; simp_all +decide [ HasTriple ] ;
+      grind +ring;
+    · -- If $x + y \geq h$, then $(x + y) \% h = x + y - h$, which is in $A$.
+      by_cases hxy_ge_h : x + y ≥ h;
+      · have hxy_mod : (x + y) % h = x + y - h := by
+          rw [ Nat.mod_eq_sub_mod hxy_ge_h ];
+          rw [ Nat.mod_eq_of_lt ( by omega ) ];
+        contrapose! hA;
+        simp_all +decide only [add_tsub_cancel_of_le, ge_iff_le, ne_eq, IsTripleFree, not_not];
+        use x, hx.1.2, y, hy.1.2, h, hh;
+        grind;
+      · simp_all +decide [ Nat.mod_eq_of_lt ( not_le.mp hxy_ge_h ) ];
+        unfold IsTripleFree at hA; simp_all +decide [ HasTriple ] ;
+        grind +ring
+
+/-
+Collisions of `B_h` land in the "excluded" set `E`.
+-/
+theorem collisions_subset_Eset {A : Finset ℕ} {N h : ℕ} (hA : IsTripleFree A) (hh : h ∈ A) :
+    collisions h (Bset A N h) ⊆ Eset A N h := by
+  intro r hr;
+  refine Finset.mem_sdiff.mpr ⟨ ?_, ?_ ⟩;
+  · unfold collisions at hr;
+    unfold lowSums highSums at hr;
+    grind;
+  · simp_all +decide only [collisions, lowSums, ne_eq, highSums, mem_inter, mem_image, mem_filter,
+      mem_product, Prod.exists, Xset, Yset, mem_union, mem_Ico, not_or, not_and, and_imp];
+    constructor <;> intros <;> simp_all +decide only [Bset, mem_inter];
+    · obtain ⟨ ⟨ a, b, ⟨ ⟨ ⟨ ha₁, ha₂ ⟩, hb₁, hb₂ ⟩, hab, hlt ⟩, rfl ⟩,
+        c, d, ⟨ ⟨ ⟨ hc₁, hc₂ ⟩, hd₁, hd₂ ⟩, hcd, hlt' ⟩, hcd' ⟩ := hr;
+      contrapose! hA;
+      unfold IsTripleFree;
+      simp_all +decide only [Xset, mem_filter, mem_Ico, Yset, and_self, true_and, not_not];
+      exact ⟨ a, ha₁.2, b, hb₁.2, h, hh, by omega, by omega, by omega, by ring_nf at *; aesop ⟩;
+    · obtain ⟨ a, b, ⟨ ⟨ ⟨ ha₁, ha₂ ⟩, ⟨ hb₁, hb₂ ⟩ ⟩, hab, hlt ⟩, rfl ⟩ := hr.2;
+      contrapose! hA;
+      unfold IsTripleFree;
+      simp_all +decide only [Xset, mem_filter, mem_Ico, Yset, and_self, true_and, not_not];
+      use a, ha₁.2, b, hb₁.2, h, hh;
+      grind
+
+/-
+The elementary counting identity `|X| + |Y| + |E| = (h-1) + |B_h|`.
+-/
+theorem 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 := by
+  rw [ Eset, Finset.card_sdiff ];
+  rw [ ← Finset.card_union_add_card_inter, Bset ];
+  rw [ show ( Xset A h ∪ Yset A N h ) ∩ Ico 1 h = Xset A h ∪ Yset A N h from ?_ ];
+  · rw [ add_right_comm, Nat.add_sub_of_le ];
+    · simp +arith +decide;
+    · exact Finset.card_le_card
+        ( Finset.union_subset ( Finset.filter_subset _ _ ) ( Finset.filter_subset _ _ ) );
+  · exact Finset.inter_eq_left.mpr
+      ( Finset.union_subset ( Finset.filter_subset _ _ ) ( Finset.filter_subset _ _ ) )
+
+/-
+**Folding lemma.** For a triple-free `A` and pivot `h ∈ A`,
+`4(|X|+|Y|) + 4|E \ C(B_h)| ≤ 5h + 4`, i.e. `|X|+|Y| ≤ 5h/4 - |E \ C(B_h)| + 1`.
+-/
+theorem 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 := by
+  by_cases h_ge_2 : 2 ≤ h;
+  · -- By the folding lemma, we have $4 * |B_h| \leq 4 * |C(B_h)| + h + 8$.
+    have h_folding : 4 * (Bset A N h).card ≤ 4 * (collisions h (Bset A N h)).card + h + 8 := by
+      exact Erdos865.folded_additive h_ge_2 ( Erdos865.foldedOK_Bset hA hh h_ge_2 );
+    have h_collisions_subset_Eset :
+        (collisions h (Bset A N h)).card + #(Eset A N h \ collisions h (Bset A N h))
+          = (Eset A N h).card := by
+      rw [ ← Finset.card_union_of_disjoint ];
+      · rw [ Finset.union_sdiff_of_subset ( collisions_subset_Eset hA hh ) ];
+      · exact Finset.disjoint_sdiff;
+    linarith [ card_XY_E A N h, Nat.sub_add_cancel ( by linarith : 1 ≤ h ) ];
+  · interval_cases h <;> simp_all +decide [ Xset, Yset, Eset, Bset ]
+
+end Erdos865
diff --git a/LeanPool/Erdos865/Main.lean b/LeanPool/Erdos865/Main.lean
new file mode 100644
index 00000000..ce526786
--- /dev/null
+++ b/LeanPool/Erdos865/Main.lean
@@ -0,0 +1,53 @@
+/-
+Copyright (c) 2026 Ricky Cipollini. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Ricky Cipollini
+-/
+import LeanPool.Erdos865.UpperBound
+import LeanPool.Erdos865.Sharpness
+
+/-!
+# A sharp `5/8` bound for Erdős Problem 865
+
+For `A ⊆ {1, …, N}` we say `A` contains a *pairwise-sum triple* if there are distinct
+`a, b, c ∈ A` with `a + b, a + c, b + c ∈ A` (`Erdos865.HasTriple`). Let `f₃(N)` be the least
+size forcing such a triple. This file assembles the proof that
+`f₃(N) = 5N/8 + O(1)`, resolving Erdős Problem 865.
+
+* `Erdos865.erdos865_upper_bound` — every triple-free `A ⊆ [1,N]` has `8|A| ≤ 5N + 53`,
+  i.e. `|A| ≤ 5N/8 + O(1)`.
+* `Erdos865.erdos865_contains_triple` — every `A ⊆ [1,N]` with `8|A| > 5N + 53` contains a
+  pairwise-sum triple (the contrapositive form matching the paper's Theorem 1.1).
+* `Erdos865.erdos865` — the packaged existence statement `∃ C, …`.
+* `Erdos865.sharpness` — for `N = 8M` (`M ≥ 1`) there is a triple-free `A ⊆ [1,N]` with
+  `8|A| = 5N + 16`, so the constant `5/8` is optimal.
+-/
+
+open Finset
+
+namespace Erdos865
+
+/-- **Upper bound (Erdős 865).** Every triple-free set `A ⊆ [1,N]` satisfies
+`8 * |A| ≤ 5 * N + 53`, i.e. `|A| ≤ (5/8) N + O(1)`. -/
+theorem erdos865_upper_bound (N : ℕ) (A : Finset ℕ) (hsub : A ⊆ Finset.Icc 1 N)
+    (hA : IsTripleFree A) : 8 * A.card ≤ 5 * N + 53 := by
+  have hsub' : A ⊆ Finset.Icc 1 (2 * ((N + 1) / 2)) :=
+    hsub.trans (Finset.Icc_subset_Icc_right (by omega))
+  have h := even_bound ((N + 1) / 2) A hsub' hA
+  omega
+
+/-- **Contains a triple (Erdős 865, Theorem 1.1 form).** Every `A ⊆ [1,N]` with
+`5 * N + 53 < 8 * |A|` (i.e. `|A| ≥ (5/8) N + O(1)`) contains a pairwise-sum triple. -/
+theorem erdos865_contains_triple (N : ℕ) (A : Finset ℕ) (hsub : A ⊆ Finset.Icc 1 N)
+    (hcard : 5 * N + 53 < 8 * A.card) : HasTriple A := by
+  by_contra h
+  have := erdos865_upper_bound N A hsub h
+  omega
+
+/-- The upper bound packaged as an existence statement: there is an absolute constant `C`
+such that every triple-free `A ⊆ [1,N]` has `8 * |A| ≤ 5 * N + C`. -/
+theorem erdos865 : ∃ C : ℕ, ∀ (N : ℕ) (A : Finset ℕ), A ⊆ Finset.Icc 1 N →
+    IsTripleFree A → 8 * A.card ≤ 5 * N + C :=
+  ⟨53, erdos865_upper_bound⟩
+
+end Erdos865
diff --git a/LeanPool/Erdos865/Sharpness.lean b/LeanPool/Erdos865/Sharpness.lean
new file mode 100644
index 00000000..4c51a0af
--- /dev/null
+++ b/LeanPool/Erdos865/Sharpness.lean
@@ -0,0 +1,53 @@
+/-
+Copyright (c) 2026 Ricky Cipollini. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Ricky Cipollini
+-/
+import LeanPool.Erdos865.Defs
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum
+import Mathlib.Tactic.Ring
+
+/-!
+# Sharpness of the 5/8 bound (Erdős 865, §5)
+
+The construction `A = [M,2M] ∪ [4M,8M]` is triple-free of size `5M + 2`, so for `N = 8M`
+one has `8·|A| = 5·N + 16`, showing the constant `5/8` is optimal.
+-/
+
+open Finset
+
+namespace Erdos865
+
+/-- The sharpness construction `A = [M, 2M] ∪ [4M, 8M]`. -/
+def sharpSet (M : ℕ) : Finset ℕ := Finset.Icc M (2 * M) ∪ Finset.Icc (4 * M) (8 * M)
+
+/-- The construction sits inside `[1, 8M]` (for `M ≥ 1`). -/
+theorem sharpSet_subset {M : ℕ} (hM : 1 ≤ M) : sharpSet M ⊆ Finset.Icc 1 (8 * M) :=
+  Finset.union_subset (Finset.Icc_subset_Icc (by linarith) (by linarith))
+    (Finset.Icc_subset_Icc (by linarith) (by linarith))
+
+/-- The construction has `5M + 2` elements. -/
+theorem sharpSet_card {M : ℕ} (hM : 1 ≤ M) : (sharpSet M).card = 5 * M + 2 := by
+  have hdisj : Disjoint (Finset.Icc M (2 * M)) (Finset.Icc (4 * M) (8 * M)) :=
+    Finset.disjoint_left.mpr fun x hx₁ hx₂ => by
+      simp only [Finset.mem_Icc] at hx₁ hx₂; omega
+  rw [sharpSet, Finset.card_union_of_disjoint hdisj, Nat.card_Icc, Nat.card_Icc]
+  omega
+
+/-- The construction is triple-free. -/
+theorem sharpSet_tripleFree (M : ℕ) : IsTripleFree (sharpSet M) := by
+  intro h;
+  obtain ⟨ a, ha, b, hb, c, hc, hab, hac, hbc, hab', hac', hbc' ⟩ := h;
+  unfold sharpSet at *;
+  grind
+
+/-- Sharpness: for `N = 8M` with `M ≥ 1` there is a triple-free subset of `[1,N]`
+of size `5M + 2`, i.e. with `8 * card = 5 * N + 16`. -/
+theorem sharpness {M : ℕ} (hM : 1 ≤ M) :
+    ∃ A : Finset ℕ, A ⊆ Finset.Icc 1 (8 * M) ∧ IsTripleFree A ∧
+      8 * A.card = 5 * (8 * M) + 16 := by
+  refine ⟨sharpSet M, sharpSet_subset hM, sharpSet_tripleFree M, ?_⟩
+  rw [sharpSet_card hM]; ring
+
+end Erdos865
diff --git a/LeanPool/Erdos865/UpperBound.lean b/LeanPool/Erdos865/UpperBound.lean
new file mode 100644
index 00000000..b8ca95de
--- /dev/null
+++ b/LeanPool/Erdos865/UpperBound.lean
@@ -0,0 +1,217 @@
+/-
+Copyright (c) 2026 Ricky Cipollini. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Ricky Cipollini
+-/
+import LeanPool.Erdos865.Folding
+
+/-!
+# 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`.
+-/
+
+open Finset
+
+namespace Erdos865
+
+/-
+Counting bound: every element of `A ⊆ [1,N]` is counted by `X`, by `Y`, is one of the
+two endpoints `h, 2h`, or lies in the tail `(2h, N]`.
+-/
+theorem 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) := by
+  -- Let's show that $A$ is a subset of
+  -- $Xset A h ∪ (Yset A N h).image (fun r => h + r) ∪ {h, 2*h} ∪ Finset.Icc (2*h + 1) N$.
+  have h_subset : A ⊆ Xset A h ∪ (Yset A N h).image (fun r => h + r) ∪ {h, 2 * h} ∪
+      Finset.Icc (2 * h + 1) N := by
+    intro a ha; by_cases ha1 : a < h <;> by_cases ha2 : a = h <;> by_cases ha3 : a = 2 * h <;>
+      simp_all +decide only [subset_iff, mem_Icc, lt_self_iff_false, not_lt, not_false_eq_true,
+        mem_singleton, insert_eq_of_mem, union_insert, union_assoc, union_singleton, insert_union,
+        mem_insert, mem_union, mem_image, Nat.add_eq_left, exists_eq_right, add_le_iff_nonpos_right,
+        Order.add_one_le_iff, and_true, or_false, false_or, true_or, or_true];
+    · exact Or.inl <|
+        Finset.mem_filter.mpr ⟨ Finset.mem_Ico.mpr ⟨ by linarith [ hsub ha ], ha1 ⟩, ha ⟩;
+    · by_cases ha4 : a < 2 * h <;>
+        simp_all +decide only [not_lt, Xset, mem_filter, mem_Ico, true_and, and_true, Yset];
+      · exact Or.inr <| Or.inl
+          ⟨ a - h, ⟨ ⟨ Nat.sub_pos_of_lt <| lt_of_le_of_ne ha1 <| Ne.symm ha2, by omega ⟩,
+            by linarith [ hsub ha, Nat.sub_add_cancel ha1 ], by convert ha using 1; omega ⟩,
+            by omega ⟩;
+      · exact Or.inr <| Or.inr <| lt_of_le_of_ne ha4 <| Ne.symm ha3;
+  refine le_trans ( Finset.card_le_card h_subset ) ?_;
+  refine le_trans ( Finset.card_union_le _ _ ) ( add_le_add ( le_trans ( Finset.card_union_le _ _ )
+    ( add_le_add ( le_trans ( Finset.card_union_le _ _ ) ( add_le_add
+      ( Finset.card_le_card ( Finset.Subset.refl _ ) ) ( Finset.card_image_le ) ) )
+      ( Finset.card_insert_le _ _ ) ) ) ( by simp +arith +decide [ Nat.card_Icc ] ) )
+
+/-
+The open interval `(p, q)` contains no element of `A`.
+-/
+theorem 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, ¬ (p < a ∧ a < q) := by
+  grind +qlia
+
+/-
+Case 1 interval `I = (max(p, N-h), h)` is contained in `E \ C(B_h)` for `h = q`.
+-/
+theorem 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) := by
+  intro x hx;
+  simp_all +decide only [mem_Ico, Order.add_one_le_iff, sup_lt_iff, Eset, Bset, mem_sdiff, and_true,
+    mem_union, not_or];
+  refine ⟨ ⟨ by linarith, ?_, ?_ ⟩, ?_ ⟩ <;>
+    simp_all +decide only [Xset, Yset, mem_filter, mem_Ico, and_true, not_and, collisions,
+      mem_inter];
+  · grind;
+  · grind;
+  · intro hx₁ hx₂; simp_all +decide [ lowSums, highSums ] ;
+    omega
+
+/-
+**Case 1** (`s ≤ 4e`): folding around `h = q`.
+-/
+theorem 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 := by
+  have := @folding_lemma A ( 2 * H ) q ?_ ?_ <;>
+    simp_all +decide only [tsub_le_iff_right, ge_iff_le];
+  have hIle := Finset.card_le_card
+    ( case1_I_sub hqlo hqmin hpmax :
+      Finset.Ico ( Max.max p ( 2 * H - q ) + 1 ) q ⊆
+        Eset A ( 2 * H ) q \ collisions q ( Bset A ( 2 * H ) q ) );
+  simp_all +decide [ Nat.card_Ico ];
+  have hcount := card_A_bound hsub q; simp_all +decide ;
+  omega
+
+/-
+In case 2 (`h = p`), the folded coordinate set avoids `[1, q-p-1]`, since for
+`1 ≤ r < q - p` the partner `p + r` lies in the empty gap `(p, q)`.
+-/
+theorem 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) = ∅ := by
+  simp +decide [ Bset, Yset ];
+  grind +splitIndPred
+
+/-
+Case 2 interval `I = [1, t] \ A` (with `t = q - p - 1`) is contained in `E \ C(B_p)`,
+provided `q - p ≤ p` (so the interval sits below the pivot).
+-/
+theorem 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) := by
+  intro x hx; simp_all +decide only [tsub_le_iff_right, mem_sdiff, mem_Ico] ;
+  constructor;
+  · simp_all +decide [ Eset, Xset, Yset ];
+    grind +splitImp;
+  · intro hx';
+    obtain ⟨ y, hy, z, hz, hyz, rfl ⟩ := Finset.mem_image.mp ( Finset.mem_inter.mp hx' |>.1 );
+    simp_all +decide [ Bset, Xset, Yset ];
+    grind
+
+/-- A subset of a triple-free set is triple-free. -/
+theorem tripleFree_subset {A B : Finset ℕ} (hA : IsTripleFree A) (h : B ⊆ A) :
+    IsTripleFree B := by
+  intro ⟨a, ha, b, hb, c, hc, hab, hac, hbc, hab', hac', hbc'⟩
+  exact hA ⟨a, h ha, b, h hb, c, h hc, hab, hac, hbc, h hab', h hac', h hbc'⟩
+
+/-
+**Case 2** (`s > 4e`): folding around `h = p`, using the induction hypothesis on
+`A ∩ [1, q-p-1]`.
+-/
+theorem 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 := by
+  by_cases hq_p : p < q - p;
+  · have hAsub : A ⊆ Finset.Icc 1 p ∪ Finset.Icc q (2 * H) := by
+      grind;
+    have := Finset.card_mono hAsub; simp_all +decide [ Finset.card_union ] ;
+    omega;
+  · -- Apply the folding_lemma to get the inequality involving the cardinalities of Xset, Yset,
+    -- and Eset.
+    have h_fold : 4 * ((Xset A p).card + (Yset A (2 * H) p).card) +
+        4 * (Eset A (2 * H) p \ collisions p (Bset A (2 * H) p)).card ≤ 5 * p + 4 := by
+      apply folding_lemma hA hp;
+    have h_I_sub : (Finset.Ico 1 (q - p) \ A) ⊆
+        Eset A (2 * H) p \ collisions p (Bset A (2 * H) p) := by
+      apply case2_I_sub (by
+      omega) hqmin hpmax;
+    have h_A0 : 4 * (A ∩ Finset.Ico 1 (q - p)).card ≤ 5 * ((q - p) / 2) + 24 := by
+      apply IH ((q - p) / 2) (A ∩ Finset.Ico 1 (q - p));
+      · omega;
+      · grind;
+      · exact tripleFree_subset hA ( Finset.inter_subset_left );
+    have h_card_A : A.card ≤ (Xset A p).card + (Yset A (2 * H) p).card + 2 + (2 * H - 2 * p) := by
+      apply card_A_bound hsub p;
+    have h_card_Ico : (Finset.Ico 1 (q - p)).card =
+        (Finset.Ico 1 (q - p) \ A).card + (A ∩ Finset.Ico 1 (q - p)).card := by
+      grind;
+    have := Finset.card_le_card h_I_sub; simp_all +decide ;
+    omega
+
+/-
+The even-`N` upper bound: every triple-free `A ⊆ [1, 2H]` has `4|A| ≤ 5H + 24`,
+i.e. `|A| ≤ 5H/4 + 6`. Proved by strong induction on `H`.
+-/
+theorem even_bound (H : ℕ) (A : Finset ℕ) (hsub : A ⊆ Finset.Icc 1 (2 * H))
+    (hA : IsTripleFree A) : 4 * A.card ≤ 5 * H + 24 := by
+  induction H using Nat.strong_induction_on generalizing A
+  rename_i H ih
+  by_cases h1 : (A ∩ Finset.Icc H (2 * H)).Nonempty;
+  · by_cases h2 : (A ∩ Finset.Icc 1 H).Nonempty;
+    · -- Let $q = \min(A \cap [H, 2H])$ and $p = \max(A \cap [1, H])$.
+      obtain ⟨q, hq⟩ : ∃ q ∈ A, H ≤ q ∧ q ≤ 2 * H ∧ ∀ a ∈ A, H ≤ a → q ≤ a := by
+        exact ⟨ Nat.find h1,
+          Nat.find_spec h1 |> fun x => Finset.mem_of_mem_inter_left x,
+          Nat.find_spec h1 |> fun x => Finset.mem_Icc.mp ( Finset.mem_inter.mp x |>.2 ) |>.1,
+          Nat.find_spec h1 |> fun x => Finset.mem_Icc.mp ( Finset.mem_inter.mp x |>.2 ) |>.2,
+          fun a ha ha' => Nat.find_min' h1 <|
+            Finset.mem_inter.mpr
+              ⟨ ha, Finset.mem_Icc.mpr ⟨ ha', by linarith [ Finset.mem_Icc.mp ( hsub ha ) ] ⟩ ⟩ ⟩
+      obtain ⟨p, hp⟩ : ∃ p ∈ A, 1 ≤ p ∧ p ≤ H ∧ ∀ a ∈ A, a ≤ H → a ≤ p := by
+        obtain ⟨p, hp⟩ : ∃ p ∈ A ∩ Finset.Icc 1 H, ∀ a ∈ A ∩ Finset.Icc 1 H, a ≤ p := by
+          exact ⟨ Finset.max' _ h2, Finset.max'_mem _ h2, fun a ha => Finset.le_max' _ _ ha ⟩;
+        exact ⟨ p, Finset.mem_of_mem_inter_left hp.1,
+          Finset.mem_Icc.mp ( Finset.mem_inter.mp hp.1 |>.2 ) |>.1,
+          Finset.mem_Icc.mp ( Finset.mem_inter.mp hp.1 |>.2 ) |>.2,
+          fun a ha ha' => hp.2 a
+            ( Finset.mem_inter.mpr
+              ⟨ ha, Finset.mem_Icc.mpr ⟨ Finset.mem_Icc.mp ( hsub ha ) |>.1, ha' ⟩ ⟩ ) ⟩;
+      by_cases hcase : q - H ≤ 4 * (H - p);
+      · apply even_bound_case1 hsub hA hq.left hq.right.left hq.right.right.left
+          hq.right.right.right hp.left hp.right.left hp.right.right.left hp.right.right.right hcase;
+      · apply even_bound_case2 hsub hA hq.right.left hq.right.right.left hq.right.right.right
+          hp.left hp.right.left hp.right.right.left hp.right.right.right (by omega)
+          (fun H' A' h1 h2 h3 => ih H' h1 A' h2 h3);
+    · simp_all +decide only [not_nonempty_iff_eq_empty, Finset.ext_iff, mem_inter, mem_Icc,
+        notMem_empty, iff_false, not_and, not_le];
+      have := Finset.card_le_card ( show A ⊆ Finset.Icc ( H + 1 ) ( 2 * H ) from fun x hx =>
+        Finset.mem_Icc.mpr ⟨ by linarith [ h2 x hx ( Finset.mem_Icc.mp ( hsub hx ) |>.1 ) ],
+          by linarith [ Finset.mem_Icc.mp ( hsub hx ) |>.2 ] ⟩ );
+      simp_all +arith +decide;
+      omega;
+  · rcases H with ( _ | H ) <;>
+      simp_all +decide only [not_lt_zero, not_isEmpty_of_nonempty, IsEmpty.forall_iff, implies_true,
+        mul_zero, Order.lt_one_iff, Icc_eq_empty_of_lt, subset_empty, Finset.Nonempty, Icc_self,
+        notMem_empty, not_false_eq_true, inter_singleton_of_notMem, exists_const, card_empty,
+        zero_add, zero_le, Order.lt_add_one_iff, mem_inter, mem_Icc, Order.add_one_le_iff,
+        not_exists, not_and, not_le];
+    exact le_trans ( Nat.mul_le_mul_left _ ( Finset.card_le_card
+      ( show A ⊆ Finset.Icc 1 ( H + 1 ) from fun x hx => Finset.mem_Icc.mpr
+        ⟨ Finset.mem_Icc.mp ( hsub hx ) |>.1,
+          Nat.le_of_not_lt fun hx' =>
+            by linarith [ Finset.mem_Icc.mp ( hsub hx ) |>.2, h1 x hx ( by linarith ) ] ⟩ ) ) )
+      ( by simp +arith +decide )
+
+end Erdos865
diff --git a/LeanPool/projects.yml b/LeanPool/projects.yml
index 0cfdd676..f177656d 100644
--- a/LeanPool/projects.yml
+++ b/LeanPool/projects.yml
@@ -833,6 +833,50 @@ projects:
       - erdos-problems
     msc:
       - "11B83"
+  - slug: erdos865
+    title: "A sharp 5/8 bound for Erdős Problem 865"
+    summary: >-
+      Formalizes the resolution of Erdős Problem 865 on pairwise sums. For A ⊆ {1,…,N}, a
+      pairwise-sum triple is a set of distinct a, b, c ∈ A with a+b, a+c, b+c all in A, and A
+      is triple-free when it has none. The development proves that every triple-free A ⊆ [1,N]
+      satisfies 8·|A| ≤ 5·N + 53, that any A exceeding this bound contains a triple, and — via
+      the construction A = [M,2M] ∪ [4M,8M] for N = 8M — that the constant 5/8 is optimal, so
+      f₃(N) = 5N/8 + O(1). The upper bound runs through a folded additive lemma over ℤ/mℤ (a
+      four-set union bound) and a folding lemma, closed by strong induction on N.
+    branch: additive combinatorics
+    entry_module: LeanPool.Erdos865
+    authors:
+      - Ricky Cipollini
+    source:
+      title: "A sharp 5/8 bound for an Erdős–Sós pairwise-sums problem"
+      url: "https://github.com/mrricky22/erdos-865-lean"
+      github_repo: mrricky22/erdos-865-lean
+    license: Apache-2.0
+    status: verified
+    provenance: AI
+    main_declarations:
+      - Erdos865.erdos865_upper_bound
+      - Erdos865.sharpness
+    main_results:
+      - declaration: Erdos865.erdos865_upper_bound
+        informal: >-
+          Every triple-free set A ⊆ [1,N] satisfies 8·|A| ≤ 5·N + 53, i.e. |A| ≤ (5/8)·N + O(1).
+      - declaration: Erdos865.erdos865_contains_triple
+        informal: >-
+          Every A ⊆ [1,N] with 5·N + 53 < 8·|A| contains a pairwise-sum triple (the paper's
+          Theorem 1.1 form).
+      - declaration: Erdos865.sharpness
+        informal: >-
+          For N = 8M with M ≥ 1 there is a triple-free A ⊆ [1,N] with 8·|A| = 5·N + 16, so the
+          constant 5/8 is optimal.
+    tags:
+      - additive-combinatorics
+      - erdos-problems
+      - sum-free-sets
+      - combinatorics
+    msc:
+      - "11B75"
+      - "11B13"
   - slug: erdos137
     title: "Erdős Problem #137: powerful products of consecutive integers"
     summary: >-