[{"type":"thinking","thinking":"`Complex.normSq_eq_norm_sq : normSq z = ‖z‖ ^ 2` exists ✓ (used at Analysis/Complex/Basic.lean:96). Use that directly.\n\nNow rewrite the scratch with all fixes:\n1. liSummand/summand_conj: use `Complex.conj` (qualified).\n2. hbase via linarith from add_one_le_exp.\n3. hnsq via Complex.normSq_eq_norm_sq.\n4. hf: clean rewrite.\n5. max_le first arg via le_add_of_nonneg_right.\n6. hSn1 via explicit e + ← sum_sub_distrib.\n7. liSummand_eq: rw [liSummand, summand_conj, Complex.add_conj]; push_cast; ring.\n\nOne more: Complex.add_conj statement: `theorem add_conj (z : ℂ) : z + conj z = (2 * z.re : ℝ)` — note the cast: the RHS `(2 * z.re : ℝ)` is ℝ then coerced: actually written `(2 * z.re : ℝ)` with target ℂ, so it's `((2 * z.re : ℝ) : ℂ)`. So after rw, goal: ↑(zeroMult)/2 * ↑(2 * f.re) = ↑(zeroMult) * ↑(f.re) — push_cast then ring ✓.\n\nAlso summand_conj's `rw [map_sub, map_one, map_pow, map_sub, map_one, map_div₀, map_one]` — conj = starRingEnd ℂ; map_sub (starRingEnd ℂ) : conj (a−b) = conj a − conj b ✓. The statement has conj ((1 − (1 − 1/z)^n)) on RHS; rw works left-to-right on goal `1 − (1 − 1/conj z)^n = conj (1 − (1 − 1/z)^n)`: the rw of map_sub applies to the RHS occurrence `conj (1 − ...)` → `conj 1 − conj ((1 − 1/z)^n)` then map_one: `1 − conj(...)`; map_pow: `conj(1 − 1/z)^n`; map_sub: `(conj 1 − conj (1/z))^n`; map_one; map_div₀: `conj 1 / conj z`; map_one: `1 / conj z` ✓ goal becomes `1 − (1 − 1/conj z)^n = 1 − (1 − 1/conj z)^n` rfl ✓.\n\nWrite the file.","signature":""},{"type":"text","text":"`Complex.normSq_eq_norm_sq` exists. Rewriting with all fixes."},{"type":"tool_use","id":"Write_95","name":"Write","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\Scratch.lean","content":"/- Session 015 scratch: ii′-1a — paired liSummand + summability (D-064 §1).\n   When green, merge into LiSkeleton.lean §1 replacing the defective liCoeff. -/\nimport Mathlib\nimport Zeta23.WeilEF.ZeroSummability\nimport Zeta23.Statement.SeamClosed\n\nopen Zeta23 Complex Filter Topology\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-- The paired (symmetrized) Li summand: ½·mult·(f ρ + f ρ̄),\nf ρ = 1 − (1−1/ρ)ⁿ. Manifestly real-valued (`liSummand_eq`), absolutely\nsummable (`liSummable`) — the correct Keiper–Li coefficient (D-064 §1:\nthe plain unordered sum of f over the zeros is not absolutely\nsummable; the pairing is the classical Bombieri–Lagarias convention). -/\ndef liSummand (n : ℕ) (ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℂ :=\n  (zeroMult ρ : ℂ) / 2 *\n    ((1 - (1 - 1 / (ρ : ℂ)) ^ n) + (1 - (1 - 1 / (Complex.conj (ρ : ℂ))) ^ n))\n\nlemma summand_conj (n : ℕ) (z : ℂ) :\n    (1 : ℂ) - (1 - 1 / (Complex.conj z)) ^ n = Complex.conj ((1 - (1 - 1 / z) ^ n)) := by\n  rw [map_sub, map_one, map_pow, map_sub, map_one, map_div₀, map_one]\n\nlemma liSummand_eq (n : ℕ) (ρ : {ρ : ℂ // IsNontrivialZero ρ}) :\n    liSummand n ρ = (zeroMult ρ : ℂ) * (((1 - (1 - 1 / (ρ : ℂ)) ^ n).re) : ℂ) := by\n  rw [liSummand, summand_conj, Complex.add_conj]\n  push_cast\n  ring\n\n/-! ### The geometric-sum estimate: |Re(1 − wⁿ)| ≤ 2n²/‖z‖² for w = 1−1/z -/\n\n/-- (1 + 1/(2n))ⁿ ≤ 2 for n ≥ 1. Via (1+x)ⁿ ≤ exp(nx) and exp(1/2) ≤ 2. -/\nlemma pow_one_add_inv_two_mul_le (n : ℕ) (hn : 1 ≤ n) :\n    ((1 : ℝ) + 1 / (2 * n)) ^ n ≤ 2 := by\n  have hn0 : (0 : ℝ) < n := by exact_mod_cast hn\n  have hbase : (1 : ℝ) + 1 / (2 * n) ≤ Real.exp (1 / (2 * n)) := by\n    have h := Real.add_one_le_exp (1 / (2 * (n : ℝ)))\n    linarith\n  have h1 : ((1 : ℝ) + 1 / (2 * n)) ^ n ≤ Real.exp (1 / 2) := by\n    calc ((1 : ℝ) + 1 / (2 * n)) ^ n\n        ≤ (Real.exp (1 / (2 * n))) ^ n := pow_le_pow_left₀ (by positivity) hbase n\n      _ = Real.exp (↑n * (1 / (2 * n))) := by rw [Real.exp_nat_mul]\n      _ = Real.exp (1 / 2) := by congr 1; field_simp\n  have h2 : Real.exp (1 / 2 : ℝ) ≤ 2 := by\n    have h3 : (1 : ℝ) / 2 ≤ Real.log 2 := by\n      have h := Real.log_two_gt_d9\n      linarith\n    calc Real.exp (1 / 2 : ℝ) ≤ Real.exp (Real.log 2) := Real.exp_le_exp.mpr h3\n      _ = 2 := Real.exp_log (by norm_num)\n  exact h1.trans h2\n\n/-- Key estimate: for n ≥ 1, z with re z ∈ [0,1], 2n ≤ ‖z‖:\n|Re(1 − (1−1/z)ⁿ)| ≤ 2n²/‖z‖². -/\nlemma re_li_summand_le {n : ℕ} (hn : 1 ≤ n) {z : ℂ}\n    (hzre0 : 0 ≤ z.re) (hzre1 : z.re ≤ 1) (hz : 2 * n ≤ ‖z‖) :\n    |(1 - (1 - 1 / z) ^ n).re| ≤ 2 * n ^ 2 / ‖z‖ ^ 2 := by\n  have hn0 : (0 : ℝ) < n := by exact_mod_cast hn\n  have hz0 : z ≠ 0 := by\n    intro h; rw [h, norm_zero] at hz; linarith\n  have hzn : (0 : ℝ) < ‖z‖ := norm_pos_iff.mpr hz0\n  have hnsq : Complex.normSq z = ‖z‖ ^ 2 := Complex.normSq_eq_norm_sq z\n  set w : ℂ := 1 - 1 / z with hw\n  -- kernel identity: 1 − wⁿ = (1/z)·S, S = Σ_{j<n} w^j\n  have hgeom : (w - 1) * ∑ j ∈ Finset.range n, w ^ j = w ^ n - 1 := mul_geom_sum w n\n  have hw1 : w - 1 = -(1 / z) := by rw [hw]; ring\n  have hf : (1 : ℂ) - w ^ n = (1 / z) * ∑ j ∈ Finset.range n, w ^ j := by\n    have e : (1 : ℂ) - w ^ n = -(w ^ n - 1) := by ring\n    rw [e, ← hgeom, hw1]; ring\n  set S : ℂ := ∑ j ∈ Finset.range n, w ^ j\n  have hS : S = (n : ℂ) + (S - n) := by ring\n  -- ‖w‖ ≤ 1 + 1/‖z‖\n  have hwnorm : ‖w‖ ≤ 1 + 1 / ‖z‖ := by\n    have e : w = 1 - z⁻¹ := by rw [hw, div_eq_mul_inv, one_mul]\n    rw [e]\n    calc ‖(1 : ℂ) - z⁻¹‖ ≤ ‖(1 : ℂ)‖ + ‖z⁻¹‖ := norm_sub_le _ _\n      _ = 1 + 1 / ‖z‖ := by rw [norm_one, norm_inv, inv_eq_one_div]\n  have h1z : 1 / ‖z‖ ≤ 1 / (2 * n) :=\n    one_div_le_one_div_of_le (by positivity) (by exact_mod_cast hz)\n  have hwmax : max 1 ‖w‖ ≤ 1 + 1 / (2 * n) := by\n    apply max_le (le_add_of_nonneg_right (by positivity))\n    exact hwnorm.trans (by linarith)\n  -- |S − n| ≤ n²/‖z‖\n  have hSn : ‖S - n‖ ≤ n ^ 2 / ‖z‖ := by\n    have hSn1 : S - n = ∑ j ∈ Finset.range n, (w ^ j - 1) := by\n      have e : (n : ℂ) = ∑ j ∈ Finset.range n, (1 : ℂ) := by\n        simp [Finset.sum_const, Finset.card_range]\n      rw [e, ← Finset.sum_sub_distrib]\n    have hbound : ∀ j ∈ Finset.range n,\n        ‖w ^ j - 1‖ ≤ (1 / ‖z‖) * (j * (1 + 1 / (2 * n)) ^ (n - 1)) := by\n      intro j hj\n      have hgeomj : (w - 1) * ∑ i ∈ Finset.range j, w ^ i = w ^ j - 1 := mul_geom_sum w j\n      have hjn : j ≤ n := le_of_lt (Finset.mem_range.mp hj)\n      have h2 : w ^ j - 1 = -(1 / z) * ∑ i ∈ Finset.range j, w ^ i := by\n        have h := hgeomj; rw [hw1] at h\n        rw [← h]; ring\n      rw [h2, norm_mul, norm_neg, norm_div, norm_one]\n      have hsum : ‖∑ i ∈ Finset.range j, w ^ i‖ ≤ j * (1 + 1 / (2 * n)) ^ (n - 1) := by\n        calc ‖∑ i ∈ Finset.range j, w ^ i‖\n            ≤ ∑ i ∈ Finset.range j, ‖w ^ i‖ := norm_sum_le _ _\n          _ ≤ ∑ i ∈ Finset.range j, (1 + 1 / (2 * n)) ^ (n - 1) := by\n              apply Finset.sum_le_sum\n              intro i hi\n              rw [norm_pow]\n              have hij : i < j := Finset.mem_range.mp hi\n              have h1 : ‖w‖ ^ i ≤ (1 + 1 / (2 * n)) ^ i :=\n                pow_le_pow_left₀ (norm_nonneg _)\n                  (le_trans (le_max_right 1 ‖w‖) hwmax) i\n              have h2 : (1 + 1 / (2 * n)) ^ i ≤ (1 + 1 / (2 * n)) ^ (n - 1) := by\n                apply pow_le_pow_right₀ (by positivity)\n                omega\n              exact h1.trans h2\n          _ = j * (1 + 1 / (2 * n)) ^ (n - 1) := by\n              rw [Finset.sum_const, Finset.card_range, nsmul_eq_mul]\n      exact mul_le_mul_of_nonneg_left hsum (by positivity)\n    calc ‖∑ j ∈ Finset.range n, (w ^ j - 1)‖\n        ≤ ∑ j ∈ Finset.range n, ‖w ^ j - 1‖ := norm_sum_le _ _\n      _ ≤ ∑ j ∈ Finset.range n, (1 / ‖z‖) * (j * (1 + 1 / (2 * n)) ^ (n - 1)) := by\n          rw [hSn1] at *\n          exact Finset.sum_le_sum hbound\n      _ = ((1 / ‖z‖) * (1 + 1 / (2 * n)) ^ (n - 1)) * ∑ j ∈ Finset.range n, j := by\n          rw [← Finset.mul_sum]\n          apply Finset.sum_congr rfl\n          intro j _; ring\n      _ ≤ n ^ 2 / ‖z‖ := by\n          have hsumj : (∑ j ∈ Finset.range n, j : ℝ) = n * (n - 1) / 2 := by\n            have h := Finset.sum_range_id_mul_two n\n            have h2 : ((∑ j ∈ Finset.range n, j : ℕ) : ℝ) * 2 = n * (n - 1) := by\n              exact_mod_cast h\n            linarith\n          rw [hsumj]\n          have hpow : (1 + 1 / (2 * n : ℝ)) ^ (n - 1) ≤ 2 :=\n            le_trans (pow_le_pow_right₀ (by positivity) (Nat.sub_le n 1))\n              (pow_one_add_inv_two_mul_le n hn)\n          have hb1 : (n : ℝ) * (n - 1) / 2 ≤ n ^ 2 / 2 := by nlinarith [hn0]\n          have hb2 : (1 + 1 / (2 * n : ℝ)) ^ (n - 1) * (n * (n - 1) / 2)\n              ≤ 2 * (n ^ 2 / 2) :=\n            mul_le_mul_of_nonneg hpow hb1 (by positivity) (by positivity)\n          have hb3 : ((1 : ℝ) / ‖z‖) * (1 + 1 / (2 * n)) ^ (n - 1) * (n * (n - 1) / 2)\n              ≤ (1 / ‖z‖) * (2 * (n ^ 2 / 2)) :=\n            mul_le_mul_of_nonneg_left hb2 (by positivity)\n          exact hb3.trans (by ring_nf)\n  -- Re(f) = n·z.re/‖z‖² + ((S−n)/z).re\n  have hre1 : ((n : ℂ) * (1 / z)).re = n * z.re / ‖z‖ ^ 2 := by\n    have hinv : ((1 : ℂ) / z).re = z.re / ‖z‖ ^ 2 := by\n      rw [one_div, Complex.inv_re, hnsq]\n    rw [Complex.mul_re]\n    simp [hinv]\n  have hfre : (1 - w ^ n).re = n * z.re / ‖z‖ ^ 2 + ((S - n) / z).re := by\n    rw [hf, hS, Complex.add_re]\n    congr 1\n    rw [mul_comm, div_eq_mul_inv]\n    exact hre1\n  rw [hfre]\n  have hA : |n * z.re / ‖z‖ ^ 2| ≤ n / ‖z‖ ^ 2 := by\n    rw [abs_div, abs_mul, abs_of_nonneg hn0.le,\n      abs_of_nonneg (sq_nonneg ‖z‖)]\n    apply (div_le_div_right (by positivity)).mpr\n    apply mul_le_mul_of_nonneg_left _ hn0.le\n    exact abs_le.mpr ⟨hzre0, hzre1⟩\n  have hB : |((S - n) / z).re| ≤ n ^ 2 / ‖z‖ ^ 2 := by\n    have h1 : |((S - n) / z).re| ≤ ‖(S - n) / z‖ := Complex.abs_re_le_norm _\n    have h2 : ‖(S - n) / z‖ ≤ (n ^ 2 / ‖z‖) / ‖z‖ := by\n      rw [norm_div]\n      exact (div_le_div_right hzn).mpr hSn\n    exact h1.trans (h2.trans (by rw [div_div, ← pow_two]))\n  have hnn : (n : ℝ) ≤ n ^ 2 := by\n    have h : (1 : ℝ) ≤ n := by exact_mod_cast hn\n    nlinarith\n  calc |n * z.re / ‖z‖ ^ 2 + ((S - n) / z).re|\n      ≤ n / ‖z‖ ^ 2 + n ^ 2 / ‖z‖ ^ 2 := (abs_add _ _).trans (add_le_add hA hB)\n    _ = (n + n ^ 2) / ‖z‖ ^ 2 := by ring\n    _ ≤ 2 * n ^ 2 / ‖z‖ ^ 2 := by\n        apply (div_le_div_right (by positivity)).mpr\n        linarith\n\nend NguyenRH1\n"},"extra_content":null}]