erdos-402

theorem Opn.erdos_402 :
    ∀ (A : Finset ℕ), 0 ∉ A → A.Nonempty → ∃ᵉ (a ∈ A) (b ∈ A), a.gcd b ≤ (a / A.card : ℚ) := by
  -- Skeleton of the Balasubramanian–Soundararajan / Szegedy argument for Graham's conjecture.
  -- Hole 1 (Farey structure): if every ratio a / gcd(a, b) over A is at most m, then every
  -- quotient a / b is a reduced fraction u / v with 1 ≤ u, v ≤ m.
  have h1 : ∀ (A : Finset ℕ) (m : ℕ), 0 ∉ A → (∀ a ∈ A, ∀ b ∈ A, a ≤ m * a.gcd b) →
      ∀ a ∈ A, ∀ b ∈ A, ∃ u v : ℕ, 0 < u ∧ u ≤ m ∧ 0 < v ∧ v ≤ m ∧ Nat.Coprime u v ∧
        a * v = b * u := sorry
  -- Hole 2 (reduction to primitive sets): the ratio a / gcd(a, b) is invariant under scaling, so
  -- the conclusion for every set of the same size with gcd 1 gives it for A.
  have h2 : ∀ A : Finset ℕ, 0 ∉ A → A.Nonempty →
      (∀ B : Finset ℕ, 0 ∉ B → B.card = A.card → B.gcd id = 1 →
        ∃ᵉ (a ∈ B) (b ∈ B), a.gcd b ≤ (a / B.card : ℚ)) →
      ∃ᵉ (a ∈ A) (b ∈ A), a.gcd b ≤ (a / A.card : ℚ) := sorry
  -- Hole 3 (the core, Balasubramanian–Soundararajan 1996; Szegedy 1986 and Zaharescu 1987 for
  -- large sets): a primitive set all of whose quotients are Farey fractions of order |A|
  -- satisfies Graham's bound.
  have h3 : ∀ A : Finset ℕ, 0 ∉ A → A.Nonempty → A.gcd id = 1 →
      (∀ a ∈ A, ∀ b ∈ A, ∃ u v : ℕ, 0 < u ∧ u ≤ A.card ∧ 0 < v ∧ v ≤ A.card ∧
        Nat.Coprime u v ∧ a * v = b * u) →
      ∃ᵉ (a ∈ A) (b ∈ A), a.gcd b ≤ (a / A.card : ℚ) := sorry
  -- Assembly: reduce to a primitive B of the same size; if the bound failed on B, every ratio
  -- would be below |B|, so B would have Farey structure of order |B|, and the core gives the
  -- bound after all.
  intro A hA hne
  refine h2 A hA hne ?_
  intro B hB hcard hg
  by_contra hcon
  push_neg at hcon
  have hBne : B.Nonempty := by
    rw [← Finset.card_pos, hcard]
    exact hne.card_pos
  have hbound : ∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b := by
    intro a ha b hb
    have h := hcon a ha b hb
    have hpos : (0 : ℚ) < B.card := by exact_mod_cast hBne.card_pos
    have h' : (a : ℚ) < (a.gcd b : ℚ) * B.card := by
      first
        | exact (div_lt_iff₀ hpos).mp h
        | exact (div_lt_iff hpos).mp h
    rw [mul_comm] at h'
    have h'' : a < B.card * a.gcd b := by exact_mod_cast h'
    exact h''.le
  obtain ⟨a, ha, b, hb, hle⟩ := h3 B hB hBne hg (h1 B B.card hB hbound)
  exact absurd hle (not_le.mpr (hcon a ha b hb))

The gate replayed this file at its merge, each hole a sorry (D-12 #5); the whole file: targets/erdos-402/nodes/erdos-402/attempts/20260917T141927Z-calib-402-f480-partial.lean

theorem erdos_402__h3 : (∀ (A : Finset ℕ) (m : ℕ),
    0 ∉ A →
      (∀ a ∈ A, ∀ b ∈ A, a ≤ m * a.gcd b) →
        ∀ a ∈ A, ∀ b ∈ A, ∃ u v, 0 < u ∧ u ≤ m ∧ 0 < v ∧ v ≤ m ∧ u.Coprime v ∧ a * v = b * u) →
  (∀ (A : Finset ℕ),
      0 ∉ A →
        A.Nonempty →
          (∀ (B : Finset ℕ), 0 ∉ B → B.card = A.card → B.gcd id = 1 → ∃ a ∈ B, ∃ b ∈ B, a.gcd b ≤ (a / B.card : ℚ)) →
            ∃ a ∈ A, ∃ b ∈ A, a.gcd b ≤ (a / A.card : ℚ)) →
    ∀ (A : Finset ℕ),
      0 ∉ A →
        A.Nonempty →
          A.gcd id = 1 →
            (∀ a ∈ A, ∀ b ∈ A, ∃ u v, 0 < u ∧ u ≤ A.card ∧ 0 < v ∧ v ≤ A.card ∧ u.Coprime v ∧ a * v = b * u) →
              ∃ a ∈ A, ∃ b ∈ A, a.gcd b ≤ (a / A.card : ℚ) := by
  -- Informal argument: annex f5450271cb4865766831f2e6b153cb532934219590cff79ed42bb2ff813b15ac on
  -- this node (graph PR #265, still in the merge queue when this was submitted, so not cited in
  -- the `annex:` form, which a precheck refuses as annex-pending until the annex has merged).
  -- Hole (the remaining sizes): Graham's bound for a primitive set whose size n is neither a
  -- prime nor one more than a prime, whose quotients a / gcd(a, b) are at most n, and in which
  -- every prime power dividing an element is below n. This is where Balasubramanian and
  -- Soundararajan (1996) is still needed.
  have hcomp : ∀ B : Finset ℕ, 0 ∉ B → B.Nonempty → B.gcd id = 1 → ¬ B.card.Prime →
      (∀ q : ℕ, q.Prime → B.card ≠ q + 1) →
      (∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) →
      (∀ a ∈ B, ∀ p k : ℕ, p.Prime → p ^ k ∣ a → p ^ k < B.card) →
      ∃ a ∈ B, ∃ b ∈ B, a.gcd b ≤ (a / B.card : ℚ) := sorry
  intro _hh1 _hh2 A hA hne hg _hfarey
  by_contra hcon
  push Not at hcon
  have hn : 0 < A.card := hne.card_pos
  have hnq : (0 : ℚ) < A.card := by exact_mod_cast hn
  -- If the bound fails, every quotient a / gcd(a, b) is below n = |A|.
  have hlt : ∀ a ∈ A, ∀ b ∈ A, a < A.card * a.gcd b := by
    intro a ha b hb
    have h' : (a : ℚ) < (a.gcd b : ℚ) * A.card := (div_lt_iff₀ hnq).mp (hcon a ha b hb)
    have h'' : (a : ℚ) < ((A.card * a.gcd b : ℕ) : ℚ) := by push_cast; linarith
    exact_mod_cast h''
  -- Prime powers: since gcd A = 1 some b is prime to p, and p ^ k divides a / gcd(a, b) < n.
  have hpp : ∀ a ∈ A, ∀ p k : ℕ, p.Prime → p ^ k ∣ a → p ^ k < A.card := by
    intro a ha p k hp hdvd
    obtain ⟨b, hb, hpb⟩ : ∃ b ∈ A, ¬ p ∣ b := by
      by_contra h
      push Not at h
      have h1 : p ∣ A.gcd id := Finset.dvd_gcd (fun b hb => h b hb)
      rw [hg] at h1
      exact hp.one_lt.ne' (Nat.dvd_one.mp h1)
    have ha0 : a ≠ 0 := fun h => hA (h ▸ ha)
    have hg0 : 0 < a.gcd b := Nat.gcd_pos_of_pos_left b (Nat.pos_of_ne_zero ha0)
    obtain ⟨x, hx⟩ := Nat.gcd_dvd_left a b
    have hcop : Nat.Coprime (p ^ k) (a.gcd b) := by
      apply Nat.Coprime.pow_left
      rw [Nat.Prime.coprime_iff_not_dvd hp]
      intro h
      exact hpb (h.trans (Nat.gcd_dvd_right a b))
    have hdx : p ^ k ∣ x := by
      have h1 : p ^ k ∣ a.gcd b * x := hx ▸ hdvd
      exact hcop.dvd_of_dvd_mul_left h1
    have hx0 : x ≠ 0 := by
      rintro rfl
      rw [mul_zero] at hx
      exact ha0 hx
    have hxlt : x < A.card := by
      have h2 : a.gcd b * x < a.gcd b * A.card := by
        rw [← hx, mul_comm]
        exact hlt a ha b hb
      exact Nat.lt_of_mul_lt_mul_left h2
    exact lt_of_le_of_lt (Nat.le_of_dvd (Nat.pos_of_ne_zero hx0) hdx) hxlt
  by_cases hpr : A.card.Prime
  · -- Prime size n = p: no element is divisible by p (p ^ 1 < p fails), so a ↦ a % p maps the p
    -- elements into the p - 1 non-zero residues. Two elements a ≠ b collide; with g = gcd(a, b),
    -- a = g x and b = g y where x, y < p and p ∤ g, so x ≡ y (mod p) forces x = y and a = b.
    have hnd : ∀ a ∈ A, ¬ A.card ∣ a := by
      intro a ha h
      have h1 := hpp a ha A.card 1 hpr (by rw [pow_one]; exact h)
      rw [pow_one] at h1
      exact lt_irrefl _ h1
    have hmaps : Set.MapsTo (fun a => a % A.card) (A : Set ℕ) (Finset.Icc 1 (A.card - 1) : Set ℕ) := by
      intro a ha
      have ha' : a ∈ A := ha
      have h1 : a % A.card < A.card := Nat.mod_lt a hn
      have h2 : a % A.card ≠ 0 := fun h => hnd a ha' (Nat.dvd_of_mod_eq_zero h)
      simp only [Finset.coe_Icc, Set.mem_Icc]
      omega
    have hcard : (Finset.Icc 1 (A.card - 1)).card < A.card := by
      rw [Nat.card_Icc]
      omega
    obtain ⟨a, ha, b, hb, hab, heq⟩ := Finset.exists_ne_map_eq_of_card_lt_of_maps_to hcard hmaps
    obtain ⟨x, hx⟩ := Nat.gcd_dvd_left a b
    obtain ⟨y, hy⟩ := Nat.gcd_dvd_right a b
    have hxlt : x < A.card := by
      have h2 : a.gcd b * x < a.gcd b * A.card := by
        rw [← hx, mul_comm]
        exact hlt a ha b hb
      exact Nat.lt_of_mul_lt_mul_left h2
    have hylt : y < A.card := by
      have h2 : a.gcd b * y < a.gcd b * A.card := by
        rw [← hy, mul_comm, Nat.gcd_comm]
        exact hlt b hb a ha
      exact Nat.lt_of_mul_lt_mul_left h2
    have hcopg : A.card.gcd (a.gcd b) = 1 := by
      have h1 : Nat.Coprime A.card (a.gcd b) := by
        rw [Nat.Prime.coprime_iff_not_dvd hpr]
        intro h
        exact hnd a ha (h.trans (Nat.gcd_dvd_left a b))
      exact h1
    have hmod : a.gcd b * x ≡ a.gcd b * y [MOD A.card] := by
      rw [← hx, ← hy]
      exact heq
    have hxy : x ≡ y [MOD A.card] := Nat.ModEq.cancel_left_of_coprime hcopg hmod
    have hxy' : x = y := by
      unfold Nat.ModEq at hxy
      rwa [Nat.mod_eq_of_lt hxlt, Nat.mod_eq_of_lt hylt] at hxy
    apply hab
    calc a = a.gcd b * x := hx
      _ = a.gcd b * y := by rw [hxy']
      _ = b := hy.symm
  · by_cases hq : ∃ q : ℕ, q.Prime ∧ A.card = q + 1
    · -- Size n = p + 1 with p prime. By the prime-power bound p ^ 2 divides no element. Send a to
      -- the residue mod p of a, or of a / p when p ∣ a: a non-zero residue. Two elements with the
      -- same residue are b and p * b with p ∤ b (the other cases force equality as in the prime
      -- case). p + 1 elements in p - 1 residues give two such pairs {c, p c}, {d, p d} with c ≠ d,
      -- and then (p c) / gcd(p c, d) ≤ p forces c ∣ d, and symmetrically d ∣ c.
      obtain ⟨p, hp, hn1⟩ := hq
      have hp2 : ∀ a ∈ A, ¬ p * p ∣ a := by
        intro a ha h
        have h1 := hpp a ha p 2 hp (by rw [pow_two]; exact h)
        rw [pow_two, hn1] at h1
        have := hp.two_le
        nlinarith
      have key : ∀ a b : ℕ, ¬ p ∣ a → ¬ p ∣ b → a % p = b % p →
          a < A.card * a.gcd b → b < A.card * b.gcd a → a = b := by
        intro a b hpa hpb hab hla hlb
        obtain ⟨x, hx⟩ := Nat.gcd_dvd_left a b
        obtain ⟨y, hy⟩ := Nat.gcd_dvd_right a b
        have hxlt : x < A.card := by
          have h2 : a.gcd b * x < a.gcd b * A.card := by
            rw [← hx, mul_comm]
            exact hla
          exact Nat.lt_of_mul_lt_mul_left h2
        have hylt : y < A.card := by
          have h2 : a.gcd b * y < a.gcd b * A.card := by
            rw [← hy, mul_comm, Nat.gcd_comm]
            exact hlb
          exact Nat.lt_of_mul_lt_mul_left h2
        have hxp : x ≠ p := by
          rintro rfl
          exact hpa (Dvd.intro_left _ hx.symm)
        have hyp : y ≠ p := by
          rintro rfl
          exact hpb (Dvd.intro_left _ hy.symm)
        have hxlt' : x < p := by omega
        have hylt' : y < p := by omega
        have hcop : p.gcd (a.gcd b) = 1 := by
          have h1 : Nat.Coprime p (a.gcd b) := by
            rw [Nat.Prime.coprime_iff_not_dvd hp]
            intro h
            exact hpa (h.trans (Nat.gcd_dvd_left a b))
          exact h1
        have hmod : a.gcd b * x ≡ a.gcd b * y [MOD p] := by
          rw [← hx, ← hy]
          exact hab
        have hxy := Nat.ModEq.cancel_left_of_coprime hcop hmod
        have hxy' : x = y := by
          unfold Nat.ModEq at hxy
          rwa [Nat.mod_eq_of_lt hxlt', Nat.mod_eq_of_lt hylt'] at hxy
        calc a = a.gcd b * x := hx
          _ = a.gcd b * y := by rw [hxy']
          _ = b := hy.symm
      have hC : ∀ a0 b : ℕ, p * a0 ∈ A → b ∈ A → ¬ p ∣ b → a0 % p = b % p → b = a0 := by
        intro a0 b ha hb hpb hf
        have hcopb : Nat.Coprime p b := (Nat.Prime.coprime_iff_not_dvd hp).2 hpb
        have hg' : (p * a0).gcd b = a0.gcd b := Nat.Coprime.gcd_mul_left_cancel a0 hcopb
        have hla := hlt (p * a0) ha b hb
        have hlb := hlt b hb (p * a0) ha
        rw [hg', hn1] at hla
        rw [Nat.gcd_comm, hg', hn1] at hlb
        obtain ⟨u, hu⟩ := Nat.gcd_dvd_left a0 b
        obtain ⟨v, hv⟩ := Nat.gcd_dvd_right a0 b
        have hu1 : u = 1 := by
          have h2 : a0.gcd b * (p * u) < a0.gcd b * (p + 1) := by
            calc a0.gcd b * (p * u) = p * (a0.gcd b * u) := by ring
              _ = p * a0 := by rw [← hu]
              _ < (p + 1) * a0.gcd b := hla
              _ = a0.gcd b * (p + 1) := by ring
          have h3 := Nat.lt_of_mul_lt_mul_left h2
          rcases u with _ | _ | u
          · exfalso
            rw [mul_zero] at hu
            rw [hu, mul_zero] at ha
            exact hA ha
          · rfl
          · have := hp.two_le
            nlinarith
        have e1 : a0.gcd b = a0 := by
          rw [hu1, mul_one] at hu
          exact hu.symm
        have hvlt : v < p + 1 := by
          have h2 : a0.gcd b * v < a0.gcd b * (p + 1) := by
            calc a0.gcd b * v = b := hv.symm
              _ < (p + 1) * a0.gcd b := hlb
              _ = a0.gcd b * (p + 1) := by ring
          exact Nat.lt_of_mul_lt_mul_left h2
        have hvp : v ≠ p := by
          rintro rfl
          exact hpb (Dvd.intro_left _ hv.symm)
        have hvlt' : v < p := by omega
        have hcopg : p.gcd (a0.gcd b) = 1 := by
          have h1 : Nat.Coprime p (a0.gcd b) := by
            rw [Nat.Prime.coprime_iff_not_dvd hp]
            intro h
            exact hpb (h.trans (Nat.gcd_dvd_right a0 b))
          exact h1
        have hmod : a0.gcd b * 1 ≡ a0.gcd b * v [MOD p] := by
          rw [mul_one, ← hv, e1]
          exact hf
        have hv1 := Nat.ModEq.cancel_left_of_coprime hcopg hmod
        have hv1' : v = 1 := by
          unfold Nat.ModEq at hv1
          rw [Nat.mod_eq_of_lt hp.one_lt, Nat.mod_eq_of_lt hvlt'] at hv1
          exact hv1.symm
        rw [hv, hv1', mul_one, e1]
      have hL : ∀ a ∈ A, ∀ b ∈ A, a ≠ b →
          (if p ∣ a then a / p else a) % p = (if p ∣ b then b / p else b) % p →
          ∃ c, ¬ p ∣ c ∧ (c = a ∨ c = b) ∧ (p * c = a ∨ p * c = b) := by
        intro a ha b hb hab hfab
        by_cases hpa : p ∣ a <;> by_cases hpb : p ∣ b
        · exfalso
          have hla := hlt a ha b hb
          have hlb := hlt b hb a ha
          obtain ⟨a0, rfl⟩ := hpa
          obtain ⟨b0, rfl⟩ := hpb
          have ha0 : ¬ p ∣ a0 := fun h => hp2 _ ha (Nat.mul_dvd_mul_left p h)
          have hb0 : ¬ p ∣ b0 := fun h => hp2 _ hb (Nat.mul_dvd_mul_left p h)
          rw [if_pos (dvd_mul_right p a0), if_pos (dvd_mul_right p b0),
            Nat.mul_div_cancel_left a0 hp.pos, Nat.mul_div_cancel_left b0 hp.pos] at hfab
          rw [Nat.gcd_mul_left] at hla hlb
          have hla' : a0 < A.card * a0.gcd b0 := by
            have h2 : p * a0 < p * (A.card * a0.gcd b0) := by
              calc p * a0 < A.card * (p * a0.gcd b0) := hla
                _ = p * (A.card * a0.gcd b0) := by ring
            exact Nat.lt_of_mul_lt_mul_left h2
          have hlb' : b0 < A.card * b0.gcd a0 := by
            have h2 : p * b0 < p * (A.card * b0.gcd a0) := by
              calc p * b0 < A.card * (p * b0.gcd a0) := hlb
                _ = p * (A.card * b0.gcd a0) := by ring
            exact Nat.lt_of_mul_lt_mul_left h2
          exact hab (by rw [key a0 b0 ha0 hb0 hfab hla' hlb'])
        · obtain ⟨a0, rfl⟩ := hpa
          rw [if_pos (dvd_mul_right p a0), if_neg hpb, Nat.mul_div_cancel_left a0 hp.pos] at hfab
          have e := hC a0 b ha hb hpb hfab
          exact ⟨b, hpb, Or.inr rfl, Or.inl (by rw [e])⟩
        · obtain ⟨b0, rfl⟩ := hpb
          rw [if_neg hpa, if_pos (dvd_mul_right p b0), Nat.mul_div_cancel_left b0 hp.pos] at hfab
          have e := hC b0 a hb ha hpa hfab.symm
          exact ⟨a, hpa, Or.inl rfl, Or.inr (by rw [e])⟩
        · exfalso
          rw [if_neg hpa, if_neg hpb] at hfab
          exact hab (key a b hpa hpb hfab (hlt a ha b hb) (hlt b hb a ha))
      have cross : ∀ c d : ℕ, c ∈ A → d ∈ A → p * c ∈ A → ¬ p ∣ d → c ∣ d := by
        intro c d hc hd hpc hpd
        have h := hlt (p * c) hpc d hd
        rw [Nat.Coprime.gcd_mul_left_cancel c ((Nat.Prime.coprime_iff_not_dvd hp).2 hpd), hn1] at h
        obtain ⟨u, hu⟩ := Nat.gcd_dvd_left c d
        have h2 : c.gcd d * (p * u) < c.gcd d * (p + 1) := by
          calc c.gcd d * (p * u) = p * (c.gcd d * u) := by ring
            _ = p * c := by rw [← hu]
            _ < (p + 1) * c.gcd d := h
            _ = c.gcd d * (p + 1) := by ring
        have h3 := Nat.lt_of_mul_lt_mul_left h2
        have hc0 : c ≠ 0 := fun h0 => hA (h0 ▸ hc)
        have hu1 : u = 1 := by
          rcases u with _ | _ | u
          · rw [mul_zero] at hu
            exact absurd hu hc0
          · rfl
          · have := hp.two_le
            nlinarith
        rw [hu, hu1, mul_one]
        exact Nat.gcd_dvd_right c d
      have hmaps : Set.MapsTo (fun a => (if p ∣ a then a / p else a) % p) (A : Set ℕ)
          (Finset.Icc 1 (p - 1) : Set ℕ) := by
        intro a ha
        have ha' : a ∈ A := ha
        have hlt' : (if p ∣ a then a / p else a) % p < p := Nat.mod_lt _ hp.pos
        have hne0 : (if p ∣ a then a / p else a) % p ≠ 0 := by
          by_cases hpa : p ∣ a
          · rw [if_pos hpa]
            obtain ⟨a0, rfl⟩ := hpa
            rw [Nat.mul_div_cancel_left a0 hp.pos]
            intro h
            exact hp2 _ ha' (Nat.mul_dvd_mul_left p (Nat.dvd_of_mod_eq_zero h))
          · rw [if_neg hpa]
            intro h
            exact hpa (Nat.dvd_of_mod_eq_zero h)
        simp only [Finset.coe_Icc, Set.mem_Icc]
        generalize (if p ∣ a then a / p else a) % p = r at hlt' hne0 ⊢
        omega
      have hcard1 : (Finset.Icc 1 (p - 1)).card < A.card := by
        rw [Nat.card_Icc, hn1]
        omega
      obtain ⟨a1, ha1, b1, hb1, hab1, heq1⟩ :=
        Finset.exists_ne_map_eq_of_card_lt_of_maps_to hcard1 hmaps
      obtain ⟨c1, hc1p, hc1, hpc1⟩ := hL a1 ha1 b1 hb1 hab1 heq1
      have hc1A : c1 ∈ A := by
        rcases hc1 with h | h <;> rw [h] <;> assumption
      have hpc1A : p * c1 ∈ A := by
        rcases hpc1 with h | h <;> rw [h] <;> assumption
      have hcard2 : (Finset.Icc 1 (p - 1)).card < (A.erase (p * c1)).card := by
        rw [Finset.card_erase_of_mem hpc1A, Nat.card_Icc, hn1]
        have := hp.two_le
        omega
      have hmaps2 : Set.MapsTo (fun a => (if p ∣ a then a / p else a) % p)
          ((A.erase (p * c1)) : Set ℕ) (Finset.Icc 1 (p - 1) : Set ℕ) :=
        fun a ha => hmaps (Finset.mem_of_mem_erase ha)
      obtain ⟨a2, ha2, b2, hb2, hab2, heq2⟩ :=
        Finset.exists_ne_map_eq_of_card_lt_of_maps_to hcard2 hmaps2
      obtain ⟨c2, hc2p, hc2, hpc2⟩ :=
        hL a2 (Finset.mem_of_mem_erase ha2) b2 (Finset.mem_of_mem_erase hb2) hab2 heq2
      have hc2A : c2 ∈ A := by
        rcases hc2 with h | h <;> rw [h]
        · exact Finset.mem_of_mem_erase ha2
        · exact Finset.mem_of_mem_erase hb2
      have hpc2E : p * c2 ∈ A.erase (p * c1) := by
        rcases hpc2 with h | h <;> rw [h] <;> assumption
      have hpc2A : p * c2 ∈ A := Finset.mem_of_mem_erase hpc2E
      have hne12 : c2 ≠ c1 := by
        rintro rfl
        exact (Finset.mem_erase.mp hpc2E).1 rfl
      exact hne12 (Nat.dvd_antisymm (cross c2 c1 hc2A hc1A hpc2A hc1p)
        (cross c1 c2 hc1A hc2A hpc1A hc2p))
    · push Not at hq
      obtain ⟨a, ha, b, hb, hle⟩ :=
        hcomp A hA hne hg hpr hq (fun a ha b hb => (hlt a ha b hb).le) hpp
      exact absurd hle (not_le.mpr (hcon a ha b hb))

The gate replayed this file at its merge, each hole a sorry (D-12 #5); the whole file: targets/erdos-402/nodes/erdos-402--h3-v2/attempts/20260929T200020Z-t0929-6-partial.lean

theorem erdos_402__h3_v2__h1 : ∀ (B : Finset ℕ),
  (0 : ℕ) ∉ B →
    B.Nonempty →
      B.gcd id = (1 : ℕ) →
        ¬Nat.Prime B.card →
          (∀ (q : ℕ), Nat.Prime q → B.card ≠ q + (1 : ℕ)) →
            (∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) →
              (∀ a ∈ B, ∀ (p k : ℕ), Nat.Prime p → p ^ k ∣ a → p ^ k < B.card) →
                ∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ) := by
  -- Informal argument: annex 6a64518f9cd863c9abea3114b518f3172f4c73c6a187eb928b43db35f77c0002 on this node (graph PR #325, in the merge queue when this was prechecked).
  -- Hole `hsmooth`: B has a pair with gcd(a, b) ≤ a / n, or an element with a prime factor p ≥ n / 2.
  -- The assembly proves that the second alternative contradicts the strict inequalities.
  have hsmooth : ∀ B : Finset ℕ, 0 ∉ B → B.Nonempty → B.gcd id = 1 → ¬ B.card.Prime →
      (∀ q : ℕ, q.Prime → B.card ≠ q + 1) →
      (∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) →
      (∀ a ∈ B, ∀ p k : ℕ, p.Prime → p ^ k ∣ a → p ^ k < B.card) →
      (∃ a ∈ B, ∃ b ∈ B, (a.gcd b : ℚ) ≤ (a : ℚ) / (B.card : ℚ)) ∨
        ∃ p : ℕ, p.Prime ∧ B.card ≤ 2 * p ∧ ∃ a ∈ B, p ∣ a := sorry
  have big : ∀ S : Finset ℕ, (∀ x ∈ S, 0 < x) → S.Nonempty → ∃ x ∈ S, S.card ≤ x := by
    intro S hpos hS
    by_contra h
    push Not at h
    have hsub : S ⊆ Finset.Ioo 0 S.card := by
      intro x hx
      exact Finset.mem_Ioo.mpr ⟨hpos x hx, h x hx⟩
    have h1 := Finset.card_le_card hsub
    rw [Nat.card_Ioo] at h1
    have h2 := hS.card_pos
    omega
  have key : ∀ (n p : ℕ) (X T : Finset ℕ), 0 < p → p < n →
      (∀ x ∈ X, ∀ t ∈ T, 0 < x * t ∧ x * t < n ∧ ¬ p ∣ x * t) →
      X.Nonempty → T.Nonempty → n ≤ X.card + T.card → False := by
    intro n p X T hp hpn hxt hX hT hcard
    have hXpos : ∀ x ∈ X, 0 < x := by
      intro x hx
      obtain ⟨t, ht⟩ := hT
      have h := (hxt x hx t ht).1
      exact Nat.pos_of_ne_zero (by rintro rfl; simp at h)
    have hTpos : ∀ t ∈ T, 0 < t := by
      intro t ht
      obtain ⟨x, hx⟩ := hX
      have h := (hxt x hx t ht).1
      exact Nat.pos_of_ne_zero (by rintro rfl; simp at h)
    obtain ⟨x0, hx0, hx0c⟩ := big X hXpos hX
    obtain ⟨t0, ht0, ht0c⟩ := big T hTpos hT
    have h1 := (hxt x0 hx0 t0 ht0).2.1
    have h2 : X.card * T.card ≤ x0 * t0 := Nat.mul_le_mul hx0c ht0c
    have hu := hX.card_pos
    have hv := hT.card_pos
    have hc2 : ((Finset.Ioo 0 n).erase p).card = n - 2 := by
      rw [Finset.card_erase_of_mem (Finset.mem_Ioo.mpr ⟨hp, hpn⟩), Nat.card_Ioo]
      omega
    have h3 : X.card = 1 ∨ T.card = 1 := by
      by_contra h
      push Not at h
      have h4 : 2 ≤ X.card := by omega
      have h5 : 2 ≤ T.card := by omega
      nlinarith
    rcases h3 with hu1 | hv1
    · have hsub : T.image (fun t => x0 * t) ⊆ (Finset.Ioo 0 n).erase p := by
        intro y hy
        obtain ⟨t, ht, rfl⟩ := Finset.mem_image.mp hy
        have h := hxt x0 hx0 t ht
        rw [Finset.mem_erase, Finset.mem_Ioo]
        exact ⟨fun e => h.2.2 (dvd_of_eq e.symm), h.1, h.2.1⟩
      have hc1 : (T.image (fun t => x0 * t)).card = T.card :=
        Finset.card_image_of_injective _ (fun a b h => Nat.eq_of_mul_eq_mul_left (hXpos x0 hx0) h)
      have h6 := Finset.card_le_card hsub
      omega
    · have hsub : X.image (fun x => x * t0) ⊆ (Finset.Ioo 0 n).erase p := by
        intro y hy
        obtain ⟨x, hx, rfl⟩ := Finset.mem_image.mp hy
        have h := hxt x hx t0 ht0
        rw [Finset.mem_erase, Finset.mem_Ioo]
        exact ⟨fun e => h.2.2 (dvd_of_eq e.symm), h.1, h.2.1⟩
      have hc1 : (X.image (fun x => x * t0)).card = X.card :=
        Finset.card_image_of_injective _ (fun a b h => Nat.eq_of_mul_eq_mul_right (hTpos t0 ht0) h)
      have h6 := Finset.card_le_card hsub
      omega
  have hlarge : ∀ B : Finset ℕ, 0 ∉ B →
      (∀ a ∈ B, ∀ b ∈ B, a < B.card * a.gcd b) →
      ∀ p : ℕ, p.Prime → p < B.card →
      (∀ a ∈ B, p ∣ a → ∀ b ∈ B, ¬ p ∣ b → a = p * a.gcd b) →
      (∃ a ∈ B, p ∣ a) → (∃ b ∈ B, ¬ p ∣ b) → False := by
    intro B h0 hlt p hp hpn hA hexa hexb
    obtain ⟨a0, ha0, hpa0⟩ := hexa
    obtain ⟨b0, hb0, hpb0⟩ := hexb
    have hG0 : (B.filter (fun b => ¬ p ∣ b)).gcd id ≠ 0 := by
      intro h
      have h1 : (B.filter (fun b => ¬ p ∣ b)).gcd id ∣ id b0 :=
        Finset.gcd_dvd (Finset.mem_filter.mpr ⟨hb0, hpb0⟩)
      rw [h] at h1
      exact hpb0 (by rw [show b0 = 0 from Nat.eq_zero_of_zero_dvd h1]; exact dvd_zero p)
    have hGb : ∀ b ∈ B, ¬ p ∣ b → (B.filter (fun b => ¬ p ∣ b)).gcd id ∣ b := by
      intro b hb hpb
      exact Finset.gcd_dvd (f := id) (Finset.mem_filter.mpr ⟨hb, hpb⟩)
    have hdG : ∀ a ∈ B, p ∣ a → ∀ b ∈ B, ¬ p ∣ b →
        a.gcd b ∣ (B.filter (fun b => ¬ p ∣ b)).gcd id := by
      intro a ha hpa b hb hpb
      apply Finset.dvd_gcd
      intro b' hb'
      obtain ⟨hb'B, hpb'⟩ := Finset.mem_filter.mp hb'
      have e1 := hA a ha hpa b hb hpb
      have e2 := hA a ha hpa b' hb'B hpb'
      have e3 : a.gcd b = a.gcd b' := Nat.eq_of_mul_eq_mul_left hp.pos (e1.symm.trans e2)
      rw [e3]
      exact Nat.gcd_dvd_right a b'
    have hprod : ∀ a ∈ B, p ∣ a → ∀ b ∈ B, ¬ p ∣ b →
        0 < ((B.filter (fun b => ¬ p ∣ b)).gcd id * p / a) * (b / (B.filter (fun b => ¬ p ∣ b)).gcd id) ∧
        ((B.filter (fun b => ¬ p ∣ b)).gcd id * p / a) * (b / (B.filter (fun b => ¬ p ∣ b)).gcd id) < B.card ∧
        ¬ p ∣ ((B.filter (fun b => ¬ p ∣ b)).gcd id * p / a) * (b / (B.filter (fun b => ¬ p ∣ b)).gcd id) ∧
        a * ((B.filter (fun b => ¬ p ∣ b)).gcd id * p / a) = (B.filter (fun b => ¬ p ∣ b)).gcd id * p := by
      intro a ha hpa b hb hpb
      generalize hG : (B.filter (fun b => ¬ p ∣ b)).gcd id = G at *
      obtain ⟨e, he⟩ := hdG a ha hpa b hb hpb
      obtain ⟨s, hs⟩ := hGb b hb hpb
      have ea := hA a ha hpa b hb hpb
      have ha0' : 0 < a := Nat.pos_of_ne_zero (fun h => h0 (h ▸ ha))
      have hb0' : b ≠ 0 := fun h => h0 (h ▸ hb)
      have hGp : G * p = e * a :=
        calc G * p = a.gcd b * e * p := by rw [he]
          _ = e * (p * a.gcd b) := by ring
          _ = e * a := by rw [← ea]
      have hx : G * p / a = e := Nat.div_eq_of_eq_mul_left ha0' hGp
      have ht : b / G = s := by
        rw [hs]
        exact Nat.mul_div_cancel_left s (Nat.pos_of_ne_zero hG0)
      rw [hx, ht]
      have hb2 : b = a.gcd b * (e * s) :=
        calc b = G * s := hs
          _ = a.gcd b * e * s := by rw [he]
          _ = a.gcd b * (e * s) := by ring
      have hes : e * s ≠ 0 := by
        intro h
        rw [h, Nat.mul_zero] at hb2
        exact hb0' hb2
      refine ⟨Nat.pos_of_ne_zero hes, ?_, ?_, ?_⟩
      · have h1 := hlt b hb a ha
        rw [Nat.gcd_comm b a] at h1
        have h2 : a.gcd b * (e * s) < a.gcd b * B.card := by
          rw [← hb2, Nat.mul_comm]; exact h1
        exact Nat.lt_of_mul_lt_mul_left h2
      · intro h
        exact hpb (hb2 ▸ Dvd.dvd.mul_left h _)
      · rw [hGp]; ring
    have hcardsum : (B.filter (fun a => p ∣ a)).card + (B.filter (fun b => ¬ p ∣ b)).card = B.card := by
      rw [← Finset.card_union_of_disjoint (Finset.disjoint_filter_filter_not B B (fun a => p ∣ a)),
        Finset.filter_union_filter_not_eq]
    have hinjX : Set.InjOn (fun a => (B.filter (fun b => ¬ p ∣ b)).gcd id * p / a)
        (B.filter (fun a => p ∣ a) : Finset ℕ) := by
      intro a ha a' ha' h
      obtain ⟨haB, hpa⟩ := Finset.mem_filter.mp ha
      obtain ⟨haB', hpa'⟩ := Finset.mem_filter.mp ha'
      have h1 := (hprod a haB hpa b0 hb0 hpb0)
      have h2 := (hprod a' haB' hpa' b0 hb0 hpb0).2.2.2
      simp only at h
      rw [← h] at h2
      have hq : 0 < (B.filter (fun b => ¬ p ∣ b)).gcd id * p / a :=
        Nat.pos_of_ne_zero (by
          intro hz
          have := h1.1
          rw [hz, Nat.zero_mul] at this
          exact lt_irrefl 0 this)
      exact Nat.eq_of_mul_eq_mul_right hq (h1.2.2.2.trans h2.symm)
    have hinjT : Set.InjOn (fun b => b / (B.filter (fun b => ¬ p ∣ b)).gcd id)
        (B.filter (fun b => ¬ p ∣ b) : Finset ℕ) := by
      intro b hb b' hb' h
      obtain ⟨hbB, hpb⟩ := Finset.mem_filter.mp hb
      obtain ⟨hbB', hpb'⟩ := Finset.mem_filter.mp hb'
      simp only at h
      rw [← Nat.div_mul_cancel (hGb b hbB hpb), ← Nat.div_mul_cancel (hGb b' hbB' hpb'), h]
    refine key B.card p
      ((B.filter (fun a => p ∣ a)).image (fun a => (B.filter (fun b => ¬ p ∣ b)).gcd id * p / a))
      ((B.filter (fun b => ¬ p ∣ b)).image (fun b => b / (B.filter (fun b => ¬ p ∣ b)).gcd id))
      hp.pos hpn ?_ ?_ ?_ ?_
    · intro x hx t ht
      obtain ⟨a, ha, rfl⟩ := Finset.mem_image.mp hx
      obtain ⟨b, hb, rfl⟩ := Finset.mem_image.mp ht
      obtain ⟨haB, hpa⟩ := Finset.mem_filter.mp ha
      obtain ⟨hbB, hpb⟩ := Finset.mem_filter.mp hb
      have h := hprod a haB hpa b hbB hpb
      exact ⟨h.1, h.2.1, h.2.2.1⟩
    · exact ⟨_, Finset.mem_image_of_mem _ (Finset.mem_filter.mpr ⟨ha0, hpa0⟩)⟩
    · exact ⟨_, Finset.mem_image_of_mem _ (Finset.mem_filter.mpr ⟨hb0, hpb0⟩)⟩
    · rw [Finset.card_image_of_injOn hinjX, Finset.card_image_of_injOn hinjT, hcardsum]
  intro B h0 hne hgcd hnp hnp1 hle hpp
  by_contra hcon
  have hn : 0 < B.card := hne.card_pos
  have hnq : (0 : ℚ) < B.card := by exact_mod_cast hn
  have hlt : ∀ a ∈ B, ∀ b ∈ B, a < B.card * a.gcd b := by
    intro a ha b hb
    rcases (hle a ha b hb).lt_or_eq with h | h
    · exact h
    · exfalso
      apply hcon
      refine ⟨a, ha, b, hb, ?_⟩
      rw [le_div_iff₀ hnq]
      have h2 : a.gcd b * B.card ≤ a := by rw [Nat.mul_comm]; exact h.ge
      exact_mod_cast h2
  have hA : ∀ p : ℕ, p.Prime → B.card ≤ 2 * p →
      ∀ a ∈ B, p ∣ a → ∀ b ∈ B, ¬ p ∣ b → a = p * a.gcd b := by
    intro p hp hnp2 a ha hpa b hb hpb
    have ha0 : a ≠ 0 := fun h => h0 (h ▸ ha)
    have hg0 : 0 < a.gcd b := Nat.gcd_pos_of_pos_left b (Nat.pos_of_ne_zero ha0)
    obtain ⟨x, hx⟩ := Nat.gcd_dvd_left a b
    have hpg : ¬ p ∣ a.gcd b := fun h => hpb (h.trans (Nat.gcd_dvd_right a b))
    have hpx : p ∣ x := by
      have h1 : p ∣ a.gcd b * x := hx ▸ hpa
      exact (hp.dvd_mul.mp h1).resolve_left hpg
    obtain ⟨t, ht⟩ := hpx
    have hlt' := hlt a ha b hb
    have hxn : x < B.card := by
      have h3 : a.gcd b * x < a.gcd b * B.card := by
        rw [← hx, Nat.mul_comm]; exact hlt'
      exact Nat.lt_of_mul_lt_mul_left h3
    have ht1 : t = 1 := by
      have hx0 : x ≠ 0 := by
        rintro rfl
        rw [Nat.mul_zero] at hx
        exact ha0 hx
      have ht0 : t ≠ 0 := by
        rintro rfl
        rw [Nat.mul_zero] at ht
        exact hx0 ht
      by_contra hne1
      have ht2 : 2 ≤ t := by omega
      have h4 : p * 2 ≤ p * t := Nat.mul_le_mul_left p ht2
      omega
    calc a = a.gcd b * x := hx
      _ = p * a.gcd b := by rw [ht, ht1]; ring
  rcases hsmooth B h0 hne hgcd hnp hnp1 hle hpp with h | ⟨p, hp, hnp2, a, ha, hpa⟩
  · exact hcon h
  · have hpn : p < B.card := by
      have h1 := hpp a ha p 1 hp (by rwa [pow_one])
      rwa [pow_one] at h1
    have hexb : ∃ b ∈ B, ¬ p ∣ b := by
      by_contra h
      push Not at h
      have h1 : p ∣ B.gcd id := Finset.dvd_gcd (fun b hb => h b hb)
      rw [hgcd] at h1
      exact hp.one_lt.ne' (Nat.dvd_one.mp h1)
    exact hlarge B h0 hlt p hp hpn (hA p hp hnp2) ⟨a, ha, hpa⟩ hexb

The gate replayed this file at its merge, each hole a sorry (D-12 #5); the whole file: targets/erdos-402/nodes/erdos-402--h3-v2--h1/attempts/20261001T115500Z-t1001-402a-partial.lean

theorem erdos_402__h3_v2__h1__h1 : ∀ (B : Finset ℕ),
  (0 : ℕ) ∉ B →
    B.Nonempty →
      B.gcd id = (1 : ℕ) →
        ¬Nat.Prime B.card →
          (∀ (q : ℕ), Nat.Prime q → B.card ≠ q + (1 : ℕ)) →
            (∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) →
              (∀ a ∈ B, ∀ (p k : ℕ), Nat.Prime p → p ^ k ∣ a → p ^ k < B.card) →
                (∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ)) ∨
                  ∃ (p : ℕ), Nat.Prime p ∧ B.card ≤ (2 : ℕ) * p ∧ ∃ a ∈ B, p ∣ a := by
  -- Informal argument and the Lean of each lemma: annex eb2314a2c5e64fe114b9093565a401979c6ef009436d2f021627b4d3d63663fd on erdos-402--h3-v2 (graph PR #340, agent 402-R2-b); dual set from agents 402-R1-b and 402-R2-c.
  -- Hole `hmid`: B has a pair with gcd(a, b) ≤ a / n, or an element with a prime factor p ≥ n / 3.
  -- The assembly proves: in a strict counterexample no prime p with 2p < n ≤ 3p divides an element
  -- (block lemma for k = 2, matching lemma for B = {2p} ∪ T, and the dual set for the other side).
  have hmid : ∀ B : Finset ℕ, 0 ∉ B → B.Nonempty → B.gcd id = 1 → ¬ B.card.Prime →
      (∀ q : ℕ, q.Prime → B.card ≠ q + 1) →
      (∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) →
      (∀ a ∈ B, ∀ p k : ℕ, p.Prime → p ^ k ∣ a → p ^ k < B.card) →
      (∃ a ∈ B, ∃ b ∈ B, (a.gcd b : ℚ) ≤ (a : ℚ) / (B.card : ℚ)) ∨
        ∃ p : ℕ, p.Prime ∧ B.card ≤ 3 * p ∧ ∃ a ∈ B, p ∣ a := sorry
  have R2b_lemI : ∀ (n p : ℕ) (T : Finset ℕ) (hp : p.Prime) (hp3 : 3 ≤ p) (h2p : 2 * p < n) (hn3 : n ≤ 3 * p) (h0 : ∀ b ∈ T, 0 < b) (hpT : ∀ b ∈ T, ¬ p ∣ b) (ho : ∀ b ∈ T, ¬ 2 ∣ b → b < n) (he : ∀ b ∈ T, 2 ∣ b → b < 2 * n) (hx : ∀ b ∈ T, ∀ t ∈ T, 2 ∣ b → ¬ 2 ∣ t → b < n * b.gcd t),
      T.card + 2 ≤ n := by
    intro n p T hp hp3 h2p hn3 h0 hpT ho he hx
    -- φ t = the unique t·2^j in [n/2, n-1]
    have hφ : ∀ b : ℕ, 0 < b → b < n →
        b * 2 ^ Nat.log 2 ((n - 1) / b) ≤ n - 1 ∧ n - 1 < 2 * (b * 2 ^ Nat.log 2 ((n - 1) / b)) := by
      intro b hb hbn
      have hne : (n - 1) / b ≠ 0 := by
        have : 0 < (n - 1) / b := Nat.div_pos (by omega) hb
        omega
      have h1 := Nat.pow_log_le_self 2 hne
      have h2 := Nat.lt_pow_succ_log_self (by norm_num : 1 < 2) ((n - 1) / b)
      have h3 : b * ((n - 1) / b) ≤ n - 1 := Nat.mul_div_le _ _
      have h4 : b * 2 ^ Nat.log 2 ((n - 1) / b) ≤ b * ((n - 1) / b) := Nat.mul_le_mul_left b h1
      have h5 : n - 1 < 2 ^ (Nat.log 2 ((n - 1) / b)).succ * b := (Nat.div_lt_iff_lt_mul hb).mp h2
      refine ⟨h4.trans h3, ?_⟩
      calc n - 1 < 2 ^ (Nat.log 2 ((n - 1) / b)).succ * b := h5
        _ = 2 * (b * 2 ^ Nat.log 2 ((n - 1) / b)) := by rw [pow_succ]; ring
    have hinj0 : ∀ b b' j j' : ℕ, ¬ 2 ∣ b → j ≤ j' → b * 2 ^ j = b' * 2 ^ j' → b = b' := by
      intro b b' j j' hb hjj h
      obtain ⟨d, rfl⟩ := Nat.exists_eq_add_of_le hjj
      have h1 : b * 2 ^ j = (b' * 2 ^ d) * 2 ^ j := by rw [h, pow_add]; ring
      have h2 : b = b' * 2 ^ d := Nat.eq_of_mul_eq_mul_right (by positivity) h1
      rcases Nat.eq_zero_or_pos d with hd | hd
      · rw [hd] at h2; simpa using h2
      · exfalso; apply hb; rw [h2]
        exact Dvd.dvd.mul_left (dvd_pow_self 2 (by omega)) _
    have hinj : ∀ b b' j j' : ℕ, ¬ 2 ∣ b → ¬ 2 ∣ b' → b * 2 ^ j = b' * 2 ^ j' → b = b' := by
      intro b b' j j' hb hb' h
      rcases le_total j j' with hjj | hjj
      · exact hinj0 b b' j j' hb hjj h
      · exact (hinj0 b' b j' j hb' hjj h.symm).symm
    -- coprimality of t with (t·m − 1)
    have hcop : ∀ t m w : ℕ, w + 1 = t * m → Nat.Coprime w t := by
      intro t m w h
      have h1 : Nat.Coprime w (w + 1) := by simp
      rw [h] at h1
      exact Nat.Coprime.coprime_mul_right_right h1
    set φ : ℕ → ℕ := fun b => b * 2 ^ Nat.log 2 ((n - 1) / b) with hφdef
    set g : ℕ → ℕ := fun b =>
      if 2 ∣ b then b / 2 else if b = 2 * p + 1 then 2 * p - 1
      else if 2 * (φ b - 1) < n then 0 else φ b - 1 with hgdef
    have hmaps : ∀ b ∈ T, g b ∈ insert 0 (((Finset.Ioo 0 n).erase p).erase (2 * p)) := by
      intro b hb
      have hb0 := h0 b hb
      have hpb := hpT b hb
      rw [Finset.mem_insert, Finset.mem_erase, Finset.mem_erase, Finset.mem_Ioo]
      simp only [hgdef]
      by_cases h2 : 2 ∣ b
      · rw [if_pos h2]
        right
        obtain ⟨c, rfl⟩ := h2
        have := he _ hb ⟨c, rfl⟩
        rw [Nat.mul_div_cancel_left c (by norm_num : 0 < 2)]
        refine ⟨?_, ?_, ?_, ?_⟩
        · rintro rfl; exact hpb ⟨4, by ring⟩
        · rintro rfl; exact hpb ⟨2, by ring⟩
        · omega
        · omega
      · rw [if_neg h2]
        by_cases h3 : b = 2 * p + 1
        · rw [if_pos h3]; right; omega
        · rw [if_neg h3]
          by_cases h4 : 2 * (φ b - 1) < n
          · rw [if_pos h4]; left; rfl
          · rw [if_neg h4]
            right
            have hb1 := hφ b hb0 (ho b hb h2)
            have hne : φ b ≠ 2 * p + 1 := by
              intro h
              have h5 : b * 2 ^ Nat.log 2 ((n - 1) / b) = (2 * p + 1) * 2 ^ 0 := by simpa using h
              exact h3 (hinj _ _ _ _ h2 (by omega) h5)
            change φ b ≤ n - 1 ∧ n - 1 < 2 * φ b at hb1
            omega
    have hginj : Set.InjOn g (T : Set ℕ) := by
      -- even / odd collision is impossible
      have hEO : ∀ b ∈ T, ∀ t ∈ T, 2 ∣ b → ¬ 2 ∣ t → g b = g t → False := by
        intro b hb t ht h2b h2t h
        have hb0 := h0 b hb
        have ht0 := h0 t ht
        have hx' := hx b hb t ht h2b h2t
        obtain ⟨c, rfl⟩ := h2b
        simp only [hgdef] at h
        rw [if_pos ⟨c, rfl⟩, if_neg h2t, Nat.mul_div_cancel_left c (by norm_num : 0 < 2)] at h
        by_cases h3 : t = 2 * p + 1
        · rw [if_pos h3] at h
          have hc : Nat.Coprime c t := by
            have h1 : Nat.Coprime c (2 + c) := by
              rw [Nat.coprime_add_self_right]
              rw [Nat.coprime_comm, Nat.Prime.coprime_iff_not_dvd Nat.prime_two]
              intro hd; omega
            have : 2 + c = t := by omega
            rwa [this] at h1
          have h2t' : Nat.Coprime 2 t := (Nat.Prime.coprime_iff_not_dvd Nat.prime_two).mpr h2t
          have hg : (2 * c).gcd t = 1 := Nat.Coprime.mul_left h2t' hc
          rw [hg] at hx'
          omega
        · rw [if_neg h3] at h
          by_cases h4 : 2 * (φ t - 1) < n
          · rw [if_pos h4] at h; omega
          · rw [if_neg h4] at h
            have ht1 := hφ t ht0 (ho t ht h2t)
            change φ t ≤ n - 1 ∧ n - 1 < 2 * φ t at ht1
            have hc : Nat.Coprime c t := hcop t (2 ^ Nat.log 2 ((n - 1) / t)) c (by
              change c + 1 = φ t
              omega)
            have h2t' : Nat.Coprime 2 t := (Nat.Prime.coprime_iff_not_dvd Nat.prime_two).mpr h2t
            have hg : (2 * c).gcd t = 1 := Nat.Coprime.mul_left h2t' hc
            rw [hg] at hx'
            omega
      intro b hb b' hb' h
      have hb0 := h0 b hb
      have hb0' := h0 b' hb'
      by_cases h2 : 2 ∣ b
      · by_cases h2' : 2 ∣ b'
        · simp only [hgdef] at h
          rw [if_pos h2, if_pos h2'] at h
          obtain ⟨c, rfl⟩ := h2
          obtain ⟨c', rfl⟩ := h2'
          rw [Nat.mul_div_cancel_left c (by norm_num : 0 < 2),
            Nat.mul_div_cancel_left c' (by norm_num : 0 < 2)] at h
          rw [h]
        · exact (hEO b hb b' hb' h2 h2' h).elim
      · by_cases h2' : 2 ∣ b'
        · exact (hEO b' hb' b hb h2' h2 h.symm).elim
        · -- both odd
          have hb1 := hφ b hb0 (ho b hb h2)
          have hb1' := hφ b' hb0' (ho b' hb' h2')
          change φ b ≤ n - 1 ∧ n - 1 < 2 * φ b at hb1
          change φ b' ≤ n - 1 ∧ n - 1 < 2 * φ b' at hb1'
          have hφinj : φ b = φ b' → b = b' := fun e => hinj _ _ _ _ h2 h2' e
          have h2p' : ∀ t ∈ T, ¬ 2 ∣ t → φ t ≠ 2 * p := by
            intro t ht h2t e
            have hd : p ∣ t * 2 ^ Nat.log 2 ((n - 1) / t) := ⟨2, by change φ t = p * 2; omega⟩
            rcases (Nat.Prime.dvd_mul hp).mp hd with h5 | h5
            · exact hpT t ht h5
            · have h6 := Nat.Prime.dvd_of_dvd_pow hp h5
              have h7 := Nat.le_of_dvd (by norm_num) h6
              omega
          have e1 := h2p' b hb h2
          have e2 := h2p' b' hb' h2'
          simp only [hgdef] at h
          rw [if_neg h2, if_neg h2'] at h
          by_cases h3 : b = 2 * p + 1 <;> by_cases h3' : b' = 2 * p + 1
          · rw [h3, h3']
          · rw [if_pos h3, if_neg h3'] at h
            by_cases h4 : 2 * (φ b' - 1) < n
            · rw [if_pos h4] at h; omega
            · rw [if_neg h4] at h; omega
          · rw [if_neg h3, if_pos h3'] at h
            by_cases h4 : 2 * (φ b - 1) < n
            · rw [if_pos h4] at h; omega
            · rw [if_neg h4] at h; omega
          · rw [if_neg h3, if_neg h3'] at h
            by_cases h4 : 2 * (φ b - 1) < n <;> by_cases h4' : 2 * (φ b' - 1) < n
            · exact hφinj (by omega)
            · rw [if_pos h4, if_neg h4'] at h; omega
            · rw [if_neg h4, if_pos h4'] at h; omega
            · rw [if_neg h4, if_neg h4'] at h; exact hφinj (by omega)
    have hcard : (insert 0 (((Finset.Ioo 0 n).erase p).erase (2 * p))).card = n - 2 := by
      rw [Finset.card_insert_of_notMem (by simp), Finset.card_erase_of_mem, Finset.card_erase_of_mem,
        Nat.card_Ioo]
      · omega
      · rw [Finset.mem_Ioo]; omega
      · rw [Finset.mem_erase, Finset.mem_Ioo]; omega
    have hle := Finset.card_le_card_of_injOn g hmaps hginj
    rw [hcard] at hle
    omega
  have R2b_K2half : ∀ (n p : ℕ) (X S : Finset ℕ) (hp0 : 0 < p) (h2p : 2 * p < n) (h9 : 9 ≤ n) (hxs : ∀ x ∈ X, ∀ s ∈ S, ∃ y, 0 < y ∧ y < n ∧ ¬ p ∣ y ∧ (x * s = 2 * y ∨ (x * s = y ∧ ¬ 2 ∣ y))) (hX : X.Nonempty) (hS : S.Nonempty) (hcard : n ≤ X.card + S.card) (hle : X.card ≤ S.card),
      ∀ x ∈ X, x = 1 := by
    intro n p X S hp0 h2p h9 hxs hX hS hcard hle
    have big : ∀ Y : Finset ℕ, (∀ x ∈ Y, 0 < x) → Y.Nonempty → ∃ x ∈ Y, Y.card ≤ x := by
      intro Y hpos hY
      by_contra h
      push Not at h
      have hsub : Y ⊆ Finset.Ioo 0 Y.card := by
        intro x hx
        exact Finset.mem_Ioo.mpr ⟨hpos x hx, h x hx⟩
      have h1 := Finset.card_le_card hsub
      rw [Nat.card_Ioo] at h1
      have h2 := hY.card_pos
      omega
    have hXpos : ∀ x ∈ X, 0 < x := by
      intro x hx
      obtain ⟨s, hs⟩ := hS
      obtain ⟨y, hy0, -, -, h⟩ := hxs x hx s hs
      apply Nat.pos_of_ne_zero
      rintro rfl
      rw [Nat.zero_mul] at h
      omega
    have hSpos : ∀ s ∈ S, 0 < s := by
      intro s hs
      obtain ⟨x, hx⟩ := hX
      obtain ⟨y, hy0, -, -, h⟩ := hxs x hx s hs
      apply Nat.pos_of_ne_zero
      rintro rfl
      rw [Nat.mul_zero] at h
      omega
    have hmul : ∀ u v : ℕ, 4 ≤ u → 5 ≤ v → 2 * u + 2 * v ≤ u * v := by
      intro u v hu hv
      obtain ⟨a, rfl⟩ := Nat.exists_eq_add_of_le hu
      obtain ⟨b, rfl⟩ := Nat.exists_eq_add_of_le hv
      nlinarith [Nat.zero_le (a * b)]
    obtain ⟨x0, hx0, hx0c⟩ := big X hXpos hX
    obtain ⟨s0, hs0, hs0c⟩ := big S hSpos hS
    have huv : X.card * S.card < 2 * n := by
      obtain ⟨y, -, hyn, -, h⟩ := hxs x0 hx0 s0 hs0
      have h2 : X.card * S.card ≤ x0 * s0 := Nat.mul_le_mul hx0c hs0c
      omega
    have hu2 : X.card ≤ 2 := by
      by_contra h
      push Not at h
      rcases Nat.lt_or_ge X.card 4 with h4 | h4
      · have h3 : X.card = 3 := by omega
        rw [h3] at huv hcard
        omega
      · have := hmul X.card S.card h4 (by omega)
        omega
    intro x hx
    by_contra hx1
    have hxpos := hXpos x hx
    rcases Nat.lt_or_ge x 3 with h3 | h3
    · have hx2 : x = 2 := by omega
      subst hx2
      have hsub : S ⊆ ((Finset.Ioo 0 n).erase p).erase (2 * p) := by
        intro s hs
        obtain ⟨y, hy0, hyn, hpy, h⟩ := hxs 2 hx s hs
        have hsy : s = y := by omega
        subst hsy
        rw [Finset.mem_erase, Finset.mem_erase, Finset.mem_Ioo]
        refine ⟨?_, ?_, hy0, hyn⟩
        · rintro rfl; exact hpy ⟨2, by ring⟩
        · rintro rfl; exact hpy ⟨1, by ring⟩
      have h1 := Finset.card_le_card hsub
      rw [Finset.card_erase_of_mem (by
          rw [Finset.mem_erase, Finset.mem_Ioo]; omega),
        Finset.card_erase_of_mem (by rw [Finset.mem_Ioo]; omega), Nat.card_Ioo] at h1
      omega
    · have hsub : S ⊆ Finset.Icc 1 (2 * (n - 1) / 3) := by
        intro s hs
        obtain ⟨y, hy0, hyn, hpy, h⟩ := hxs x hx s hs
        have h4 : 3 * s ≤ x * s := Nat.mul_le_mul_right s h3
        rw [Finset.mem_Icc]
        exact ⟨hSpos s hs, by omega⟩
      have h1 := Finset.card_le_card hsub
      rw [Nat.card_Icc] at h1
      omega
  have R2b_K2 : ∀ (n p : ℕ) (X S : Finset ℕ) (hp0 : 0 < p) (h2p : 2 * p < n) (h9 : 9 ≤ n) (hxs : ∀ x ∈ X, ∀ s ∈ S, ∃ y, 0 < y ∧ y < n ∧ ¬ p ∣ y ∧ (x * s = 2 * y ∨ (x * s = y ∧ ¬ 2 ∣ y))) (hX : X.Nonempty) (hS : S.Nonempty) (hcard : n ≤ X.card + S.card),
      (∀ x ∈ X, x = 1) ∨ (∀ s ∈ S, s = 1) := by
    intro n p X S hp0 h2p h9 hxs hX hS hcard
    rcases le_total X.card S.card with h | h
    · exact Or.inl (R2b_K2half n p X S hp0 h2p h9 hxs hX hS hcard h)
    · refine Or.inr (R2b_K2half n p S X hp0 h2p h9 ?_ hS hX (by omega) h)
      intro s hs x hx
      rw [Nat.mul_comm]
      exact hxs x hx s hs
  have R2b_block : ∀ (B : Finset ℕ) (h0 : 0 ∉ B) (hgcd : B.gcd id = 1) (hlt : ∀ a ∈ B, ∀ b ∈ B, a < B.card * a.gcd b) (p : ℕ) (hp : p.Prime) (hp3 : 3 ≤ p) (h2p : 2 * p < B.card) (hn3 : B.card ≤ 3 * p) (h9 : 9 ≤ B.card) (hex : ∃ a ∈ B, p ∣ a),
      ∃ g ∈ B, ¬ p ∣ g ∧ (∀ b ∈ B, ¬ p ∣ b → b = g) ∧ ∀ a ∈ B, a ∣ 2 * p * g := by
    intro B h0 hgcd hlt p hp hp3 h2p hn3 h9 hex
    obtain ⟨a0, ha0, hpa0⟩ := hex
    have hexb : ∃ b ∈ B, ¬ p ∣ b := by
      by_contra h
      push Not at h
      have h1 : p ∣ B.gcd id := Finset.dvd_gcd (fun b hb => h b hb)
      rw [hgcd] at h1
      exact hp.one_lt.ne' (Nat.dvd_one.mp h1)
    obtain ⟨b0, hb0, hpb0⟩ := hexb
    have hpos : ∀ a ∈ B, 0 < a := fun a ha => Nat.pos_of_ne_zero (fun h => h0 (h ▸ ha))
    -- the pair analysis: a = g·x, b = g·y, x ∈ {p, 2p}
    have hA : ∀ a ∈ B, p ∣ a → ∀ b ∈ B, ¬ p ∣ b → ∃ y, 0 < y ∧ y < B.card ∧ ¬ p ∣ y ∧
        b = a.gcd b * y ∧ (a = p * a.gcd b ∨ (a = 2 * p * a.gcd b ∧ ¬ 2 ∣ y)) := by
      intro a ha hpa b hb hpb
      have hg0 : 0 < a.gcd b := Nat.gcd_pos_of_pos_left b (hpos a ha)
      obtain ⟨x, hx⟩ := Nat.gcd_dvd_left a b
      obtain ⟨y, hy⟩ := Nat.gcd_dvd_right a b
      have hpg : ¬ p ∣ a.gcd b := fun h => hpb (h.trans (Nat.gcd_dvd_right a b))
      have hpx : p ∣ x := by
        have h1 : p ∣ a.gcd b * x := hx ▸ hpa
        exact (hp.dvd_mul.mp h1).resolve_left hpg
      obtain ⟨t, ht⟩ := hpx
      have hxn : x < B.card := by
        have h3 : a.gcd b * x < a.gcd b * B.card := by
          rw [← hx, Nat.mul_comm]; exact hlt a ha b hb
        exact Nat.lt_of_mul_lt_mul_left h3
      have hyn : y < B.card := by
        have h3 : a.gcd b * y < a.gcd b * B.card := by
          rw [← hy, Nat.mul_comm, Nat.gcd_comm]; exact hlt b hb a ha
        exact Nat.lt_of_mul_lt_mul_left h3
      have hx0 : x ≠ 0 := by
        rintro rfl
        rw [Nat.mul_zero] at hx
        exact (hpos a ha).ne' hx
      have hy0 : y ≠ 0 := by
        rintro rfl
        rw [Nat.mul_zero] at hy
        exact (hpos b hb).ne' hy
      have hpy : ¬ p ∣ y := fun h => hpb (hy ▸ Dvd.dvd.mul_left h _)
      have hcop : Nat.Coprime x y := by
        have h1 := Nat.coprime_div_gcd_div_gcd hg0
        have e1 : a / a.gcd b = x := Nat.div_eq_of_eq_mul_right hg0 hx
        have e2 : b / a.gcd b = y := Nat.div_eq_of_eq_mul_right hg0 hy
        rwa [e1, e2] at h1
      have ht0 : t ≠ 0 := by
        rintro rfl
        rw [Nat.mul_zero] at ht
        exact hx0 ht
      have ht3 : t < 3 := by
        by_contra h
        push Not at h
        have h4 : p * 3 ≤ p * t := Nat.mul_le_mul_left p h
        omega
      refine ⟨y, Nat.pos_of_ne_zero hy0, hyn, hpy, hy, ?_⟩
      rcases (by omega : t = 1 ∨ t = 2) with rfl | rfl
      · left
        calc a = a.gcd b * x := hx
          _ = p * a.gcd b := by rw [ht]; ring
      · right
        refine ⟨(calc a = a.gcd b * x := hx
          _ = 2 * p * a.gcd b := by rw [ht]; ring), ?_⟩
        intro h2y
        have h2x : 2 ∣ x := ⟨p, by rw [ht]; ring⟩
        have := Nat.Coprime.eq_one_of_dvd (Nat.Coprime.coprime_dvd_left h2x hcop) h2y
        omega
    have hG0 : (B.filter (fun b => ¬ p ∣ b)).gcd id ≠ 0 := by
      intro h
      have h1 : (B.filter (fun b => ¬ p ∣ b)).gcd id ∣ id b0 :=
        Finset.gcd_dvd (Finset.mem_filter.mpr ⟨hb0, hpb0⟩)
      rw [h] at h1
      exact hpb0 (by rw [show b0 = 0 from Nat.eq_zero_of_zero_dvd h1]; exact dvd_zero p)
    have hGb : ∀ b ∈ B, ¬ p ∣ b → (B.filter (fun b => ¬ p ∣ b)).gcd id ∣ b := by
      intro b hb hpb
      exact Finset.gcd_dvd (f := id) (Finset.mem_filter.mpr ⟨hb, hpb⟩)
    have hdiv : ∀ a ∈ B, p ∣ a → a ∣ 2 * p * (B.filter (fun b => ¬ p ∣ b)).gcd id := by
      intro a ha hpa
      have h1 : a ∣ (B.filter (fun b => ¬ p ∣ b)).gcd (fun b => (2 * p) * id b) := by
        apply Finset.dvd_gcd
        intro b hb
        obtain ⟨hbB, hpb⟩ := Finset.mem_filter.mp hb
        obtain ⟨y, -, -, -, hy, h⟩ := hA a ha hpa b hbB hpb
        have h2 : a ∣ 2 * p * a.gcd b := by
          rcases h with h | ⟨h, -⟩
          · exact ⟨2, by linarith⟩
          · exact ⟨1, by linarith⟩
        exact h2.trans (Nat.mul_dvd_mul_left _ (Nat.gcd_dvd_right a b))
      rw [Finset.gcd_mul_left] at h1
      simpa using h1
    have hprod : ∀ a ∈ B, p ∣ a → ∀ b ∈ B, ¬ p ∣ b →
        (∃ y, 0 < y ∧ y < B.card ∧ ¬ p ∣ y ∧
          ((2 * p * (B.filter (fun b => ¬ p ∣ b)).gcd id / a) * (b / (B.filter (fun b => ¬ p ∣ b)).gcd id) = 2 * y ∨
           ((2 * p * (B.filter (fun b => ¬ p ∣ b)).gcd id / a) * (b / (B.filter (fun b => ¬ p ∣ b)).gcd id) = y ∧ ¬ 2 ∣ y))) ∧
        a * (2 * p * (B.filter (fun b => ¬ p ∣ b)).gcd id / a) = 2 * p * (B.filter (fun b => ¬ p ∣ b)).gcd id := by
      intro a ha hpa b hb hpb
      have hd := hdiv a ha hpa
      have hGb' := hGb b hb hpb
      generalize (B.filter (fun b => ¬ p ∣ b)).gcd id = G at *
      obtain ⟨e, he⟩ := hd
      obtain ⟨s, hs⟩ := hGb'
      obtain ⟨y, hy0, hyn, hpy, hy, h⟩ := hA a ha hpa b hb hpb
      have ha0' := hpos a ha
      have hg0 : 0 < a.gcd b := Nat.gcd_pos_of_pos_left b ha0'
      have hx : 2 * p * G / a = e := by rw [he]; exact Nat.mul_div_cancel_left e ha0'
      have ht : b / G = s := by
        rw [hs]; exact Nat.mul_div_cancel_left s (Nat.pos_of_ne_zero hG0)
      rw [hx, ht]
      have hmain : a * (e * s) = 2 * p * (a.gcd b * y) := by
        calc a * (e * s) = (a * e) * s := by ring
          _ = 2 * p * (G * s) := by rw [← he]; ring
          _ = 2 * p * (a.gcd b * y) := by rw [← hs, ← hy]
      refine ⟨⟨y, hy0, hyn, hpy, ?_⟩, he.symm⟩
      rcases h with h | ⟨h, h2y⟩
      · left
        have h5 : p * a.gcd b * (e * s) = p * a.gcd b * (2 * y) := by
          calc p * a.gcd b * (e * s) = a * (e * s) := by rw [← h]
            _ = 2 * p * (a.gcd b * y) := hmain
            _ = p * a.gcd b * (2 * y) := by ring
        exact Nat.eq_of_mul_eq_mul_left (Nat.mul_pos hp.pos hg0) h5
      · right
        refine ⟨?_, h2y⟩
        have h5 : 2 * p * a.gcd b * (e * s) = 2 * p * a.gcd b * y := by
          calc 2 * p * a.gcd b * (e * s) = a * (e * s) := by rw [← h]
            _ = 2 * p * (a.gcd b * y) := hmain
            _ = 2 * p * a.gcd b * y := by ring
        exact Nat.eq_of_mul_eq_mul_left (Nat.mul_pos (Nat.mul_pos (by norm_num) hp.pos) hg0) h5
    have hcardsum : (B.filter (fun a => p ∣ a)).card + (B.filter (fun b => ¬ p ∣ b)).card = B.card := by
      rw [← Finset.card_union_of_disjoint (Finset.disjoint_filter_filter_not B B (fun a => p ∣ a)),
        Finset.filter_union_filter_not_eq]
    have hinjX : Set.InjOn (fun a => 2 * p * (B.filter (fun b => ¬ p ∣ b)).gcd id / a)
        (B.filter (fun a => p ∣ a) : Finset ℕ) := by
      intro a ha a' ha' h
      obtain ⟨haB, hpa⟩ := Finset.mem_filter.mp ha
      obtain ⟨haB', hpa'⟩ := Finset.mem_filter.mp ha'
      have h1 := (hprod a haB hpa b0 hb0 hpb0).2
      have h2 := (hprod a' haB' hpa' b0 hb0 hpb0).2
      simp only at h
      rw [← h] at h2
      have hq : 0 < 2 * p * (B.filter (fun b => ¬ p ∣ b)).gcd id / a := by
        apply Nat.pos_of_ne_zero
        intro hz
        rw [hz, Nat.mul_zero] at h1
        have := Nat.mul_pos (Nat.mul_pos (by norm_num : 0 < 2) hp.pos) (Nat.pos_of_ne_zero hG0)
        omega
      exact Nat.eq_of_mul_eq_mul_right hq (h1.trans h2.symm)
    have hinjT : Set.InjOn (fun b => b / (B.filter (fun b => ¬ p ∣ b)).gcd id)
        (B.filter (fun b => ¬ p ∣ b) : Finset ℕ) := by
      intro b hb b' hb' h
      obtain ⟨hbB, hpb⟩ := Finset.mem_filter.mp hb
      obtain ⟨hbB', hpb'⟩ := Finset.mem_filter.mp hb'
      simp only at h
      rw [← Nat.div_mul_cancel (hGb b hbB hpb), ← Nat.div_mul_cancel (hGb b' hbB' hpb'), h]
    have hK := R2b_K2 B.card p
      ((B.filter (fun a => p ∣ a)).image (fun a => 2 * p * (B.filter (fun b => ¬ p ∣ b)).gcd id / a))
      ((B.filter (fun b => ¬ p ∣ b)).image (fun b => b / (B.filter (fun b => ¬ p ∣ b)).gcd id))
      hp.pos h2p h9
      (by
        intro x hx t ht
        obtain ⟨a, ha, rfl⟩ := Finset.mem_image.mp hx
        obtain ⟨b, hb, rfl⟩ := Finset.mem_image.mp ht
        obtain ⟨haB, hpa⟩ := Finset.mem_filter.mp ha
        obtain ⟨hbB, hpb⟩ := Finset.mem_filter.mp hb
        exact (hprod a haB hpa b hbB hpb).1)
      ⟨_, Finset.mem_image_of_mem _ (Finset.mem_filter.mpr ⟨ha0, hpa0⟩)⟩
      ⟨_, Finset.mem_image_of_mem _ (Finset.mem_filter.mpr ⟨hb0, hpb0⟩)⟩
      (by rw [Finset.card_image_of_injOn hinjX, Finset.card_image_of_injOn hinjT, hcardsum])
    rcases hK with hX1 | hS1
    · -- every multiple of p equals 2pG, G = 1: B = {2p} ∪ T, impossible by Lemma I
      exfalso
      have hall : ∀ a ∈ B, p ∣ a → a = 2 * p * (B.filter (fun b => ¬ p ∣ b)).gcd id := by
        intro a ha hpa
        have h1 := hX1 _ (Finset.mem_image_of_mem _ (Finset.mem_filter.mpr ⟨ha, hpa⟩))
        have h2 := (hprod a ha hpa b0 hb0 hpb0).2
        rw [h1, Nat.mul_one] at h2
        exact h2
      have hG1 : (B.filter (fun b => ¬ p ∣ b)).gcd id = 1 := by
        have h1 : (B.filter (fun b => ¬ p ∣ b)).gcd id ∣ B.gcd id := by
          apply Finset.dvd_gcd
          intro b hb
          by_cases hpb : p ∣ b
          · exact ⟨2 * p, by rw [id, hall b hb hpb]; ring⟩
          · exact hGb b hb hpb
        rw [hgcd] at h1
        exact Nat.dvd_one.mp h1
      rw [hG1, Nat.mul_one] at hall
      have h2pB : 2 * p ∈ B := by rw [← hall a0 ha0 hpa0]; exact ha0
      have hT : ∀ b ∈ B.erase (2 * p), b ∈ B ∧ ¬ p ∣ b := by
        intro b hb
        obtain ⟨hne, hbB⟩ := Finset.mem_erase.mp hb
        exact ⟨hbB, fun h => hne (hall b hbB h)⟩
      have hbound : ∀ b ∈ B.erase (2 * p), b < B.card * b.gcd 2 := by
        intro b hb
        obtain ⟨hbB, hpb⟩ := hT b hb
        have h1 := hlt b hbB (2 * p) h2pB
        have hc : Nat.Coprime p b := (Nat.Prime.coprime_iff_not_dvd hp).mpr hpb
        rwa [Nat.Coprime.gcd_mul_right_cancel_right 2 hc] at h1
      have hI := R2b_lemI B.card p (B.erase (2 * p)) hp hp3 h2p hn3
        (fun b hb => hpos b (hT b hb).1) (fun b hb => (hT b hb).2)
        (by
          intro b hb h2
          have h1 := hbound b hb
          have hc : Nat.Coprime b 2 :=
            Nat.Coprime.symm ((Nat.Prime.coprime_iff_not_dvd Nat.prime_two).mpr h2)
          rw [Nat.Coprime.gcd_eq_one hc] at h1
          omega)
        (by
          intro b hb _
          have h1 := hbound b hb
          have h3 : b.gcd 2 ≤ 2 := Nat.gcd_le_right b (by norm_num)
          have h4 : B.card * b.gcd 2 ≤ B.card * 2 := Nat.mul_le_mul_left _ h3
          omega)
        (fun b hb t ht _ _ => hlt b (hT b hb).1 t (hT t ht).1)
      rw [Finset.card_erase_of_mem h2pB] at hI
      omega
    · -- every non-multiple equals G
      have hall : ∀ b ∈ B, ¬ p ∣ b → b = (B.filter (fun b => ¬ p ∣ b)).gcd id := by
        intro b hb hpb
        have h1 := hS1 _ (Finset.mem_image_of_mem _ (Finset.mem_filter.mpr ⟨hb, hpb⟩))
        have h2 := Nat.div_mul_cancel (hGb b hb hpb)
        rw [h1, Nat.one_mul] at h2
        exact h2.symm
      have hb0G := hall b0 hb0 hpb0
      refine ⟨b0, hb0, hpb0, ?_, ?_⟩
      · intro b hb hpb
        rw [hall b hb hpb, ← hb0G]
      · intro a ha
        by_cases hpa : p ∣ a
        · rw [hb0G]; exact hdiv a ha hpa
        · rw [hall a ha hpa, ← hb0G]; exact Dvd.intro_left _ rfl
  have R1b_dual_quot : ∀ (L a a' b b' : ℕ) (ha : a * a' = L) (hb : b * b' = L) (h0 : 0 < a),
      a' * Nat.gcd a b = b * Nat.gcd a' b' := by
    intro L a a' b b' ha hb h0
    have h1 : Nat.gcd a' b' * (a * b) = L * Nat.gcd a b := by
      rw [← Nat.gcd_mul_right]
      have e1 : a' * (a * b) = L * b := by rw [← ha]; ring
      have e2 : b' * (a * b) = L * a := by rw [← hb]; ring
      rw [e1, e2, Nat.gcd_mul_left, Nat.gcd_comm b a]
    have h2 : a * (a' * Nat.gcd a b) = a * (b * Nat.gcd a' b') := by
      rw [← mul_assoc, ha, ← h1]; ring
    exact Nat.eq_of_mul_eq_mul_left h0 h2
  have R1b_dual_strict : ∀ (L a a' b b' n : ℕ) (ha : a * a' = L) (hb : b * b' = L) (hL : 0 < L) (h : a < n * Nat.gcd a b),
      b' < n * Nat.gcd b' a' := by
    intro L a a' b b' n ha hb hL h
    have hb0 : 0 < b := Nat.pos_of_ne_zero (by rintro rfl; simp at hb; omega)
    have hb'0 : 0 < b' := Nat.pos_of_ne_zero (by rintro rfl; simp at hb; omega)
    have ha0 : 0 < a := Nat.pos_of_ne_zero (by rintro rfl; simp at ha; omega)
    have e := R1b_dual_quot L b b' a a' hb ha hb0
    have hg : 0 < Nat.gcd b a := Nat.gcd_pos_of_pos_left _ hb0
    have hg' : 0 < Nat.gcd b' a' := Nat.gcd_pos_of_pos_left _ hb'0
    rw [Nat.gcd_comm a b] at h
    by_contra hcon
    push Not at hcon
    have h3 : n * Nat.gcd b' a' * Nat.gcd b a ≤ b' * Nat.gcd b a := Nat.mul_le_mul_right _ hcon
    have h4 : a * Nat.gcd b' a' < n * Nat.gcd b a * Nat.gcd b' a' := Nat.mul_lt_mul_of_pos_right h hg'
    rw [e] at h3
    nlinarith
  have R1b_dual_set : ∀ (B : Finset ℕ) (n : ℕ) (hne : B.Nonempty) (h0 : 0 ∉ B) (hs : ∀ a ∈ B, ∀ b ∈ B, a < n * Nat.gcd a b),
      (B.image (fun a => B.lcm id / a)).card = B.card ∧ 0 ∉ B.image (fun a => B.lcm id / a) ∧ (B.image (fun a => B.lcm id / a)).gcd id = 1 ∧ ∀ a ∈ B.image (fun a => B.lcm id / a), ∀ b ∈ B.image (fun a => B.lcm id / a), a < n * Nat.gcd a b := by
    intro B n hne h0 hs
    set L := B.lcm id with hLdef
    have hdvd : ∀ a ∈ B, a ∣ L := fun a ha => Finset.dvd_lcm (f := id) ha
    have hL0 : L ≠ 0 := by
      intro h
      rw [hLdef, Finset.lcm_eq_zero_iff] at h
      simp at h
      exact h0 h
    have hLpos : 0 < L := Nat.pos_of_ne_zero hL0
    have hmul : ∀ a ∈ B, a * (L / a) = L := fun a ha => Nat.mul_div_cancel' (hdvd a ha)
    have hqpos : ∀ a ∈ B, 0 < L / a := by
      intro a ha
      rcases Nat.eq_zero_or_pos (L / a) with h | h
      · have := hmul a ha
        rw [h] at this
        simp at this
        exact absurd this.symm hL0
      · exact h
    have hapos : ∀ a ∈ B, 0 < a := fun a ha => Nat.pos_of_ne_zero (fun e => h0 (e ▸ ha))
    refine ⟨?_, ?_, ?_, ?_⟩
    · apply Finset.card_image_of_injOn
      intro a ha b hb hab
      simp only at hab
      have e1 := hmul a ha
      have e2 := hmul b hb
      rw [hab] at e1
      have : a * (L / b) = b * (L / b) := by rw [e1, e2]
      exact Nat.eq_of_mul_eq_mul_right (hqpos b hb) this
    · intro h
      rw [Finset.mem_image] at h
      obtain ⟨a, ha, e⟩ := h
      have := hqpos a ha
      omega
    · set d := (B.image (fun a => L / a)).gcd id with hd
      have hdd : ∀ a ∈ B, d ∣ L / a := by
        intro a ha
        exact Finset.gcd_dvd (f := id) (Finset.mem_image_of_mem _ ha)
      obtain ⟨a0, ha0⟩ := hne
      have hdL : d ∣ L := (hdd a0 ha0).trans (Nat.div_dvd_of_dvd (hdvd a0 ha0))
      have hdpos : 0 < d := Nat.pos_of_dvd_of_pos hdL hLpos
      have hall : ∀ a ∈ B, id a ∣ L / d := by
        intro a ha
        obtain ⟨k, hk⟩ := hdd a ha
        have e : L = d * (a * k) := by
          have := hmul a ha
          rw [hk] at this
          rw [← this]; ring
        have : L / d = a * k := by rw [e]; exact Nat.mul_div_cancel_left _ hdpos
        rw [this]; exact Dvd.intro _ rfl
      have hLdvd : L ∣ L / d := Finset.lcm_dvd hall
      have hpos' : 0 < L / d := Nat.div_pos (Nat.le_of_dvd hLpos hdL) hdpos
      have hle : L ≤ L / d := Nat.le_of_dvd hpos' hLdvd
      by_contra hne1
      have h2 : 2 ≤ d := by omega
      have := Nat.div_lt_self hLpos h2
      omega
    · intro x hx y hy
      rw [Finset.mem_image] at hx hy
      obtain ⟨a, ha, rfl⟩ := hx
      obtain ⟨b, hb, rfl⟩ := hy
      exact R1b_dual_strict L b (L / b) a (L / a) n (hmul b hb) (hmul a ha) hLpos (hs b hb a ha)
  have R2b_small : ∀ (n p : ℕ) (hp : p.Prime) (h2p : 2 * p < n) (hn3 : n ≤ 3 * p) (hnp : ¬ n.Prime) (hnp1 : ∀ q : ℕ, q.Prime → n ≠ q + 1),
      3 ≤ p ∧ 9 ≤ n := by
    intro n p hp h2p hn3 hnp hnp1
    have h2 := hp.two_le
    rcases Nat.lt_or_ge p 5 with h5 | h5
    · interval_cases p
      · exfalso
        interval_cases n
        · exact hnp (by norm_num)
        · exact hnp1 5 (by norm_num) rfl
      · refine ⟨le_refl _, ?_⟩
        interval_cases n
        · exact (hnp (by norm_num)).elim
        · exact (hnp1 7 (by norm_num) rfl).elim
        · exact le_refl _
      · exact absurd hp (by norm_num)
    · omega
  have R2b_no_mid_prime : ∀ (B : Finset ℕ) (h0 : 0 ∉ B) (hgcd : B.gcd id = 1) (hlt : ∀ a ∈ B, ∀ b ∈ B, a < B.card * a.gcd b) (p : ℕ) (hp : p.Prime) (hp3 : 3 ≤ p) (h2p : 2 * p < B.card) (hn3 : B.card ≤ 3 * p) (h9 : 9 ≤ B.card),
      ∀ a ∈ B, ¬ p ∣ a := by
    intro B h0 hgcd hlt p hp hp3 h2p hn3 h9
    intro a0 ha0 hpa0
    obtain ⟨g, hg, hpg, huniq, hdvd⟩ := R2b_block B h0 hgcd hlt p hp hp3 h2p hn3 h9 ⟨a0, ha0, hpa0⟩
    obtain ⟨hcard, h0', hgcd', hlt'⟩ := R1b_dual_set B B.card ⟨a0, ha0⟩ h0 hlt
    have hpos : ∀ a ∈ B, 0 < a := fun a ha => Nat.pos_of_ne_zero (fun h => h0 (h ▸ ha))
    have hL : B.lcm id ∣ 2 * p * g := Finset.lcm_dvd (fun a ha => hdvd a ha)
    have hLpos : 0 < B.lcm id :=
      Nat.pos_of_dvd_of_pos hL (Nat.mul_pos (Nat.mul_pos (by norm_num) hp.pos) (hpos g hg))
    have hmul : ∀ a ∈ B, a * (B.lcm id / a) = B.lcm id :=
      fun a ha => Nat.mul_div_cancel' (Finset.dvd_lcm (f := id) ha)
    have hpLg : p ∣ B.lcm id / g := by
      have h1 : p ∣ g * (B.lcm id / g) := by
        rw [hmul g hg]; exact hpa0.trans (Finset.dvd_lcm (f := id) ha0)
      exact (hp.dvd_mul.mp h1).resolve_left hpg
    rw [← hcard] at hlt' h2p hn3 h9
    obtain ⟨g', hg', hpg', huniq', -⟩ := R2b_block _ h0' hgcd' hlt' p hp hp3 h2p hn3 h9
      ⟨_, Finset.mem_image_of_mem _ hg, hpLg⟩
    have h2 : 1 < (B.erase g).card := by
      rw [Finset.card_erase_of_mem hg, ← hcard]; omega
    obtain ⟨a1, ha1, a2, ha2, hne⟩ := Finset.one_lt_card.mp h2
    obtain ⟨hne1, ha1B⟩ := Finset.mem_erase.mp ha1
    obtain ⟨hne2, ha2B⟩ := Finset.mem_erase.mp ha2
    have hfin : ∀ a ∈ B, a ≠ g → p ∣ B.lcm id / a → False := by
      intro a ha hag hpLa
      have hpa : p ∣ a := by
        by_contra h
        exact hag (huniq a ha h)
      obtain ⟨c, hc⟩ := hpa
      obtain ⟨d, hd⟩ := hpLa
      have h3 : p * (p * (c * d)) ∣ p * (2 * g) := by
        have h4 : p * (p * (c * d)) = B.lcm id := by
          rw [← hmul a ha, hd]; rw [hc]; ring
        rw [h4]
        exact hL.trans (dvd_of_eq (by ring))
      have h5 : p ∣ 2 * g := (Dvd.intro _ rfl).trans (Nat.dvd_of_mul_dvd_mul_left hp.pos h3)
      rcases hp.dvd_mul.mp h5 with h6 | h6
      · have := Nat.le_of_dvd (by norm_num) h6
        omega
      · exact hpg h6
    by_cases hp1 : p ∣ B.lcm id / a1
    · exact hfin a1 ha1B hne1 hp1
    · by_cases hp2 : p ∣ B.lcm id / a2
      · exact hfin a2 ha2B hne2 hp2
      · have e1 := huniq' _ (Finset.mem_image_of_mem _ ha1B) hp1
        have e2 := huniq' _ (Finset.mem_image_of_mem _ ha2B) hp2
        have e3 : B.lcm id / a1 = B.lcm id / a2 := e1.trans e2.symm
        have m1 := hmul a1 ha1B
        have m2 := hmul a2 ha2B
        rw [e3] at m1
        have hq : 0 < B.lcm id / a2 := by
          apply Nat.pos_of_ne_zero
          intro hz
          rw [hz, Nat.mul_zero] at m2
          omega
        exact hne (Nat.eq_of_mul_eq_mul_right hq (m1.trans m2.symm))
  intro B h0 hne hgcd hnp hnp1 hle hpp
  rcases hmid B h0 hne hgcd hnp hnp1 hle hpp with h | ⟨p, hp, hn3, a, ha, hpa⟩
  · exact Or.inl h
  · by_cases h2 : B.card ≤ 2 * p
    · exact Or.inr ⟨p, hp, h2, a, ha, hpa⟩
    · left
      by_contra hcon
      have hn : 0 < B.card := hne.card_pos
      have hnq : (0 : ℚ) < B.card := by exact_mod_cast hn
      have hlt : ∀ a ∈ B, ∀ b ∈ B, a < B.card * a.gcd b := by
        intro a ha b hb
        rcases (hle a ha b hb).lt_or_eq with h | h
        · exact h
        · exfalso
          apply hcon
          refine ⟨a, ha, b, hb, ?_⟩
          rw [le_div_iff₀ hnq]
          have h2 : a.gcd b * B.card ≤ a := by rw [Nat.mul_comm]; exact h.ge
          exact_mod_cast h2
      obtain ⟨hp3, h9⟩ := R2b_small B.card p hp (by omega) hn3 hnp hnp1
      exact R2b_no_mid_prime B h0 hgcd hlt p hp hp3 (by omega) hn3 h9 a ha hpa

The gate replayed this file at its merge, each hole a sorry (D-12 #5); the whole file: targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1/attempts/20261001T143056Z-t1001-402a-partial.lean

theorem erdos_402__h3_v2__h1__h1__h1 : ∀ (B : Finset ℕ),
  (0 : ℕ) ∉ B →
    B.Nonempty →
      B.gcd id = (1 : ℕ) →
        ¬Nat.Prime B.card →
          (∀ (q : ℕ), Nat.Prime q → B.card ≠ q + (1 : ℕ)) →
            (∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) →
              (∀ a ∈ B, ∀ (p k : ℕ), Nat.Prime p → p ^ k ∣ a → p ^ k < B.card) →
                (∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ)) ∨
                  ∃ (p : ℕ), Nat.Prime p ∧ B.card ≤ (3 : ℕ) * p ∧ ∃ a ∈ B, p ∣ a := by
  -- Informal argument: the annex appended to this node on 2026-10-01 by this pseudonym (agent 402-R5-a), "window-prime criterion".
  -- Lean of the assembly: agent 402-R4-c (clean-room; engineering/evidence/testers-2026-10-01/402-R4-c), re-verified by 402-R5-a.
  -- Hole `hwin`: under this node's hypotheses, B has a pair with gcd(a, b) ≤ a / n, or there is a prime p with
  -- n < p < 2n and (2n − p)² ≤ n (n = |B|). The assembly proves that such a prime forces a pair.
  have hwin : ∀ (B : Finset ℕ),
    (0 : ℕ) ∉ B →
      B.Nonempty →
        B.gcd id = (1 : ℕ) →
          ¬Nat.Prime B.card →
            (∀ (q : ℕ), Nat.Prime q → B.card ≠ q + (1 : ℕ)) →
              (∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) →
                (∀ a ∈ B, ∀ (p k : ℕ), Nat.Prime p → p ^ k ∣ a → p ^ k < B.card) →
                  (∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ)) ∨
                    ∃ (p : ℕ), Nat.Prime p ∧ B.card < p ∧ p < 2 * B.card ∧
                    (2 * B.card - p) * (2 * B.card - p) ≤ B.card := by
    sorry
  obtain ⟨cls, hcls⟩ : ∃ cls : ℕ → ℕ → ℕ, ∀ p a, cls p a =
      min (ZMod.val ((a / p ^ a.factorization p : ℕ) : ZMod p))
        (p - ZMod.val ((a / p ^ a.factorization p : ℕ) : ZMod p)) := ⟨_, fun _ _ => rfl⟩

  -- 402-R4-c. Arithmetic heart of the rectangle lemma: two coprime divisors of α whose ratio is
  -- squeezed between α/n and n/α are equal (hence both 1), when α is within k of n and k² ≤ n.
  have r4c_arith (n k α e1 e2 : ℕ) (hk : k * k ≤ n) (hα : n < α + k)
      (he : e1 * e2 ≤ α) (h1 : α * e1 < n * e2) (h4 : α * e2 < n * e1) : e1 = e2 := by
    have key : ∀ x y : ℕ, x < y → x * y ≤ α → α * y < n * x → False := by
      intro x y hxy hx h
      have hαn : α ≤ n := by
        by_contra hc
        have : n * x ≤ α * y := Nat.mul_le_mul (by omega) (by omega)
        omega
      obtain ⟨s, rfl⟩ : ∃ s, n = α + s := ⟨n - α, by omega⟩
      have hs : s < k := by omega
      have a1 : α * (x + 1) ≤ α * y := Nat.mul_le_mul_left _ hxy
      have a2 : α < s * x := by nlinarith
      have a3 : x * (x + 1) ≤ x * y := Nat.mul_le_mul_left _ hxy
      have a4 : x + 1 < s := by
        by_contra hc
        have : s * x ≤ (x + 1) * x := Nat.mul_le_mul_right _ (by omega)
        nlinarith
      have a5 : (s + 1) * (s + 1) ≤ k * k := Nat.mul_le_mul hs hs
      have a6 : s * x ≤ s * s := Nat.mul_le_mul_left _ (by omega)
      nlinarith
    rcases Nat.lt_trichotomy e1 e2 with h | h | h
    · exact (key e1 e2 h he h4).elim
    · exact h
    · exact (key e2 e1 h (by rwa [Nat.mul_comm]) h1).elim


  -- 402-R4-c. Rectangle lemma, coprime core: α, β coprime and both within k of n (k² ≤ n), d1, d2
  -- coprime; if all four cross quotients of {α d1, β d1, α d2, β d2} are below n then d1 = d2 = 1.
  have r4c_rect_core (n k α β d1 d2 : ℕ) (hk : k * k ≤ n) (hα : n < α + k) (hβ : n < β + k)
      (α0 : 0 < α) (β0 : 0 < β) (hαβ : Nat.Coprime α β) (hd : Nat.Coprime d1 d2)
      (h1 : 0 < d1) (h2 : 0 < d2)
      (H1 : α * d1 < n * Nat.gcd (α * d1) (β * d2)) (H2 : β * d2 < n * Nat.gcd (α * d1) (β * d2))
      (H3 : β * d1 < n * Nat.gcd (β * d1) (α * d2)) (H4 : α * d2 < n * Nat.gcd (β * d1) (α * d2)) :
      d1 = 1 ∧ d2 = 1 := by
    have e1p : 0 < Nat.gcd α d1 := Nat.gcd_pos_of_pos_left _ α0
    have e2p : 0 < Nat.gcd α d2 := Nat.gcd_pos_of_pos_left _ α0
    have f1p : 0 < Nat.gcd β d1 := Nat.gcd_pos_of_pos_left _ β0
    have f2p : 0 < Nat.gcd β d2 := Nat.gcd_pos_of_pos_left _ β0
    have hG : Nat.gcd (α * d1) (β * d2) ≤ Nat.gcd α d2 * Nat.gcd β d1 := by
      apply Nat.le_of_dvd (Nat.mul_pos e2p f1p)
      have h := Nat.gcd_mul_right_dvd_mul_gcd (α * d1) β d2
      rw [Nat.Coprime.gcd_mul_left_cancel d1 hαβ, Nat.Coprime.gcd_mul_right_cancel α hd] at h
      rw [Nat.gcd_comm d1 β, Nat.mul_comm (β.gcd d1)] at h; exact h
    have hG' : Nat.gcd (β * d1) (α * d2) ≤ Nat.gcd α d1 * Nat.gcd β d2 := by
      apply Nat.le_of_dvd (Nat.mul_pos e1p f2p)
      have h := Nat.gcd_mul_right_dvd_mul_gcd (β * d1) α d2
      rw [Nat.Coprime.gcd_mul_left_cancel d1 hαβ.symm, Nat.Coprime.gcd_mul_right_cancel β hd] at h
      rw [Nat.gcd_comm d1 α] at h; exact h
    have ce : Nat.Coprime (Nat.gcd α d1) (Nat.gcd α d2) :=
      Nat.Coprime.coprime_dvd_left (Nat.gcd_dvd_right _ _)
        (Nat.Coprime.coprime_dvd_right (Nat.gcd_dvd_right _ _) hd)
    have cf : Nat.Coprime (Nat.gcd β d1) (Nat.gcd β d2) :=
      Nat.Coprime.coprime_dvd_left (Nat.gcd_dvd_right _ _)
        (Nat.Coprime.coprime_dvd_right (Nat.gcd_dvd_right _ _) hd)
    have c1 : Nat.Coprime (Nat.gcd α d1) (Nat.gcd β d1) :=
      Nat.Coprime.coprime_dvd_left (Nat.gcd_dvd_left _ _)
        (Nat.Coprime.coprime_dvd_right (Nat.gcd_dvd_left _ _) hαβ)
    have c2 : Nat.Coprime (Nat.gcd α d2) (Nat.gcd β d2) :=
      Nat.Coprime.coprime_dvd_left (Nat.gcd_dvd_left _ _)
        (Nat.Coprime.coprime_dvd_right (Nat.gcd_dvd_left _ _) hαβ)
    have m1 : Nat.gcd α d1 * Nat.gcd β d1 ≤ d1 := Nat.le_of_dvd h1
      (Nat.Coprime.mul_dvd_of_dvd_of_dvd c1 (Nat.gcd_dvd_right _ _) (Nat.gcd_dvd_right _ _))
    have m2 : Nat.gcd α d2 * Nat.gcd β d2 ≤ d2 := Nat.le_of_dvd h2
      (Nat.Coprime.mul_dvd_of_dvd_of_dvd c2 (Nat.gcd_dvd_right _ _) (Nat.gcd_dvd_right _ _))
    have mα : Nat.gcd α d1 * Nat.gcd α d2 ≤ α := Nat.le_of_dvd α0
      (Nat.Coprime.mul_dvd_of_dvd_of_dvd ce (Nat.gcd_dvd_left _ _) (Nat.gcd_dvd_left _ _))
    have mβ : Nat.gcd β d1 * Nat.gcd β d2 ≤ β := Nat.le_of_dvd β0
      (Nat.Coprime.mul_dvd_of_dvd_of_dvd cf (Nat.gcd_dvd_left _ _) (Nat.gcd_dvd_left _ _))
    generalize Nat.gcd α d1 = e1 at *
    generalize Nat.gcd α d2 = e2 at *
    generalize Nat.gcd β d1 = f1 at *
    generalize Nat.gcd β d2 = f2 at *
    generalize Nat.gcd (α * d1) (β * d2) = G at *
    generalize Nat.gcd (β * d1) (α * d2) = G' at *
    have i1 : α * e1 < n * e2 := by
      have a : α * (e1 * f1) ≤ α * d1 := Nat.mul_le_mul_left _ m1
      have b : n * G ≤ n * (e2 * f1) := Nat.mul_le_mul_left _ hG
      have c : (α * e1) * f1 < (n * e2) * f1 := by
        calc (α * e1) * f1 = α * (e1 * f1) := by ring
          _ ≤ α * d1 := a
          _ < n * G := H1
          _ ≤ n * (e2 * f1) := b
          _ = (n * e2) * f1 := by ring
      exact Nat.lt_of_mul_lt_mul_right c
    have i4 : α * e2 < n * e1 := by
      have a : α * (e2 * f2) ≤ α * d2 := Nat.mul_le_mul_left _ m2
      have b : n * G' ≤ n * (e1 * f2) := Nat.mul_le_mul_left _ hG'
      have c : (α * e2) * f2 < (n * e1) * f2 := by
        calc (α * e2) * f2 = α * (e2 * f2) := by ring
          _ ≤ α * d2 := a
          _ < n * G' := H4
          _ ≤ n * (e1 * f2) := b
          _ = (n * e1) * f2 := by ring
      exact Nat.lt_of_mul_lt_mul_right c
    have i2 : β * f2 < n * f1 := by
      have a : β * (e2 * f2) ≤ β * d2 := Nat.mul_le_mul_left _ m2
      have b : n * G ≤ n * (e2 * f1) := Nat.mul_le_mul_left _ hG
      have c : (β * f2) * e2 < (n * f1) * e2 := by
        calc (β * f2) * e2 = β * (e2 * f2) := by ring
          _ ≤ β * d2 := a
          _ < n * G := H2
          _ ≤ n * (e2 * f1) := b
          _ = (n * f1) * e2 := by ring
      exact Nat.lt_of_mul_lt_mul_right c
    have i3 : β * f1 < n * f2 := by
      have a : β * (e1 * f1) ≤ β * d1 := Nat.mul_le_mul_left _ m1
      have b : n * G' ≤ n * (e1 * f2) := Nat.mul_le_mul_left _ hG'
      have c : (β * f1) * e1 < (n * f2) * e1 := by
        calc (β * f1) * e1 = β * (e1 * f1) := by ring
          _ ≤ β * d1 := a
          _ < n * G' := H3
          _ ≤ n * (e1 * f2) := b
          _ = (n * f2) * e1 := by ring
      exact Nat.lt_of_mul_lt_mul_right c
    have ee : e1 = e2 := r4c_arith n k α e1 e2 hk hα mα i1 i4
    have ff : f1 = f2 := r4c_arith n k β f1 f2 hk hβ mβ i3 i2
    subst ee; subst ff
    have e1 : e1 = 1 := Nat.coprime_self e1 |>.mp ce
    have f1 : f1 = 1 := Nat.coprime_self f1 |>.mp cf
    subst e1; subst f1
    have kα : k ≤ α := by
      by_contra hc
      have : (α + 1) * k ≤ k * k := Nat.mul_le_mul_right _ (by omega)
      nlinarith
    have g1 : n * G ≤ n := by simpa using Nat.mul_le_mul_left n hG
    have g2 : n * G' ≤ n := by simpa using Nat.mul_le_mul_left n hG'
    constructor
    · by_contra hc
      have : α * 2 ≤ α * d1 := Nat.mul_le_mul_left _ (by omega)
      omega
    · by_contra hc
      have : α * 2 ≤ α * d2 := Nat.mul_le_mul_left _ (by omega)
      omega


  -- 402-R4-c. Collision lemma for one pair: both quotients below n ≤ p and equal fold classes
  -- force a = b or reduced quotients adding up to p.
  have r4c_pair (p n a b : ℕ) (hp : p.Prime) (hnp : n ≤ p) (a0 : 0 < a) (b0 : 0 < b)
      (ha : a < n * Nat.gcd a b) (hb : b < n * Nat.gcd a b) (hc : cls p a = cls p b) :
      a = b ∨ ∃ x y g, x + y = p ∧ Nat.Coprime x y ∧ a = x * g ∧ b = y * g := by
    have := Fact.mk hp
    obtain ⟨x, y, hxy, hax, hby⟩ := Nat.exists_coprime a b
    have g0 : 0 < Nat.gcd a b := Nat.gcd_pos_of_pos_left _ a0
    generalize Nat.gcd a b = g at *
    have xn : x < n := by
      rw [hax] at ha; exact Nat.lt_of_mul_lt_mul_right ha
    have yn : y < n := by
      rw [hby] at hb; exact Nat.lt_of_mul_lt_mul_right hb
    have x0 : 0 < x := by
      rcases Nat.eq_zero_or_pos x with h | h
      · subst h; omega
      · exact h
    have y0 : 0 < y := by
      rcases Nat.eq_zero_or_pos y with h | h
      · subst h; omega
      · exact h
    have key : a * y = b * x := by rw [hax, hby]; ring
    have oc : ∀ z : ℕ, 0 < z → z < p → z / p ^ z.factorization p = z := by
      intro z hz hzp
      have : ¬ p ∣ z := fun h => by have := Nat.le_of_dvd hz h; omega
      rw [Nat.factorization_eq_zero_of_not_dvd this]; simp
    have key2 : (a / p ^ a.factorization p) * y = (b / p ^ b.factorization p) * x := by
      have h := congrArg (fun m => m / p ^ m.factorization p) key
      simp only [Nat.ordCompl_mul] at h
      rwa [oc y y0 (by omega), oc x x0 (by omega)] at h
    have na : ((a / p ^ a.factorization p : ℕ) : ZMod p) ≠ 0 := by
      rw [Ne, ZMod.natCast_eq_zero_iff]; exact Nat.not_dvd_ordCompl hp (by omega)
    have nb : ((b / p ^ b.factorization p : ℕ) : ZMod p) ≠ 0 := by
      rw [Ne, ZMod.natCast_eq_zero_iff]; exact Nat.not_dvd_ordCompl hp (by omega)
    have key3 : ((a / p ^ a.factorization p : ℕ) : ZMod p) * (y : ZMod p)
        = ((b / p ^ b.factorization p : ℕ) : ZMod p) * (x : ZMod p) := by
      exact_mod_cast congrArg (Nat.cast : ℕ → ZMod p) key2
    rw [hcls, hcls] at hc
    generalize ((a / p ^ a.factorization p : ℕ) : ZMod p) = ra at *
    generalize ((b / p ^ b.factorization p : ℕ) : ZMod p) = rb at *
    have va := ZMod.val_lt ra
    have vb := ZMod.val_lt rb
    have va0 : 0 < ra.val := (ZMod.val_pos).mpr na
    have vb0 : 0 < rb.val := (ZMod.val_pos).mpr nb
    have hcase : ra.val = rb.val ∨ ra.val + rb.val = p := by omega
    rcases hcase with h | h
    · left
      have hr : ra = rb := ZMod.val_injective p h
      rw [hr] at key3
      have h2 : (y : ZMod p) = (x : ZMod p) := mul_left_cancel₀ nb key3
      have h3 := (ZMod.natCast_eq_natCast_iff' y x p).mp h2
      rw [Nat.mod_eq_of_lt (by omega), Nat.mod_eq_of_lt (by omega)] at h3
      rw [hax, hby, h3]
    · right
      have hr : ra + rb = 0 := by
        have h4 : ((ra.val + rb.val : ℕ) : ZMod p) = ((p : ℕ) : ZMod p) := by rw [h]
        rw [Nat.cast_add, ZMod.natCast_zmod_val, ZMod.natCast_zmod_val, ZMod.natCast_self] at h4
        exact h4
      have hra : ra = -rb := eq_neg_of_add_eq_zero_left hr
      rw [hra] at key3
      have h5 : rb * ((x : ZMod p) + (y : ZMod p)) = 0 := by
        have : rb * ((x : ZMod p) + (y : ZMod p)) = rb * x - (-rb * y) := by ring
        rw [this, key3]; ring
      have h6 : ((x + y : ℕ) : ZMod p) = 0 := by
        rcases mul_eq_zero.mp h5 with h | h
        · exact (nb h).elim
        · exact_mod_cast h
      rw [ZMod.natCast_eq_zero_iff] at h6
      exact ⟨x, y, g, Nat.eq_of_dvd_of_lt_two_mul (by omega) h6 (by omega), hxy, hax, hby⟩


  -- 402-R4-c. Rectangle lemma: α u, β u, α w, β w with all four cross quotients below n force u = w.
  have r4c_rect (n k α β u w : ℕ) (hk : k * k ≤ n) (hα : n < α + k) (hβ : n < β + k)
      (α0 : 0 < α) (β0 : 0 < β) (hαβ : Nat.Coprime α β) (u0 : 0 < u) (w0 : 0 < w)
      (H1 : α * u < n * Nat.gcd (α * u) (β * w)) (H2 : β * w < n * Nat.gcd (α * u) (β * w))
      (H3 : β * u < n * Nat.gcd (β * u) (α * w)) (H4 : α * w < n * Nat.gcd (β * u) (α * w)) :
      u = w := by
    obtain ⟨d1, d2, hd, hu, hw⟩ := Nat.exists_coprime u w
    have C0 : 0 < Nat.gcd u w := Nat.gcd_pos_of_pos_left _ u0
    generalize Nat.gcd u w = C at *
    subst hu; subst hw
    have d10 : 0 < d1 := Nat.pos_of_mul_pos_right u0
    have d20 : 0 < d2 := Nat.pos_of_mul_pos_right w0
    have s1 : Nat.gcd (α * (d1 * C)) (β * (d2 * C)) = Nat.gcd (α * d1) (β * d2) * C := by
      rw [← Nat.mul_assoc, ← Nat.mul_assoc, Nat.gcd_mul_right]
    have s2 : Nat.gcd (β * (d1 * C)) (α * (d2 * C)) = Nat.gcd (β * d1) (α * d2) * C := by
      rw [← Nat.mul_assoc, ← Nat.mul_assoc, Nat.gcd_mul_right]
    rw [s1] at H1 H2
    rw [s2] at H3 H4
    have c : ∀ s t : ℕ, s * (t * C) < n * (Nat.gcd (α * d1) (β * d2) * C) →
        s * t < n * Nat.gcd (α * d1) (β * d2) := by
      intro s t h
      rw [← Nat.mul_assoc, ← Nat.mul_assoc] at h; exact Nat.lt_of_mul_lt_mul_right h
    have c' : ∀ s t : ℕ, s * (t * C) < n * (Nat.gcd (β * d1) (α * d2) * C) →
        s * t < n * Nat.gcd (β * d1) (α * d2) := by
      intro s t h
      rw [← Nat.mul_assoc, ← Nat.mul_assoc] at h; exact Nat.lt_of_mul_lt_mul_right h
    obtain ⟨e1, e2⟩ := r4c_rect_core n k α β d1 d2 hk hα hβ α0 β0 hαβ hd d10 d20
      (c _ _ H1) (c _ _ H2) (c' _ _ H3) (c' _ _ H4)
    rw [e1, e2]

  -- 402-R4-c. THE CRITERION (Zaharescu's Proposition 1 in strict form): a prime p with
  -- n < p < 2n and (2n − p)² ≤ n forces a pair with n · gcd(a, b) ≤ a in every set of n positive integers.
  have r4c_criterion (A : Finset ℕ) (h0 : 0 ∉ A) (p : ℕ) (hp : p.Prime) (h1 : A.card < p)
      (h2 : p < 2 * A.card) (h3 : (2 * A.card - p) * (2 * A.card - p) ≤ A.card) :
      ∃ a ∈ A, ∃ b ∈ A, A.card * Nat.gcd a b ≤ a := by
    by_contra hne
    push Not at hne
    generalize hn : A.card = n at *
    have pos : ∀ a ∈ A, 0 < a := fun a ha =>
      Nat.pos_of_ne_zero (fun h => h0 (h ▸ ha))
    have podd : p % 2 = 1 := by
      rcases hp.eq_two_or_odd with h | h
      · omega
      · exact h
    -- pairs in one fold class
    have P : ∀ a ∈ A, ∀ b ∈ A, cls p a = cls p b →
        a = b ∨ ∃ x y g, x + y = p ∧ Nat.Coprime x y ∧ a = x * g ∧ b = y * g :=
      fun a ha b hb h => r4c_pair p n a b hp h1.le (pos a ha) (pos b hb) (hne a ha b hb)
        (by rw [Nat.gcd_comm]; exact hne b hb a ha) h
    have clsr : ∀ a ∈ A, cls p a ∈ Finset.Icc 1 ((p - 1) / 2) := by
      intro a ha
      have := Fact.mk hp
      have na : ((a / p ^ a.factorization p : ℕ) : ZMod p) ≠ 0 := by
        rw [Ne, ZMod.natCast_eq_zero_iff]; exact Nat.not_dvd_ordCompl hp (pos a ha).ne'
      have v1 := ZMod.val_lt ((a / p ^ a.factorization p : ℕ) : ZMod p)
      have v0 : 0 < ZMod.val ((a / p ^ a.factorization p : ℕ) : ZMod p) := (ZMod.val_pos).mpr na
      rw [hcls]
      rw [Finset.mem_Icc]
      omega
    classical
    -- the elements with a smaller partner in their class, and the rest
    have split := Finset.card_filter_add_card_filter_not (s := A)
      (fun a => ∃ a' ∈ A, a' < a ∧ cls p a' = cls p a)
    have c1 : (A.filter (fun a => ¬ ∃ a' ∈ A, a' < a ∧ cls p a' = cls p a)).card
        ≤ (Finset.Icc 1 ((p - 1) / 2)).card := by
      apply Finset.card_le_card_of_injOn (cls p)
      · intro a ha
        exact clsr a (Finset.mem_filter.mp (Finset.mem_coe.mp ha)).1
      · intro a ha b hb hab
        have ha' := Finset.mem_filter.mp (Finset.mem_coe.mp ha)
        have hb' := Finset.mem_filter.mp (Finset.mem_coe.mp hb)
        rcases Nat.lt_trichotomy a b with h | h | h
        · exact (hb'.2 ⟨a, ha'.1, h, hab⟩).elim
        · exact h
        · exact (ha'.2 ⟨b, hb'.1, h, hab.symm⟩).elim
    have hex : ∀ a, ∃ a' x y g, (∃ a' ∈ A, a' < a ∧ cls p a' = cls p a) → a ∈ A →
        (a' ∈ A ∧ a' < a ∧ x + y = p ∧ Nat.Coprime x y ∧ a = x * g ∧ a' = y * g) := by
      intro a
      by_cases h : (∃ a' ∈ A, a' < a ∧ cls p a' = cls p a) ∧ a ∈ A
      · obtain ⟨⟨a', ha', hlt, hc⟩, ha⟩ := h
        rcases P a ha a' ha' hc.symm with h | ⟨x, y, g, h⟩
        · omega
        · exact ⟨a', x, y, g, fun _ _ => ⟨ha', hlt, h⟩⟩
      · exact ⟨0, 0, 0, 0, fun h1 h2 => (h ⟨h1, h2⟩).elim⟩
    choose f X Y G hf using hex
    -- the rectangle step, with the four elements named
    have R : ∀ a a' b b' α β u w : ℕ, a ∈ A → a' ∈ A → b ∈ A → b' ∈ A → α + β = p →
        Nat.Coprime α β → a = α * u → a' = β * u → b = α * w → b' = β * w → u = w := by
      intro a a' b b' α β u w ha ha' hb hb' hs hco e1 e2 e3 e4
      have q1 := hne a ha b' hb'
      have q2 := hne b' hb' a ha
      have q3 := hne a' ha' b hb
      have q4 := hne b hb a' ha'
      rw [Nat.gcd_comm] at q2 q4
      have pa := pos a ha
      have pa' := pos a' ha'
      have pb := pos b hb
      have qa := hne a ha a' ha'
      have qa' := hne a' ha' a ha
      rw [Nat.gcd_comm] at qa'
      subst e1 e2 e3 e4
      have u0 : 0 < u := Nat.pos_of_mul_pos_left pa
      have w0 : 0 < w := Nat.pos_of_mul_pos_left pb
      have α0 : 0 < α := Nat.pos_of_mul_pos_right pa
      have β0 : 0 < β := Nat.pos_of_mul_pos_right pa'
      have gu : Nat.gcd (α * u) (β * u) = u := by
        rw [Nat.gcd_mul_right, hco, Nat.one_mul]
      rw [gu] at qa qa'
      have αn : α < n := Nat.lt_of_mul_lt_mul_right qa
      have βn : β < n := Nat.lt_of_mul_lt_mul_right qa'
      exact r4c_rect n (2 * n - p) α β u w h3 (by omega) (by omega) α0 β0 hco u0 w0 q1 q2 q3 q4
    have c2 : (A.filter (fun a => ∃ a' ∈ A, a' < a ∧ cls p a' = cls p a)).card
        ≤ (Finset.Icc ((p + 1) / 2) (n - 1)).card := by
      apply Finset.card_le_card_of_injOn (fun a => max (X a) (Y a))
      · intro a ha
        have ha' := Finset.mem_filter.mp (Finset.mem_coe.mp ha)
        obtain ⟨m1, m2, m3, m4, m5, m6⟩ := hf a ha'.2 ha'.1
        have qa := hne a ha'.1 (f a) m1
        have qa' := hne (f a) m1 a ha'.1
        rw [Nat.gcd_comm] at qa'
        have g0 : 0 < G a := Nat.pos_of_mul_pos_left (m5 ▸ pos a ha'.1)
        have gg : ∀ s t x y g : ℕ, s = x * g → t = y * g → Nat.Coprime x y → Nat.gcd s t = g := by
          intro s t x y g e1 e2 hc
          rw [e1, e2, Nat.gcd_mul_right, hc, Nat.one_mul]
        rw [gg a (f a) (X a) (Y a) (G a) m5 m6 m4] at qa qa'
        have xn : X a < n := by
          have : X a * G a < n * G a := lt_of_eq_of_lt m5.symm qa
          exact Nat.lt_of_mul_lt_mul_right this
        have yn : Y a < n := by
          have : Y a * G a < n * G a := lt_of_eq_of_lt m6.symm qa'
          exact Nat.lt_of_mul_lt_mul_right this
        simp only [Finset.coe_Icc, Set.mem_Icc]
        omega
      · intro a ha b hb hab
        have ha' := Finset.mem_filter.mp (Finset.mem_coe.mp ha)
        have hb' := Finset.mem_filter.mp (Finset.mem_coe.mp hb)
        obtain ⟨m1, m2, m3, m4, m5, m6⟩ := hf a ha'.2 ha'.1
        obtain ⟨k1, k2, k3, k4, k5, k6⟩ := hf b hb'.2 hb'.1
        simp only at hab
        have hcase : (X b = X a ∧ Y b = Y a) ∨ (X b = Y a ∧ Y b = X a) := by omega
        rcases hcase with ⟨hx, hy⟩ | ⟨hx, hy⟩
        · rw [hx] at k5; rw [hy] at k6
          have := R a (f a) b (f b) (X a) (Y a) (G a) (G b) ha'.1 m1 hb'.1 k1 m3 m4 m5 m6 k5 k6
          rw [m5, k5, this]
        · rw [hx] at k5; rw [hy] at k6
          have := R a (f a) (f b) b (X a) (Y a) (G a) (G b) ha'.1 m1 k1 hb'.1 m3 m4 m5 m6 k6 k5
          have e1 : a = f b := by rw [m5, k6, this]
          have e2 : f a = b := by rw [m6, k5, this]
          omega
    rw [Nat.card_Icc] at c1 c2
    omega
  intro B h0 hne hg hnp hq hle hpk
  left
  rcases hwin B h0 hne hg hnp hq hle hpk with h | ⟨p, hp, h1, h2, h3⟩
  · exact h
  · obtain ⟨a, ha, b, hb, h⟩ := r4c_criterion B h0 p hp h1 h2 h3
    refine ⟨a, ha, b, hb, ?_⟩
    have n0 : (0 : ℚ) < (B.card : ℚ) := by
      have : 0 < B.card := Finset.card_pos.mpr ⟨a, ha⟩
      exact_mod_cast this
    rw [le_div_iff₀ n0]
    have : a.gcd b * B.card ≤ a := by rw [Nat.mul_comm]; exact h
    exact_mod_cast this

The gate replayed this file at its merge, each hole a sorry (D-12 #5); the whole file: targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1/attempts/20261001T154750Z-t1001-402a-partial.lean

theorem erdos_402__h3_v2__h1__h1__h1 : ∀ (B : Finset ℕ),
  (0 : ℕ) ∉ B →
    B.Nonempty →
      B.gcd id = (1 : ℕ) →
        ¬Nat.Prime B.card →
          (∀ (q : ℕ), Nat.Prime q → B.card ≠ q + (1 : ℕ)) →
            (∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) →
              (∀ a ∈ B, ∀ (p k : ℕ), Nat.Prime p → p ^ k ∣ a → p ^ k < B.card) →
                (∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ)) ∨
                  ∃ (p : ℕ), Nat.Prime p ∧ B.card ≤ (3 : ℕ) * p ∧ ∃ a ∈ B, p ∣ a := by
  -- Second route on this node (the first is the merged window-criterion partial with hole `hwin`). Agent 402-R6-a;
  -- Lean of the assembly by agent 402-R5-b (same pseudonym's sitting; generalised from 402-R4-c's criterion), re-verified.
  -- Hole `hgen`: under this node's hypotheses, B has a pair with gcd(a, b) ≤ a / n, or there is a prime p with
  -- n < p < 2n, 2(2n − p) ≤ n + 2, such that every α with p − n < α < n either has a prime q ≥ n/3 dividing α(p − α)
  -- or has no divisors x < y with x·y ∣ α and α·y < n·x (n = |B|). The assembly proves that such a prime forces a
  -- pair or a prime ≥ n/3 dividing an element. Unlike `hwin`, such a prime exists for EVERY n from 2 to 200014.
  have hgen : ∀ (B : Finset ℕ),
    (0 : ℕ) ∉ B →
      B.Nonempty →
        B.gcd id = (1 : ℕ) →
          ¬Nat.Prime B.card →
            (∀ (q : ℕ), Nat.Prime q → B.card ≠ q + (1 : ℕ)) →
              (∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) →
                (∀ a ∈ B, ∀ (p k : ℕ), Nat.Prime p → p ^ k ∣ a → p ^ k < B.card) →
                  (∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ)) ∨
                    ∃ (p : ℕ), Nat.Prime p ∧ B.card < p ∧ p < 2 * B.card ∧ 2 * (2 * B.card - p) ≤ B.card + 2 ∧
                    ∀ α : ℕ, α < B.card → p < α + B.card →
                      (∃ q : ℕ, Nat.Prime q ∧ B.card ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
                      (∀ x y : ℕ, x < y → x * y ∣ α → B.card * x ≤ α * y) := by
    sorry
  have r5b_gen_criterion : ∀ (A : Finset ℕ), 0 ∉ A → ∀ p : ℕ, p.Prime → A.card < p →
      p < 2 * A.card → 2 * (2 * A.card - p) ≤ A.card + 2 →
      (∀ α : ℕ, α < A.card → p < α + A.card →
        (∃ q : ℕ, q.Prime ∧ A.card ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
        (∀ x y : ℕ, x < y → x * y ∣ α → A.card * x ≤ α * y)) →
      (∃ a ∈ A, ∃ b ∈ A, (a.gcd b : ℚ) ≤ (a : ℚ) / (A.card : ℚ)) ∨
        ∃ q : ℕ, q.Prime ∧ A.card ≤ 3 * q ∧ ∃ a ∈ A, q ∣ a := by
    obtain ⟨cls, hcls⟩ : ∃ cls : ℕ → ℕ → ℕ, ∀ p a, cls p a =
        min (ZMod.val ((a / p ^ a.factorization p : ℕ) : ZMod p))
          (p - ZMod.val ((a / p ^ a.factorization p : ℕ) : ZMod p)) := ⟨_, fun _ _ => rfl⟩

    -- 402-R5-b. Arithmetic heart, generalised: the divisor-gap hypothesis on α is exactly what is needed.
    have r4c_arith (n α e1 e2 : ℕ) (hg : ∀ x y : ℕ, x < y → x * y ∣ α → n * x ≤ α * y)
        (he : e1 * e2 ∣ α) (h1 : α * e1 < n * e2) (h4 : α * e2 < n * e1) : e1 = e2 := by
      rcases Nat.lt_trichotomy e1 e2 with h | h | h
      · have := hg e1 e2 h he
        omega
      · exact h
      · have := hg e2 e1 h (by rwa [Nat.mul_comm])
        omega

    -- 402-R4-c. Rectangle lemma, coprime core: α, β coprime and both within k of n (k² ≤ n), d1, d2
    -- coprime; if all four cross quotients of {α d1, β d1, α d2, β d2} are below n then d1 = d2 = 1.
    have r4c_rect_core (n α β d1 d2 : ℕ) (gα : (∀ x y : ℕ, x < y → x * y ∣ α → n * x ≤ α * y)) (gβ : (∀ x y : ℕ, x < y → x * y ∣ β → n * x ≤ β * y))
        (tα : n ≤ 2 * α)
        (α0 : 0 < α) (β0 : 0 < β) (hαβ : Nat.Coprime α β) (hd : Nat.Coprime d1 d2)
        (h1 : 0 < d1) (h2 : 0 < d2)
        (H1 : α * d1 < n * Nat.gcd (α * d1) (β * d2)) (H2 : β * d2 < n * Nat.gcd (α * d1) (β * d2))
        (H3 : β * d1 < n * Nat.gcd (β * d1) (α * d2)) (H4 : α * d2 < n * Nat.gcd (β * d1) (α * d2)) :
        d1 = 1 ∧ d2 = 1 := by
      have e1p : 0 < Nat.gcd α d1 := Nat.gcd_pos_of_pos_left _ α0
      have e2p : 0 < Nat.gcd α d2 := Nat.gcd_pos_of_pos_left _ α0
      have f1p : 0 < Nat.gcd β d1 := Nat.gcd_pos_of_pos_left _ β0
      have f2p : 0 < Nat.gcd β d2 := Nat.gcd_pos_of_pos_left _ β0
      have hG : Nat.gcd (α * d1) (β * d2) ≤ Nat.gcd α d2 * Nat.gcd β d1 := by
        apply Nat.le_of_dvd (Nat.mul_pos e2p f1p)
        have h := Nat.gcd_mul_right_dvd_mul_gcd (α * d1) β d2
        rw [Nat.Coprime.gcd_mul_left_cancel d1 hαβ, Nat.Coprime.gcd_mul_right_cancel α hd] at h
        rw [Nat.gcd_comm d1 β, Nat.mul_comm (β.gcd d1)] at h; exact h
      have hG' : Nat.gcd (β * d1) (α * d2) ≤ Nat.gcd α d1 * Nat.gcd β d2 := by
        apply Nat.le_of_dvd (Nat.mul_pos e1p f2p)
        have h := Nat.gcd_mul_right_dvd_mul_gcd (β * d1) α d2
        rw [Nat.Coprime.gcd_mul_left_cancel d1 hαβ.symm, Nat.Coprime.gcd_mul_right_cancel β hd] at h
        rw [Nat.gcd_comm d1 α] at h; exact h
      have ce : Nat.Coprime (Nat.gcd α d1) (Nat.gcd α d2) :=
        Nat.Coprime.coprime_dvd_left (Nat.gcd_dvd_right _ _)
          (Nat.Coprime.coprime_dvd_right (Nat.gcd_dvd_right _ _) hd)
      have cf : Nat.Coprime (Nat.gcd β d1) (Nat.gcd β d2) :=
        Nat.Coprime.coprime_dvd_left (Nat.gcd_dvd_right _ _)
          (Nat.Coprime.coprime_dvd_right (Nat.gcd_dvd_right _ _) hd)
      have c1 : Nat.Coprime (Nat.gcd α d1) (Nat.gcd β d1) :=
        Nat.Coprime.coprime_dvd_left (Nat.gcd_dvd_left _ _)
          (Nat.Coprime.coprime_dvd_right (Nat.gcd_dvd_left _ _) hαβ)
      have c2 : Nat.Coprime (Nat.gcd α d2) (Nat.gcd β d2) :=
        Nat.Coprime.coprime_dvd_left (Nat.gcd_dvd_left _ _)
          (Nat.Coprime.coprime_dvd_right (Nat.gcd_dvd_left _ _) hαβ)
      have m1 : Nat.gcd α d1 * Nat.gcd β d1 ≤ d1 := Nat.le_of_dvd h1
        (Nat.Coprime.mul_dvd_of_dvd_of_dvd c1 (Nat.gcd_dvd_right _ _) (Nat.gcd_dvd_right _ _))
      have m2 : Nat.gcd α d2 * Nat.gcd β d2 ≤ d2 := Nat.le_of_dvd h2
        (Nat.Coprime.mul_dvd_of_dvd_of_dvd c2 (Nat.gcd_dvd_right _ _) (Nat.gcd_dvd_right _ _))
      have mα : Nat.gcd α d1 * Nat.gcd α d2 ∣ α :=
        Nat.Coprime.mul_dvd_of_dvd_of_dvd ce (Nat.gcd_dvd_left _ _) (Nat.gcd_dvd_left _ _)
      have mβ : Nat.gcd β d1 * Nat.gcd β d2 ∣ β :=
        Nat.Coprime.mul_dvd_of_dvd_of_dvd cf (Nat.gcd_dvd_left _ _) (Nat.gcd_dvd_left _ _)
      generalize Nat.gcd α d1 = e1 at *
      generalize Nat.gcd α d2 = e2 at *
      generalize Nat.gcd β d1 = f1 at *
      generalize Nat.gcd β d2 = f2 at *
      generalize Nat.gcd (α * d1) (β * d2) = G at *
      generalize Nat.gcd (β * d1) (α * d2) = G' at *
      have i1 : α * e1 < n * e2 := by
        have a : α * (e1 * f1) ≤ α * d1 := Nat.mul_le_mul_left _ m1
        have b : n * G ≤ n * (e2 * f1) := Nat.mul_le_mul_left _ hG
        have c : (α * e1) * f1 < (n * e2) * f1 := by
          calc (α * e1) * f1 = α * (e1 * f1) := by ring
            _ ≤ α * d1 := a
            _ < n * G := H1
            _ ≤ n * (e2 * f1) := b
            _ = (n * e2) * f1 := by ring
        exact Nat.lt_of_mul_lt_mul_right c
      have i4 : α * e2 < n * e1 := by
        have a : α * (e2 * f2) ≤ α * d2 := Nat.mul_le_mul_left _ m2
        have b : n * G' ≤ n * (e1 * f2) := Nat.mul_le_mul_left _ hG'
        have c : (α * e2) * f2 < (n * e1) * f2 := by
          calc (α * e2) * f2 = α * (e2 * f2) := by ring
            _ ≤ α * d2 := a
            _ < n * G' := H4
            _ ≤ n * (e1 * f2) := b
            _ = (n * e1) * f2 := by ring
        exact Nat.lt_of_mul_lt_mul_right c
      have i2 : β * f2 < n * f1 := by
        have a : β * (e2 * f2) ≤ β * d2 := Nat.mul_le_mul_left _ m2
        have b : n * G ≤ n * (e2 * f1) := Nat.mul_le_mul_left _ hG
        have c : (β * f2) * e2 < (n * f1) * e2 := by
          calc (β * f2) * e2 = β * (e2 * f2) := by ring
            _ ≤ β * d2 := a
            _ < n * G := H2
            _ ≤ n * (e2 * f1) := b
            _ = (n * f1) * e2 := by ring
        exact Nat.lt_of_mul_lt_mul_right c
      have i3 : β * f1 < n * f2 := by
        have a : β * (e1 * f1) ≤ β * d1 := Nat.mul_le_mul_left _ m1
        have b : n * G' ≤ n * (e1 * f2) := Nat.mul_le_mul_left _ hG'
        have c : (β * f1) * e1 < (n * f2) * e1 := by
          calc (β * f1) * e1 = β * (e1 * f1) := by ring
            _ ≤ β * d1 := a
            _ < n * G' := H3
            _ ≤ n * (e1 * f2) := b
            _ = (n * f2) * e1 := by ring
        exact Nat.lt_of_mul_lt_mul_right c
      have ee : e1 = e2 := r4c_arith n α e1 e2 gα mα i1 i4
      have ff : f1 = f2 := r4c_arith n β f1 f2 gβ mβ i3 i2
      subst ee; subst ff
      have e1 : e1 = 1 := Nat.coprime_self e1 |>.mp ce
      have f1 : f1 = 1 := Nat.coprime_self f1 |>.mp cf
      subst e1; subst f1
      have g1 : n * G ≤ n := by simpa using Nat.mul_le_mul_left n hG
      have g2 : n * G' ≤ n := by simpa using Nat.mul_le_mul_left n hG'
      constructor
      · by_contra hc
        have : α * 2 ≤ α * d1 := Nat.mul_le_mul_left _ (by omega)
        omega
      · by_contra hc
        have : α * 2 ≤ α * d2 := Nat.mul_le_mul_left _ (by omega)
        omega


    -- 402-R4-c. Collision lemma for one pair: both quotients below n ≤ p and equal fold classes
    -- force a = b or reduced quotients adding up to p.
    have r4c_pair (p n a b : ℕ) (hp : p.Prime) (hnp : n ≤ p) (a0 : 0 < a) (b0 : 0 < b)
        (ha : a < n * Nat.gcd a b) (hb : b < n * Nat.gcd a b) (hc : cls p a = cls p b) :
        a = b ∨ ∃ x y g, x + y = p ∧ Nat.Coprime x y ∧ a = x * g ∧ b = y * g := by
      have := Fact.mk hp
      obtain ⟨x, y, hxy, hax, hby⟩ := Nat.exists_coprime a b
      have g0 : 0 < Nat.gcd a b := Nat.gcd_pos_of_pos_left _ a0
      generalize Nat.gcd a b = g at *
      have xn : x < n := by
        rw [hax] at ha; exact Nat.lt_of_mul_lt_mul_right ha
      have yn : y < n := by
        rw [hby] at hb; exact Nat.lt_of_mul_lt_mul_right hb
      have x0 : 0 < x := by
        rcases Nat.eq_zero_or_pos x with h | h
        · subst h; omega
        · exact h
      have y0 : 0 < y := by
        rcases Nat.eq_zero_or_pos y with h | h
        · subst h; omega
        · exact h
      have key : a * y = b * x := by rw [hax, hby]; ring
      have oc : ∀ z : ℕ, 0 < z → z < p → z / p ^ z.factorization p = z := by
        intro z hz hzp
        have : ¬ p ∣ z := fun h => by have := Nat.le_of_dvd hz h; omega
        rw [Nat.factorization_eq_zero_of_not_dvd this]; simp
      have key2 : (a / p ^ a.factorization p) * y = (b / p ^ b.factorization p) * x := by
        have h := congrArg (fun m => m / p ^ m.factorization p) key
        simp only [Nat.ordCompl_mul] at h
        rwa [oc y y0 (by omega), oc x x0 (by omega)] at h
      have na : ((a / p ^ a.factorization p : ℕ) : ZMod p) ≠ 0 := by
        rw [Ne, ZMod.natCast_eq_zero_iff]; exact Nat.not_dvd_ordCompl hp (by omega)
      have nb : ((b / p ^ b.factorization p : ℕ) : ZMod p) ≠ 0 := by
        rw [Ne, ZMod.natCast_eq_zero_iff]; exact Nat.not_dvd_ordCompl hp (by omega)
      have key3 : ((a / p ^ a.factorization p : ℕ) : ZMod p) * (y : ZMod p)
          = ((b / p ^ b.factorization p : ℕ) : ZMod p) * (x : ZMod p) := by
        exact_mod_cast congrArg (Nat.cast : ℕ → ZMod p) key2
      rw [hcls, hcls] at hc
      generalize ((a / p ^ a.factorization p : ℕ) : ZMod p) = ra at *
      generalize ((b / p ^ b.factorization p : ℕ) : ZMod p) = rb at *
      have va := ZMod.val_lt ra
      have vb := ZMod.val_lt rb
      have va0 : 0 < ra.val := (ZMod.val_pos).mpr na
      have vb0 : 0 < rb.val := (ZMod.val_pos).mpr nb
      have hcase : ra.val = rb.val ∨ ra.val + rb.val = p := by omega
      rcases hcase with h | h
      · left
        have hr : ra = rb := ZMod.val_injective p h
        rw [hr] at key3
        have h2 : (y : ZMod p) = (x : ZMod p) := mul_left_cancel₀ nb key3
        have h3 := (ZMod.natCast_eq_natCast_iff' y x p).mp h2
        rw [Nat.mod_eq_of_lt (by omega), Nat.mod_eq_of_lt (by omega)] at h3
        rw [hax, hby, h3]
      · right
        have hr : ra + rb = 0 := by
          have h4 : ((ra.val + rb.val : ℕ) : ZMod p) = ((p : ℕ) : ZMod p) := by rw [h]
          rw [Nat.cast_add, ZMod.natCast_zmod_val, ZMod.natCast_zmod_val, ZMod.natCast_self] at h4
          exact h4
        have hra : ra = -rb := eq_neg_of_add_eq_zero_left hr
        rw [hra] at key3
        have h5 : rb * ((x : ZMod p) + (y : ZMod p)) = 0 := by
          have : rb * ((x : ZMod p) + (y : ZMod p)) = rb * x - (-rb * y) := by ring
          rw [this, key3]; ring
        have h6 : ((x + y : ℕ) : ZMod p) = 0 := by
          rcases mul_eq_zero.mp h5 with h | h
          · exact (nb h).elim
          · exact_mod_cast h
        rw [ZMod.natCast_eq_zero_iff] at h6
        exact ⟨x, y, g, Nat.eq_of_dvd_of_lt_two_mul (by omega) h6 (by omega), hxy, hax, hby⟩


    -- 402-R4-c. Rectangle lemma: α u, β u, α w, β w with all four cross quotients below n force u = w.
    have r4c_rect (n α β u w : ℕ) (gα : (∀ x y : ℕ, x < y → x * y ∣ α → n * x ≤ α * y)) (gβ : (∀ x y : ℕ, x < y → x * y ∣ β → n * x ≤ β * y))
        (tα : n ≤ 2 * α)
        (α0 : 0 < α) (β0 : 0 < β) (hαβ : Nat.Coprime α β) (u0 : 0 < u) (w0 : 0 < w)
        (H1 : α * u < n * Nat.gcd (α * u) (β * w)) (H2 : β * w < n * Nat.gcd (α * u) (β * w))
        (H3 : β * u < n * Nat.gcd (β * u) (α * w)) (H4 : α * w < n * Nat.gcd (β * u) (α * w)) :
        u = w := by
      obtain ⟨d1, d2, hd, hu, hw⟩ := Nat.exists_coprime u w
      have C0 : 0 < Nat.gcd u w := Nat.gcd_pos_of_pos_left _ u0
      generalize Nat.gcd u w = C at *
      subst hu; subst hw
      have d10 : 0 < d1 := Nat.pos_of_mul_pos_right u0
      have d20 : 0 < d2 := Nat.pos_of_mul_pos_right w0
      have s1 : Nat.gcd (α * (d1 * C)) (β * (d2 * C)) = Nat.gcd (α * d1) (β * d2) * C := by
        rw [← Nat.mul_assoc, ← Nat.mul_assoc, Nat.gcd_mul_right]
      have s2 : Nat.gcd (β * (d1 * C)) (α * (d2 * C)) = Nat.gcd (β * d1) (α * d2) * C := by
        rw [← Nat.mul_assoc, ← Nat.mul_assoc, Nat.gcd_mul_right]
      rw [s1] at H1 H2
      rw [s2] at H3 H4
      have c : ∀ s t : ℕ, s * (t * C) < n * (Nat.gcd (α * d1) (β * d2) * C) →
          s * t < n * Nat.gcd (α * d1) (β * d2) := by
        intro s t h
        rw [← Nat.mul_assoc, ← Nat.mul_assoc] at h; exact Nat.lt_of_mul_lt_mul_right h
      have c' : ∀ s t : ℕ, s * (t * C) < n * (Nat.gcd (β * d1) (α * d2) * C) →
          s * t < n * Nat.gcd (β * d1) (α * d2) := by
        intro s t h
        rw [← Nat.mul_assoc, ← Nat.mul_assoc] at h; exact Nat.lt_of_mul_lt_mul_right h
      obtain ⟨e1, e2⟩ := r4c_rect_core n α β d1 d2 gα gβ tα α0 β0 hαβ hd d10 d20
        (c _ _ H1) (c _ _ H2) (c' _ _ H3) (c' _ _ H4)
      rw [e1, e2]

    -- 402-R5-b (from 402-R4-c). THE GENERALISED CRITERION: a prime p with
    -- n < p < 2n and (2n − p)² ≤ n forces a pair with n · gcd(a, b) ≤ a in every set of n positive integers.
    have r4c_criterion (A : Finset ℕ) (h0 : 0 ∉ A) (p : ℕ) (hp : p.Prime) (h1 : A.card < p)
        (h2 : p < 2 * A.card) (h3 : 2 * (2 * A.card - p) ≤ A.card + 2)
        (H : ∀ α : ℕ, α < A.card → p < α + A.card →
          (∃ q : ℕ, q.Prime ∧ A.card ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
          (∀ x y : ℕ, x < y → x * y ∣ α → A.card * x ≤ α * y)) :
        (∃ a ∈ A, ∃ b ∈ A, A.card * Nat.gcd a b ≤ a) ∨
          ∃ q : ℕ, q.Prime ∧ A.card ≤ 3 * q ∧ ∃ a ∈ A, q ∣ a := by
      by_contra hcon
      have hne : ∀ a ∈ A, ∀ b ∈ A, a < A.card * Nat.gcd a b := by
        intro a ha b hb
        by_contra h
        exact hcon (Or.inl ⟨a, ha, b, hb, by omega⟩)
      have hnq : ∀ q : ℕ, q.Prime → A.card ≤ 3 * q → ∀ a ∈ A, ¬ q ∣ a :=
        fun q hq h a ha hd => hcon (Or.inr ⟨q, hq, h, a, ha, hd⟩)
      clear hcon
      generalize hn : A.card = n at *
      have pos : ∀ a ∈ A, 0 < a := fun a ha =>
        Nat.pos_of_ne_zero (fun h => h0 (h ▸ ha))
      have podd : p % 2 = 1 := by
        rcases hp.eq_two_or_odd with h | h
        · omega
        · exact h
      -- pairs in one fold class
      have P : ∀ a ∈ A, ∀ b ∈ A, cls p a = cls p b →
          a = b ∨ ∃ x y g, x + y = p ∧ Nat.Coprime x y ∧ a = x * g ∧ b = y * g :=
        fun a ha b hb h => r4c_pair p n a b hp h1.le (pos a ha) (pos b hb) (hne a ha b hb)
          (by rw [Nat.gcd_comm]; exact hne b hb a ha) h
      have clsr : ∀ a ∈ A, cls p a ∈ Finset.Icc 1 ((p - 1) / 2) := by
        intro a ha
        have := Fact.mk hp
        have na : ((a / p ^ a.factorization p : ℕ) : ZMod p) ≠ 0 := by
          rw [Ne, ZMod.natCast_eq_zero_iff]; exact Nat.not_dvd_ordCompl hp (pos a ha).ne'
        have v1 := ZMod.val_lt ((a / p ^ a.factorization p : ℕ) : ZMod p)
        have v0 : 0 < ZMod.val ((a / p ^ a.factorization p : ℕ) : ZMod p) := (ZMod.val_pos).mpr na
        rw [hcls]
        rw [Finset.mem_Icc]
        omega
      classical
      -- the elements with a smaller partner in their class, and the rest
      have split := Finset.card_filter_add_card_filter_not (s := A)
        (fun a => ∃ a' ∈ A, a' < a ∧ cls p a' = cls p a)
      have c1 : (A.filter (fun a => ¬ ∃ a' ∈ A, a' < a ∧ cls p a' = cls p a)).card
          ≤ (Finset.Icc 1 ((p - 1) / 2)).card := by
        apply Finset.card_le_card_of_injOn (cls p)
        · intro a ha
          exact clsr a (Finset.mem_filter.mp (Finset.mem_coe.mp ha)).1
        · intro a ha b hb hab
          have ha' := Finset.mem_filter.mp (Finset.mem_coe.mp ha)
          have hb' := Finset.mem_filter.mp (Finset.mem_coe.mp hb)
          rcases Nat.lt_trichotomy a b with h | h | h
          · exact (hb'.2 ⟨a, ha'.1, h, hab⟩).elim
          · exact h
          · exact (ha'.2 ⟨b, hb'.1, h, hab.symm⟩).elim
      have hex : ∀ a, ∃ a' x y g, (∃ a' ∈ A, a' < a ∧ cls p a' = cls p a) → a ∈ A →
          (a' ∈ A ∧ a' < a ∧ x + y = p ∧ Nat.Coprime x y ∧ a = x * g ∧ a' = y * g) := by
        intro a
        by_cases h : (∃ a' ∈ A, a' < a ∧ cls p a' = cls p a) ∧ a ∈ A
        · obtain ⟨⟨a', ha', hlt, hc⟩, ha⟩ := h
          rcases P a ha a' ha' hc.symm with h | ⟨x, y, g, h⟩
          · omega
          · exact ⟨a', x, y, g, fun _ _ => ⟨ha', hlt, h⟩⟩
        · exact ⟨0, 0, 0, 0, fun h1 h2 => (h ⟨h1, h2⟩).elim⟩
      choose f X Y G hf using hex
      -- the rectangle step, with the four elements named
      have R : ∀ a a' b b' α β u w : ℕ, a ∈ A → a' ∈ A → b ∈ A → b' ∈ A → α + β = p →
          Nat.Coprime α β → a = α * u → a' = β * u → b = α * w → b' = β * w → u = w := by
        intro a a' b b' α β u w ha ha' hb hb' hs hco e1 e2 e3 e4
        have q1 := hne a ha b' hb'
        have q2 := hne b' hb' a ha
        have q3 := hne a' ha' b hb
        have q4 := hne b hb a' ha'
        rw [Nat.gcd_comm] at q2 q4
        have pa := pos a ha
        have pa' := pos a' ha'
        have pb := pos b hb
        have qa := hne a ha a' ha'
        have qa' := hne a' ha' a ha
        rw [Nat.gcd_comm] at qa'
        subst e1 e2 e3 e4
        have u0 : 0 < u := Nat.pos_of_mul_pos_left pa
        have w0 : 0 < w := Nat.pos_of_mul_pos_left pb
        have α0 : 0 < α := Nat.pos_of_mul_pos_right pa
        have β0 : 0 < β := Nat.pos_of_mul_pos_right pa'
        have gu : Nat.gcd (α * u) (β * u) = u := by
          rw [Nat.gcd_mul_right, hco, Nat.one_mul]
        rw [gu] at qa qa'
        have αn : α < n := Nat.lt_of_mul_lt_mul_right qa
        have βn : β < n := Nat.lt_of_mul_lt_mul_right qa'
        have tα : n ≤ 2 * α := by omega
        have Hα := H α αn (by omega)
        have Hβ := H β βn (by omega)
        have pα : p - α = β := by omega
        have pβ : p - β = α := by omega
        rw [pα] at Hα
        rw [pβ] at Hβ
        have excl : ∀ q : ℕ, q.Prime → n ≤ 3 * q → q ∣ α * β → False := by
          intro q hq hq3 hd
          rcases (Nat.Prime.dvd_mul hq).mp hd with h | h
          · exact hnq q hq hq3 (α * u) ha (Dvd.dvd.mul_right h u)
          · exact hnq q hq hq3 (β * u) ha' (Dvd.dvd.mul_right h u)
        have gα : ∀ x y : ℕ, x < y → x * y ∣ α → n * x ≤ α * y := by
          rcases Hα with ⟨q, hq, h3q, hd⟩ | h
          · exact (excl q hq h3q hd).elim
          · exact h
        have gβ : ∀ x y : ℕ, x < y → x * y ∣ β → n * x ≤ β * y := by
          rcases Hβ with ⟨q, hq, h3q, hd⟩ | h
          · exact (excl q hq h3q (by rwa [Nat.mul_comm])).elim
          · exact h
        exact r4c_rect n α β u w gα gβ tα α0 β0 hco u0 w0 q1 q2 q3 q4
      have c2 : (A.filter (fun a => ∃ a' ∈ A, a' < a ∧ cls p a' = cls p a)).card
          ≤ (Finset.Icc ((p + 1) / 2) (n - 1)).card := by
        apply Finset.card_le_card_of_injOn (fun a => max (X a) (Y a))
        · intro a ha
          have ha' := Finset.mem_filter.mp (Finset.mem_coe.mp ha)
          obtain ⟨m1, m2, m3, m4, m5, m6⟩ := hf a ha'.2 ha'.1
          have qa := hne a ha'.1 (f a) m1
          have qa' := hne (f a) m1 a ha'.1
          rw [Nat.gcd_comm] at qa'
          have g0 : 0 < G a := Nat.pos_of_mul_pos_left (m5 ▸ pos a ha'.1)
          have gg : ∀ s t x y g : ℕ, s = x * g → t = y * g → Nat.Coprime x y → Nat.gcd s t = g := by
            intro s t x y g e1 e2 hc
            rw [e1, e2, Nat.gcd_mul_right, hc, Nat.one_mul]
          rw [gg a (f a) (X a) (Y a) (G a) m5 m6 m4] at qa qa'
          have xn : X a < n := by
            have : X a * G a < n * G a := lt_of_eq_of_lt m5.symm qa
            exact Nat.lt_of_mul_lt_mul_right this
          have yn : Y a < n := by
            have : Y a * G a < n * G a := lt_of_eq_of_lt m6.symm qa'
            exact Nat.lt_of_mul_lt_mul_right this
          simp only [Finset.coe_Icc, Set.mem_Icc]
          omega
        · intro a ha b hb hab
          have ha' := Finset.mem_filter.mp (Finset.mem_coe.mp ha)
          have hb' := Finset.mem_filter.mp (Finset.mem_coe.mp hb)
          obtain ⟨m1, m2, m3, m4, m5, m6⟩ := hf a ha'.2 ha'.1
          obtain ⟨k1, k2, k3, k4, k5, k6⟩ := hf b hb'.2 hb'.1
          simp only at hab
          have hcase : (X b = X a ∧ Y b = Y a) ∨ (X b = Y a ∧ Y b = X a) := by omega
          rcases hcase with ⟨hx, hy⟩ | ⟨hx, hy⟩
          · rw [hx] at k5; rw [hy] at k6
            have := R a (f a) b (f b) (X a) (Y a) (G a) (G b) ha'.1 m1 hb'.1 k1 m3 m4 m5 m6 k5 k6
            rw [m5, k5, this]
          · rw [hx] at k5; rw [hy] at k6
            have := R a (f a) (f b) b (X a) (Y a) (G a) (G b) ha'.1 m1 k1 hb'.1 m3 m4 m5 m6 k6 k5
            have e1 : a = f b := by rw [m5, k6, this]
            have e2 : f a = b := by rw [m6, k5, this]
            omega
      rw [Nat.card_Icc] at c1 c2
      omega
    intro A h0 p hp h1 h2 h3 H
    rcases r4c_criterion A h0 p hp h1 h2 h3 H with ⟨a, ha, b, hb, h⟩ | h
    · left
      refine ⟨a, ha, b, hb, ?_⟩
      have n0 : (0 : ℚ) < (A.card : ℚ) := by
        have : 0 < A.card := Finset.card_pos.mpr ⟨a, ha⟩
        exact_mod_cast this
      rw [le_div_iff₀ n0]
      have : a.gcd b * A.card ≤ a := by rw [Nat.mul_comm]; exact h
      exact_mod_cast this
    · exact Or.inr h
  intro B h0 hne hg hnp hnq hle hpp
  rcases hgen B h0 hne hg hnp hnq hle hpp with h | ⟨p, hp, h1, h2, h3, H⟩
  · exact Or.inl h
  · exact r5b_gen_criterion B h0 p hp h1 h2 h3 H

The gate replayed this file at its merge, each hole a sorry (D-12 #5); the whole file: targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1/attempts/20261001T163302Z-t1001-402a-partial.lean

theorem erdos_402__h3_v2__h1__h1__h1__h2 : ∀ (B : Finset ℕ),
  (0 : ℕ) ∉ B →
    B.Nonempty →
      B.gcd id = (1 : ℕ) →
        ¬Nat.Prime B.card →
          (∀ (q : ℕ), Nat.Prime q → B.card ≠ q + (1 : ℕ)) →
            (∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) →
              (∀ a ∈ B, ∀ (p k : ℕ), Nat.Prime p → p ^ k ∣ a → p ^ k < B.card) →
                (∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ)) ∨
                  ∃ (p : ℕ),
                    Nat.Prime p ∧
                      B.card < p ∧
                        p < (2 : ℕ) * B.card ∧
                          (2 : ℕ) * ((2 : ℕ) * B.card - p) ≤ B.card + (2 : ℕ) ∧
                            ∀ α < B.card,
                              p < α + B.card →
                                (∃ (q : ℕ), Nat.Prime q ∧ B.card ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨
                                  ∀ (x y : ℕ), x < y → x * y ∣ α → B.card * x ≤ α * y := by
  -- Split of `hgen` by size n = |B| (agent 402-R6-a; statements prepared with agents 402-R5-b and 402-R6-b). Three holes,
  -- each in its own goal so none inherits another:
  -- `hs1` (10 ≤ n ≤ 228) and `hs2` (229 ≤ n ≤ 200014): a prime with the generalised window hypotheses exists. Finite
  -- certificates; both have complete Lean proofs ready.
  -- `hlarge` (n > 200014): the node's own conclusion for large sets. This is NOT a finite check and not a small lemma: it
  -- needs, for every large n, a prime within about √n below 2n, which no unconditional theorem gives; see the annex on it.
  -- The assembly proves the sizes below 10 and the case split.
  have hall : (∀ n : ℕ, 10 ≤ n → n ≤ 228 →
          ∃ p : ℕ, p.Prime ∧ n < p ∧ p < 2 * n ∧ 2 * (2 * n - p) ≤ n + 2 ∧
            ∀ α : ℕ, α < n → p < α + n →
              (∃ q : ℕ, q.Prime ∧ n ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
              (∀ x y : ℕ, x < y → x * y ∣ α → n * x ≤ α * y))
      ∧ (∀ n : ℕ, 229 ≤ n → n ≤ 200014 →
          ∃ p : ℕ, p.Prime ∧ n < p ∧ p < 2 * n ∧ 2 * (2 * n - p) ≤ n + 2 ∧
            ∀ α : ℕ, α < n → p < α + n →
              (∃ q : ℕ, q.Prime ∧ n ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
              (∀ x y : ℕ, x < y → x * y ∣ α → n * x ≤ α * y))
      ∧ (∀ (B : Finset ℕ),
    (0 : ℕ) ∉ B →
      B.Nonempty →
        B.gcd id = (1 : ℕ) →
          ¬Nat.Prime B.card →
            (∀ (q : ℕ), Nat.Prime q → B.card ≠ q + (1 : ℕ)) →
              (∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) →
                (∀ a ∈ B, ∀ (p k : ℕ), Nat.Prime p → p ^ k ∣ a → p ^ k < B.card) →
                  200014 < B.card →
                    (∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ)) ∨
                    ∃ p : ℕ, p.Prime ∧ B.card < p ∧ p < 2 * B.card ∧ 2 * (2 * B.card - p) ≤ B.card + 2 ∧
                      ∀ α : ℕ, α < B.card → p < α + B.card →
                        (∃ q : ℕ, q.Prime ∧ B.card ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
                        (∀ x y : ℕ, x < y → x * y ∣ α → B.card * x ≤ α * y)) := by
    refine ⟨?_, ?_, ?_⟩
    · have hs1 : ∀ n : ℕ, 10 ≤ n → n ≤ 228 →
          ∃ p : ℕ, p.Prime ∧ n < p ∧ p < 2 * n ∧ 2 * (2 * n - p) ≤ n + 2 ∧
            ∀ α : ℕ, α < n → p < α + n →
              (∃ q : ℕ, q.Prime ∧ n ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
              (∀ x y : ℕ, x < y → x * y ∣ α → n * x ≤ α * y) := by
        sorry
      exact hs1
    · have hs2 : ∀ n : ℕ, 229 ≤ n → n ≤ 200014 →
          ∃ p : ℕ, p.Prime ∧ n < p ∧ p < 2 * n ∧ 2 * (2 * n - p) ≤ n + 2 ∧
            ∀ α : ℕ, α < n → p < α + n →
              (∃ q : ℕ, q.Prime ∧ n ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
              (∀ x y : ℕ, x < y → x * y ∣ α → n * x ≤ α * y) := by
        sorry
      exact hs2
    · have hlarge : ∀ (B : Finset ℕ),
    (0 : ℕ) ∉ B →
      B.Nonempty →
        B.gcd id = (1 : ℕ) →
          ¬Nat.Prime B.card →
            (∀ (q : ℕ), Nat.Prime q → B.card ≠ q + (1 : ℕ)) →
              (∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) →
                (∀ a ∈ B, ∀ (p k : ℕ), Nat.Prime p → p ^ k ∣ a → p ^ k < B.card) →
                  200014 < B.card →
                    (∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ)) ∨
                    ∃ p : ℕ, p.Prime ∧ B.card < p ∧ p < 2 * B.card ∧ 2 * (2 * B.card - p) ≤ B.card + 2 ∧
                      ∀ α : ℕ, α < B.card → p < α + B.card →
                        (∃ q : ℕ, q.Prime ∧ B.card ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
                        (∀ x y : ℕ, x < y → x * y ∣ α → B.card * x ≤ α * y) := by
        sorry
      exact hlarge
  obtain ⟨hs1, hs2, hlarge⟩ := hall
  intro B h0 hne hg hnp hq hle hpk
  by_cases hbig : 200014 < B.card
  · exact hlarge B h0 hne hg hnp hq hle hpk hbig
  by_cases c229 : 229 ≤ B.card
  · exact Or.inr (hs2 B.card c229 (by omega))
  by_cases c10 : 10 ≤ B.card
  · exact Or.inr (hs1 B.card c10 (by omega))
  by_cases h1 : B.card = 1
  · obtain ⟨a, ha⟩ := hne
    refine Or.inl ⟨a, ha, a, ha, ?_⟩
    rw [h1]
    simp
  by_cases h9 : B.card = 9
  · refine Or.inr ⟨17, by norm_num, by omega, by omega, by omega, fun α h1 h2 => ?_⟩
    omega
  have hpos : 0 < B.card := Finset.card_pos.mpr hne
  have x2 : B.card ≠ 2 := by
    intro h
    rw [h] at hnp
    exact hnp (by norm_num)
  have x3 : B.card ≠ 3 := by
    intro h
    rw [h] at hnp
    exact hnp (by norm_num)
  have x5 : B.card ≠ 5 := by
    intro h
    rw [h] at hnp
    exact hnp (by norm_num)
  have x7 : B.card ≠ 7 := by
    intro h
    rw [h] at hnp
    exact hnp (by norm_num)
  have x4 : B.card ≠ 4 := hq 3 (by norm_num)
  have x6 : B.card ≠ 6 := hq 5 (by norm_num)
  have x8 : B.card ≠ 8 := hq 7 (by norm_num)
  omega

The gate replayed this file at its merge, each hole a sorry (D-12 #5); the whole file: targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2/attempts/20261001T170100Z-t1001-402a-partial.lean