Four-speed amended lonely-runner spectrum

end Bounty

/- Component: Base. -/
noncomputable section

namespace Bounty.Families

open Finset Set Math15.LonelyRunner

/-- Any integer is zero on the unit additive circle. -/
theorem coe_int_zero (m : ℤ) : ((m : ℝ) : Time) = 0 := by
  apply (AddCircle.coe_eq_zero_iff (1 : ℝ)).2
  exact ⟨m, by simp⟩

/-- Integer changes of a real representative do not change its circle norm. -/
theorem coe_sub_int (x : ℝ) (m : ℤ) : ((x - m : ℝ) : Time) = (x : Time) := by
  rw [AddCircle.coe_sub, coe_int_zero, sub_zero]

theorem distance_le_abs_sub_int (x : ℝ) (m : ℤ) :
    distance (x : Time) ≤ |x - m| := by
  simp only [distance, AddCircle.norm_eq, inv_one, one_mul, mul_one]
  exact round_le x m

/-- A representative within half a period of an integer has the expected norm. -/
theorem distance_eq_abs_sub_int (x : ℝ) (m : ℤ) (hx : |x - m| ≤ (1 : ℝ) / 2) :
    distance (x : Time) = |x - m| := by
  rw [← coe_sub_int x m]
  apply (AddCircle.norm_coe_eq_abs_iff (1 : ℝ) (by norm_num)).2
  simpa using hx

theorem distance_nsmul_coe (n : ℕ) (x : ℝ) :
    distance (n • (x : Time)) = distance (((n : ℝ) * x : ℝ) : Time) := by
  congr 1
  simpa only [nsmul_eq_mul] using (AddCircle.coe_nsmul (p := (1 : ℝ)) (n := n) (x := x)).symm

theorem score_le_distance {V : Finset ℕ} {n : ℕ} (hn : n ∈ V) (t : Time) :
    score V t ≤ distance (n • t) := by
  have hV : V.Nonempty := ⟨n, hn⟩
  simpa only [score, dite_eq_left hV] using Finset.inf'_le (fun n => distance (n • t)) hn

theorem le_score_iff {V : Finset ℕ} (hV : V.Nonempty) {t : Time} {L : ℝ} :
    L ≤ score V t ↔ ∀ n ∈ V, L ≤ distance (n • t) := by
  simp only [score, dite_eq_left hV]
  exact Finset.le_inf'_iff hV (fun n => distance (n • t))

theorem score_le_ML (V : Finset ℕ) (t : Time) : score V t ≤ ML V := by
  have hBdd : BddAbove (Set.range (score V)) := by
    refine ⟨(1 : ℝ) / 2, ?_⟩
    rintro y ⟨u, rfl⟩
    by_cases hV : V.Nonempty
    · obtain ⟨n, hn⟩ := hV
      apply (score_le_distance hn u).trans
      simpa only [distance, abs_one] using
        AddCircle.norm_le_half_period (1 : ℝ) (by norm_num) (x := n • u)
    · simp only [score, dite_eq_right hV]
      norm_num
  exact le_csSup hBdd ⟨t, rfl⟩

theorem ML_le_of_scores_le (V : Finset ℕ) {L : ℝ}
    (h : ∀ t : Time, score V t ≤ L) : ML V ≤ L := by
  apply csSup_le (Set.range_nonempty _)
  rintro y ⟨t, rfl⟩
  exact h t

theorem score_neg (V : Finset ℕ) (t : Time) : score V (-t) = score V t := by
  by_cases hV : V.Nonempty
  · simp only [score, dite_eq_left hV, distance, smul_neg, norm_neg]
  · simp only [score, dite_eq_right hV]

/-- Time symmetry reduces score estimates to a real half period. -/
theorem exists_half_representative (V : Finset ℕ) (t : Time) :
    ∃ x : ℝ, 0 ≤ x ∧ x ≤ 1 / 2 ∧ score V (x : Time) = score V t := by
  letI : Fact (0 < (1 : ℝ)) := ⟨by norm_num⟩
  let r : ℝ := (AddCircle.equivIco (1 : ℝ) (-(1 / 2 : ℝ)) t).1
  have hr := (AddCircle.equivIco (1 : ℝ) (-(1 / 2 : ℝ)) t).2
  have he : (r : Time) = t := AddCircle.coe_equivIco
  have hr₁ : -(1 / 2 : ℝ) ≤ r := hr.1
  have hr₂ : r < (1 / 2 : ℝ) := by linarith [hr.2]
  by_cases h : 0 ≤ r
  · exact ⟨r, h, hr₂.le, by rw [he]⟩
  · refine ⟨-r, by linarith, by linarith, ?_⟩
    rw [AddCircle.coe_neg, score_neg, he]

def familyOne (h : ℕ) : Finset ℕ := {1, 2, 3, 4 * h}

theorem familyOne_lower (h : ℕ) (hh : 0 < h) :
    (h : ℝ) / (4 * (h : ℝ) + 1) ≤ ML (familyOne h) := by
  let L : ℝ := (h : ℝ) / (4 * (h : ℝ) + 1)
  have hR : (1 : ℝ) ≤ h := by exact_mod_cast hh
  have hden : 0 < 4 * (h : ℝ) + 1 := by positivity
  have hL : (1 : ℝ) / 5 ≤ L := by dsimp [L]; apply (le_div_iff₀ hden).2; nlinarith
  have hL' : L < (1 : ℝ) / 4 := by dsimp [L]; apply (div_lt_iff₀ hden).2; nlinarith
  have hL0 : 0 ≤ L := by linarith
  have hprod : (4 * (h : ℝ)) * L = (h : ℝ) - L := by
    dsimp [L]
    field_simp
    ring
  apply le_trans _ (score_le_ML (familyOne h) (L : Time))
  change L ≤ score (familyOne h) (L : Time)
  apply (le_score_iff (by simp [familyOne])).2
  intro n hn
  simp only [familyOne, Finset.mem_insert, Finset.mem_singleton] at hn
  rcases hn with rfl | rfl | rfl | rfl
  · rw [distance_nsmul_coe]
    norm_num
    rw [distance_eq_abs_sub_int L 0 (by simpa using (show |L| ≤ (1 : ℝ) / 2 by rw [abs_of_nonneg hL0]; linarith))]
    simpa [abs_of_nonneg hL0]
  · rw [distance_nsmul_coe]
    norm_num
    rw [distance_eq_abs_sub_int (2 * L) 0 (by rw [Int.cast_zero, sub_zero, abs_of_nonneg (by linarith)]; linarith)]
    simp only [Int.cast_zero, sub_zero, abs_of_nonneg (by linarith : 0 ≤ 2 * L)]
    linarith
  · rw [distance_nsmul_coe]
    norm_num
    rw [distance_eq_abs_sub_int (3 * L) 1 (by rw [Int.cast_one, abs_of_nonpos (by linarith)]; linarith)]
    simp only [Int.cast_one, abs_of_nonpos (by linarith : 3 * L - 1 ≤ 0)]
    linarith
  · rw [distance_nsmul_coe]
    push_cast
    rw [hprod]
    rw [distance_eq_abs_sub_int ((h : ℝ) - L) (h : ℤ) (by
      push_cast
      rw [show (h : ℝ) - L - h = -L by ring, abs_neg, abs_of_nonneg hL0]
      linarith)]
    push_cast
    rw [show (h : ℝ) - L - h = -L by ring, abs_neg, abs_of_nonneg hL0]

theorem familyOne_upper (h : ℕ) (hh : 0 < h) :
    ML (familyOne h) ≤ (h : ℝ) / (4 * (h : ℝ) + 1) := by
  let L : ℝ := (h : ℝ) / (4 * (h : ℝ) + 1)
  have hR : (1 : ℝ) ≤ h := by exact_mod_cast hh
  have hden : 0 < 4 * (h : ℝ) + 1 := by positivity
  have hL : (1 : ℝ) / 5 ≤ L := by dsimp [L]; apply (le_div_iff₀ hden).2; nlinarith
  have hL' : L < (1 : ℝ) / 4 := by dsimp [L]; apply (div_lt_iff₀ hden).2; nlinarith
  have hprod : (4 * (h : ℝ)) * L = (h : ℝ) - L := by dsimp [L]; field_simp; ring
  apply ML_le_of_scores_le
  intro t
  obtain ⟨x, hx0, hxhalf, hxt⟩ := exists_half_representative (familyOne h) t
  rw [← hxt]
  by_contra hbad
  have hscore : L < score (familyOne h) (x : Time) := lt_of_not_ge hbad
  have h₁ : L < |x| := by
    apply hscore.trans_le
    apply (score_le_distance (n := 1) (by simp [familyOne]) (x : Time)).trans
    simpa using distance_le_abs_sub_int x 0
  have h₂ : L < |2 * x - 1| := by
    apply hscore.trans_le
    apply (score_le_distance (n := 2) (by simp [familyOne]) (x : Time)).trans
    rw [distance_nsmul_coe]
    norm_num
    simpa only [Int.cast_one] using distance_le_abs_sub_int (2 * x) 1
  have h₃ : L < |3 * x - 1| := by
    apply hscore.trans_le
    apply (score_le_distance (n := 3) (by simp [familyOne]) (x : Time)).trans
    rw [distance_nsmul_coe]
    norm_num
    simpa only [Int.cast_one] using distance_le_abs_sub_int (3 * x) 1
  rw [abs_of_nonneg hx0] at h₁
  rw [abs_of_nonpos (by linarith : 2 * x - 1 ≤ 0)] at h₂
  have hxupper : 3 * x < 1 - L := by
    rcases lt_or_ge (3 * x - 1) 0 with hsign | hsign
    · rw [abs_of_neg hsign] at h₃
      linarith
    · rw [abs_of_nonneg hsign] at h₃
      linarith
  have hclose₁ : -L ≤ (4 * (h : ℝ)) * x - h := by nlinarith
  have hclose₂ : (4 * (h : ℝ)) * x - h ≤ L := by
    have hLt : 4 * (h : ℝ) * (1 - L) = 3 * (h : ℝ) + L := by nlinarith [hprod]
    nlinarith
  have hlast : distance (((4 * (h : ℝ)) * x : ℝ) : Time) ≤ L :=
    (distance_le_abs_sub_int ((4 * (h : ℝ)) * x) (h : ℤ)).trans (by
      push_cast
      exact abs_le.mpr ⟨hclose₁, hclose₂⟩)
  have hm := score_le_distance (V := familyOne h) (n := 4 * h) (by simp [familyOne]) (x : Time)
  rw [distance_nsmul_coe] at hm
  push_cast at hm
  exact (not_lt_of_ge (hm.trans hlast)) hscore

theorem familyOne_ML (h : ℕ) (hh : 0 < h) :
    ML (familyOne h) = (h : ℝ) / (4 * (h : ℝ) + 1) :=
  le_antisymm (familyOne_upper h hh) (familyOne_lower h hh)

theorem familyOne_spectrum (h : ℕ) (hh : 0 < h) :
    ∃ s k : ℕ, 1 ≤ k ∧ k ≤ 4 ∧ k ≤ s ∧
      ML (familyOne h) = (s : ℝ) / (4 * (s : ℝ) + k) := by
  refine ⟨h, 1, by omega, by omega, hh, ?_⟩
  simpa only [Nat.cast_one] using familyOne_ML h hh

def sporadic : Finset ℕ := {1, 3, 4, 14}

theorem sporadic_lower : (4 : ℝ) / 17 ≤ ML sporadic := by
  apply le_trans _ (score_le_ML sporadic ((7 / 17 : ℝ) : Time))
  apply (le_score_iff (by simp [sporadic])).2
  intro n hn
  simp only [sporadic, Finset.mem_insert, Finset.mem_singleton] at hn
  rcases hn with rfl | rfl | rfl | rfl <;> rw [distance_nsmul_coe] <;> norm_num
  · rw [distance_eq_abs_sub_int (7 / 17) 0 (by norm_num)]
    norm_num
  · rw [distance_eq_abs_sub_int (21 / 17) 1 (by norm_num)]
    norm_num
  · rw [distance_eq_abs_sub_int (28 / 17) 2 (by norm_num)]
    norm_num
  · rw [distance_eq_abs_sub_int (98 / 17) 6 (by norm_num)]
    norm_num

theorem sporadic_upper : ML sporadic ≤ (4 : ℝ) / 17 := by
  apply ML_le_of_scores_le
  intro t
  obtain ⟨x, hx0, hxhalf, hxt⟩ := exists_half_representative sporadic t
  rw [← hxt]
  by_contra hbad
  have hs : (4 : ℝ) / 17 < score sporadic (x : Time) := lt_of_not_ge hbad
  have hbound (n : ℕ) (hn : n ∈ sporadic) (m : ℤ) : (4 : ℝ) / 17 < |(n : ℝ) * x - m| := by
    apply hs.trans_le
    apply (score_le_distance hn (x : Time)).trans
    rw [distance_nsmul_coe]
    exact distance_le_abs_sub_int ((n : ℝ) * x) m
  have h₁ := hbound 1 (by simp [sporadic]) 0
  have h₃ := hbound 3 (by simp [sporadic]) 1
  have h₄ := hbound 4 (by simp [sporadic]) 1
  have h₄' := hbound 4 (by simp [sporadic]) 2
  norm_num at h₁ h₃ h₄ h₄'
  rw [abs_of_nonneg hx0] at h₁
  have hxlower : (7 : ℝ) / 17 < x := by
    rcases lt_or_ge (3 * x - 1) 0 with hsign | hsign
    · rw [abs_of_neg hsign] at h₃
      rcases lt_or_ge (4 * x - 1) 0 with hsign4 | hsign4
      · rw [abs_of_neg hsign4] at h₄
        linarith
      · rw [abs_of_nonneg hsign4] at h₄
        linarith
    · rw [abs_of_nonneg hsign] at h₃
      linarith
  rw [abs_of_nonpos (by linarith : 4 * x - 2 ≤ 0)] at h₄'
  have hxupper : x < (15 : ℝ) / 34 := by linarith
  have hclose : |14 * x - 6| ≤ (4 : ℝ) / 17 := by
    apply abs_le.mpr
    constructor <;> linarith
  have hb := hbound 14 (by simp [sporadic]) 6
  norm_num at hb
  exact (not_lt_of_ge hclose) hb

theorem sporadic_ML : ML sporadic = (4 : ℝ) / 17 :=
  le_antisymm sporadic_upper sporadic_lower

theorem sporadic_spectrum :
    ∃ s k : ℕ, 1 ≤ k ∧ k ≤ 4 ∧ k ≤ s ∧
      ML sporadic = (s : ℝ) / (4 * (s : ℝ) + k) := by
  refine ⟨4, 1, by norm_num, by norm_num, by norm_num, ?_⟩
  norm_num only [Nat.cast_ofNat]
  simpa using sporadic_ML

/-- The target's spectrum conclusion for a proposed real value. -/
def SpectrumValue (x : ℝ) : Prop :=
  (1 / 4 : ℝ) ≤ x ∨ ∃ s k : ℕ, 1 ≤ k ∧ k ≤ 4 ∧ k ≤ s ∧
    x = (s : ℝ) / (4 * (s : ℝ) + k)

theorem spectrum_of_gap_zero {x : ℝ} (h : 1 - 4 * x = 0) : SpectrumValue x := by
  exact Or.inl (by linarith)

theorem spectrum_of_gap_one {x : ℝ} {D : ℕ}
    (hD : 5 ≤ D) (hmod : D % 4 = 1) (hx : 1 - 4 * x = 1 / (D : ℝ)) :
    SpectrumValue x := by
  let s : ℕ := D / 4
  have hDeq : D = 4 * s + 1 := by
    dsimp [s]
    omega
  have hs : 1 ≤ s := by omega
  have hsR : (1 : ℝ) ≤ s := by exact_mod_cast hs
  have hcast : (D : ℝ) = 4 * (s : ℝ) + 1 := by exact_mod_cast hDeq
  apply Or.inr
  refine ⟨s, 1, by omega, by omega, hs, ?_⟩
  norm_num only [Nat.cast_one]
  rw [hcast] at hx
  have hden : 0 < 4 * (s : ℝ) + 1 := by positivity
  apply (eq_div_iff hden.ne').2
  have hmul := (eq_div_iff hden.ne').mp hx
  nlinarith

theorem spectrum_of_gap_two {x : ℝ} {D : ℕ}
    (hD : 10 ≤ D) (hmod : D % 4 = 2) (hx : 1 - 4 * x = 2 / (D : ℝ)) :
    SpectrumValue x := by
  let s : ℕ := D / 4
  have hDeq : D = 4 * s + 2 := by dsimp [s]; omega
  have hs : 2 ≤ s := by omega
  have hsR : (2 : ℝ) ≤ s := by exact_mod_cast hs
  have hcast : (D : ℝ) = 4 * (s : ℝ) + 2 := by exact_mod_cast hDeq
  apply Or.inr
  refine ⟨s, 2, by omega, by omega, hs, ?_⟩
  rw [hcast] at hx
  have hden : 0 < 4 * (s : ℝ) + 2 := by positivity
  apply (eq_div_iff hden.ne').2
  have hmul := (eq_div_iff hden.ne').mp hx
  norm_num only [Nat.cast_ofNat]
  nlinarith

def min4 (a b c d : ℝ) : ℝ := min (min a b) (min c d)

theorem min4_eq_second {a b c d : ℝ} (hba : b ≤ a) (hbc : b ≤ c) (hbd : b ≤ d) :
    min4 a b c d = b := by
  unfold min4
  rw [min_eq_right hba, min_eq_left (le_min hbc hbd)]

theorem min4_eq_third {a b c d : ℝ} (hca : c ≤ a) (hcb : c ≤ b) (hcd : c ≤ d) :
    min4 a b c d = c := by
  unfold min4
  rw [min_eq_left hcd, min_eq_right (le_min hca hcb)]

theorem min4_eq_fourth {a b c d : ℝ} (hda : d ≤ a) (hdb : d ≤ b) (hdc : d ≤ c) :
    min4 a b c d = d := by
  unfold min4
  rw [min_eq_right hdc, min_eq_right (le_min hda hdb)]

theorem min4_eq_second_fourth {a b c d : ℝ} (hba : b ≤ a) (hdc : d ≤ c) :
    min4 a b c d = min b d := by
  unfold min4
  rw [min_eq_right hba, min_eq_right hdc]

theorem ratio_le_ratio {a b c d : ℝ} (hc : 0 < c) (hd : 0 < d)
    (h : a * d ≤ b * c) : a / c ≤ b / d :=
  (div_le_div_iff₀ hc hd).2 h

/-- The two residues of the centres of the feasible triangles, represented in [0,4). -/
def residueOne (c b : ℕ) : ℕ := (2 * (b % 4) + (4 - c % 4)) % 4
def residueTwo (c b : ℕ) : ℕ := (b % 4 + (8 - 2 * (c % 4))) % 4

def familyTwoGap (c b : ℕ) : ℝ :=
  min4 ((residueOne c b : ℝ) / (c : ℝ))
    ((((4 - residueOne c b) % 4 : ℕ) : ℝ) / ((c : ℝ) + 2 * b))
    ((residueTwo c b : ℝ) / (2 * (c : ℝ) + b))
    ((((4 - residueTwo c b) % 4 : ℕ) : ℝ) / (2 * (c : ℝ) - b))

def familyTwo (c b : ℕ) : Finset ℕ := {c - b, b, c, c + b}

theorem familyTwoGap_01 {c b : ℕ} (hb : 0 < b) (hbc : b < c)
    (hcmod : c % 4 = 0) (hbmod : b % 4 = 1) :
    familyTwoGap c b = 1 / (2 * (c : ℝ) + b) := by
  have hbR : (0 : ℝ) < b := by exact_mod_cast hb
  have hbcR : (b : ℝ) < c := by exact_mod_cast hbc
  have hcR : (0 : ℝ) < c := by linarith
  norm_num [familyTwoGap, residueOne, residueTwo, hcmod, hbmod]
  apply min4_eq_third <;> (try simp only [← one_div]; apply ratio_le_ratio <;> nlinarith)

theorem familyTwoGap_03 {c b : ℕ} (hb : 0 < b) (hbc : b < c)
    (hcmod : c % 4 = 0) (hbmod : b % 4 = 3) :
    familyTwoGap c b = min (2 / ((c : ℝ) + 2 * b)) (1 / (2 * (c : ℝ) - b)) := by
  have hbR : (0 : ℝ) < b := by exact_mod_cast hb
  have hbcR : (b : ℝ) < c := by exact_mod_cast hbc
  have hcR : (0 : ℝ) < c := by linarith
  norm_num [familyTwoGap, residueOne, residueTwo, hcmod, hbmod]
  apply min4_eq_second_fourth
  · apply ratio_le_ratio <;> nlinarith
  · rw [← one_div]
    apply ratio_le_ratio <;> nlinarith

theorem familyTwoGap_10 {c b : ℕ} (hb : 0 < b) (hbc : b < c)
    (hcmod : c % 4 = 1) (hbmod : b % 4 = 0) :
    familyTwoGap c b = 1 / ((c : ℝ) + 2 * b) := by
  have hbR : (0 : ℝ) < b := by exact_mod_cast hb
  have hbcR : (b : ℝ) < c := by exact_mod_cast hbc
  have hcR : (0 : ℝ) < c := by linarith
  norm_num [familyTwoGap, residueOne, residueTwo, hcmod, hbmod]
  apply min4_eq_second <;> (try simp only [← one_div]; apply ratio_le_ratio <;> nlinarith)

theorem familyTwoGap_11 {c b : ℕ} (hb : 0 < b) (hbc : b < c)
    (hcmod : c % 4 = 1) (hbmod : b % 4 = 1) :
    familyTwoGap c b = 1 / (2 * (c : ℝ) - b) := by
  have hbR : (0 : ℝ) < b := by exact_mod_cast hb
  have hbcR : (b : ℝ) < c := by exact_mod_cast hbc
  have hcR : (0 : ℝ) < c := by linarith
  norm_num [familyTwoGap, residueOne, residueTwo, hcmod, hbmod]
  apply min4_eq_fourth <;> (try simp only [← one_div]; apply ratio_le_ratio <;> nlinarith)

theorem familyTwoGap_13 {c b : ℕ} (hb : 0 < b) (hbc : b < c)
    (hcmod : c % 4 = 1) (hbmod : b % 4 = 3) :
    familyTwoGap c b = 1 / (2 * (c : ℝ) + b) := by
  have hbR : (0 : ℝ) < b := by exact_mod_cast hb
  have hbcR : (b : ℝ) < c := by exact_mod_cast hbc
  have hcR : (0 : ℝ) < c := by linarith
  norm_num [familyTwoGap, residueOne, residueTwo, hcmod, hbmod]
  apply min4_eq_third <;> (try simp only [← one_div]; apply ratio_le_ratio <;> nlinarith)

theorem familyTwoGap_30 {c b : ℕ} (hb : 0 < b) (hbc : b < c)
    (hcmod : c % 4 = 3) (hbmod : b % 4 = 0) :
    familyTwoGap c b = 2 / (2 * (c : ℝ) + b) := by
  have hbR : (0 : ℝ) < b := by exact_mod_cast hb
  have hbcR : (b : ℝ) < c := by exact_mod_cast hbc
  have hcR : (0 : ℝ) < c := by linarith
  norm_num [familyTwoGap, residueOne, residueTwo, hcmod, hbmod]
  apply min4_eq_third
  · rw [← one_div]
    apply ratio_le_ratio <;> nlinarith
  · apply ratio_le_ratio <;> nlinarith
  · apply ratio_le_ratio <;> nlinarith

theorem familyTwoGap_31 {c b : ℕ} (hb : 0 < b) (hbc : b < c)
    (hcmod : c % 4 = 3) (hbmod : b % 4 = 1) :
    familyTwoGap c b = min (1 / ((c : ℝ) + 2 * b)) (1 / (2 * (c : ℝ) - b)) := by
  have hbR : (0 : ℝ) < b := by exact_mod_cast hb
  have hbcR : (b : ℝ) < c := by exact_mod_cast hbc
  have hcR : (0 : ℝ) < c := by linarith
  norm_num [familyTwoGap, residueOne, residueTwo, hcmod, hbmod]
  apply min4_eq_second_fourth <;> (try simp only [← one_div]; apply ratio_le_ratio <;> nlinarith)

theorem familyTwoGap_33 {c b : ℕ} (hb : 0 < b) (hbc : b < c)
    (hcmod : c % 4 = 3) (hbmod : b % 4 = 3) :
    familyTwoGap c b = 1 / (2 * (c : ℝ) + b) := by
  have hbR : (0 : ℝ) < b := by exact_mod_cast hb
  have hbcR : (b : ℝ) < c := by exact_mod_cast hbc
  have hcR : (0 : ℝ) < c := by linarith
  norm_num [familyTwoGap, residueOne, residueTwo, hcmod, hbmod]
  apply min4_eq_third <;> (try simp only [← one_div]; apply ratio_le_ratio <;> nlinarith)

theorem familyTwoGap_zero_left {c b : ℕ} (hb : 0 < b) (hbc : b < c)
    (hcmod : c % 4 = 2) (hbmod : b % 4 = 1 ∨ b % 4 = 3) :
    familyTwoGap c b = 0 := by
  have hbR : (0 : ℝ) < b := by exact_mod_cast hb
  have hbcR : (b : ℝ) < c := by exact_mod_cast hbc
  have hcR : (0 : ℝ) < c := by linarith
  have hdR : 0 < 2 * (c : ℝ) - b := by linarith
  rcases hbmod with hbmod | hbmod <;>
    norm_num [familyTwoGap, residueOne, residueTwo, hcmod, hbmod] <;>
    apply min4_eq_second <;> positivity

theorem familyTwoGap_zero_right {c b : ℕ} (hb : 0 < b) (hbc : b < c)
    (hcmod : c % 4 = 1 ∨ c % 4 = 3) (hbmod : b % 4 = 2) :
    familyTwoGap c b = 0 := by
  have hbR : (0 : ℝ) < b := by exact_mod_cast hb
  have hbcR : (b : ℝ) < c := by exact_mod_cast hbc
  have hcR : (0 : ℝ) < c := by linarith
  have hdR : 0 < 2 * (c : ℝ) - b := by linarith
  rcases hcmod with hcmod | hcmod <;>
    norm_num [familyTwoGap, residueOne, residueTwo, hcmod, hbmod] <;>
    apply min4_eq_fourth <;> positivity

/-- Coprimality excludes the four even/even residue pairs. -/
theorem odd_residue_of_coprime {c b : ℕ} (hcop : Nat.Coprime c b) :
    (c % 4 = 1 ∨ c % 4 = 3) ∨ (b % 4 = 1 ∨ b % 4 = 3) := by
  by_contra hbad
  have hc : c % 2 = 0 := by have := Nat.mod_lt c (by omega : 0 < 4); omega
  have hb : b % 2 = 0 := by have := Nat.mod_lt b (by omega : 0 < 4); omega
  have hdc : 2 ∣ c := Nat.dvd_iff_mod_eq_zero.mpr hc
  have hdb : 2 ∣ b := Nat.dvd_iff_mod_eq_zero.mpr hb
  have hg : 2 ∣ Nat.gcd c b := Nat.dvd_gcd hdc hdb
  rw [hcop.gcd_eq_one] at hg
  norm_num at hg

/-- Pure integer/real algebra turns the four-triangle formula into the target spectrum. -/
theorem familyTwoGap_spectrum {c b : ℕ} {x : ℝ}
    (hb : 0 < b) (hbc : b < c) (hcop : Nat.Coprime c b)
    (hx : 1 - 4 * x = familyTwoGap c b) : SpectrumValue x := by
  have hodd := odd_residue_of_coprime hcop
  have hc0 : c % 4 < 4 := Nat.mod_lt c (by omega)
  have hb0 : b % 4 < 4 := Nat.mod_lt b (by omega)
  have hdc : b ≤ 2 * c := by omega
  have hcast : ((2 * c - b : ℕ) : ℝ) = 2 * (c : ℝ) - b := by
    rw [Nat.cast_sub hdc]
    push_cast
    ring
  obtain hc | hc | hc | hc : c % 4 = 0 ∨ c % 4 = 1 ∨ c % 4 = 2 ∨ c % 4 = 3 := by omega
  · obtain hbmod | hbmod | hbmod | hbmod : b % 4 = 0 ∨ b % 4 = 1 ∨ b % 4 = 2 ∨ b % 4 = 3 := by omega
    · omega
    · rw [familyTwoGap_01 hb hbc hc hbmod] at hx
      apply spectrum_of_gap_one (D := 2 * c + b) (by omega) (by omega)
      simpa only [Nat.cast_add, Nat.cast_mul, Nat.cast_ofNat] using hx
    · omega
    · rw [familyTwoGap_03 hb hbc hc hbmod] at hx
      rcases le_total (2 / ((c : ℝ) + 2 * b)) (1 / (2 * (c : ℝ) - b)) with hmin | hmin
      · rw [min_eq_left hmin] at hx
        apply spectrum_of_gap_two (D := c + 2 * b) (by omega) (by omega)
        simpa only [Nat.cast_add, Nat.cast_mul, Nat.cast_ofNat] using hx
      · rw [min_eq_right hmin] at hx
        apply spectrum_of_gap_one (D := 2 * c - b) (by omega) (by omega)
        simpa only [hcast] using hx
  · obtain hbmod | hbmod | hbmod | hbmod : b % 4 = 0 ∨ b % 4 = 1 ∨ b % 4 = 2 ∨ b % 4 = 3 := by omega
    · rw [familyTwoGap_10 hb hbc hc hbmod] at hx
      apply spectrum_of_gap_one (D := c + 2 * b) (by omega) (by omega)
      simpa only [Nat.cast_add, Nat.cast_mul, Nat.cast_ofNat] using hx
    · rw [familyTwoGap_11 hb hbc hc hbmod] at hx
      apply spectrum_of_gap_one (D := 2 * c - b) (by omega) (by omega)
      simpa only [hcast] using hx
    · rw [familyTwoGap_zero_right hb hbc (Or.inl hc) hbmod] at hx
      exact spectrum_of_gap_zero hx
    · rw [familyTwoGap_13 hb hbc hc hbmod] at hx
      apply spectrum_of_gap_one (D := 2 * c + b) (by omega) (by omega)
      simpa only [Nat.cast_add, Nat.cast_mul, Nat.cast_ofNat] using hx
  · obtain hbmod | hbmod | hbmod | hbmod : b % 4 = 0 ∨ b % 4 = 1 ∨ b % 4 = 2 ∨ b % 4 = 3 := by omega
    · omega
    · rw [familyTwoGap_zero_left hb hbc hc (Or.inl hbmod)] at hx
      exact spectrum_of_gap_zero hx
    · omega
    · rw [familyTwoGap_zero_left hb hbc hc (Or.inr hbmod)] at hx
      exact spectrum_of_gap_zero hx
  · obtain hbmod | hbmod | hbmod | hbmod : b % 4 = 0 ∨ b % 4 = 1 ∨ b % 4 = 2 ∨ b % 4 = 3 := by omega
    · rw [familyTwoGap_30 hb hbc hc hbmod] at hx
      apply spectrum_of_gap_two (D := 2 * c + b) (by omega) (by omega)
      simpa only [Nat.cast_add, Nat.cast_mul, Nat.cast_ofNat] using hx
    · rw [familyTwoGap_31 hb hbc hc hbmod] at hx
      rcases le_total (1 / ((c : ℝ) + 2 * b)) (1 / (2 * (c : ℝ) - b)) with hmin | hmin
      · rw [min_eq_left hmin] at hx