{"id":"82ab85ee-5dfc-4775-b3e1-8abc16e213b9","hotkey":"5GeGrYFpMrNSh3Nwcx987zWz4cME9A9NbCkEbjBvv4uLUScV","public_credit":null,"slug":"green29-green-29","filename":"Main.lean","source":"open scoped Pointwise\n\nprivate def slabCoord {H : Type*} (g : Multiplicative ℤ × H) : ℤ :=\n  Multiplicative.toAdd g.1\n\nprivate def slabOuter (H : Type*) [Group H] [Fintype H] [DecidableEq H] :\n    Finset (Multiplicative ℤ × H) :=\n  ({Multiplicative.ofAdd (-1 : ℤ), Multiplicative.ofAdd (1 : ℤ)} :\n      Finset (Multiplicative ℤ)) ×ˢ (Finset.univ : Finset H)\n\nprivate def slabA (H : Type*) [Group H] [Fintype H] [DecidableEq H] :\n    Finset (Multiplicative ℤ × H) :=\n  slabOuter H ∪ {(Multiplicative.ofAdd (0 : ℤ), 1)}\n\nprivate def slabX (H : Type*) [Group H] [DecidableEq H] :\n    Finset (Multiplicative ℤ × H) :=\n  {(Multiplicative.ofAdd (-1 : ℤ), 1),\n   (Multiplicative.ofAdd (0 : ℤ), 1),\n   (Multiplicative.ofAdd (1 : ℤ), 1)}\n\nprivate lemma slab_mem_iff (H : Type*) [Group H] [Fintype H] [DecidableEq H]\n    (g : Multiplicative ℤ × H) :\n    g ∈ slabA H ↔\n      g.1 = Multiplicative.ofAdd (-1 : ℤ) ∨\n      g.1 = Multiplicative.ofAdd (1 : ℤ) ∨\n      g = (Multiplicative.ofAdd (0 : ℤ), 1) := by\n  simp [slabA, slabOuter] <;> tauto\n\nprivate lemma slabCoord_mul {H : Type*} [Group H]\n    (x y : Multiplicative ℤ × H) :\n    slabCoord (x * y) = slabCoord x + slabCoord y := by\n  simp [slabCoord]\n\nprivate lemma slabCoord_pow {H : Type*} [Group H]\n    (g : Multiplicative ℤ × H) (n : ℕ) :\n    slabCoord (g ^ n) = n • slabCoord g := by\n  simp [slabCoord]\n\nprivate lemma slab_mem_coord_bound (H : Type*) [Group H] [Fintype H] [DecidableEq H]\n    {g : Multiplicative ℤ × H} (hg : g ∈ slabA H) :\n    -1 ≤ slabCoord g ∧ slabCoord g ≤ 1 := by\n  rw [slab_mem_iff] at hg\n  rcases hg with h | h | h\n  · have hc : slabCoord g = -1 := by simp [slabCoord, h]\n    omega\n  · have hc : slabCoord g = 1 := by simp [slabCoord, h]\n    omega\n  · subst g\n    norm_num [slabCoord]\n\nprivate lemma slab_pow_coord_bound (H : Type*) [Group H] [Fintype H] [DecidableEq H]\n    (m : ℕ) {g : Multiplicative ℤ × H} (hg : g ∈ slabA H ^ m) :\n    -(m : ℤ) ≤ slabCoord g ∧ slabCoord g ≤ (m : ℤ) := by\n  induction m generalizing g with\n  | zero =>\n      have h : g = 1 := by simpa using hg\n      subst g\n      simp [slabCoord]\n  | succ m ih =>\n      rw [pow_succ] at hg\n      rcases Finset.mem_mul.mp hg with ⟨x, hx, y, hy, hxy⟩\n      subst g\n      have hx' := ih hx\n      have hy' := slab_mem_coord_bound H hy\n      rw [slabCoord_mul]\n      omega\n\nprivate lemma slabX_mem_of_bounds (H : Type*) [Group H] [DecidableEq H]\n    (z : ℤ) (hl : -1 ≤ z) (hu : z ≤ 1) :\n    (Multiplicative.ofAdd z, 1) ∈ slabX H := by\n  have hz : z = -1 ∨ z = 0 ∨ z = 1 := by omega\n  rcases hz with rfl | rfl | rfl <;> simp [slabX]\n\nprivate lemma slab_neg_one_mem (H : Type*) [Group H] [Fintype H] [DecidableEq H]\n    (h : H) :\n    (Multiplicative.ofAdd (-1 : ℤ), h) ∈ slabA H := by\n  simp [slabA, slabOuter]\n\nprivate lemma slab_one_mem (H : Type*) [Group H] [Fintype H] [DecidableEq H]\n    (h : H) :\n    (Multiplicative.ofAdd (1 : ℤ), h) ∈ slabA H := by\n  simp [slabA, slabOuter]\n\nprivate lemma slab_sq_subset_mul (H : Type*) [Group H] [Fintype H] [DecidableEq H] :\n    slabA H ^ 2 ⊆ slabX H * slabA H := by\n  intro g hg\n  rw [pow_two] at hg\n  rcases Finset.mem_mul.mp hg with ⟨a, ha, b, hb, hab⟩\n  subst g\n  have ha' := slab_mem_coord_bound H ha\n  have hb' := slab_mem_coord_bound H hb\n  let q : ℤ := slabCoord a + slabCoord b\n  have hqlo : -2 ≤ q := by dsimp [q]; omega\n  have hqhi : q ≤ 2 := by dsimp [q]; omega\n  by_cases hq : q ≤ 0\n  · refine Finset.mem_mul.mpr\n      ⟨(Multiplicative.ofAdd (q + 1), 1),\n       slabX_mem_of_bounds H (q + 1) (by omega) (by omega),\n       (Multiplicative.ofAdd (-1 : ℤ), a.2 * b.2),\n       slab_neg_one_mem H (a.2 * b.2), ?_⟩\n    apply Prod.ext\n    · apply Multiplicative.ext\n      simp [q, slabCoord]\n    · simp\n  · refine Finset.mem_mul.mpr\n      ⟨(Multiplicative.ofAdd (q - 1), 1),\n       slabX_mem_of_bounds H (q - 1) (by omega) (by omega),\n       (Multiplicative.ofAdd (1 : ℤ), a.2 * b.2),\n       slab_one_mem H (a.2 * b.2), ?_⟩\n    apply Prod.ext\n    · apply Multiplicative.ext\n      simp [q, slabCoord]\n    · simp\n\nprivate lemma slab_inv_mem_iff (H : Type*) [Group H] [Fintype H] [DecidableEq H]\n    (g : Multiplicative ℤ × H) :\n    g⁻¹ ∈ slabA H ↔ g ∈ slabA H := by\n  have forward : ∀ x : Multiplicative ℤ × H, x⁻¹ ∈ slabA H → x ∈ slabA H := by\n    intro x hx\n    rw [slab_mem_iff] at hx ⊢\n    rcases hx with h | h | h\n    · right\n      left\n      have h' := congrArg Inv.inv h\n      simpa using h'\n    · left\n      have h' := congrArg Inv.inv h\n      simpa using h'\n    · right\n      right\n      have h' := congrArg Inv.inv h\n      simpa using h'\n  constructor\n  · exact forward g\n  · intro hg\n    exact forward (g⁻¹) (by simpa using hg)\n\nprivate lemma slab_inv_eq (H : Type*) [Group H] [Fintype H] [DecidableEq H] :\n    (↑(slabA H) : Set (Multiplicative ℤ × H))⁻¹ = ↑(slabA H) := by\n  ext g\n  simpa using slab_inv_mem_iff H g\n\nprivate lemma slab_isApproximateSubgroup\n    (H : Type*) [Group H] [Fintype H] [DecidableEq H] :\n    IsApproximateSubgroup 3\n      (↑(slabA H) : Set (Multiplicative ℤ × H)) := by\n  refine ⟨?_, slab_inv_eq H, ?_⟩\n  · change (1 : Multiplicative ℤ × H) ∈ slabA H\n    rw [slabA]\n    exact Finset.mem_union_right _ (by simp; rfl)\n  · refine ⟨slabX H, ?_, ?_⟩\n    · have hcard : (slabX H).card ≤ 3 := by\n        unfold slabX\n        exact Finset.card_le_three\n      exact_mod_cast hcard\n    · intro g hg\n      have hg' : g ∈ slabA H ^ 2 := by\n        simpa only [← Finset.coe_pow, Finset.mem_coe] using hg\n      have hm := slab_sq_subset_mul H hg'\n      simpa only [← Finset.mem_coe, Finset.coe_mul, smul_eq_mul] using hm\n\nprivate lemma slab_good_subset_singleton\n    (H : Type*) [Group H] [Fintype H] [DecidableEq H]\n    {S : Finset (Multiplicative ℤ × H)}\n    (hSA : S ⊆ slabA H) (hpow : S ^ 8 ⊆ slabA H ^ 4) :\n    S ⊆ {(Multiplicative.ofAdd (0 : ℤ), 1)} := by\n  intro s hs\n  have hs8 : s ^ 8 ∈ S ^ 8 := Finset.pow_mem_pow (n := 8) hs\n  have hA4 := hpow hs8\n  have hb := slab_pow_coord_bound H 4 hA4\n  rw [slabCoord_pow] at hb\n  norm_num [Int.nsmul_eq_mul] at hb\n  have hzero : slabCoord s = 0 := by omega\n  have hsA := hSA hs\n  rw [slab_mem_iff] at hsA\n  rcases hsA with h | h | h\n  · have hc : slabCoord s = -1 := by simp [slabCoord, h]\n    omega\n  · have hc : slabCoord s = 1 := by simp [slabCoord, h]\n    omega\n  · simpa [h]\n\nprivate lemma slab_good_card_le_one\n    (H : Type*) [Group H] [Fintype H] [DecidableEq H]\n    {S : Finset (Multiplicative ℤ × H)}\n    (hSA : S ⊆ slabA H) (hpow : S ^ 8 ⊆ slabA H ^ 4) :\n    S.card ≤ 1 := by\n  calc\n    S.card ≤ ({(Multiplicative.ofAdd (0 : ℤ), 1)} :\n        Finset (Multiplicative ℤ × H)).card :=\n      Finset.card_le_card (slab_good_subset_singleton H hSA hpow)\n    _ = 1 := by simp\n\nprivate def slabFiber (H : Type*) [Group H] [Fintype H] [DecidableEq H] :\n    Finset (Multiplicative ℤ × H) :=\n  ({Multiplicative.ofAdd (1 : ℤ)} : Finset (Multiplicative ℤ)) ×ˢ\n    (Finset.univ : Finset H)\n\nprivate lemma slabFiber_subset (H : Type*) [Group H] [Fintype H] [DecidableEq H] :\n    slabFiber H ⊆ slabA H := by\n  intro g hg\n  rcases Finset.mem_product.mp hg with ⟨h1, h2⟩\n  apply Finset.mem_union_left\n  exact Finset.mem_product.mpr ⟨Finset.mem_insert_of_mem h1, h2⟩\n\nprivate lemma fintype_card_le_slabA_card\n    (H : Type*) [Group H] [Fintype H] [DecidableEq H] :\n    Fintype.card H ≤ (slabA H).card := by\n  have h := Finset.card_le_card (slabFiber_subset H)\n  simpa [slabFiber] using h\n\ntheorem target : ¬ (fcTypeOfName% \"Green29.green_29\") := by\n  intro h\n  rcases h.mp True.intro with ⟨C, c, hC, hc, hall⟩\n  let α : ℝ := C * (3 : ℝ) ^ (-c)\n  have hα : 0 < α := by\n    dsimp [α]\n    positivity\n  obtain ⟨n : ℕ, hn⟩ := exists_nat_gt (1 / α)\n  let H := ULift (Multiplicative (Fin (n + 1)))\n  let A : Finset (Multiplicative ℤ × H) := slabA H\n  have hApprox : IsApproximateSubgroup (3 : ℝ)\n      (↑A : Set (Multiplicative ℤ × H)) := by\n    dsimp [A]\n    exact slab_isApproximateSubgroup H\n  rcases hall (G := Multiplicative ℤ × H) 3 A (by norm_num) hApprox with\n    ⟨S, hSA, hsize, hpow⟩\n  have hAcardNat : n + 1 ≤ A.card := by\n    calc\n      n + 1 = Fintype.card H := by simp [H]\n      _ ≤ A.card := by\n        dsimp [A]\n        exact fintype_card_le_slabA_card H\n  have hAcardReal : ((n + 1 : ℕ) : ℝ) ≤ (A.card : ℝ) := by\n    exact_mod_cast hAcardNat\n  have h1n : (1 : ℝ) < (n : ℝ) * α := (div_lt_iff₀ hα).mp hn\n  have hnle : (n : ℝ) ≤ ((n + 1 : ℕ) : ℝ) := by norm_num\n  have h1succ : (1 : ℝ) < α * ((n + 1 : ℕ) : ℝ) := by\n    calc\n      1 < (n : ℝ) * α := h1n\n      _ ≤ ((n + 1 : ℕ) : ℝ) * α :=\n        mul_le_mul_of_nonneg_right hnle (le_of_lt hα)\n      _ = α * ((n + 1 : ℕ) : ℝ) := by ring\n  have hSgt : (1 : ℝ) < (S.card : ℝ) := by\n    calc\n      1 < α * ((n + 1 : ℕ) : ℝ) := h1succ\n      _ ≤ α * (A.card : ℝ) :=\n        mul_le_mul_of_nonneg_left hAcardReal (le_of_lt hα)\n      _ ≤ (S.card : ℝ) := by simpa [α] using hsize\n  have hSleNat : S.card ≤ 1 := by\n    apply slab_good_card_le_one H\n    · simpa [A] using hSA\n    · simpa [A] using hpow\n  have hSle : (S.card : ℝ) ≤ 1 := by exact_mod_cast hSleNat\n  linarith\n","proof_sha256":"sha256:cd39995efd69cfa3f64e6dbf93ba236c672a2de0b3d6ea815b718e2c0bfeaa5c","byte_length":9358,"attribution":"conjectures.io"}