← Session 33 — ii′-3b/3c crux + F-D finding; Lagarias letter package
thinking (19155 chars)
Now §2: the bridge `zeroSum_norm_le_four_FAlt_add_one`. Append before `end NguyenRH1`:
```lean
/-! ## 2. The bridge -/
/-- The per-term bound on the line: |1 − (ρ/(ρ−1))ⁿ| ≤ 2 when re ρ = 1/2
(|ρ| = |1−ρ| then). -/
lemma zeroTerm_norm_le_two {ρ : ℂ} (hρ : IsNontrivialZero ρ) (hre : ρ.re = 1 / 2) (n : ℕ) :
‖(zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n)‖ ≤ 2 * (zeroMult ρ : ℝ) := by
...
```
Proof: ‖ρ‖² = re² + im² = 1/4 + γ²; ‖ρ−1‖² = (re−1)² + im² = 1/4 + γ². So ‖ρ/(ρ−1)‖ = 1 (ρ ≠ 1 since nontrivial re < 1; ρ − 1 ≠ 0). Then ‖(ρ/(ρ−1))ⁿ‖ = 1, ‖1 − (ρ/(ρ−1))ⁿ‖ ≤ ‖1‖ + 1 = 2. Term norm: ‖mult‖ · ‖1 − ...‖ = mult · ‖1−...‖ ≤ mult·2 = 2·mult.
```lean
have hρ1 : ρ - 1 ≠ 0 := by
intro h
have : ρ = 1 := sub_eq_zero.mp h
rw [this, Complex.one_re] at hre
norm_num at hre
have hnorm_ratio : ‖ρ / (ρ - 1)‖ = 1 := by
rw [norm_div]
have h1 : ‖ρ‖ = ‖ρ - 1‖ := by
have hsq : ‖ρ‖ ^ 2 = ‖ρ - 1‖ ^ 2 := by
rw [← Complex.normSq_eq_norm_sq, ← Complex.normSq_eq_norm_sq]
rw [Complex.normSq_apply, Complex.normSq_apply, hre]
simp [sub_re, one_re, sub_im]
ring
exact (sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _)).mp hsq
rw [h1, div_self (norm_pos_iff.mpr hρ1)]
```
Hmm — sq_eq_sq₀ : 0 ≤ a → 0 ≤ b → (a² = b² ↔ a = b): `sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _) |>.mp hsq` ✓ (exists? — there's `sq_eq_sq₀`... alternatively `pow_left_injective₀`. Or use the norm_div_sub_one_le_one pattern from LiContour:271-287 — they proved ‖s/(s−1)‖ ≤ 1 for re s ≤ 1/2 via normSq. For EQUALITY at re = 1/2: same computation with = instead of ≤. Let me mirror LiContour's norm_div_sub_one_le_one:
```lean
have hnorm : ‖ρ‖ = ‖ρ - 1‖ := by
have h : ‖ρ‖ ^ 2 = ‖ρ - 1‖ ^ 2 := by
rw [← Complex.normSq_eq_norm_sq, ← Complex.normSq_eq_norm_sq]
rw [Complex.normSq_apply ρ, Complex.normSq_apply (ρ - 1), hre]
simp only [sub_re, one_re, sub_im, one_im, sub_zero]
ring
exact (sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _)).mp h
```
Hmm — Complex.normSq_apply: normSq z = z.re*z.re + z.im*z.im ✓ with hre (re = 1/2): LHS = (1/2)² + im²; RHS = (1/2−1)² + im²: ring ✓. sq_eq_sq₀ — check name: `sq_eq_sq₀ : 0 ≤ a → 0 ≤ b → (a ^ 2 = b ^ 2 ↔ a = b)` ✓ exists (used in LiContour:284 as sq_le_sq₀ — for the eq version: `sq_eq_sq₀`? or `(pow_left_injective₀ ...).eq_iff`? LiContour:284 used `sq_le_sq₀ (norm_nonneg _) (norm_nonneg _) |>.mp h` for the ≤ version. For equality: `sq_eq_sq₀` — hmm — safer: (pow_left_injective₀ (norm_nonneg _) (norm_nonneg _) two_ne_zero).eq_iff? There's `pow_left_injective₀ : 0 ≤ a → 0 ≤ b → n ≠ 0 → (a ^ n = b ^ n ↔ a = b)`? Hmm. Alternative: `abs_of_nonneg`: ‖ρ‖ = ‖ρ−1‖ ⟺ ‖ρ‖² = ‖ρ−1‖² with nonneg: use `sq_eq_sq₀` if it exists else:
```lean
exact pow_left_injective₀ (norm_nonneg _) (norm_nonneg _) two_ne_zero h
```
pow_left_injective₀ : 0 ≤ a → 0 ≤ b → n ≠ 0 → a^n = b^n → a = b? Signature: `pow_left_injective₀ (ha : 0 ≤ a) (hb : 0 ≤ b) (hn : n ≠ 0) : a ^ n = b ^ n → a = b`? I think it's `pow_left_injective₀ : 0 ≤ x → 0 ≤ y → x ^ n = y ^ n → n ≠ 0 → x = y`? Ugh. Let me use: `sq_eq_sq₀` — I'm fairly confident it exists in Mathlib (Algebra.Order... `sq_eq_sq₀ : 0 ≤ a → 0 ≤ b → a ^ 2 = b ^ 2 ↔ a = b`? hmm — actually the iff form: `sq_eq_sq₀ (ha : 0 ≤ a) (hb : 0 ≤ b) : a ^ 2 = b ^ 2 ↔ a = b`? There's `sq_eq_sq'`... Let me just probe it in the build.
Then:
```lean
calc ‖(zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n)‖
= (zeroMult ρ : ℝ) * ‖1 - (ρ / (ρ - 1)) ^ n‖ := by
rw [norm_mul, RCLike.norm_natCast]
_ ≤ (zeroMult ρ : ℝ) * 2 := by
apply mul_le_mul_of_nonneg_left _ (Nat.cast_nonneg _)
calc ‖1 - (ρ / (ρ - 1)) ^ n‖
≤ ‖(1 : ℂ)‖ + ‖(ρ / (ρ - 1)) ^ n‖ := norm_sub_le _ _
_ = 1 + 1 := by rw [norm_one, norm_pow, hnorm_ratio, one_pow]
_ = 2 := by norm_num
_ = 2 * (zeroMult ρ : ℝ) := by ring
```
Then the sum:
```lean
lemma zeroSum_nontriv_norm_le (hRH : RHUpTo (3 * 10 ^ 12)) {n : ℕ} {T : ℝ}
(hTle : T ≤ 3 * 10 ^ 12) :
‖∑ ρ ∈ (zeroBothWindow_finite T).toFinset,
(zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n)‖ ≤
2 * ∑ ρ ∈ (zeroBothWindow_finite T).toFinset, (zeroMult ρ : ℝ) := by
calc ‖∑ ρ ∈ (zeroBothWindow_finite T).toFinset,
(zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n)‖
≤ ∑ ρ ∈ (zeroBothWindow_finite T).toFinset,
‖(zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n)‖ := norm_sum_le _ _
_ ≤ ∑ ρ ∈ (zeroBothWindow_finite T).toFinset, 2 * (zeroMult ρ : ℝ) := by
apply Finset.sum_le_sum
intro ρ hρ
have hnt : IsNontrivialZero ρ := ((zeroBothWindow_finite T).mem_toFinset.mp hρ).1
have him : |ρ.im| ≤ T := ((zeroBothWindow_finite T).mem_toFinset.mp hρ).2
have hre : ρ.re = 1 / 2 := hRH ρ hnt (by linarith [him, hTle] : |ρ.im| ≤ 3 * 10 ^ 12)
exact zeroTerm_norm_le_two hnt hre n
_ = 2 * ∑ ρ ∈ (zeroBothWindow_finite T).toFinset, (zeroMult ρ : ℝ) := by
rw [Finset.mul_sum]
```
norm_sum_le : ‖∑ x ∈ s, f x‖ ≤ ∑ x ∈ s, ‖f x‖ ✓ (check exact name: `norm_sum_le (s : Finset ι) (f : ι → α) : ‖∑ x ∈ s, f x‖ ≤ ∑ x ∈ s, ‖f x‖` ✓). Finset.mul_sum : a * ∑ f = ∑ a * f — direction: ∑ x, 2 * g x = 2 * ∑ g: rw [Finset.mul_sum] rewrites 2 * ∑ → ∑ 2 * ... hmm — the goal's RHS is 2 * ∑ ... and I want to END there: the calc's last step: ∑ 2·mult = 2·∑ mult — Finset.mul_sum : b * ∑ x ∈ s, f x = ∑ x ∈ s, b * f x — rw [Finset.mul_sum] on goal `∑ 2·mult = 2·∑ mult` rewrites the RHS `2 * ∑` → `∑ 2·mult` ✓ closes by rfl.
Then the both-signs count:
```lean
lemma zeroBothWindow_sum_eq_two_mul (hNLZ : NoLowZeros) (T : ℝ) :
∑ ρ ∈ (zeroBothWindow_finite T).toFinset, (zeroMult ρ : ℝ) =
2 * ∑ ρ ∈ (zeroGlobalWindow_finite T).toFinset, (zeroMult ρ : ℝ) := by
classical
set P := (zeroGlobalWindow_finite T).toFinset with hP
set N := (zeroGlobalWindowNeg_finite T).toFinset with hN
have hW : (zeroBothWindow_finite T).toFinset = P ∪ N := by
ext ρ
rw [Finset.mem_union, (zeroBothWindow_finite T).mem_toFinset,
(zeroGlobalWindow_finite T).mem_toFinset, (zeroGlobalWindowNeg_finite T).mem_toFinset]
constructor
· intro ⟨hnt, himT⟩
have him0 : ρ.im ≠ 0 := by
have h14 := hNLZ ρ hnt
intro h
rw [h, abs_zero] at h14
exact (by norm_num : ¬ (14 : ℝ) ≤ 0) h14
rcases lt_or_gt_of_ne him0 with hneg | hpos
· exact Or.inr ⟨hnt, by linarith [abs_le.mp himT |>.1], hneg⟩
· exact Or.inl ⟨hnt, hpos, by linarith [abs_le.mp himT |>.2]⟩
· intro h
rcases h with ⟨hnt, hpos, himT⟩ | ⟨hnt, himT, hneg⟩
· exact ⟨hnt, by rw [abs_of_pos hpos]; exact himT⟩
· exact ⟨hnt, by rw [abs_of_neg hneg]; linarith⟩
rw [hW]
have hdisj : Disjoint P N := by
rw [Finset.disjoint_left]
intro ρ hρP hρN
have h1 : 0 < ρ.im := ((zeroGlobalWindow_finite T).mem_toFinset.mp hρP).2.1
have h2 : ρ.im < 0 := ((zeroGlobalWindowNeg_finite T).mem_toFinset.mp hρN).2.2
linarith
rw [Finset.sum_union hdisj]
-- Σ over N = Σ over P via conj
have hNsum : (∑ ρ ∈ N, (zeroMult ρ : ℝ)) = ∑ ρ ∈ P, (zeroMult ρ : ℝ) := by
have himg : N = P.image ⟨(starRingEnd ℂ), isNontrivialZero_conj⟩ := by
ext ρ
rw [Finset.mem_image, (zeroGlobalWindowNeg_finite T).mem_toFinset,
(zeroGlobalWindow_finite T).mem_toFinset]
constructor
· intro ⟨hnt, himT, hneg⟩
refine ⟨(starRingEnd ℂ) ρ, ⟨isNontrivialZero_conj hnt, ?_, ?_⟩, ?_⟩
· rw [Complex.conj_im]
exact neg_pos.mpr hneg
· rw [Complex.conj_im]
linarith
· rw [starRingEnd_apply, starRingEnd_apply, star_star]
· rintro ⟨σ, ⟨hσnt, hσpos, hσT⟩, rfl⟩
refine ⟨isNontrivialZero_conj hσnt, ?_, ?_⟩
· rw [Complex.conj_im]
linarith
· rw [Complex.conj_im]
exact neg_neg_of_pos hσpos -- hmm: (conj σ).im = −σ.im < 0 ⟸ σ.im > 0
rw [himg]
rw [Finset.sum_image (fun ρ _ σ _ h => starRingEnd_injective.injective h)]
-- hmm: sum over image = sum over P of mult (conj ρ) = mult ρ (zeroMult_conj)
apply Finset.sum_congr rfl
intro ρ hρ
exact_mod_cast zeroMult_conj (((zeroGlobalWindow_finite T).mem_toFinset.mp hρ).1)
linarith [hNsum]
```
Hmm — the image form: P.image ⟨conj, proof⟩ — Finset.image needs an EMBEDDING (Function.Embedding): ⟨(starRingEnd ℂ), isNontrivialZero_conj⟩ — that's not an embedding (isNontrivialZero_conj is the nontrivial-zero proof, not injectivity!). The embedding for conj: `Function.Embedding (starRingEnd ℂ) ?inj` — there's `starRingEnd_injective`? or use `Equiv` — conj is an equiv: starRingEquiv? For Finset.image with equiv: `Finset.image (starRingEnd ℂ)`? Finset.image takes an embedding: `⟨(starRingEnd ℂ), injective⟩` with injective : Function.Injective (starRingEnd ℂ) — starRingEnd is an involution hence injective: `starRingEnd_injective`? or `starRingEquiv.injective`. In Mathlib: `starRingEnd_injective : Function.Injective (starRingEnd R)`? There's `starRingEquiv : R ≃+* R` with .injective. Hmm — LiMoments used conjZeroEquiv (subtype equiv) with Finset-free tsum reindex. For Finset: simplest is Finset.image with the embedding `⟨(starRingEnd ℂ), starRingEnd_injective⟩` — check if starRingEnd_injective exists: likely `starRingEnd_injective` or use `starRingEquiv.injective`.
And the sum over the image: Finset.sum_image : (∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y) → ∑ x ∈ s.image f, g x = ∑ x ∈ s, g (f x). With g := zeroMult: ∑ ρ ∈ image conj P, zeroMult ρ = ∑ ρ ∈ P, zeroMult (conj ρ) = ∑ ρ ∈ P, zeroMult ρ (zeroMult_conj) ✓.
hmm — zeroMult_conj's statement (LiTightR:2294): zeroMult ((starRingEnd ℂ) ρ) = zeroMult ρ — for ρ with IsNontrivialZero? It takes (hρ : IsNontrivialZero ρ)? Looking at LiTightR:2294-2299: `lemma zeroMult_conj {ρ : ℂ} (hρ : IsNontrivialZero ρ) : zeroMult ((starRingEnd ℂ) ρ) = zeroMult ρ` — takes hρ ✓. exact_mod_cast zeroMult_conj hρ-proof — the sum terms are (zeroMult ρ : ℝ) casts: zeroMult_conj gives the ℕ equality: cast both sides ✓ exact_mod_cast.
For the negative-side membership backward direction ((conj σ).im < 0): (conj σ).im = −σ.im < 0 ⟸ σ.im > 0: `neg_neg_of_pos`? that's a ≠ 0. Use: rw [Complex.conj_im]; linarith.
And the embedding: let me define conjEmb : Function.Embedding := ⟨(starRingEnd ℂ), starRingEnd_injective⟩? — probe `starRingEnd_injective`. Alternative: `starRingEquiv ℂ`? In Mathlib: `starRingEquiv : R ≃+* R` — for R a star ring with commutative... `starRingEquiv : R ≃ R`? There's `starRingEquiv : R ≃+* R` (the star ring equiv). Its .toFun = starRingEnd. So `starRingEquiv.injective`. Hmm — for ℂ: `Complex.starRingEquiv`? or just `starRingEquiv`? Let me probe in the build.
Then the triv:
```lean
lemma trivTerm_norm_le_one (n : ℕ) :
‖(zeroMult (-2 : ℂ) : ℂ) * (1 - ((-2 : ℂ) / (-2 - 1)) ^ n)‖ ≤ 1 := by
rw [zeroMult_neg_two]
-- (−2)/(−3) = 2/3: term = 1 − (2/3)ⁿ ∈ [0, 1)
have e : (-2 : ℂ) / (-2 - 1) = 2 / 3 := by norm_num
rw [e]
...
```
Hmm — (−2)/(−2−1) = (−2)/(−3) = 2/3 ✓ norm_num proves? (−2:ℂ)/(−3:ℂ) = 2/3: field_simp + norm_num ✓ `by norm_num`. Then term: (1:ℂ)·(1 − (2/3)ⁿ): ‖1 − (2/3)ⁿ‖: (2/3 : ℂ) is real positive: (2/3)ⁿ real positive ≤ 1: 1 − (2/3)ⁿ ∈ [0, 1): ‖·‖ = 1 − (2/3)ⁿ ≤ 1:
```lean
have h23 : ((2 : ℂ) / 3) = ((2 / 3 : ℝ) : ℂ) := by push_cast; ring
rw [h23, ← ofReal_pow] -- hmm
```
Simpler: show 0 ≤ (2/3:ℂ) and (2/3:ℂ) ≤ 1 via the ofReal cast:
```lean
have h1 : (0 : ℝ) ≤ (2 / 3 : ℝ) := by norm_num
have h2 : (2 / 3 : ℝ) ≤ 1 := by norm_num
have h3 : ‖(1 : ℂ) - ((2 : ℂ) / 3) ^ n‖ = 1 - (2 / 3 : ℝ) ^ n := by
have hpow : (0 : ℝ) ≤ (2 / 3 : ℝ) ^ n := pow_nonneg h1 n
have hpow1 : (2 / 3 : ℝ) ^ n ≤ 1 := pow_le_one₀ h1 h2 n
have e : ((2 : ℂ) / 3) = ((2 / 3 : ℝ) : ℂ) := by push_cast; ring
rw [e, ← ofReal_pow, ← ofReal_one, ← ofReal_sub, Complex.norm_real, Real.norm_eq_abs,
abs_of_nonneg (by linarith)]
rw [h1', h3] -- hmm the mult part: zeroMult_neg_two gives zeroMult (-2) = 1: (zeroMult (-2:ℂ) : ℂ) = 1
...
```
Getting long. The full bridge:
```lean
theorem zeroSum_norm_le_four_FAlt_add_one (hRH : RHUpTo (3 * 10 ^ 12))
(hZCG : ZeroCountGlobalProp) (hNLZ : NoLowZeros) {n : ℕ} {T : ℝ}
(hTle : T ≤ 3 * 10 ^ 12 - 1) (hT2 : 2 ≤ T) :
‖∑ ρ ∈ ((zeroBothWindow_finite T).toFinset ∪ {(-2 : ℂ)}),
(zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n)‖ ≤ 4 * FAlt T + 1 := by
have h2not : (-2 : ℂ) ∉ (zeroBothWindow_finite T).toFinset := by
intro h
have hnt : IsNontrivialZero (-2 : ℂ) := (zeroBothWindow_finite T).mem_toFinset.mp h |>.1
rw [show (-2 : ℂ).re = -2 by simp] at hnt
... -- re = −2 ∉ (0,1)
rw [Finset.sum_union h2not]
have htriv : ‖(zeroMult (-2 : ℂ) : ℂ) * (1 - ((-2 : ℂ) / (-2 - 1)) ^ n)‖ ≤ 1 := trivTerm_norm_le_one n
have hbridge := zeroSum_nontriv_norm_le hRH (n := n) (T := T) (by linarith [hTle])
have hcount := zeroBothWindow_sum_eq_two_mul hNLZ T
have hZ := hZCG T hT2
calc ‖∑ ρ ∈ (zeroBothWindow_finite T).toFinset, ... +
(zeroMult (-2 : ℂ) : ℂ) * (1 - ((-2 : ℂ) / (-2 - 1)) ^ n)‖
≤ ‖∑ ...‖ + ‖triv‖ := norm_add_le _ _
_ ≤ 2 * ∑ ... + 1 := by linarith [hbridge, htriv]
_ = 2 * (2 * ∑ P) + 1 := by rw [hcount]; ring
_ ≤ 4 * FAlt T + 1 := by linarith [hZ]
```
Hmm — hZCG gives Σ_P mult ≤ FAlt T: 2·(2·Σ_P) = 4·Σ_P ≤ 4·FAlt T ✓ linarith.
h2not: (−2:ℂ) ∉ toFinset: mem gives IsNontrivialZero (−2): re = −2 not in (0,1): hnt.2.1 : 0 < (−2:ℂ).re = −2: contradiction:
```lean
have h2not : (-2 : ℂ) ∉ (zeroBothWindow_finite T).toFinset := by
intro h
have hnt := (zeroBothWindow_finite T).mem_toFinset.mp h |>.1
have h21 : (0 : ℝ) < (-2 : ℂ).re := hnt.2.1
simp at h21
```
simp at h21 : 0 < (−2:ℂ).re → 0 < −2 → False ✓.
Now — RHUpTo's exact form: `RHUpTo (T₀ : ℝ) : Prop := ∀ ρ : ℂ, IsNontrivialZero ρ → |ρ.im| ≤ T₀ → ρ.re = 1 / 2` ✓ (LiSkeleton:354). hRH ρ hnt (|im| ≤ 3×10¹²): |ρ.im| ≤ T ≤ 3×10¹² − 1 ≤ 3×10¹² ✓ linarith [him, hTle]... in zeroSum_nontriv_norm_le I used hTle : T ≤ 3×10¹² directly. In the bridge hTle : T ≤ 3×10¹² − 1: pass (by linarith [hTle] : T ≤ 3×10¹²).
OK — assemble the whole §2 and append. Also need zeroGlobalWindow_finite's sum — hZCG T hT2 gives the mult-sum ≤ FAlt T ✓.
One more check — `zeroMult_neg_two` (LiContour:701) : zeroMult (-2) = 1 ✓ — (zeroMult (-2:ℂ) : ℂ) = 1 after cast ✓.
The trivTerm proof:
```lean
lemma trivTerm_norm_le_one (n : ℕ) :
‖(zeroMult (-2 : ℂ) : ℂ) * (1 - ((-2 : ℂ) / (-2 - 1)) ^ n)‖ ≤ 1 := by
have hm : (zeroMult (-2 : ℂ) : ℂ) = 1 := by
rw [zeroMult_neg_two]
norm_num
rw [hm, one_mul]
have e : (-2 : ℂ) / (-2 - 1) = (2 / 3 : ℝ) := by
rw [show ((2 : ℝ) / 3 : ℝ) = 2 / 3 by ring]
field_simp
norm_num
rw [e, ← ofReal_pow]
have h1 : (0 : ℝ) ≤ (2 / 3 : ℝ) := by norm_num
have h2 : (2 / 3 : ℝ) ≤ 1 := by norm_num
have hpow1 : (2 / 3 : ℝ) ^ n ≤ 1 := pow_le_one₀ h1 h2 n
rw [← ofReal_one, ← ofReal_sub, Complex.norm_real, Real.norm_eq_abs,
abs_of_nonneg (by linarith [pow_nonneg h1 n] : (0 : ℝ) ≤ 1 - (2 / 3) ^ n)]
have hpow_nonneg : (0 : ℝ) ≤ (2 / 3 : ℝ) ^ n := pow_nonneg h1 n
linarith
```
e : (−2:ℂ)/(−2−1) = ((2/3 : ℝ) : ℂ): the LHS: (−2)/(−3) = 2/3: field_simp; norm_num? Let me write:
```lean
have e : (-2 : ℂ) / (-2 - 1) = ((2 / 3 : ℝ) : ℂ) := by
rw [show ((-2 : ℂ) / (-2 - 1)) = ((-2 : ℝ) / (-3 : ℝ) : ℝ) by push_cast; ring]
rw [show ((-2 : ℝ) / (-3 : ℝ)) = (2 / 3 : ℝ) by norm_num]
```
Hmm — push_cast on (−2:ℂ)/(−2−1): (−2−1 : ℂ) = −3: push_cast turns it into ↑(−2/−3)? Let me do it in two steps:
```lean
have e1 : (-2 : ℂ) / (-2 - 1) = (-2 : ℂ) / (-3 : ℂ) := by norm_num
have e : (-2 : ℂ) / (-2 - 1) = ((2 / 3 : ℝ) : ℂ) := by
rw [e1]
rw [show ((-2 : ℂ) / (-3 : ℂ)) = (((-2 : ℝ) / (-3 : ℝ) : ℝ) : ℂ) by push_cast; ring]
rw [show ((-2 : ℝ) / (-3 : ℝ)) = (2 / 3 : ℝ) by norm_num]
```
push_cast on ((−2:ℂ)/(−3:ℂ)): the casts: (−2:ℂ) = ↑(−2:ℝ)? (−2 : ℂ) is OfNat's negation — push_cast normalizes ((−2:ℂ)/(−3:ℂ)) to ↑(−2/−3 : ℝ)? push_cast goes the OTHER direction (eliminates casts inside-out). The show-proof `by push_cast; ring` — risky. Alternative: field_simp + norm_num:
```lean
have e : (-2 : ℂ) / (-2 - 1) = ((2 / 3 : ℝ) : ℂ) := by
rw [show ((-2 : ℂ) / (-2 - 1)) = ((-2 : ℂ) / (-3 : ℂ)) by norm_num]
field_simp
norm_num
```
field_simp on (−2:ℂ)/(−3:ℂ) = ↑(2/3 : ℝ): clears: −2 = ↑(2/3)·(−3) = −2·... norm_num ✓ maybe. Or:
```lean
have e : (-2 : ℂ) / (-2 - 1) = ((2 / 3 : ℝ) : ℂ) := by
have h3 : (-2 : ℂ) - 1 = -3 := by norm_num
rw [h3]
rw [div_eq_iff (by norm_num : (-3 : ℂ) ≠ 0)]
push_cast
ring
```
div_eq_iff : a / b = c ↔ a = c * b (b ≠ 0) — goal becomes −2 = ↑(2/3)·(−3): push_cast: ↑(2/3) = 2/3 as ℂ... the goal after div_eq_iff: (-2 : ℂ) = ((2/3 : ℝ) : ℂ) * (-3 : ℂ): push_cast turns RHS into ↑((2/3)·(−3))?? push_cast moves casts outward: ↑(2/3)·↑(−3) → ↑((2/3)·(−3)): then goal −2 = ↑((2/3)·(−3)) — then rw [show ...] or norm_num: `push_cast; norm_num`? The final: (−2 : ℂ) = ((2/3 : ℝ) : ℂ) * (-3 : ℂ) — `norm_num` might close it directly (it can evaluate (2/3)·(−3) = −2 via ofReal simp lemmas) — `norm_num [push_cast]`? Let me just use `field_simp; norm_num` and iterate at build.
Actually simplest robust: avoid the cast dance — keep everything in ℂ:
```lean
have e : (-2 : ℂ) / (-2 - 1) = 2 / 3 := by
field_simp
norm_num
rw [e]
```
goal: ‖1 − (2/3 : ℂ)ⁿ‖ ≤ 1: write (2/3 : ℂ) = ofReal (2/3):
```lean
have e2 : ((2 : ℂ) / 3) = ((2 / 3 : ℝ) : ℂ) := by norm_num
```
norm_num proves ((2:ℂ)/3) = ↑(2/3:ℝ)? — LHS: 2/3 in ℂ; RHS: ofReal(2/3 ℝ): norm_num with push_cast should close: `by push_cast; norm_num`? or `by norm_num`? Risky. Use: `by rw [show ((2 / 3 : ℝ) : ℂ) = 2 / 3 by push_cast; ring]` — converts RHS to 2/3 in ℂ, then e's form matches. Hmm — actually the cleanest: don't cast at all:
```lean
have hpow : (0 : ℝ) ≤ (2 / 3 : ℝ) ^ n := ...
have hnorm : ‖(1 : ℂ) - ((2 : ℂ) / 3) ^ n‖ = 1 - (2 / 3 : ℝ) ^ n := by
have h23 : ((2 : ℂ) / 3) = ((2 / 3 : ℝ) : ℂ) := by push_cast; ring
rw [h23, ← ofReal_pow, ← ofReal_one, ← ofReal_sub, Complex.norm_real, Real.norm_eq_abs,
abs_of_nonneg (by linarith : (0 : ℝ) ≤ 1 - (2 / 3 : ℝ) ^ n)]
```
`((2:ℂ)/3) = ((2/3:ℝ):ℂ)` — push_cast on the RHS: ↑(2/3) → 2/3 in ℂ: `by push_cast; ring` — push_cast normalizes ↑((2:ℝ)/3) to (2:ℂ)/3: then ring closes ((2:ℂ)/3) = (2:ℂ)/3 ✓. And `by linarith : (0:ℝ) ≤ 1 − (2/3)^n` — needs pow_le_one₀: pass it: `abs_of_nonneg (by have h := pow_le_one₀ h1 h2 n; linarith : (0 : ℝ) ≤ 1 - (2 / 3 : ℝ) ^ n)`.
OK — I'll write it with these forms and iterate on build errors. Also `Finset.mul_sum` — check name: `Finset.mul_sum : b * ∑ x ∈ s, f x = ∑ x ∈ s, b * f x` ✓ standard.
`norm_sum_le` — `norm_sum_le (s : Finset ι) (f : ι → α) : ‖∑ x ∈ s, f x‖ ≤ ∑ x ∈ s, ‖f x‖` ✓ exists (norm_sum_le or Finset.norm_sum_le? — there's `norm_sum_le` in Mathlib ✓).
`starRingEnd_injective` — probe. If not: starRingEquiv.injective? or `(starRingEnd ℂ).injective`? — `starRingEnd` is an equiv: `(starRingEnd ℂ).injective` ✓ — starRingEnd R : R ≃+* R (a ring equiv) — .injective ✓. For the Finset.image embedding: `⟨(starRingEnd ℂ), (starRingEnd ℂ).injective⟩` ✓.
Finset.sum_image : (∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y) → ∑ x ∈ s.image f, g x = ∑ x ∈ s, g (f x) ✓.
Let me write §2.
Now writing §2 (the bridge).
tool: Edit
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiAssembly.lean",
"old_string": " rw [e]\n exact norm_sub_le _ _\n\nend NguyenRH1",
"new_string": " rw [e]\n exact norm_sub_le _ _\n\n/-! ## 2. The bridge -/\n\n/-- On the line re \u03c1 = 1/2: |\u03c1/(\u03c1\u22121)| = 1, so each zero term has norm\n\u2264 2\u00b7mult. -/\nlemma zeroTerm_norm_le_two {\u03c1 : \u2102} (h\u03c1 : IsNontrivialZero \u03c1) (hre : \u03c1.re = 1 / 2)\n (n : \u2115) :\n \u2016(zeroMult \u03c1 : \u2102) * (1 - (\u03c1 / (\u03c1 - 1)) ^ n)\u2016 \u2264 2 * (zeroMult \u03c1 : \u211d) := by\n have h\u03c11 : \u03c1 - 1 \u2260 0 := by\n intro h\n have h2 : \u03c1 = 1 := sub_eq_zero.mp h\n rw [h2, Complex.one_re] at hre\n norm_num at hre\n have hnorm : \u2016\u03c1\u2016 = \u2016\u03c1 - 1\u2016 := by\n have h : \u2016\u03c1\u2016 ^ 2 = \u2016\u03c1 - 1\u2016 ^ 2 := by\n rw [\u2190 Complex.normSq_eq_norm_sq, \u2190 Complex.normSq_eq_norm_sq]\n rw [Complex.normSq_apply \u03c1, Complex.normSq_apply (\u03c1 - 1), hre]\n simp only [sub_re, one_re, sub_im, one_im, sub_zero]\n ring\n exact (sq_eq_sq\u2080 (norm_nonneg _) (norm_nonneg _)).mp h\n have hnorm_ratio : \u2016\u03c1 / (\u03c1 - 1)\u2016 = 1 := by\n rw [norm_div, hnorm, div_self (norm_pos_iff.mpr h\u03c11)]\n calc \u2016(zeroMult \u03c1 : \u2102) * (1 - (\u03c1 / (\u03c1 - 1)) ^ n)\u2016\n = (zeroMult \u03c1 : \u211d) * \u20161 - (\u03c1 / (\u03c1 - 1)) ^ n\u2016 := by\n rw [norm_mul, RCLike.norm_natCast]\n _ \u2264 (zeroMult \u03c1 : \u211d) * 2 := by\n apply mul_le_mul_of_nonneg_left _ (Nat.cast_nonneg _)\n calc \u20161 - (\u03c1 / (\u03c1 - 1)) ^ n\u2016\n \u2264 \u2016(1 : \u2102)\u2016 + \u2016(\u03c1 / (\u03c1 - 1)) ^ n\u2016 := norm_sub_le _ _\n _ = 1 + 1 := by rw [norm_one, norm_pow, hnorm_ratio, one_pow]\n _ = 2 := by norm_num\n _ = 2 * (zeroMult \u03c1 : \u211d) := by ring\n\n/-- The nontrivial part of the zero sum: \u2016\u03a3\u2016 \u2264 2\u00b7\u03a3 mult (each term \u2264 2\non the line via `RHUpTo`). -/\nlemma zeroSum_nontriv_norm_le (hRH : RHUpTo (3 * 10 ^ 12)) {n : \u2115} {T : \u211d}\n (hTle : T \u2264 3 * 10 ^ 12) :\n \u2016\u2211 \u03c1 \u2208 (zeroBothWindow_finite T).toFinset,\n (zeroMult \u03c1 : \u2102) * (1 - (\u03c1 / (\u03c1 - 1)) ^ n)\u2016 \u2264\n 2 * \u2211 \u03c1 \u2208 (zeroBothWindow_finite T).toFinset, (zeroMult \u03c1 : \u211d) := by\n calc \u2016\u2211 \u03c1 \u2208 (zeroBothWindow_finite T).toFinset,\n (zeroMult \u03c1 : \u2102) * (1 - (\u03c1 / (\u03c1 - 1)) ^ n)\u2016\n \u2264 \u2211 \u03c1 \u2208 (zeroBothWindow_finite T).toFinset,\n \u2016(zeroMult \u03c1 : \u2102) * (1 - (\u03c1 / (\u03c1 - 1)) ^ n)\u2016 := norm_sum_le _ _\n _ \u2264 \u2211 \u03c1 \u2208 (zeroBothWindow_finite T).toFinset, 2 * (zeroMult \u03c1 : \u211d) := by\n apply Finset.sum_le_sum\n intro \u03c1 h\u03c1\n have hnt : IsNontrivialZero \u03c1 := ((zeroBothWindow_finite T).mem_toFinset.mp h\u03c1).1\n have him : |\u03c1.im| \u2264 T := ((zeroBothWindow_finite T).mem_toFinset.mp h\u03c1).2\n have hre : \u03c1.re = 1 / 2 := hRH \u03c1 hnt (by linarith [him, hTle] : |\u03c1.im| \u2264 3 * 10 ^ 12)\n exact zeroTerm_norm_le_two hnt hre n\n _ = 2 * \u2211 \u03c1 \u2208 (zeroBothWindow_finite T).toFinset, (zeroMult \u03c1 : \u211d) := by\n rw [Finset.mul_sum]\n\n/-- The both-signs mult count is 2\u00d7 the one-sign count (NoLowZeros gives\nim \u2260 0; the conj bijection with `zeroMult_conj` identifies the two\nhalves). -/\nlemma zeroBothWindow_sum_eq_two_mul (hNLZ : NoLowZeros) (T : \u211d) :\n \u2211 \u03c1 \u2208 (zeroBothWindow_finite T).toFinset, (zeroMult \u03c1 : \u211d) =\n 2 * \u2211 \u03c1 \u2208 (zeroGlobalWindow_finite T).toFinset, (zeroMult \u03c1 : \u211d) := by\n classical\n set P := (zeroGlobalWindow_finite T).toFinset with hP\n set N := (zeroGlobalWindowNeg_finite T).toFinset with hN\n have hW : (zeroBothWindow_finite T).toFinset = P \u222a N := by\n ext \u03c1\n rw [Finset.mem_union, (zeroBothWindow_finite T).mem_toFinset,\n (zeroGlobalWindow_finite T).mem_toFinset, (zeroGlobalWindowNeg_finite T).mem_toFinset]\n constructor\n \u00b7 intro \u27e8hnt, himT\u27e9\n have him0 : \u03c1.im \u2260 0 := by\n have h14 := hNLZ \u03c1 hnt\n intro h\n rw [h, abs_zero] at h14\n exact (by norm_num : \u00ac (14 : \u211d) \u2264 0) h14\n rcases lt_or_gt_of_ne him0 with hneg | hpos\n \u00b7 exact Or.inr \u27e8hnt, by linarith [abs_le.mp himT |>.1], hneg\u27e9\n \u00b7 exact Or.inl \u27e8hnt, hpos, by linarith [abs_le.mp himT |>.2]\u27e9\n \u00b7 intro h\n rcases h with \u27e8hnt, hpos, himT\u27e9 | \u27e8hnt, himT, hneg\u27e9\n \u00b7 exact \u27e8hnt, by rw [abs_of_pos hpos]; exact himT\u27e9\n \u00b7 exact \u27e8hnt, by rw [abs_of_neg hneg]; linarith\u27e9\n have hdisj : Disjoint P N := by\n rw [Finset.disjoint_left]\n intro \u03c1 h\u03c1P h\u03c1N\n have h1 : 0 < \u03c1.im := ((zeroGlobalWindow_finite T).mem_toFinset.mp h\u03c1P).2.1\n have h2 : \u03c1.im < 0 := ((zeroGlobalWindowNeg_finite T).mem_toFinset.mp h\u03c1N).2.2\n linarith\n have hNeq : N = P.image \u27e8(starRingEnd \u2102), (starRingEnd \u2102).injective\u27e9 := by\n ext \u03c1\n rw [Finset.mem_image, (zeroGlobalWindowNeg_finite T).mem_toFinset,\n (zeroGlobalWindow_finite T).mem_toFinset]\n constructor\n \u00b7 intro \u27e8hnt, himT, hneg\u27e9\n refine \u27e8(starRingEnd \u2102) \u03c1, \u27e8isNontrivialZero_conj hnt, ?_, ?_\u27e9, ?_\u27e9\n \u00b7 rw [Complex.conj_im]\n exact neg_pos.mpr hneg\n \u00b7 rw [Complex.conj_im]\n linarith\n \u00b7 rw [starRingEnd_apply, starRingEnd_apply, star_star]\n \u00b7 rintro \u27e8\u03c3, \u27e8h\u03c3nt, h\u03c3pos, h\u03c3T\u27e9, rfl\u27e9\n refine \u27e8isNontrivialZero_conj h\u03c3nt, ?_, ?_\u27e9\n \u00b7 rw [Complex.conj_im]\n linarith\n \u00b7 rw [Complex.conj_im]\n linarith\n have hNsum : (\u2211 \u03c1 \u2208 N, (zeroMult \u03c1 : \u211d)) = \u2211 \u03c1 \u2208 P, (zeroMult \u03c1 : \u211d) := by\n rw [hNeq, Finset.sum_image (fun \u03c1 _ \u03c3 _ h => (starRingEnd \u2102).injective h)]\n apply Finset.sum_congr rfl\n intro \u03c1 h\u03c1\n have hnt : IsNontrivialZero \u03c1 := ((zeroGlobalWindow_finite T).mem_toFinset.mp h\u03c1).1\n have h := zeroMult_conj hnt\n rw [h]\n rw [hW, Finset.sum_union hdisj, hNsum]\n ring\n\n/-- The trivial-zero term at \u22122: |1 \u2212 (2/3)\u207f| \u2264 1. -/\nlemma trivTerm_norm_le_one (n : \u2115) :\n \u2016(zeroMult (-2 : \u2102) : \u2102) * (1 - ((-2 : \u2102) / (-2 - 1)) ^ n)\u2016 \u2264 1 := by\n have hm : (zeroMult (-2 : \u2102) : \u2102) = 1 := by\n rw [zeroMult_neg_two]\n norm_num\n rw [hm, one_mul]\n have h1 : (0 : \u211d) \u2264 (2 / 3 : \u211d) := by norm_num\n have h2 : (2 / 3 : \u211d) \u2264 1 := by norm_num\n have hpow1 : (2 / 3 : \u211d) ^ n \u2264 1 := pow_le_one\u2080 h1 h2 n\n have hnorm : \u2016(1 : \u2102) - ((-2 : \u2102) / (-2 - 1)) ^ n\u2016 = 1 - (2 / 3 : \u211d) ^ n := by\n have e : (-2 : \u2102) / (-2 - 1) = ((2 / 3 : \u211d) : \u2102) := by\n have h3 : (-2 : \u2102) - 1 = -3 := by norm_num\n rw [h3]\n rw [div_eq_iff (by norm_num : (-3 : \u2102) \u2260 0)]\n push_cast\n ring\n rw [e, \u2190 ofReal_pow, \u2190 ofReal_one, \u2190 ofReal_sub, Complex.norm_real, Real.norm_eq_abs,\n abs_of_nonneg (by linarith : (0 : \u211d) \u2264 1 - (2 / 3 : \u211d) ^ n)]\n rw [hnorm]\n linarith\n\n/-- **The bridge** (D-071 \u00a74.2): \u2016\u03a3 zero terms\u2016 \u2264 4\u00b7FAlt T + 1. The +1\nis the trivial-zero term at \u22122; the 4\u00b7FAlt is the both-signs count\n(2\u00b7mult per term \u00d7 2\u00d7 one-sign count \u2264 FAlt via the perimeter\n`ZeroCountGlobalProp`). -/\ntheorem zeroSum_norm_le_four_FAlt_add_one (hRH : RHUpTo (3 * 10 ^ 12))\n (hZCG : ZeroCountGlobalProp) (hNLZ : NoLowZeros) {n : \u2115} {T : \u211d}\n (hTle : T \u2264 3 * 10 ^ 12 - 1) (hT2 : 2 \u2264 T) :\n \u2016\u2211 \u03c1 \u2208 ((zeroBothWindow_finite T).toFinset \u222a {(-2 : \u2102)}),\n (zeroMult \u03c1 : \u2102) * (1 - (\u03c1 / (\u03c1 - 1)) ^ n)\u2016 \u2264 4 * FAlt T + 1 := by\n have h2not : (-2 : \u2102) \u2209 (zeroBothWindow_finite T).toFinset := by\n intro h\n have hnt := (zeroBothWindow_finite T).mem_toFinset.mp h |>.1\n have h21 : (0 : \u211d) < (-2 : \u2102).re := hnt.2.1\n simp at h21\n rw [Finset.sum_union h2not]\n have htriv := trivTerm_norm_le_one n\n have hbridge := zeroSum_nontriv_norm_le hRH (n := n) (T := T) (by linarith [hTle])\n have hcount := zeroBothWindow_sum_eq_two_mul hNLZ T\n have hZ := hZCG T hT2\n calc \u2016\u2211 \u03c1 \u2208 (zeroBothWindow_finite T).toFinset,\n (zeroMult \u03c1 : \u2102) * (1 - (\u03c1 / (\u03c1 - 1)) ^ n) +\n (zeroMult (-2 : \u2102) : \u2102) * (1 - ((-2 : \u2102) / (-2 - 1)) ^ n)\u2016\n \u2264 \u2016\u2211 \u03c1 \u2208 (zeroBothWindow_finite T).toFinset,\n (zeroMult \u03c1 : \u2102) * (1 - (\u03c1 / (\u03c1 - 1)) ^ n)\u2016 +\n \u2016(zeroMult (-2 : \u2102) : \u2102) * (1 - ((-2 : \u2102) / (-2 - 1)) ^ n)\u2016 := norm_add_le _ _\n _ \u2264 (2 * \u2211 \u03c1 \u2208 (zeroBothWindow_finite T).toFinset, (zeroMult \u03c1 : \u211d)) + 1 := by\n linarith [hbridge, htriv]\n _ = 2 * (2 * \u2211 \u03c1 \u2208 (zeroGlobalWindow_finite T).toFinset, (zeroMult \u03c1 : \u211d)) + 1 := by\n rw [hcount]\n _ \u2264 4 * FAlt T + 1 := by linarith [hZ]\n\nend NguyenRH1"
}
raw content_json (database row)
[{"type":"thinking","thinking":"Now §2: the bridge `zeroSum_norm_le_four_FAlt_add_one`. Append before `end NguyenRH1`:\n\n```lean\n/-! ## 2. The bridge -/\n\n/-- The per-term bound on the line: |1 − (ρ/(ρ−1))ⁿ| ≤ 2 when re ρ = 1/2\n(|ρ| = |1−ρ| then). -/\nlemma zeroTerm_norm_le_two {ρ : ℂ} (hρ : IsNontrivialZero ρ) (hre : ρ.re = 1 / 2) (n : ℕ) :\n ‖(zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n)‖ ≤ 2 * (zeroMult ρ : ℝ) := by\n ...\n```\n\nProof: ‖ρ‖² = re² + im² = 1/4 + γ²; ‖ρ−1‖² = (re−1)² + im² = 1/4 + γ². So ‖ρ/(ρ−1)‖ = 1 (ρ ≠ 1 since nontrivial re < 1; ρ − 1 ≠ 0). Then ‖(ρ/(ρ−1))ⁿ‖ = 1, ‖1 − (ρ/(ρ−1))ⁿ‖ ≤ ‖1‖ + 1 = 2. Term norm: ‖mult‖ · ‖1 − ...‖ = mult · ‖1−...‖ ≤ mult·2 = 2·mult.\n\n```lean\n have hρ1 : ρ - 1 ≠ 0 := by\n intro h\n have : ρ = 1 := sub_eq_zero.mp h\n rw [this, Complex.one_re] at hre\n norm_num at hre\n have hnorm_ratio : ‖ρ / (ρ - 1)‖ = 1 := by\n rw [norm_div]\n have h1 : ‖ρ‖ = ‖ρ - 1‖ := by\n have hsq : ‖ρ‖ ^ 2 = ‖ρ - 1‖ ^ 2 := by\n rw [← Complex.normSq_eq_norm_sq, ← Complex.normSq_eq_norm_sq]\n rw [Complex.normSq_apply, Complex.normSq_apply, hre]\n simp [sub_re, one_re, sub_im]\n ring\n exact (sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _)).mp hsq\n rw [h1, div_self (norm_pos_iff.mpr hρ1)]\n```\nHmm — sq_eq_sq₀ : 0 ≤ a → 0 ≤ b → (a² = b² ↔ a = b): `sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _) |>.mp hsq` ✓ (exists? — there's `sq_eq_sq₀`... alternatively `pow_left_injective₀`. Or use the norm_div_sub_one_le_one pattern from LiContour:271-287 — they proved ‖s/(s−1)‖ ≤ 1 for re s ≤ 1/2 via normSq. For EQUALITY at re = 1/2: same computation with = instead of ≤. Let me mirror LiContour's norm_div_sub_one_le_one:\n```lean\n have hnorm : ‖ρ‖ = ‖ρ - 1‖ := by\n have h : ‖ρ‖ ^ 2 = ‖ρ - 1‖ ^ 2 := by\n rw [← Complex.normSq_eq_norm_sq, ← Complex.normSq_eq_norm_sq]\n rw [Complex.normSq_apply ρ, Complex.normSq_apply (ρ - 1), hre]\n simp only [sub_re, one_re, sub_im, one_im, sub_zero]\n ring\n exact (sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _)).mp h\n```\nHmm — Complex.normSq_apply: normSq z = z.re*z.re + z.im*z.im ✓ with hre (re = 1/2): LHS = (1/2)² + im²; RHS = (1/2−1)² + im²: ring ✓. sq_eq_sq₀ — check name: `sq_eq_sq₀ : 0 ≤ a → 0 ≤ b → (a ^ 2 = b ^ 2 ↔ a = b)` ✓ exists (used in LiContour:284 as sq_le_sq₀ — for the eq version: `sq_eq_sq₀`? or `(pow_left_injective₀ ...).eq_iff`? LiContour:284 used `sq_le_sq₀ (norm_nonneg _) (norm_nonneg _) |>.mp h` for the ≤ version. For equality: `sq_eq_sq₀` — hmm — safer: (pow_left_injective₀ (norm_nonneg _) (norm_nonneg _) two_ne_zero).eq_iff? There's `pow_left_injective₀ : 0 ≤ a → 0 ≤ b → n ≠ 0 → (a ^ n = b ^ n ↔ a = b)`? Hmm. Alternative: `abs_of_nonneg`: ‖ρ‖ = ‖ρ−1‖ ⟺ ‖ρ‖² = ‖ρ−1‖² with nonneg: use `sq_eq_sq₀` if it exists else:\n```lean\n exact pow_left_injective₀ (norm_nonneg _) (norm_nonneg _) two_ne_zero h\n```\npow_left_injective₀ : 0 ≤ a → 0 ≤ b → n ≠ 0 → a^n = b^n → a = b? Signature: `pow_left_injective₀ (ha : 0 ≤ a) (hb : 0 ≤ b) (hn : n ≠ 0) : a ^ n = b ^ n → a = b`? I think it's `pow_left_injective₀ : 0 ≤ x → 0 ≤ y → x ^ n = y ^ n → n ≠ 0 → x = y`? Ugh. Let me use: `sq_eq_sq₀` — I'm fairly confident it exists in Mathlib (Algebra.Order... `sq_eq_sq₀ : 0 ≤ a → 0 ≤ b → a ^ 2 = b ^ 2 ↔ a = b`? hmm — actually the iff form: `sq_eq_sq₀ (ha : 0 ≤ a) (hb : 0 ≤ b) : a ^ 2 = b ^ 2 ↔ a = b`? There's `sq_eq_sq'`... Let me just probe it in the build.\n\nThen:\n```lean\n calc ‖(zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n)‖\n = (zeroMult ρ : ℝ) * ‖1 - (ρ / (ρ - 1)) ^ n‖ := by\n rw [norm_mul, RCLike.norm_natCast]\n _ ≤ (zeroMult ρ : ℝ) * 2 := by\n apply mul_le_mul_of_nonneg_left _ (Nat.cast_nonneg _)\n calc ‖1 - (ρ / (ρ - 1)) ^ n‖\n ≤ ‖(1 : ℂ)‖ + ‖(ρ / (ρ - 1)) ^ n‖ := norm_sub_le _ _\n _ = 1 + 1 := by rw [norm_one, norm_pow, hnorm_ratio, one_pow]\n _ = 2 := by norm_num\n _ = 2 * (zeroMult ρ : ℝ) := by ring\n```\n\nThen the sum:\n```lean\nlemma zeroSum_nontriv_norm_le (hRH : RHUpTo (3 * 10 ^ 12)) {n : ℕ} {T : ℝ}\n (hTle : T ≤ 3 * 10 ^ 12) :\n ‖∑ ρ ∈ (zeroBothWindow_finite T).toFinset,\n (zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n)‖ ≤\n 2 * ∑ ρ ∈ (zeroBothWindow_finite T).toFinset, (zeroMult ρ : ℝ) := by\n calc ‖∑ ρ ∈ (zeroBothWindow_finite T).toFinset,\n (zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n)‖\n ≤ ∑ ρ ∈ (zeroBothWindow_finite T).toFinset,\n ‖(zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n)‖ := norm_sum_le _ _\n _ ≤ ∑ ρ ∈ (zeroBothWindow_finite T).toFinset, 2 * (zeroMult ρ : ℝ) := by\n apply Finset.sum_le_sum\n intro ρ hρ\n have hnt : IsNontrivialZero ρ := ((zeroBothWindow_finite T).mem_toFinset.mp hρ).1\n have him : |ρ.im| ≤ T := ((zeroBothWindow_finite T).mem_toFinset.mp hρ).2\n have hre : ρ.re = 1 / 2 := hRH ρ hnt (by linarith [him, hTle] : |ρ.im| ≤ 3 * 10 ^ 12)\n exact zeroTerm_norm_le_two hnt hre n\n _ = 2 * ∑ ρ ∈ (zeroBothWindow_finite T).toFinset, (zeroMult ρ : ℝ) := by\n rw [Finset.mul_sum]\n```\nnorm_sum_le : ‖∑ x ∈ s, f x‖ ≤ ∑ x ∈ s, ‖f x‖ ✓ (check exact name: `norm_sum_le (s : Finset ι) (f : ι → α) : ‖∑ x ∈ s, f x‖ ≤ ∑ x ∈ s, ‖f x‖` ✓). Finset.mul_sum : a * ∑ f = ∑ a * f — direction: ∑ x, 2 * g x = 2 * ∑ g: rw [Finset.mul_sum] rewrites 2 * ∑ → ∑ 2 * ... hmm — the goal's RHS is 2 * ∑ ... and I want to END there: the calc's last step: ∑ 2·mult = 2·∑ mult — Finset.mul_sum : b * ∑ x ∈ s, f x = ∑ x ∈ s, b * f x — rw [Finset.mul_sum] on goal `∑ 2·mult = 2·∑ mult` rewrites the RHS `2 * ∑` → `∑ 2·mult` ✓ closes by rfl.\n\nThen the both-signs count:\n```lean\nlemma zeroBothWindow_sum_eq_two_mul (hNLZ : NoLowZeros) (T : ℝ) :\n ∑ ρ ∈ (zeroBothWindow_finite T).toFinset, (zeroMult ρ : ℝ) =\n 2 * ∑ ρ ∈ (zeroGlobalWindow_finite T).toFinset, (zeroMult ρ : ℝ) := by\n classical\n set P := (zeroGlobalWindow_finite T).toFinset with hP\n set N := (zeroGlobalWindowNeg_finite T).toFinset with hN\n have hW : (zeroBothWindow_finite T).toFinset = P ∪ N := by\n ext ρ\n rw [Finset.mem_union, (zeroBothWindow_finite T).mem_toFinset,\n (zeroGlobalWindow_finite T).mem_toFinset, (zeroGlobalWindowNeg_finite T).mem_toFinset]\n constructor\n · intro ⟨hnt, himT⟩\n have him0 : ρ.im ≠ 0 := by\n have h14 := hNLZ ρ hnt\n intro h\n rw [h, abs_zero] at h14\n exact (by norm_num : ¬ (14 : ℝ) ≤ 0) h14\n rcases lt_or_gt_of_ne him0 with hneg | hpos\n · exact Or.inr ⟨hnt, by linarith [abs_le.mp himT |>.1], hneg⟩\n · exact Or.inl ⟨hnt, hpos, by linarith [abs_le.mp himT |>.2]⟩\n · intro h\n rcases h with ⟨hnt, hpos, himT⟩ | ⟨hnt, himT, hneg⟩\n · exact ⟨hnt, by rw [abs_of_pos hpos]; exact himT⟩\n · exact ⟨hnt, by rw [abs_of_neg hneg]; linarith⟩\n rw [hW]\n have hdisj : Disjoint P N := by\n rw [Finset.disjoint_left]\n intro ρ hρP hρN\n have h1 : 0 < ρ.im := ((zeroGlobalWindow_finite T).mem_toFinset.mp hρP).2.1\n have h2 : ρ.im < 0 := ((zeroGlobalWindowNeg_finite T).mem_toFinset.mp hρN).2.2\n linarith\n rw [Finset.sum_union hdisj]\n -- Σ over N = Σ over P via conj\n have hNsum : (∑ ρ ∈ N, (zeroMult ρ : ℝ)) = ∑ ρ ∈ P, (zeroMult ρ : ℝ) := by\n have himg : N = P.image ⟨(starRingEnd ℂ), isNontrivialZero_conj⟩ := by\n ext ρ\n rw [Finset.mem_image, (zeroGlobalWindowNeg_finite T).mem_toFinset,\n (zeroGlobalWindow_finite T).mem_toFinset]\n constructor\n · intro ⟨hnt, himT, hneg⟩\n refine ⟨(starRingEnd ℂ) ρ, ⟨isNontrivialZero_conj hnt, ?_, ?_⟩, ?_⟩\n · rw [Complex.conj_im]\n exact neg_pos.mpr hneg\n · rw [Complex.conj_im]\n linarith\n · rw [starRingEnd_apply, starRingEnd_apply, star_star]\n · rintro ⟨σ, ⟨hσnt, hσpos, hσT⟩, rfl⟩\n refine ⟨isNontrivialZero_conj hσnt, ?_, ?_⟩\n · rw [Complex.conj_im]\n linarith\n · rw [Complex.conj_im]\n exact neg_neg_of_pos hσpos -- hmm: (conj σ).im = −σ.im < 0 ⟸ σ.im > 0\n rw [himg]\n rw [Finset.sum_image (fun ρ _ σ _ h => starRingEnd_injective.injective h)]\n -- hmm: sum over image = sum over P of mult (conj ρ) = mult ρ (zeroMult_conj)\n apply Finset.sum_congr rfl\n intro ρ hρ\n exact_mod_cast zeroMult_conj (((zeroGlobalWindow_finite T).mem_toFinset.mp hρ).1)\n linarith [hNsum]\n```\nHmm — the image form: P.image ⟨conj, proof⟩ — Finset.image needs an EMBEDDING (Function.Embedding): ⟨(starRingEnd ℂ), isNontrivialZero_conj⟩ — that's not an embedding (isNontrivialZero_conj is the nontrivial-zero proof, not injectivity!). The embedding for conj: `Function.Embedding (starRingEnd ℂ) ?inj` — there's `starRingEnd_injective`? or use `Equiv` — conj is an equiv: starRingEquiv? For Finset.image with equiv: `Finset.image (starRingEnd ℂ)`? Finset.image takes an embedding: `⟨(starRingEnd ℂ), injective⟩` with injective : Function.Injective (starRingEnd ℂ) — starRingEnd is an involution hence injective: `starRingEnd_injective`? or `starRingEquiv.injective`. In Mathlib: `starRingEnd_injective : Function.Injective (starRingEnd R)`? There's `starRingEquiv : R ≃+* R` with .injective. Hmm — LiMoments used conjZeroEquiv (subtype equiv) with Finset-free tsum reindex. For Finset: simplest is Finset.image with the embedding `⟨(starRingEnd ℂ), starRingEnd_injective⟩` — check if starRingEnd_injective exists: likely `starRingEnd_injective` or use `starRingEquiv.injective`.\n\nAnd the sum over the image: Finset.sum_image : (∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y) → ∑ x ∈ s.image f, g x = ∑ x ∈ s, g (f x). With g := zeroMult: ∑ ρ ∈ image conj P, zeroMult ρ = ∑ ρ ∈ P, zeroMult (conj ρ) = ∑ ρ ∈ P, zeroMult ρ (zeroMult_conj) ✓.\n\nhmm — zeroMult_conj's statement (LiTightR:2294): zeroMult ((starRingEnd ℂ) ρ) = zeroMult ρ — for ρ with IsNontrivialZero? It takes (hρ : IsNontrivialZero ρ)? Looking at LiTightR:2294-2299: `lemma zeroMult_conj {ρ : ℂ} (hρ : IsNontrivialZero ρ) : zeroMult ((starRingEnd ℂ) ρ) = zeroMult ρ` — takes hρ ✓. exact_mod_cast zeroMult_conj hρ-proof — the sum terms are (zeroMult ρ : ℝ) casts: zeroMult_conj gives the ℕ equality: cast both sides ✓ exact_mod_cast.\n\nFor the negative-side membership backward direction ((conj σ).im < 0): (conj σ).im = −σ.im < 0 ⟸ σ.im > 0: `neg_neg_of_pos`? that's a ≠ 0. Use: rw [Complex.conj_im]; linarith.\n\nAnd the embedding: let me define conjEmb : Function.Embedding := ⟨(starRingEnd ℂ), starRingEnd_injective⟩? — probe `starRingEnd_injective`. Alternative: `starRingEquiv ℂ`? In Mathlib: `starRingEquiv : R ≃+* R` — for R a star ring with commutative... `starRingEquiv : R ≃ R`? There's `starRingEquiv : R ≃+* R` (the star ring equiv). Its .toFun = starRingEnd. So `starRingEquiv.injective`. Hmm — for ℂ: `Complex.starRingEquiv`? or just `starRingEquiv`? Let me probe in the build.\n\nThen the triv:\n```lean\nlemma trivTerm_norm_le_one (n : ℕ) :\n ‖(zeroMult (-2 : ℂ) : ℂ) * (1 - ((-2 : ℂ) / (-2 - 1)) ^ n)‖ ≤ 1 := by\n rw [zeroMult_neg_two]\n -- (−2)/(−3) = 2/3: term = 1 − (2/3)ⁿ ∈ [0, 1)\n have e : (-2 : ℂ) / (-2 - 1) = 2 / 3 := by norm_num\n rw [e]\n ...\n```\nHmm — (−2)/(−2−1) = (−2)/(−3) = 2/3 ✓ norm_num proves? (−2:ℂ)/(−3:ℂ) = 2/3: field_simp + norm_num ✓ `by norm_num`. Then term: (1:ℂ)·(1 − (2/3)ⁿ): ‖1 − (2/3)ⁿ‖: (2/3 : ℂ) is real positive: (2/3)ⁿ real positive ≤ 1: 1 − (2/3)ⁿ ∈ [0, 1): ‖·‖ = 1 − (2/3)ⁿ ≤ 1:\n```lean\n have h23 : ((2 : ℂ) / 3) = ((2 / 3 : ℝ) : ℂ) := by push_cast; ring\n rw [h23, ← ofReal_pow] -- hmm\n```\nSimpler: show 0 ≤ (2/3:ℂ) and (2/3:ℂ) ≤ 1 via the ofReal cast:\n```lean\n have h1 : (0 : ℝ) ≤ (2 / 3 : ℝ) := by norm_num\n have h2 : (2 / 3 : ℝ) ≤ 1 := by norm_num\n have h3 : ‖(1 : ℂ) - ((2 : ℂ) / 3) ^ n‖ = 1 - (2 / 3 : ℝ) ^ n := by\n have hpow : (0 : ℝ) ≤ (2 / 3 : ℝ) ^ n := pow_nonneg h1 n\n have hpow1 : (2 / 3 : ℝ) ^ n ≤ 1 := pow_le_one₀ h1 h2 n\n have e : ((2 : ℂ) / 3) = ((2 / 3 : ℝ) : ℂ) := by push_cast; ring\n rw [e, ← ofReal_pow, ← ofReal_one, ← ofReal_sub, Complex.norm_real, Real.norm_eq_abs,\n abs_of_nonneg (by linarith)]\n rw [h1', h3] -- hmm the mult part: zeroMult_neg_two gives zeroMult (-2) = 1: (zeroMult (-2:ℂ) : ℂ) = 1\n ...\n```\nGetting long. The full bridge:\n```lean\ntheorem zeroSum_norm_le_four_FAlt_add_one (hRH : RHUpTo (3 * 10 ^ 12))\n (hZCG : ZeroCountGlobalProp) (hNLZ : NoLowZeros) {n : ℕ} {T : ℝ}\n (hTle : T ≤ 3 * 10 ^ 12 - 1) (hT2 : 2 ≤ T) :\n ‖∑ ρ ∈ ((zeroBothWindow_finite T).toFinset ∪ {(-2 : ℂ)}),\n (zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n)‖ ≤ 4 * FAlt T + 1 := by\n have h2not : (-2 : ℂ) ∉ (zeroBothWindow_finite T).toFinset := by\n intro h\n have hnt : IsNontrivialZero (-2 : ℂ) := (zeroBothWindow_finite T).mem_toFinset.mp h |>.1\n rw [show (-2 : ℂ).re = -2 by simp] at hnt\n ... -- re = −2 ∉ (0,1)\n rw [Finset.sum_union h2not]\n have htriv : ‖(zeroMult (-2 : ℂ) : ℂ) * (1 - ((-2 : ℂ) / (-2 - 1)) ^ n)‖ ≤ 1 := trivTerm_norm_le_one n\n have hbridge := zeroSum_nontriv_norm_le hRH (n := n) (T := T) (by linarith [hTle])\n have hcount := zeroBothWindow_sum_eq_two_mul hNLZ T\n have hZ := hZCG T hT2\n calc ‖∑ ρ ∈ (zeroBothWindow_finite T).toFinset, ... +\n (zeroMult (-2 : ℂ) : ℂ) * (1 - ((-2 : ℂ) / (-2 - 1)) ^ n)‖\n ≤ ‖∑ ...‖ + ‖triv‖ := norm_add_le _ _\n _ ≤ 2 * ∑ ... + 1 := by linarith [hbridge, htriv]\n _ = 2 * (2 * ∑ P) + 1 := by rw [hcount]; ring\n _ ≤ 4 * FAlt T + 1 := by linarith [hZ]\n```\nHmm — hZCG gives Σ_P mult ≤ FAlt T: 2·(2·Σ_P) = 4·Σ_P ≤ 4·FAlt T ✓ linarith.\n\nh2not: (−2:ℂ) ∉ toFinset: mem gives IsNontrivialZero (−2): re = −2 not in (0,1): hnt.2.1 : 0 < (−2:ℂ).re = −2: contradiction:\n```lean\n have h2not : (-2 : ℂ) ∉ (zeroBothWindow_finite T).toFinset := by\n intro h\n have hnt := (zeroBothWindow_finite T).mem_toFinset.mp h |>.1\n have h21 : (0 : ℝ) < (-2 : ℂ).re := hnt.2.1\n simp at h21\n```\nsimp at h21 : 0 < (−2:ℂ).re → 0 < −2 → False ✓.\n\nNow — RHUpTo's exact form: `RHUpTo (T₀ : ℝ) : Prop := ∀ ρ : ℂ, IsNontrivialZero ρ → |ρ.im| ≤ T₀ → ρ.re = 1 / 2` ✓ (LiSkeleton:354). hRH ρ hnt (|im| ≤ 3×10¹²): |ρ.im| ≤ T ≤ 3×10¹² − 1 ≤ 3×10¹² ✓ linarith [him, hTle]... in zeroSum_nontriv_norm_le I used hTle : T ≤ 3×10¹² directly. In the bridge hTle : T ≤ 3×10¹² − 1: pass (by linarith [hTle] : T ≤ 3×10¹²).\n\nOK — assemble the whole §2 and append. Also need zeroGlobalWindow_finite's sum — hZCG T hT2 gives the mult-sum ≤ FAlt T ✓.\n\nOne more check — `zeroMult_neg_two` (LiContour:701) : zeroMult (-2) = 1 ✓ — (zeroMult (-2:ℂ) : ℂ) = 1 after cast ✓.\n\nThe trivTerm proof:\n```lean\nlemma trivTerm_norm_le_one (n : ℕ) :\n ‖(zeroMult (-2 : ℂ) : ℂ) * (1 - ((-2 : ℂ) / (-2 - 1)) ^ n)‖ ≤ 1 := by\n have hm : (zeroMult (-2 : ℂ) : ℂ) = 1 := by\n rw [zeroMult_neg_two]\n norm_num\n rw [hm, one_mul]\n have e : (-2 : ℂ) / (-2 - 1) = (2 / 3 : ℝ) := by\n rw [show ((2 : ℝ) / 3 : ℝ) = 2 / 3 by ring]\n field_simp\n norm_num\n rw [e, ← ofReal_pow]\n have h1 : (0 : ℝ) ≤ (2 / 3 : ℝ) := by norm_num\n have h2 : (2 / 3 : ℝ) ≤ 1 := by norm_num\n have hpow1 : (2 / 3 : ℝ) ^ n ≤ 1 := pow_le_one₀ h1 h2 n\n rw [← ofReal_one, ← ofReal_sub, Complex.norm_real, Real.norm_eq_abs,\n abs_of_nonneg (by linarith [pow_nonneg h1 n] : (0 : ℝ) ≤ 1 - (2 / 3) ^ n)]\n have hpow_nonneg : (0 : ℝ) ≤ (2 / 3 : ℝ) ^ n := pow_nonneg h1 n\n linarith\n```\ne : (−2:ℂ)/(−2−1) = ((2/3 : ℝ) : ℂ): the LHS: (−2)/(−3) = 2/3: field_simp; norm_num? Let me write:\n```lean\n have e : (-2 : ℂ) / (-2 - 1) = ((2 / 3 : ℝ) : ℂ) := by\n rw [show ((-2 : ℂ) / (-2 - 1)) = ((-2 : ℝ) / (-3 : ℝ) : ℝ) by push_cast; ring]\n rw [show ((-2 : ℝ) / (-3 : ℝ)) = (2 / 3 : ℝ) by norm_num]\n```\nHmm — push_cast on (−2:ℂ)/(−2−1): (−2−1 : ℂ) = −3: push_cast turns it into ↑(−2/−3)? Let me do it in two steps:\n```lean\n have e1 : (-2 : ℂ) / (-2 - 1) = (-2 : ℂ) / (-3 : ℂ) := by norm_num\n have e : (-2 : ℂ) / (-2 - 1) = ((2 / 3 : ℝ) : ℂ) := by\n rw [e1]\n rw [show ((-2 : ℂ) / (-3 : ℂ)) = (((-2 : ℝ) / (-3 : ℝ) : ℝ) : ℂ) by push_cast; ring]\n rw [show ((-2 : ℝ) / (-3 : ℝ)) = (2 / 3 : ℝ) by norm_num]\n```\npush_cast on ((−2:ℂ)/(−3:ℂ)): the casts: (−2:ℂ) = ↑(−2:ℝ)? (−2 : ℂ) is OfNat's negation — push_cast normalizes ((−2:ℂ)/(−3:ℂ)) to ↑(−2/−3 : ℝ)? push_cast goes the OTHER direction (eliminates casts inside-out). The show-proof `by push_cast; ring` — risky. Alternative: field_simp + norm_num:\n```lean\n have e : (-2 : ℂ) / (-2 - 1) = ((2 / 3 : ℝ) : ℂ) := by\n rw [show ((-2 : ℂ) / (-2 - 1)) = ((-2 : ℂ) / (-3 : ℂ)) by norm_num]\n field_simp\n norm_num\n```\nfield_simp on (−2:ℂ)/(−3:ℂ) = ↑(2/3 : ℝ): clears: −2 = ↑(2/3)·(−3) = −2·... norm_num ✓ maybe. Or:\n```lean\n have e : (-2 : ℂ) / (-2 - 1) = ((2 / 3 : ℝ) : ℂ) := by\n have h3 : (-2 : ℂ) - 1 = -3 := by norm_num\n rw [h3]\n rw [div_eq_iff (by norm_num : (-3 : ℂ) ≠ 0)]\n push_cast\n ring\n```\ndiv_eq_iff : a / b = c ↔ a = c * b (b ≠ 0) — goal becomes −2 = ↑(2/3)·(−3): push_cast: ↑(2/3) = 2/3 as ℂ... the goal after div_eq_iff: (-2 : ℂ) = ((2/3 : ℝ) : ℂ) * (-3 : ℂ): push_cast turns RHS into ↑((2/3)·(−3))?? push_cast moves casts outward: ↑(2/3)·↑(−3) → ↑((2/3)·(−3)): then goal −2 = ↑((2/3)·(−3)) — then rw [show ...] or norm_num: `push_cast; norm_num`? The final: (−2 : ℂ) = ((2/3 : ℝ) : ℂ) * (-3 : ℂ) — `norm_num` might close it directly (it can evaluate (2/3)·(−3) = −2 via ofReal simp lemmas) — `norm_num [push_cast]`? Let me just use `field_simp; norm_num` and iterate at build.\n\nActually simplest robust: avoid the cast dance — keep everything in ℂ: \n```lean\n have e : (-2 : ℂ) / (-2 - 1) = 2 / 3 := by\n field_simp\n norm_num\n rw [e]\n```\ngoal: ‖1 − (2/3 : ℂ)ⁿ‖ ≤ 1: write (2/3 : ℂ) = ofReal (2/3):\n```lean\n have e2 : ((2 : ℂ) / 3) = ((2 / 3 : ℝ) : ℂ) := by norm_num\n```\nnorm_num proves ((2:ℂ)/3) = ↑(2/3:ℝ)? — LHS: 2/3 in ℂ; RHS: ofReal(2/3 ℝ): norm_num with push_cast should close: `by push_cast; norm_num`? or `by norm_num`? Risky. Use: `by rw [show ((2 / 3 : ℝ) : ℂ) = 2 / 3 by push_cast; ring]` — converts RHS to 2/3 in ℂ, then e's form matches. Hmm — actually the cleanest: don't cast at all:\n```lean\n have hpow : (0 : ℝ) ≤ (2 / 3 : ℝ) ^ n := ...\n have hnorm : ‖(1 : ℂ) - ((2 : ℂ) / 3) ^ n‖ = 1 - (2 / 3 : ℝ) ^ n := by\n have h23 : ((2 : ℂ) / 3) = ((2 / 3 : ℝ) : ℂ) := by push_cast; ring\n rw [h23, ← ofReal_pow, ← ofReal_one, ← ofReal_sub, Complex.norm_real, Real.norm_eq_abs,\n abs_of_nonneg (by linarith : (0 : ℝ) ≤ 1 - (2 / 3 : ℝ) ^ n)]\n```\n`((2:ℂ)/3) = ((2/3:ℝ):ℂ)` — push_cast on the RHS: ↑(2/3) → 2/3 in ℂ: `by push_cast; ring` — push_cast normalizes ↑((2:ℝ)/3) to (2:ℂ)/3: then ring closes ((2:ℂ)/3) = (2:ℂ)/3 ✓. And `by linarith : (0:ℝ) ≤ 1 − (2/3)^n` — needs pow_le_one₀: pass it: `abs_of_nonneg (by have h := pow_le_one₀ h1 h2 n; linarith : (0 : ℝ) ≤ 1 - (2 / 3 : ℝ) ^ n)`.\n\nOK — I'll write it with these forms and iterate on build errors. Also `Finset.mul_sum` — check name: `Finset.mul_sum : b * ∑ x ∈ s, f x = ∑ x ∈ s, b * f x` ✓ standard.\n\n`norm_sum_le` — `norm_sum_le (s : Finset ι) (f : ι → α) : ‖∑ x ∈ s, f x‖ ≤ ∑ x ∈ s, ‖f x‖` ✓ exists (norm_sum_le or Finset.norm_sum_le? — there's `norm_sum_le` in Mathlib ✓).\n\n`starRingEnd_injective` — probe. If not: starRingEquiv.injective? or `(starRingEnd ℂ).injective`? — `starRingEnd` is an equiv: `(starRingEnd ℂ).injective` ✓ — starRingEnd R : R ≃+* R (a ring equiv) — .injective ✓. For the Finset.image embedding: `⟨(starRingEnd ℂ), (starRingEnd ℂ).injective⟩` ✓.\n\nFinset.sum_image : (∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y) → ∑ x ∈ s.image f, g x = ∑ x ∈ s, g (f x) ✓.\n\nLet me write §2.","signature":""},{"type":"text","text":"Now writing §2 (the bridge)."},{"type":"tool_use","id":"Edit_298","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiAssembly.lean","old_string":" rw [e]\n exact norm_sub_le _ _\n\nend NguyenRH1","new_string":" rw [e]\n exact norm_sub_le _ _\n\n/-! ## 2. The bridge -/\n\n/-- On the line re ρ = 1/2: |ρ/(ρ−1)| = 1, so each zero term has norm\n≤ 2·mult. -/\nlemma zeroTerm_norm_le_two {ρ : ℂ} (hρ : IsNontrivialZero ρ) (hre : ρ.re = 1 / 2)\n (n : ℕ) :\n ‖(zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n)‖ ≤ 2 * (zeroMult ρ : ℝ) := by\n have hρ1 : ρ - 1 ≠ 0 := by\n intro h\n have h2 : ρ = 1 := sub_eq_zero.mp h\n rw [h2, Complex.one_re] at hre\n norm_num at hre\n have hnorm : ‖ρ‖ = ‖ρ - 1‖ := by\n have h : ‖ρ‖ ^ 2 = ‖ρ - 1‖ ^ 2 := by\n rw [← Complex.normSq_eq_norm_sq, ← Complex.normSq_eq_norm_sq]\n rw [Complex.normSq_apply ρ, Complex.normSq_apply (ρ - 1), hre]\n simp only [sub_re, one_re, sub_im, one_im, sub_zero]\n ring\n exact (sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _)).mp h\n have hnorm_ratio : ‖ρ / (ρ - 1)‖ = 1 := by\n rw [norm_div, hnorm, div_self (norm_pos_iff.mpr hρ1)]\n calc ‖(zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n)‖\n = (zeroMult ρ : ℝ) * ‖1 - (ρ / (ρ - 1)) ^ n‖ := by\n rw [norm_mul, RCLike.norm_natCast]\n _ ≤ (zeroMult ρ : ℝ) * 2 := by\n apply mul_le_mul_of_nonneg_left _ (Nat.cast_nonneg _)\n calc ‖1 - (ρ / (ρ - 1)) ^ n‖\n ≤ ‖(1 : ℂ)‖ + ‖(ρ / (ρ - 1)) ^ n‖ := norm_sub_le _ _\n _ = 1 + 1 := by rw [norm_one, norm_pow, hnorm_ratio, one_pow]\n _ = 2 := by norm_num\n _ = 2 * (zeroMult ρ : ℝ) := by ring\n\n/-- The nontrivial part of the zero sum: ‖Σ‖ ≤ 2·Σ mult (each term ≤ 2\non the line via `RHUpTo`). -/\nlemma zeroSum_nontriv_norm_le (hRH : RHUpTo (3 * 10 ^ 12)) {n : ℕ} {T : ℝ}\n (hTle : T ≤ 3 * 10 ^ 12) :\n ‖∑ ρ ∈ (zeroBothWindow_finite T).toFinset,\n (zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n)‖ ≤\n 2 * ∑ ρ ∈ (zeroBothWindow_finite T).toFinset, (zeroMult ρ : ℝ) := by\n calc ‖∑ ρ ∈ (zeroBothWindow_finite T).toFinset,\n (zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n)‖\n ≤ ∑ ρ ∈ (zeroBothWindow_finite T).toFinset,\n ‖(zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n)‖ := norm_sum_le _ _\n _ ≤ ∑ ρ ∈ (zeroBothWindow_finite T).toFinset, 2 * (zeroMult ρ : ℝ) := by\n apply Finset.sum_le_sum\n intro ρ hρ\n have hnt : IsNontrivialZero ρ := ((zeroBothWindow_finite T).mem_toFinset.mp hρ).1\n have him : |ρ.im| ≤ T := ((zeroBothWindow_finite T).mem_toFinset.mp hρ).2\n have hre : ρ.re = 1 / 2 := hRH ρ hnt (by linarith [him, hTle] : |ρ.im| ≤ 3 * 10 ^ 12)\n exact zeroTerm_norm_le_two hnt hre n\n _ = 2 * ∑ ρ ∈ (zeroBothWindow_finite T).toFinset, (zeroMult ρ : ℝ) := by\n rw [Finset.mul_sum]\n\n/-- The both-signs mult count is 2× the one-sign count (NoLowZeros gives\nim ≠ 0; the conj bijection with `zeroMult_conj` identifies the two\nhalves). -/\nlemma zeroBothWindow_sum_eq_two_mul (hNLZ : NoLowZeros) (T : ℝ) :\n ∑ ρ ∈ (zeroBothWindow_finite T).toFinset, (zeroMult ρ : ℝ) =\n 2 * ∑ ρ ∈ (zeroGlobalWindow_finite T).toFinset, (zeroMult ρ : ℝ) := by\n classical\n set P := (zeroGlobalWindow_finite T).toFinset with hP\n set N := (zeroGlobalWindowNeg_finite T).toFinset with hN\n have hW : (zeroBothWindow_finite T).toFinset = P ∪ N := by\n ext ρ\n rw [Finset.mem_union, (zeroBothWindow_finite T).mem_toFinset,\n (zeroGlobalWindow_finite T).mem_toFinset, (zeroGlobalWindowNeg_finite T).mem_toFinset]\n constructor\n · intro ⟨hnt, himT⟩\n have him0 : ρ.im ≠ 0 := by\n have h14 := hNLZ ρ hnt\n intro h\n rw [h, abs_zero] at h14\n exact (by norm_num : ¬ (14 : ℝ) ≤ 0) h14\n rcases lt_or_gt_of_ne him0 with hneg | hpos\n · exact Or.inr ⟨hnt, by linarith [abs_le.mp himT |>.1], hneg⟩\n · exact Or.inl ⟨hnt, hpos, by linarith [abs_le.mp himT |>.2]⟩\n · intro h\n rcases h with ⟨hnt, hpos, himT⟩ | ⟨hnt, himT, hneg⟩\n · exact ⟨hnt, by rw [abs_of_pos hpos]; exact himT⟩\n · exact ⟨hnt, by rw [abs_of_neg hneg]; linarith⟩\n have hdisj : Disjoint P N := by\n rw [Finset.disjoint_left]\n intro ρ hρP hρN\n have h1 : 0 < ρ.im := ((zeroGlobalWindow_finite T).mem_toFinset.mp hρP).2.1\n have h2 : ρ.im < 0 := ((zeroGlobalWindowNeg_finite T).mem_toFinset.mp hρN).2.2\n linarith\n have hNeq : N = P.image ⟨(starRingEnd ℂ), (starRingEnd ℂ).injective⟩ := by\n ext ρ\n rw [Finset.mem_image, (zeroGlobalWindowNeg_finite T).mem_toFinset,\n (zeroGlobalWindow_finite T).mem_toFinset]\n constructor\n · intro ⟨hnt, himT, hneg⟩\n refine ⟨(starRingEnd ℂ) ρ, ⟨isNontrivialZero_conj hnt, ?_, ?_⟩, ?_⟩\n · rw [Complex.conj_im]\n exact neg_pos.mpr hneg\n · rw [Complex.conj_im]\n linarith\n · rw [starRingEnd_apply, starRingEnd_apply, star_star]\n · rintro ⟨σ, ⟨hσnt, hσpos, hσT⟩, rfl⟩\n refine ⟨isNontrivialZero_conj hσnt, ?_, ?_⟩\n · rw [Complex.conj_im]\n linarith\n · rw [Complex.conj_im]\n linarith\n have hNsum : (∑ ρ ∈ N, (zeroMult ρ : ℝ)) = ∑ ρ ∈ P, (zeroMult ρ : ℝ) := by\n rw [hNeq, Finset.sum_image (fun ρ _ σ _ h => (starRingEnd ℂ).injective h)]\n apply Finset.sum_congr rfl\n intro ρ hρ\n have hnt : IsNontrivialZero ρ := ((zeroGlobalWindow_finite T).mem_toFinset.mp hρ).1\n have h := zeroMult_conj hnt\n rw [h]\n rw [hW, Finset.sum_union hdisj, hNsum]\n ring\n\n/-- The trivial-zero term at −2: |1 − (2/3)ⁿ| ≤ 1. -/\nlemma trivTerm_norm_le_one (n : ℕ) :\n ‖(zeroMult (-2 : ℂ) : ℂ) * (1 - ((-2 : ℂ) / (-2 - 1)) ^ n)‖ ≤ 1 := by\n have hm : (zeroMult (-2 : ℂ) : ℂ) = 1 := by\n rw [zeroMult_neg_two]\n norm_num\n rw [hm, one_mul]\n have h1 : (0 : ℝ) ≤ (2 / 3 : ℝ) := by norm_num\n have h2 : (2 / 3 : ℝ) ≤ 1 := by norm_num\n have hpow1 : (2 / 3 : ℝ) ^ n ≤ 1 := pow_le_one₀ h1 h2 n\n have hnorm : ‖(1 : ℂ) - ((-2 : ℂ) / (-2 - 1)) ^ n‖ = 1 - (2 / 3 : ℝ) ^ n := by\n have e : (-2 : ℂ) / (-2 - 1) = ((2 / 3 : ℝ) : ℂ) := by\n have h3 : (-2 : ℂ) - 1 = -3 := by norm_num\n rw [h3]\n rw [div_eq_iff (by norm_num : (-3 : ℂ) ≠ 0)]\n push_cast\n ring\n rw [e, ← ofReal_pow, ← ofReal_one, ← ofReal_sub, Complex.norm_real, Real.norm_eq_abs,\n abs_of_nonneg (by linarith : (0 : ℝ) ≤ 1 - (2 / 3 : ℝ) ^ n)]\n rw [hnorm]\n linarith\n\n/-- **The bridge** (D-071 §4.2): ‖Σ zero terms‖ ≤ 4·FAlt T + 1. The +1\nis the trivial-zero term at −2; the 4·FAlt is the both-signs count\n(2·mult per term × 2× one-sign count ≤ FAlt via the perimeter\n`ZeroCountGlobalProp`). -/\ntheorem zeroSum_norm_le_four_FAlt_add_one (hRH : RHUpTo (3 * 10 ^ 12))\n (hZCG : ZeroCountGlobalProp) (hNLZ : NoLowZeros) {n : ℕ} {T : ℝ}\n (hTle : T ≤ 3 * 10 ^ 12 - 1) (hT2 : 2 ≤ T) :\n ‖∑ ρ ∈ ((zeroBothWindow_finite T).toFinset ∪ {(-2 : ℂ)}),\n (zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n)‖ ≤ 4 * FAlt T + 1 := by\n have h2not : (-2 : ℂ) ∉ (zeroBothWindow_finite T).toFinset := by\n intro h\n have hnt := (zeroBothWindow_finite T).mem_toFinset.mp h |>.1\n have h21 : (0 : ℝ) < (-2 : ℂ).re := hnt.2.1\n simp at h21\n rw [Finset.sum_union h2not]\n have htriv := trivTerm_norm_le_one n\n have hbridge := zeroSum_nontriv_norm_le hRH (n := n) (T := T) (by linarith [hTle])\n have hcount := zeroBothWindow_sum_eq_two_mul hNLZ T\n have hZ := hZCG T hT2\n calc ‖∑ ρ ∈ (zeroBothWindow_finite T).toFinset,\n (zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n) +\n (zeroMult (-2 : ℂ) : ℂ) * (1 - ((-2 : ℂ) / (-2 - 1)) ^ n)‖\n ≤ ‖∑ ρ ∈ (zeroBothWindow_finite T).toFinset,\n (zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n)‖ +\n ‖(zeroMult (-2 : ℂ) : ℂ) * (1 - ((-2 : ℂ) / (-2 - 1)) ^ n)‖ := norm_add_le _ _\n _ ≤ (2 * ∑ ρ ∈ (zeroBothWindow_finite T).toFinset, (zeroMult ρ : ℝ)) + 1 := by\n linarith [hbridge, htriv]\n _ = 2 * (2 * ∑ ρ ∈ (zeroGlobalWindow_finite T).toFinset, (zeroMult ρ : ℝ)) + 1 := by\n rw [hcount]\n _ ≤ 4 * FAlt T + 1 := by linarith [hZ]\n\nend NguyenRH1"},"extra_content":null}]