← Session 33 — ii′-3b/3c crux + F-D finding; Lagarias letter package
Now the wide pigeonhole — appending after `exists_zero_avoiding_T`.
tool: Edit
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiContour.lean",
"old_string": " have hle : 2 * ((WF.card : \u211d) + 1) \u2264 3 * C0hat (a + 1) := by\n linarith [hWFcard]\n exact le_trans (one_div_le_one_div_of_le hpos hle) h1\n\n/-! ## 4. L1: kernel norm bounds (D-036 \u00a73) -/",
"new_string": " have hle : 2 * ((WF.card : \u211d) + 1) \u2264 3 * C0hat (a + 1) := by\n linarith [hWFcard]\n exact le_trans (one_div_le_one_div_of_le hpos hle) h1\n\n/-! ## 3b. The wide zero-avoiding ordinate (D-071 Finding-2 repair) -/\n\n/-- The wide ordinate window: nontrivial zeros with ordinate in\n[a\u22121, a+2] (the 3-unit window for the Finding-2-extended pigeonhole \u2014\nzeros just outside [a, a+1] can sit at distance < 1/(3\u0108\u2080) from T). -/\ndef zeroWindowWide (a : \u211d) : Set \u2102 :=\n {\u03c1 | IsNontrivialZero \u03c1 \u2227 a - 1 \u2264 \u03c1.im \u2227 \u03c1.im \u2264 a + 2}\n\n/-- Finiteness of the wide window (union of the three unit windows). -/\ntheorem zeroWindowWide_finite (a : \u211d) : (zeroWindowWide a).Finite := by\n apply Set.Finite.subset ((zeroWindow_finite (a - 1)).union\n ((zeroWindow_finite a).union (zeroWindow_finite (a + 1))))\n intro \u03c1 h\u03c1\n obtain \u27e8hz, hlo, hhi\u27e9 := h\u03c1\n by_cases h1 : \u03c1.im \u2264 a\n \u00b7 exact Or.inl \u27e8hz, hlo, h1\u27e9\n \u00b7 by_cases h2 : \u03c1.im \u2264 a + 1\n \u00b7 exact Or.inr (Or.inl \u27e8hz, by linarith, h2\u27e9)\n \u00b7 exact Or.inr (Or.inr \u27e8hz, by linarith, hhi\u27e9)\n\n/-- The wide window's cardinality \u2264 3\u00b7\u0108\u2080(a+2) (three unit windows via\nthe perimeter + `C0hat_mono`). -/\ntheorem zeroWindowWide_card_le (hZC : ZeroCountProp) {a : \u211d} (ha : 3 \u2264 a) :\n ((zeroWindowWide_finite a).toFinset.card : \u211d) \u2264 3 * C0hat (a + 2) := by\n have hsub : (zeroWindowWide_finite a).toFinset \u2286\n (zeroWindow_finite (a - 1)).toFinset \u222a\n ((zeroWindow_finite a).toFinset \u222a (zeroWindow_finite (a + 1)).toFinset) := by\n intro \u03c1 h\u03c1\n have hmem : \u03c1 \u2208 zeroWindowWide a := (zeroWindowWide_finite a).mem_toFinset.mpr h\u03c1\n obtain \u27e8hz, hlo, hhi\u27e9 := hmem\n by_cases h1 : \u03c1.im \u2264 a\n \u00b7 exact Finset.mem_union.mpr (Or.inl\n ((zeroWindow_finite (a - 1)).mem_toFinset.mpr \u27e8hz, hlo, h1\u27e9))\n \u00b7 by_cases h2 : \u03c1.im \u2264 a + 1\n \u00b7 exact Finset.mem_union.mpr (Or.inr (Finset.mem_union.mpr (Or.inl\n ((zeroWindow_finite a).mem_toFinset.mpr \u27e8hz, by linarith, h2\u27e9))))\n \u00b7 exact Finset.mem_union.mpr (Or.inr (Finset.mem_union.mpr (Or.inr\n ((zeroWindow_finite (a + 1)).mem_toFinset.mpr \u27e8hz, by linarith, hhi\u27e9))))\n have hsum1 : (\u2211 \u03c1 \u2208 (zeroWindowWide_finite a).toFinset, (zeroMult \u03c1 : \u211d)) \u2264\n \u2211 \u03c1 \u2208 ((zeroWindow_finite (a - 1)).toFinset \u222a\n ((zeroWindow_finite a).toFinset \u222a (zeroWindow_finite (a + 1)).toFinset)),\n (zeroMult \u03c1 : \u211d) :=\n Finset.sum_le_sum_of_subset_of_nonneg hsub (fun \u03c1 _ => Nat.cast_nonneg _)\n have hsum2 : (\u2211 \u03c1 \u2208 ((zeroWindow_finite (a - 1)).toFinset \u222a\n ((zeroWindow_finite a).toFinset \u222a (zeroWindow_finite (a + 1)).toFinset)),\n (zeroMult \u03c1 : \u211d)) \u2264\n (\u2211 \u03c1 \u2208 (zeroWindow_finite (a - 1)).toFinset, (zeroMult \u03c1 : \u211d)) +\n ((\u2211 \u03c1 \u2208 (zeroWindow_finite a).toFinset, (zeroMult \u03c1 : \u211d)) +\n (\u2211 \u03c1 \u2208 (zeroWindow_finite (a + 1)).toFinset, (zeroMult \u03c1 : \u211d))) := by\n have hu1 := Finset.sum_union_inter (s := (zeroWindow_finite (a - 1)).toFinset)\n (t := (zeroWindow_finite a).toFinset \u222a (zeroWindow_finite (a + 1)).toFinset)\n (f := fun \u03c1 => (zeroMult \u03c1 : \u211d))\n have hnn : (0 : \u211d) \u2264 \u2211 \u03c1 \u2208 (zeroWindow_finite (a - 1)).toFinset \u2229\n ((zeroWindow_finite a).toFinset \u222a (zeroWindow_finite (a + 1)).toFinset),\n (zeroMult \u03c1 : \u211d) :=\n Finset.sum_nonneg (fun \u03c1 _ => Nat.cast_nonneg _)\n have hu2 := Finset.sum_union_inter (s := (zeroWindow_finite a).toFinset)\n (t := (zeroWindow_finite (a + 1)).toFinset) (f := fun \u03c1 => (zeroMult \u03c1 : \u211d))\n have hnn2 : (0 : \u211d) \u2264 \u2211 \u03c1 \u2208 (zeroWindow_finite a).toFinset \u2229\n (zeroWindow_finite (a + 1)).toFinset, (zeroMult \u03c1 : \u211d) :=\n Finset.sum_nonneg (fun \u03c1 _ => Nat.cast_nonneg _)\n linarith\n have h1 := hZC (a - 1) (by linarith)\n have h2 := hZC a (by linarith)\n have h3 := hZC (a + 1) (by linarith)\n have hmono1 : C0hat a \u2264 C0hat (a + 2) := C0hat_mono (by linarith) (by linarith)\n have hmono2 : C0hat (a + 1) \u2264 C0hat (a + 2) := C0hat_mono (by linarith) (by linarith)\n have hcard_le_sum : ((zeroWindowWide_finite a).toFinset.card : \u211d) \u2264\n \u2211 \u03c1 \u2208 (zeroWindowWide_finite a).toFinset, (zeroMult \u03c1 : \u211d) := by\n rw [show ((zeroWindowWide_finite a).toFinset.card : \u211d) =\n \u2211 _\u03c1 \u2208 (zeroWindowWide_finite a).toFinset, (1 : \u211d) by simp]\n apply Finset.sum_le_sum\n intro \u03c1 h\u03c1\n exact_mod_cast one_le_zeroMult (((zeroWindowWide_finite a).mem_toFinset.mp h\u03c1).1)\n calc ((zeroWindowWide_finite a).toFinset.card : \u211d)\n \u2264 \u2211 \u03c1 \u2208 (zeroWindowWide_finite a).toFinset, (zeroMult \u03c1 : \u211d) := hcard_le_sum\n _ \u2264 C0hat a + C0hat (a + 1) + C0hat (a + 2) := by linarith [hsum1, hsum2, h1, h2, h3]\n _ \u2264 3 * C0hat (a + 2) := by linarith [hmono1, hmono2]\n\n/-- **L3-wide** (D-071 Finding-2 repair): given the perimeter count\nbound, every unit window [a, a+1] with a \u2265 3 contains an ordinate T at\ndistance \u2265 1/(9\u00b7\u0108\u2080(a+2)) from EVERY zero ordinate in the 3-unit window\n(a\u22121, a+2) \u2014 covering the zeros just outside [a, a+1] that the plain\nL3 clearance misses. -/\ntheorem exists_zero_avoiding_T_wide (hZC : ZeroCountProp) {a : \u211d} (ha : 3 \u2264 a) :\n \u2203 T : \u211d, a \u2264 T \u2227 T \u2264 a + 1 \u2227\n \u2200 \u03c1 : \u2102, IsNontrivialZero \u03c1 \u2192 a - 1 < \u03c1.im \u2192 \u03c1.im < a + 2 \u2192\n 1 / (9 * C0hat (a + 2)) \u2264 |\u03c1.im - T| := by\n classical\n have hfin := zeroWindowWide_finite a\n set WF : Finset \u2102 := hfin.toFinset with hWF_def\n have hWFmem : \u2200 \u03c1 : \u2102, \u03c1 \u2208 WF \u2194 \u03c1 \u2208 zeroWindowWide a :=\n fun \u03c1 => Set.Finite.mem_toFinset hfin\n set S : Finset \u211d := WF.image Complex.im with hS_def\n have hScard : S.card \u2264 WF.card := Finset.card_image_le\n have hWFcard : (WF.card : \u211d) \u2264 3 * C0hat (a + 2) := zeroWindowWide_card_le hZC ha\n obtain \u27e8T, hT1, hT2, hT3\u27e9 := exists_avoiding_midpoint a S hScard\n refine \u27e8T, hT1, hT2, fun \u03c1 h\u03c1 h\u03c1lo h\u03c1hi => ?_\u27e9\n have h\u03c1mem : \u03c1 \u2208 WF := (hWFmem \u03c1).mpr \u27e8h\u03c1, by linarith, by linarith\u27e9\n have himmem : \u03c1.im \u2208 S := Finset.mem_image.mpr \u27e8\u03c1, h\u03c1mem, rfl\u27e9\n have h1 := hT3 \u03c1.im himmem\n have hC : 2 \u2264 C0hat (a + 2) := two_le_C0hat (by linarith)\n have hpos : (0:\u211d) < 2 * ((WF.card : \u211d) + 1) := by positivity\n have hle : 2 * ((WF.card : \u211d) + 1) \u2264 9 * C0hat (a + 2) := by\n linarith [hWFcard, hC]\n exact le_trans (one_div_le_one_div_of_le hpos hle) h1\n\n/-! ## 4. L1: kernel norm bounds (D-036 \u00a73) -/"
}
raw content_json (database row)
[{"type":"text","text":"Now the wide pigeonhole — appending after `exists_zero_avoiding_T`."},{"type":"tool_use","id":"Edit_255","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiContour.lean","old_string":" have hle : 2 * ((WF.card : ℝ) + 1) ≤ 3 * C0hat (a + 1) := by\n linarith [hWFcard]\n exact le_trans (one_div_le_one_div_of_le hpos hle) h1\n\n/-! ## 4. L1: kernel norm bounds (D-036 §3) -/","new_string":" have hle : 2 * ((WF.card : ℝ) + 1) ≤ 3 * C0hat (a + 1) := by\n linarith [hWFcard]\n exact le_trans (one_div_le_one_div_of_le hpos hle) h1\n\n/-! ## 3b. The wide zero-avoiding ordinate (D-071 Finding-2 repair) -/\n\n/-- The wide ordinate window: nontrivial zeros with ordinate in\n[a−1, a+2] (the 3-unit window for the Finding-2-extended pigeonhole —\nzeros just outside [a, a+1] can sit at distance < 1/(3Ĉ₀) from T). -/\ndef zeroWindowWide (a : ℝ) : Set ℂ :=\n {ρ | IsNontrivialZero ρ ∧ a - 1 ≤ ρ.im ∧ ρ.im ≤ a + 2}\n\n/-- Finiteness of the wide window (union of the three unit windows). -/\ntheorem zeroWindowWide_finite (a : ℝ) : (zeroWindowWide a).Finite := by\n apply Set.Finite.subset ((zeroWindow_finite (a - 1)).union\n ((zeroWindow_finite a).union (zeroWindow_finite (a + 1))))\n intro ρ hρ\n obtain ⟨hz, hlo, hhi⟩ := hρ\n by_cases h1 : ρ.im ≤ a\n · exact Or.inl ⟨hz, hlo, h1⟩\n · by_cases h2 : ρ.im ≤ a + 1\n · exact Or.inr (Or.inl ⟨hz, by linarith, h2⟩)\n · exact Or.inr (Or.inr ⟨hz, by linarith, hhi⟩)\n\n/-- The wide window's cardinality ≤ 3·Ĉ₀(a+2) (three unit windows via\nthe perimeter + `C0hat_mono`). -/\ntheorem zeroWindowWide_card_le (hZC : ZeroCountProp) {a : ℝ} (ha : 3 ≤ a) :\n ((zeroWindowWide_finite a).toFinset.card : ℝ) ≤ 3 * C0hat (a + 2) := by\n have hsub : (zeroWindowWide_finite a).toFinset ⊆\n (zeroWindow_finite (a - 1)).toFinset ∪\n ((zeroWindow_finite a).toFinset ∪ (zeroWindow_finite (a + 1)).toFinset) := by\n intro ρ hρ\n have hmem : ρ ∈ zeroWindowWide a := (zeroWindowWide_finite a).mem_toFinset.mpr hρ\n obtain ⟨hz, hlo, hhi⟩ := hmem\n by_cases h1 : ρ.im ≤ a\n · exact Finset.mem_union.mpr (Or.inl\n ((zeroWindow_finite (a - 1)).mem_toFinset.mpr ⟨hz, hlo, h1⟩))\n · by_cases h2 : ρ.im ≤ a + 1\n · exact Finset.mem_union.mpr (Or.inr (Finset.mem_union.mpr (Or.inl\n ((zeroWindow_finite a).mem_toFinset.mpr ⟨hz, by linarith, h2⟩))))\n · exact Finset.mem_union.mpr (Or.inr (Finset.mem_union.mpr (Or.inr\n ((zeroWindow_finite (a + 1)).mem_toFinset.mpr ⟨hz, by linarith, hhi⟩))))\n have hsum1 : (∑ ρ ∈ (zeroWindowWide_finite a).toFinset, (zeroMult ρ : ℝ)) ≤\n ∑ ρ ∈ ((zeroWindow_finite (a - 1)).toFinset ∪\n ((zeroWindow_finite a).toFinset ∪ (zeroWindow_finite (a + 1)).toFinset)),\n (zeroMult ρ : ℝ) :=\n Finset.sum_le_sum_of_subset_of_nonneg hsub (fun ρ _ => Nat.cast_nonneg _)\n have hsum2 : (∑ ρ ∈ ((zeroWindow_finite (a - 1)).toFinset ∪\n ((zeroWindow_finite a).toFinset ∪ (zeroWindow_finite (a + 1)).toFinset)),\n (zeroMult ρ : ℝ)) ≤\n (∑ ρ ∈ (zeroWindow_finite (a - 1)).toFinset, (zeroMult ρ : ℝ)) +\n ((∑ ρ ∈ (zeroWindow_finite a).toFinset, (zeroMult ρ : ℝ)) +\n (∑ ρ ∈ (zeroWindow_finite (a + 1)).toFinset, (zeroMult ρ : ℝ))) := by\n have hu1 := Finset.sum_union_inter (s := (zeroWindow_finite (a - 1)).toFinset)\n (t := (zeroWindow_finite a).toFinset ∪ (zeroWindow_finite (a + 1)).toFinset)\n (f := fun ρ => (zeroMult ρ : ℝ))\n have hnn : (0 : ℝ) ≤ ∑ ρ ∈ (zeroWindow_finite (a - 1)).toFinset ∩\n ((zeroWindow_finite a).toFinset ∪ (zeroWindow_finite (a + 1)).toFinset),\n (zeroMult ρ : ℝ) :=\n Finset.sum_nonneg (fun ρ _ => Nat.cast_nonneg _)\n have hu2 := Finset.sum_union_inter (s := (zeroWindow_finite a).toFinset)\n (t := (zeroWindow_finite (a + 1)).toFinset) (f := fun ρ => (zeroMult ρ : ℝ))\n have hnn2 : (0 : ℝ) ≤ ∑ ρ ∈ (zeroWindow_finite a).toFinset ∩\n (zeroWindow_finite (a + 1)).toFinset, (zeroMult ρ : ℝ) :=\n Finset.sum_nonneg (fun ρ _ => Nat.cast_nonneg _)\n linarith\n have h1 := hZC (a - 1) (by linarith)\n have h2 := hZC a (by linarith)\n have h3 := hZC (a + 1) (by linarith)\n have hmono1 : C0hat a ≤ C0hat (a + 2) := C0hat_mono (by linarith) (by linarith)\n have hmono2 : C0hat (a + 1) ≤ C0hat (a + 2) := C0hat_mono (by linarith) (by linarith)\n have hcard_le_sum : ((zeroWindowWide_finite a).toFinset.card : ℝ) ≤\n ∑ ρ ∈ (zeroWindowWide_finite a).toFinset, (zeroMult ρ : ℝ) := by\n rw [show ((zeroWindowWide_finite a).toFinset.card : ℝ) =\n ∑ _ρ ∈ (zeroWindowWide_finite a).toFinset, (1 : ℝ) by simp]\n apply Finset.sum_le_sum\n intro ρ hρ\n exact_mod_cast one_le_zeroMult (((zeroWindowWide_finite a).mem_toFinset.mp hρ).1)\n calc ((zeroWindowWide_finite a).toFinset.card : ℝ)\n ≤ ∑ ρ ∈ (zeroWindowWide_finite a).toFinset, (zeroMult ρ : ℝ) := hcard_le_sum\n _ ≤ C0hat a + C0hat (a + 1) + C0hat (a + 2) := by linarith [hsum1, hsum2, h1, h2, h3]\n _ ≤ 3 * C0hat (a + 2) := by linarith [hmono1, hmono2]\n\n/-- **L3-wide** (D-071 Finding-2 repair): given the perimeter count\nbound, every unit window [a, a+1] with a ≥ 3 contains an ordinate T at\ndistance ≥ 1/(9·Ĉ₀(a+2)) from EVERY zero ordinate in the 3-unit window\n(a−1, a+2) — covering the zeros just outside [a, a+1] that the plain\nL3 clearance misses. -/\ntheorem exists_zero_avoiding_T_wide (hZC : ZeroCountProp) {a : ℝ} (ha : 3 ≤ a) :\n ∃ T : ℝ, a ≤ T ∧ T ≤ a + 1 ∧\n ∀ ρ : ℂ, IsNontrivialZero ρ → a - 1 < ρ.im → ρ.im < a + 2 →\n 1 / (9 * C0hat (a + 2)) ≤ |ρ.im - T| := by\n classical\n have hfin := zeroWindowWide_finite a\n set WF : Finset ℂ := hfin.toFinset with hWF_def\n have hWFmem : ∀ ρ : ℂ, ρ ∈ WF ↔ ρ ∈ zeroWindowWide a :=\n fun ρ => Set.Finite.mem_toFinset hfin\n set S : Finset ℝ := WF.image Complex.im with hS_def\n have hScard : S.card ≤ WF.card := Finset.card_image_le\n have hWFcard : (WF.card : ℝ) ≤ 3 * C0hat (a + 2) := zeroWindowWide_card_le hZC ha\n obtain ⟨T, hT1, hT2, hT3⟩ := exists_avoiding_midpoint a S hScard\n refine ⟨T, hT1, hT2, fun ρ hρ hρlo hρhi => ?_⟩\n have hρmem : ρ ∈ WF := (hWFmem ρ).mpr ⟨hρ, by linarith, by linarith⟩\n have himmem : ρ.im ∈ S := Finset.mem_image.mpr ⟨ρ, hρmem, rfl⟩\n have h1 := hT3 ρ.im himmem\n have hC : 2 ≤ C0hat (a + 2) := two_le_C0hat (by linarith)\n have hpos : (0:ℝ) < 2 * ((WF.card : ℝ) + 1) := by positivity\n have hle : 2 * ((WF.card : ℝ) + 1) ≤ 9 * C0hat (a + 2) := by\n linarith [hWFcard, hC]\n exact le_trans (one_div_le_one_div_of_le hpos hle) h1\n\n/-! ## 4. L1: kernel norm bounds (D-036 §3) -/"},"extra_content":null}]