Six-speed maximum-speed/denominator bound

open Finset Math15.LonelyRunner

-- W5 component T04

noncomputable def cdist (x L : ℕ) : ℕ := min (x % L) (L - x % L)

theorem pg_integer_zero (k : ℤ) : ((k : ℝ) : Time) = 0 := by
  apply (AddCircle.coe_eq_zero_iff (1 : ℝ)).mpr
  exact ⟨k, by simp [zsmul_eq_mul]⟩

theorem pg_norm_unit (x : ℝ) (hl : 0 ≤ x) (hu : x ≤ 1) :
    ‖(x : Time)‖ = min x (1-x) := by
  by_cases hhalf : x ≤ 1 / 2
  · have he := (AddCircle.norm_coe_eq_abs_iff (1 : ℝ) (by norm_num) (x := x)).mpr
      (by rw [abs_of_nonneg hl]; simpa using hhalf)
    rw [he, abs_of_nonneg hl, min_eq_left (by linarith)]
  · have he := (AddCircle.norm_coe_eq_abs_iff (1 : ℝ) (by norm_num) (x := 1-x)).mpr
      (by rw [abs_of_nonneg (by linarith)]; norm_num; linarith)
    have hone : ((1 : ℝ) : Time) = 0 := by simpa using pg_integer_zero 1
    rw [AddCircle.coe_sub, hone, zero_sub, norm_neg, abs_of_nonneg (by linarith)] at he
    rw [he, min_eq_right (by linarith)]

theorem pg_norm_residue (x L : ℕ) (hL : 0 < L) :
    ‖(((x : ℝ) / L : ℝ) : Time)‖ = (cdist x L : ℝ) / L := by
  have hLR : (0 : ℝ) < L := by exact_mod_cast hL
  have hr : x % L < L := Nat.mod_lt x hL
  have he : (x : ℝ) / L = (x % L : ℕ) / (L : ℝ) + (x / L : ℕ) := by
    have hx : ((x % L : ℕ) : ℝ) + (L : ℝ) * (x / L : ℕ) = x := by
      exact_mod_cast Nat.mod_add_div x L
    apply (div_eq_iff hLR.ne').mpr
    field_simp
    nlinarith
  rw [he, AddCircle.coe_add]
  have hk : (((x / L : ℕ) : ℝ) : Time) = 0 := by
    exact_mod_cast pg_integer_zero (x / L)
  rw [hk, add_zero, pg_norm_unit]
  · unfold cdist
    rw [Nat.cast_min, Nat.cast_sub hr.le, ← min_div_div_right hLR.le]
    congr 1
    field_simp
  · positivity
  · apply (div_le_one hLR).mpr
    exact_mod_cast hr.le

theorem pg_score_le_ML (V : Finset ℕ) (t : Time) : score V t ≤ ML V := by
  apply le_csSup (s := Set.range (score V)) _ ⟨t, rfl⟩
  refine ⟨1 / 2, ?_⟩
  rintro _ ⟨u, rfl⟩
  by_cases hV : V.Nonempty
  · obtain ⟨v, hv⟩ := hV
    have hV : V.Nonempty := ⟨v, hv⟩
    have hi : score V u ≤ distance (v • u) := by
      simpa only [score, dite_eq_left hV] using
        Finset.inf'_le (fun v => distance (v • u)) hv
    exact hi.trans (by
      simpa [distance] using AddCircle.norm_le_half_period (1 : ℝ) (by norm_num) (x := v • u))
  · simp [score, hV]

theorem pg_grid_distance (a x L : ℕ) (hL : 0 < L) :
    distance (x • (((a : ℝ) / L : ℝ) : Time)) = (cdist (a*x) L : ℝ) / L := by
  rw [distance, ← AddCircle.coe_nsmul, nsmul_eq_mul]
  have he : (x : ℝ) * ((a : ℝ) / L) = ((a*x : ℕ) : ℝ) / L := by push_cast; ring
  rw [he, pg_norm_residue _ _ hL]

theorem pg_pair_distance (a M b : ℕ) (hL : 0 < M+b) :
    distance (M • (((a : ℝ)/(M+b) : ℝ) : Time)) =
    distance (b • (((a : ℝ)/(M+b) : ℝ) : Time)) := by
  have hz : (M+b) • (((a : ℝ)/(M+b) : ℝ) : Time) = 0 := by
    rw [← AddCircle.coe_nsmul, nsmul_eq_mul]
    have hLR : (M : ℝ)+b ≠ 0 := by exact_mod_cast hL.ne'
    have he : ((M+b : ℕ) : ℝ)*((a : ℝ)/(M+b)) = a := by
      push_cast
      field_simp
    rw [he]
    exact_mod_cast pg_integer_zero a
  rw [add_nsmul] at hz
  have he := eq_neg_of_add_eq_zero_left hz
  rw [he, distance, norm_neg]
  rfl

theorem pair_grid_cover (V : Finset ℕ) (M b : ℕ)
    (hM : M ∈ V) (hb : b ∈ V) (hbM : b ≠ M)
    (hL : 0 < M+b) (hML : ML V < 1/6) (a : ℕ) :
    ∃ x ∈ V, x ≠ b ∧ 6 * cdist (a*x) (M+b) < M+b := by
  let t : Time := (((a : ℝ)/(M+b) : ℝ) : Time)
  have hV : V.Nonempty := ⟨M,hM⟩
  have hs : score V t < 1/6 := (pg_score_le_ML V t).trans_lt hML
  have hx : ∃ x ∈ V, distance (x • t) < 1/6 := by
    by_contra! h
    have hh : (1:ℝ)/6 ≤ score V t := by
      simp only [score, dite_eq_left hV]
      apply Finset.le_inf'
      exact h
    linarith
  obtain ⟨x,hx,hd⟩ := hx
  have convert (y : ℕ) (hy : distance (y • t) < 1/6) :
      6 * cdist (a*y) (M+b) < M+b := by
    dsimp [t] at hy
    rw [← Nat.cast_add M b, pg_grid_distance _ _ _ hL] at hy
    have hLR : (0:ℝ)<(M+b:ℕ) := by exact_mod_cast hL
    have ht := (div_lt_iff₀ hLR).mp hy
    have hh : (6:ℝ)*cdist (a*y) (M+b)<(M+b:ℕ) := by nlinarith
    exact_mod_cast hh
  by_cases hxb : x=b
  · subst x
    refine ⟨M,hM,Ne.symm hbM,convert M ?_⟩
    change distance (M • (((a:ℝ)/(M+b):ℝ):Time)) < 1/6
    rw [pg_pair_distance _ _ _ hL]
    exact hd
  · exact ⟨x,hx,hxb,convert x hd⟩

theorem pair_grid_gcd (V : Finset ℕ) (M b : ℕ)
    (hM : M ∈ V) (hbM : b ≠ M) (hprim : Primitive V) :
    Nat.gcd ((V.erase b).gcd id) (M+b) = 1 := by
  apply Nat.dvd_one.mp
  rw [← hprim]
  apply Finset.dvd_gcd
  intro x hx
  let d := Nat.gcd ((V.erase b).gcd id) (M+b)
  have hdM : d ∣ M := (Nat.gcd_dvd_left _ _).trans
    (Finset.gcd_dvd (f := id) (Finset.mem_erase.mpr ⟨Ne.symm hbM,hM⟩))
  by_cases hxb : x=b
  · subst x
    exact (Nat.dvd_add_iff_right hdM).mpr (Nat.gcd_dvd_right _ _)
  · exact (Nat.gcd_dvd_left _ _).trans
      (Finset.gcd_dvd (f := id) (Finset.mem_erase.mpr ⟨hxb,hx⟩))

theorem pair_grid_residue_range (V : Finset ℕ) (M b : ℕ)
    (hpos : Positive V) (hb : b ∈ V) (hmax : ∀ x ∈ V, x ≤ M) :
    ∀ x ∈ V.erase b, 0 < x ∧ x < M+b := by
  intro x hx
  have hxV := Finset.mem_of_mem_erase hx
  have hbpos := hpos b hb
  exact ⟨hpos x hxV, by have := hmax x hxV; omega⟩

theorem pair_grid (V : Finset ℕ) (M b : ℕ)
    (hpos : Positive V) (hcard : V.card = 6) (hprim : Primitive V)
    (hM : M = V.sup id) (hb : b ∈ V) (hbM : b ≠ M) (hML : ML V < 1/6) :
    (V.erase b).card = 5 ∧
    (∀ x ∈ V.erase b, 0 < x ∧ x < M+b) ∧
    Nat.gcd ((V.erase b).gcd id) (M+b) = 1 ∧
    (∀ a : ℕ, 0 < a → a < M+b →
      ∃ x ∈ V.erase b, 6 * cdist (a*x) (M+b) < M+b) := by
  have hne : V.Nonempty := Finset.card_pos.mp (by omega)
  have hMm : M ∈ V := by
    rw [hM]
    simpa using Finset.sup_mem_of_nonempty (f := id) hne
  have hmax : ∀ x ∈ V, x ≤ M := by
    intro x hx
    rw [hM]
    exact Finset.le_sup (f := id) hx
  have hL : 0 < M+b := by have := hpos b hb; omega
  refine ⟨by rw [Finset.card_erase_of_mem hb,hcard],
    pair_grid_residue_range V M b hpos hb hmax,
    pair_grid_gcd V M b hMm hbM hprim, ?_⟩
  intro a _ _
  obtain ⟨x,hx,hxb,hd⟩ := pair_grid_cover V M b hMm hb hbM hL hML a
  exact ⟨x,Finset.mem_erase.mpr ⟨hxb,hx⟩,hd⟩
-- ===== lean-work/FamiliesAB.lean =====




theorem LRFamilyNormalization.integer_coe_zero (z : ℤ) : ((z : ℝ) : Time) = 0 := by
  apply (AddCircle.coe_eq_zero_iff (1 : ℝ)).mpr
  exact ⟨z, by simp [zsmul_eq_mul]⟩

theorem LRFamilyNormalization.coprime_grid_shift (a b c : ℕ) (ha : 0 < a) (hab : Nat.Coprime a b) :
    ∃ j : ℤ, b • (((j : ℝ) / (a : ℝ)) : Time) =
      (((c : ℝ) / (a : ℝ)) : Time) := by
  let j : ℤ := (c : ℤ) * Nat.gcdA b a
  let k : ℤ := (c : ℤ) * Nat.gcdB b a
  have hbez : (1 : ℤ) = (b : ℤ) * Nat.gcdA b a + (a : ℤ) * Nat.gcdB b a := by
    simpa [hab.symm.gcd_eq_one] using Nat.gcd_eq_gcd_ab b a
  have hrel : (b : ℤ) * j + (a : ℤ) * k = c := by
    dsimp [j, k]
    calc
      (b : ℤ) * ((c : ℤ) * Nat.gcdA b a) + (a : ℤ) * ((c : ℤ) * Nat.gcdB b a) =
          (c : ℤ) * ((b : ℤ) * Nat.gcdA b a + (a : ℤ) * Nat.gcdB b a) := by ring
      _ = c := by rw [← hbez]; ring
  have haR : (a : ℝ) ≠ 0 := by exact_mod_cast ha.ne'
  have hreal : (b : ℝ) * (j : ℝ) / (a : ℝ) = (c : ℝ) / (a : ℝ) - (k : ℝ) := by
    apply (div_eq_iff haR).mpr
    have hr : (b : ℝ) * (j : ℝ) + (a : ℝ) * (k : ℝ) = (c : ℝ) := by exact_mod_cast hrel
    field_simp
    nlinarith
  refine ⟨j, ?_⟩
  rw [← AddCircle.coe_nsmul, nsmul_eq_mul, ← mul_div_assoc, hreal,
    AddCircle.coe_sub, LRFamilyNormalization.integer_coe_zero, sub_zero]

theorem LRFamilyNormalization.half_grid_norm_lower (a : ℕ) (ha : 2 ≤ a) :
    (1 / 3 : ℝ) ≤ ‖((((a / 2 : ℕ) : ℝ) / (a : ℝ)) : Time)‖ := by
  have haR : (0 : ℝ) < a := by exact_mod_cast (show 0 < a by omega)
  have hlo : a ≤ 3 * (a / 2) := by omega
  have hhi : 2 * (a / 2) ≤ a := by omega
  have hlor : (a : ℝ) ≤ 3 * ((a / 2 : ℕ) : ℝ) := by exact_mod_cast hlo
  have hhir : 2 * ((a / 2 : ℕ) : ℝ) ≤ (a : ℝ) := by exact_mod_cast hhi
  have hl : (1 / 3 : ℝ) ≤ ((a / 2 : ℕ) : ℝ) / (a : ℝ) := by
    apply (le_div_iff₀ haR).mpr
    linarith
  have hh : ((a / 2 : ℕ) : ℝ) / (a : ℝ) ≤ 1 / 2 := by
    apply (div_le_iff₀ haR).mpr
    linarith
  have hz : (0 : ℝ) ≤ ((a / 2 : ℕ) : ℝ) / (a : ℝ) := by positivity
  have hn := (AddCircle.norm_coe_eq_abs_iff (p := (1 : ℝ))
    (x := ((a / 2 : ℕ) : ℝ) / (a : ℝ)) (by norm_num)).mpr
      (show |((a / 2 : ℕ) : ℝ) / (a : ℝ)| ≤ |(1 : ℝ)| / 2 by
        rw [abs_of_nonneg hz]
        simpa using hh)
  rw [hn, abs_of_nonneg hz]
  exact hl


theorem LRFamilyNormalization.exists_grid_far (a b : ℕ) (ha : 2 ≤ a) (hab : Nat.Coprime a b) (t : Time) :
    ∃ j : ℤ, (1 / 6 : ℝ) ≤
      distance (b • (t + (((j : ℝ) / (a : ℝ)) : Time))) := by
  by_cases ht : (1 / 6 : ℝ) ≤ distance (b • t)
  · exact ⟨0, by simpa using ht⟩
  obtain ⟨j, hj⟩ := LRFamilyNormalization.coprime_grid_shift a b (a / 2) (by omega) hab
  refine ⟨j, ?_⟩
  by_contra hfar
  have htlt : distance (b • t) < 1 / 6 := lt_of_not_ge ht
  have hylt : distance (b • (t + (((j : ℝ) / (a : ℝ)) : Time))) < 1 / 6 :=
    lt_of_not_ge hfar
  have hdiff : b • (t + (((j : ℝ) / (a : ℝ)) : Time)) - b • t =
      ((((a / 2 : ℕ) : ℝ) / (a : ℝ)) : Time) := by
    rw [nsmul_add, hj]
    abel
  have htri := norm_sub_le (b • (t + (((j : ℝ) / (a : ℝ)) : Time))) (b • t)
  rw [hdiff] at htri
  have hlower := LRFamilyNormalization.half_grid_norm_lower a ha
  unfold distance at htlt hylt
  linarith

theorem LRFamilyNormalization.scale_eq_one_of_grid_close (a b : ℕ) (ha : 0 < a)
    (hab : Nat.Coprime a b) (t : Time)
    (hclose : ∀ j : ℤ, distance (b • (t + (((j : ℝ) / (a : ℝ)) : Time))) < 1 / 6) :
    a = 1 := by
  by_contra hne
  have htwo : 2 ≤ a := by omega
  obtain ⟨j, hj⟩ := LRFamilyNormalization.exists_grid_far a b htwo hab t
  exact (not_lt_of_ge hj) (hclose j)





noncomputable def lr06FamilyA (a b : ℕ) : Finset ℕ := {a, 2*a, 3*a, 4*a, 5*a, b}
noncomputable def lr06FamilyB (a b : ℕ) : Finset ℕ := {a, 3*a, 4*a, 5*a, 9*a, b}

noncomputable def lr06ABShift (a : ℕ) (j : ℤ) : Time :=
  ((1 / (6 * (a : ℝ)) + (j : ℝ) / a : ℝ) : Time)

theorem lr06AB_integer_zero (k : ℤ) : (((k : ℝ) : Time)) = 0 := by
  apply (AddCircle.coe_eq_zero_iff (1 : ℝ)).mpr
  exact ⟨k, by simp⟩


theorem lr06AB_structured_shift (a m : ℕ) (ha : 0 < a) (j : ℤ) :
    distance ((m * a) • lr06ABShift a j) =
      (min (m % 6) (6 - m % 6) : ℕ) / (6 : ℝ) := by
  have haR : (a : ℝ) ≠ 0 := by exact_mod_cast ha.ne'
  rw [lr06ABShift, distance, ← AddCircle.coe_nsmul, nsmul_eq_mul]
  have he : ((m * a : ℕ) : ℝ) * (1 / (6 * (a : ℝ)) + (j : ℝ) / a) =
      (m : ℝ) / 6 + ((m : ℤ) * j : ℤ) := by
    push_cast
    field_simp
  rw [he, AddCircle.coe_add, lr06AB_integer_zero, add_zero]
  simpa using
    (AddCircle.norm_div_natCast (p := (1 : ℝ)) (m := m) (n := 6))

theorem lr06AB_structured_shift_lower (a m : ℕ) (ha : 0 < a) (j : ℤ)
    (hm : m ∈ ({1, 2, 3, 4, 5, 9} : Finset ℕ)) :
    (1 / 6 : ℝ) ≤ distance ((m * a) • lr06ABShift a j) := by
  rw [lr06AB_structured_shift a m ha j]
  simp only [Finset.mem_insert, Finset.mem_singleton] at hm
  rcases hm with rfl | rfl | rfl | rfl | rfl | rfl <;> norm_num

theorem lr06AB_score_le_ML (V : Finset ℕ) (t : Time) : score V t ≤ ML V := by
  apply le_csSup (s := Set.range (score V)) _ ⟨t, rfl⟩
  refine ⟨1 / 2, ?_⟩
  rintro _ ⟨u, rfl⟩
  by_cases hV : V.Nonempty
  · obtain ⟨v, hv⟩ := hV
    have hV : V.Nonempty := ⟨v, hv⟩
    have hi : score V u ≤ distance (v • u) := by
      simpa only [score, dite_eq_left hV] using
        Finset.inf'_le (fun v => distance (v • u)) hv
    exact hi.trans (by
      simpa [distance] using AddCircle.norm_le_half_period (1 : ℝ) (by norm_num) (x := v • u))
  · simp [score, hV]


theorem lr06AB_extra_small (V : Finset ℕ) (b : ℕ) (hV : V.Nonempty)
    (hML : ML V < 1 / 6) (t : Time)
    (hstructured : ∀ w ∈ V, w ≠ b → (1 / 6 : ℝ) ≤ distance (w • t)) :
    distance (b • t) < 1 / 6 := by
  by_contra h
  have hb : (1 / 6 : ℝ) ≤ distance (b • t) := le_of_not_gt h
  have hlower : (1 / 6 : ℝ) ≤ score V t := by
    simp only [score, dite_eq_left hV]
    apply Finset.le_inf'
    intro w hw
    by_cases hwb : w = b
    · simpa [hwb] using hb
    · exact hstructured w hw hwb
  exact (not_lt_of_ge (hlower.trans (lr06AB_score_le_ML V t))) hML

theorem lr06FamilyA_shift_small (a b : ℕ) (ha : 0 < a)
    (hML : ML (lr06FamilyA a b) < 1 / 6) (j : ℤ) :
    distance (b • lr06ABShift a j) < 1 / 6 := by
  apply lr06AB_extra_small (lr06FamilyA a b) b (by simp [lr06FamilyA]) hML
  intro w hw hwb
  simp only [lr06FamilyA, Finset.mem_insert, Finset.mem_singleton] at hw
  rcases hw with hw | hw | hw | hw | hw | hw <;> subst w
  · simpa using lr06AB_structured_shift_lower a 1 ha j (by simp)
  · exact lr06AB_structured_shift_lower a 2 ha j (by simp)
  · exact lr06AB_structured_shift_lower a 3 ha j (by simp)
  · exact lr06AB_structured_shift_lower a 4 ha j (by simp)
  · exact lr06AB_structured_shift_lower a 5 ha j (by simp)
  · exact (hwb rfl).elim

theorem lr06FamilyB_shift_small (a b : ℕ) (ha : 0 < a)
    (hML : ML (lr06FamilyB a b) < 1 / 6) (j : ℤ) :
    distance (b • lr06ABShift a j) < 1 / 6 := by
  apply lr06AB_extra_small (lr06FamilyB a b) b (by simp [lr06FamilyB]) hML
  intro w hw hwb
  simp only [lr06FamilyB, Finset.mem_insert, Finset.mem_singleton] at hw
  rcases hw with hw | hw | hw | hw | hw | hw <;> subst w
  · simpa using lr06AB_structured_shift_lower a 1 ha j (by simp)
  · exact lr06AB_structured_shift_lower a 3 ha j (by simp)
  · exact lr06AB_structured_shift_lower a 4 ha j (by simp)
  · exact lr06AB_structured_shift_lower a 5 ha j (by simp)
  · exact lr06AB_structured_shift_lower a 9 ha j (by simp)
  · exact (hwb rfl).elim

theorem lr06AB_coprime_of_primitive (V : Finset ℕ) (a b : ℕ) (hp : Primitive V)
    (hV : ∀ w ∈ V, a ∣ w ∨ w = b) : Nat.Coprime a b := by
  have hd : Nat.gcd a b ∣ V.gcd id := Finset.dvd_gcd_iff.mpr (by
    intro w hw
    rcases hV w hw with hdiv | heq
    · exact (Nat.gcd_dvd_left a b).trans hdiv
    · rw [heq]
      exact Nat.gcd_dvd_right a b)
  change V.gcd id = 1 at hp
  rw [hp] at hd
  exact Nat.dvd_one.mp hd

theorem lr06FamilyA_coprime (a b : ℕ) (hp : Primitive (lr06FamilyA a b)) :
    Nat.Coprime a b := by
  apply lr06AB_coprime_of_primitive _ a b hp
  intro w hw
  simp only [lr06FamilyA, Finset.mem_insert, Finset.mem_singleton] at hw
  rcases hw with rfl | rfl | rfl | rfl | rfl | rfl
  · exact Or.inl dvd_rfl
  · exact Or.inl (dvd_mul_left a 2)
  · exact Or.inl (dvd_mul_left a 3)
  · exact Or.inl (dvd_mul_left a 4)
  · exact Or.inl (dvd_mul_left a 5)
  · exact Or.inr rfl

theorem lr06FamilyB_coprime (a b : ℕ) (hp : Primitive (lr06FamilyB a b)) :
    Nat.Coprime a b := by
  apply lr06AB_coprime_of_primitive _ a b hp
  intro w hw
  simp only [lr06FamilyB, Finset.mem_insert, Finset.mem_singleton] at hw
  rcases hw with rfl | rfl | rfl | rfl | rfl | rfl
  · exact Or.inl dvd_rfl
  · exact Or.inl (dvd_mul_left a 3)
  · exact Or.inl (dvd_mul_left a 4)
  · exact Or.inl (dvd_mul_left a 5)
  · exact Or.inl (dvd_mul_left a 9)
  · exact Or.inr rfl



theorem lr06AB_norm_cell (x : ℝ) (k : ℤ) (hl : (k : ℝ) ≤ x) (hu : x ≤ k + 1) :
    ‖(x : Time)‖ = min (x - k) (k + 1 - x) := by
  have hk := lr06AB_integer_zero k
  have hone : ((1 : ℝ) : Time) = 0 := by simpa using lr06AB_integer_zero 1
  by_cases hhalf : x - k ≤ 1 / 2
  · have he : ‖((x - k : ℝ) : Time)‖ = |x - k| :=
      (AddCircle.norm_coe_eq_abs_iff (1 : ℝ) (by norm_num)).mpr (by
        rw [abs_of_nonneg (sub_nonneg.mpr hl)]
        simpa using hhalf)
    rw [AddCircle.coe_sub, hk, sub_zero, abs_of_nonneg (sub_nonneg.mpr hl)] at he
    rw [he, min_eq_left (by linarith)]
  · have he : ‖((k + 1 - x : ℝ) : Time)‖ = |k + 1 - x| :=
      (AddCircle.norm_coe_eq_abs_iff (1 : ℝ) (by norm_num)).mpr (by
        rw [abs_of_nonneg (sub_nonneg.mpr hu)]
        norm_num
        linarith)
    rw [AddCircle.coe_sub, AddCircle.coe_add, hk, hone, zero_add, zero_sub,
      norm_neg, abs_of_nonneg (sub_nonneg.mpr hu)] at he
    rw [he, min_eq_right (by linarith)]

theorem lr06AB_divisible_six (b : ℕ)
    (h : distance (b • (((1 / 6 : ℝ)) : Time)) < 1 / 6) : 6 ∣ b := by
  have he : distance (b • (((1 / 6 : ℝ)) : Time)) =
      (min (b % 6) (6 - b % 6) : ℕ) / (6 : ℝ) := by
    rw [distance, ← AddCircle.coe_nsmul, nsmul_eq_mul]
    simpa only [mul_one, one_mul, Nat.cast_ofNat, mul_one_div] using
      (AddCircle.norm_div_natCast (p := (1 : ℝ)) (m := b) (n := 6))
  rw [he] at h
  have hmin : min (b % 6) (6 - b % 6) < 1 := by exact_mod_cast (show
    ((min (b % 6) (6 - b % 6) : ℕ) : ℝ) < 1 by linarith)
  have hmod : b % 6 < 6 := Nat.mod_lt _ (by norm_num)
  have hzero : b % 6 = 0 := by omega
  exact Nat.dvd_of_mod_eq_zero hzero

noncomputable def lr06ABWitness (k : ℕ) : ℝ := (k : ℝ) / (6 * (k : ℝ) + 1)

theorem lr06ABWitness_bounds (k : ℕ) (hk : 1 ≤ k) :
    (1 / 7 : ℝ) ≤ lr06ABWitness k ∧ lr06ABWitness k ≤ 1 / 6 := by
  have hkR : (1 : ℝ) ≤ k := by exact_mod_cast hk
  have hd : 0 < 6 * (k : ℝ) + 1 := by positivity
  constructor
  · apply (le_div_iff₀ hd).mpr
    linarith
  · apply (div_le_iff₀ hd).mpr
    linarith

theorem lr06AB_witness_structured (k m : ℕ) (hk : 1 ≤ k)
    (hm : m ∈ ({1, 2, 3, 4, 5, 9} : Finset ℕ)) :
    lr06ABWitness k ≤ distance (m • (lr06ABWitness k : Time)) := by
  have hb := lr06ABWitness_bounds k hk
  have ht0 : 0 ≤ lr06ABWitness k := by linarith
  rw [distance, ← AddCircle.coe_nsmul, nsmul_eq_mul]
  have hmcase : (1 ≤ m ∧ m ≤ 5) ∨ m = 9 := by
    simp only [Finset.mem_insert, Finset.mem_singleton] at hm
    omega
  rcases hmcase with hm | rfl
  · have hm0 : (1 : ℝ) ≤ m := by exact_mod_cast hm.1
    have hm5 : (m : ℝ) ≤ 5 := by exact_mod_cast hm.2
    rw [lr06AB_norm_cell _ 0 (by norm_num; positivity) (by norm_num; nlinarith)]
    norm_num
    constructor <;> nlinarith
  · rw [lr06AB_norm_cell _ 1 (by norm_num; linarith) (by norm_num; linarith)]
    norm_num
    constructor <;> linarith

theorem lr06AB_witness_extra (k : ℕ) (hk : 1 ≤ k) :
    distance ((6 * k) • (lr06ABWitness k : Time)) = lr06ABWitness k := by
  have hb := lr06ABWitness_bounds k hk
  have hkR : (0 : ℝ) < k := by exact_mod_cast (show 0 < k by omega)
  have hd : (6 * (k : ℝ) + 1) ≠ 0 := by positivity
  rw [distance, ← AddCircle.coe_nsmul, nsmul_eq_mul]
  have he : ((6 * k : ℕ) : ℝ) * lr06ABWitness k = (k : ℝ) - lr06ABWitness k := by
    dsimp [lr06ABWitness]
    push_cast
    field_simp
    ring
  have hk0 : ((k : ℝ) : Time) = 0 := by simpa using lr06AB_integer_zero (k : ℤ)
  rw [he, AddCircle.coe_sub, hk0, zero_sub, norm_neg]
  have ht0 : 0 ≤ lr06ABWitness k := by linarith
  rw [(AddCircle.norm_coe_eq_abs_iff (1 : ℝ) (by norm_num)).mpr
    (by rw [abs_of_nonneg ht0]; norm_num; linarith), abs_of_nonneg ht0]



theorem lr06FamilyA_scale_one (a b : ℕ) (ha : 0 < a)
    (hp : Primitive (lr06FamilyA a b)) (hML : ML (lr06FamilyA a b) < 1 / 6) :
    a = 1 := by
  apply LRFamilyNormalization.scale_eq_one_of_grid_close a b ha
    (lr06FamilyA_coprime a b hp) (((1 / (6 * (a : ℝ)) : ℝ)) : Time)
  intro j
  simpa only [lr06ABShift, AddCircle.coe_add] using lr06FamilyA_shift_small a b ha hML j


theorem lr06FamilyB_scale_one (a b : ℕ) (ha : 0 < a)
    (hp : Primitive (lr06FamilyB a b)) (hML : ML (lr06FamilyB a b) < 1 / 6) :
    a = 1 := by
  apply LRFamilyNormalization.scale_eq_one_of_grid_close a b ha
    (lr06FamilyB_coprime a b hp) (((1 / (6 * (a : ℝ)) : ℝ)) : Time)
  intro j
  simpa only [lr06ABShift, AddCircle.coe_add] using lr06FamilyB_shift_small a b ha hML j

theorem lr06FamilyA_divisible_six (b : ℕ) (hML : ML (lr06FamilyA 1 b) < 1 / 6) :
    6 ∣ b := by
  apply lr06AB_divisible_six b
  simpa [lr06ABShift] using lr06FamilyA_shift_small 1 b (by norm_num) hML 0

theorem lr06FamilyB_divisible_six (b : ℕ) (hML : ML (lr06FamilyB 1 b) < 1 / 6) :
    6 ∣ b := by
  apply lr06AB_divisible_six b
  simpa [lr06ABShift] using lr06FamilyB_shift_small 1 b (by norm_num) hML 0

theorem lr06FamilyA_ML_lower (k : ℕ) (hk : 1 ≤ k) :
    lr06ABWitness k ≤ ML (lr06FamilyA 1 (6*k)) := by
  apply le_trans _ (lr06AB_score_le_ML _ (lr06ABWitness k : Time))
  have hn : (lr06FamilyA 1 (6*k)).Nonempty := by simp [lr06FamilyA]
  simp only [score, dite_eq_left hn]
  apply Finset.le_inf'
  intro w hw
  simp only [lr06FamilyA, mul_one, Finset.mem_insert, Finset.mem_singleton] at hw
  rcases hw with hw | hw | hw | hw | hw | hw <;> subst w
  · exact lr06AB_witness_structured k _ hk (by simp)
  · exact lr06AB_witness_structured k _ hk (by simp)
  · exact lr06AB_witness_structured k _ hk (by simp)
  · exact lr06AB_witness_structured k _ hk (by simp)