[{"type":"thinking","thinking":"Good news: `zetaZeroConfig_carrier : zetaZeroConfig.carrier = {ρ | IsNontrivialZero ρ}` is rfl — and the header comment mentions `riemannZeta_conj` exists in ZetaReflect (Schwarz reflection uses it) — so the conj-symmetry lemma `riemannZeta_conj` EXISTS somewhere. Let me check zero_sum_inv_sq's exact form once more: it's stated for `(zetaZeros hs).carrier` — the `zetaZeros` function takes hs : ZetaSeam and returns a ZeroConfig. zetaZeroConfig = zetaZeros zetaSeam. The carrier of that = {ρ | IsNontrivialZero ρ} by rfl.\n\nSo the subtype `(zetaZeros zetaSeam).carrier` = `{ρ // ρ ∈ {ρ | IsNontrivialZero ρ}}` = `{ρ // IsNontrivialZero ρ}` — definitionally the same type (Set membership in a setOf is the predicate). So I can use `zero_sum_inv_sq zetaSeam` directly with our subtype via `show`.\n\nNow let me write the proof. Structure:\n\n```lean\n/-- The paired Li summand. -/\ndef liSummand (n : ℕ) (ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℂ :=\n  (zeroMult ρ : ℂ) / 2 * ((1 - (1 - 1 / (ρ : ℂ)) ^ n) + (1 - (1 - 1 / (star (ρ : ℂ))) ^ n))\n\ndef liCoeff (n : ℕ) : ℂ := ∑' ρ, liSummand n ρ\n```\n\nKey steps:\n1. `liSummand_eq_re : liSummand n ρ = (zeroMult ρ : ℂ) * (((1 - (1 - 1/(ρ:ℂ))^n).re) : ℂ)`\n   proof: ½(f + star f) = re f: show 1 - (1 - 1/(star z))^n = star (1 - (1 - 1/z)^n). star is RingEquiv... simp with: map_sub, map_pow, map_one, map_div, map_natCast? The expression: 1 - (1 - 1/z)^n where n : ℕ and z : ℂ. star(1) = 1, star(z⁻¹) = (star z)⁻¹ — `map_inv₀`, `map_div₀`? In Mathlib: `star_div` (star (a/b) = star a / star b) — for division ring with star: `star_div'`. `star_pow`, `star_sub`, `star_one`, `star_natCast`? For the 1 in \"1/ρ\": (1 : ℂ). Should be `by simp [star_div, star_pow, star_sub, star_one]` or with `map_sub (starRingEnd ℂ) _ _`-style. Try simp first.\n   Then (zeroMult : ℂ)/2 * (f + star f) = (zeroMult : ℂ) * ((f + star f)/2) and (f + star f)/2 = (f.re : ℂ): `Complex.add_conj : z + star z = 2 * (z.re : ℂ)`. So f + star f = 2 re f: ½·mult·(f + star f) = mult·re f ✓.\n\n2. Norm bound: for ρ with 2n ≤ ‖(ρ:ℂ)‖ (and n ≥ 1):\n   ‖liSummand n ρ‖ = mult·|Re f| ≤ 2n²·mult/‖ρ‖².\n   \n   Wait — mult is a Nat; in the norm: ‖(zeroMult ρ : ℂ)‖ = zeroMult ρ (as a real, ≥ 0) ✓.\n   \n   The analytic lemma: |Re(1 − wⁿ)| ≤ 2n²/‖ρ‖² with w = 1 − 1/ρ.\n   \n   Sub-lemmas:\n   (a) f = (1/ρ)·S, S = Σ_{j<n} w^j: 1 − wⁿ = −(wⁿ−1) = −(w−1)·S; w−1 = −1/ρ; so 1−wⁿ = S/ρ. Mathlib: `geom_sum_mul : (x - 1) * ∑ i ∈ range n, x ^ i = x ^ n - 1` — need (w−1): use (w - 1) * geom = w^n - 1 (that's geom_sum_mul ✓) so wⁿ−1 = (w−1)·geom ✓.\n   (b) Re(S/ρ) = n·ρ.re/‖ρ‖² + Re((S−n)/ρ).\n   (c) |S − n| ≤ n²/‖ρ‖: S − n = Σ_{j<n}(w^j − 1); w^j − 1 = (w−1)·Σ_{i<j} w^i (geom_sum_mul again with j terms); |Σ_{i<j} w^i| ≤ Σ_{i<j} |w|^i ≤ j·(max 1 |w|)^j ≤ j·(max 1 |w|)^{n-1}. So |S−n| ≤ |w−1|·n²/2·(max 1 |w|)^{n-1}·... Σ_{j<n} j = n(n−1)/2 ≤ n²/2.\n   (d) |w| ≤ 1 + 1/‖ρ‖ so max 1 |w| ≤ 1+1/‖ρ‖ ≤ 1 + 1/(2n): (1+1/(2n))^{n-1} ≤ (1+1/(2n))^n ≤ 2. The last: (1+x)^n ≤ exp(nx) ≤ exp(1/2) ≤ 2 for x = 1/(2n).\n   (e) Re(1/ρ) = ρ.re/‖ρ‖²: `Complex.div_re`? For 1/z: 1/z = conj z/‖z‖²: re = z.re/‖z‖². There's `Complex.inv_re : (z⁻¹.re) = z.re / ‖z‖²`? I recall `Complex.inv_re : z⁻¹.re = z.re / (z.re^2 + z.im^2)` or via normSq. Whatever — provable.\n   |Re f| ≤ n·|ρ.re|/‖ρ‖² + |S−n|/‖ρ‖ ≤ n/‖ρ‖² + n²/‖ρ‖² = (n+n²)/‖ρ‖² ≤ 2n²/‖ρ‖² (n ≥ 1). Note ρ.re ≥ 0? Re(1/ρ) = ρ.re/‖ρ‖² and ρ.re ∈ (0,1) for nontrivial zeros: |Re(1/ρ)| = |ρ.re|/‖ρ‖² ≤ 1/‖ρ‖² ✓ (|ρ.re| ≤ 1).\n\n3. Comparison: (1+‖gammaOf ρ‖²) ≤ (9/4)‖ρ‖² for ‖ρ‖ ≥ 2n (n ≥ 1):\n   1+‖γ_ρ‖² = 1+γ²+(σ−1/2)² ≤ 1+γ²+1/4 = 5/4+γ²; (9/4)‖ρ‖² = (9/4)(σ²+γ²) ≥ (9/4)γ².\n   5/4+γ² ≤ (9/4)γ² ⟺ 5/4 ≤ (5/4)γ² ⟺ 1 ≤ γ²: γ² = ‖ρ‖²−σ² ≥ 4n²−1 ≥ 3 (n ≥ 1) ✓.\n   So mult/‖ρ‖² ≤ (9/4)·mult/(1+‖γ_ρ‖²).\n\n4. Dominator: D(ρ) = if 2n ≤ ‖(ρ:ℂ)‖ then (9/2)n²·mult/(1+‖γ_ρ‖²) else ‖liSummand n ρ‖.\n   D summable: D = D₀ + (D − D₀) where D₀(ρ) = (9/2)n²·mult/(1+‖γ‖²) summable (zero_sum_inv_sq zetaSeam .mul_left); D − D₀ supported in {ρ : ‖ρ‖ < 2n} — finite (ball ∩ zeros, via IsCompact.inter_riemannZetaZeros_finite — wait, that's for riemannZetaZeros (the full preimage of 0); our subtype is IsNontrivialZero ρ which includes riemannZeta ρ = 0 ✓ so the set {ρ : IsNontrivialZero ρ ∧ ‖ρ‖ < 2n} ⊆ (closedBall 0 2n) ∩ riemannZetaZeros — finite ✓).\n   Hmm wait — D−D₀ on the ball: D−D₀(ρ) = ‖liSummand‖ − (9/2)n²·mult/(1+‖γ‖²) — supported where NOT 2n ≤ ‖ρ‖, i.e. ‖ρ‖ < 2n ✓ finite support. `summable_of_finite_support`.\n   Hmm — but careful: on the support, D−D₀ could be negative; summable is fine anyway.\n   \n   Then Summable (fun ρ => liSummand n ρ) via `Summable.of_norm_bounded (hD : Summable D) (h : ∀ ρ, ‖liSummand n ρ‖ ≤ D ρ)` — the inequality: if 2n ≤ ‖ρ‖: by step 2+3: ‖liSummand‖ ≤ 2n² mult/‖ρ‖² ≤ (9/2)n² mult/(1+‖γ‖²) = D ✓. else: D = ‖liSummand‖ ✓ le_refl.\n\n   Note: `Summable.of_norm_bounded : Summable g → (∀ i, ‖f i‖ ≤ g i) → Summable f` — signature: `Summable.of_norm_bounded (hg : Summable g) (h : ∀ i, ‖f i‖ ≤ g i) : Summable f`? Let me check exact: in Mathlib it's `Summable.of_norm_bounded {f : α → E} {g : α → ℝ} (hg : Summable g) (h : ∀ i, ‖f i‖ ≤ g i) : Summable f`? I think it's `Summable.of_norm_bounded (hg : Summable g) (h : ∀ i, ‖f i‖ ≤ g i)`. Yes.\n\n5. Also need: `Complex.normSq (gammaOf ρ)` = γ² + (σ−1/2)² — for step 3. gammaOf ρ = (ρ − 1/2)/I. normSq: Complex.normSq z = z.re² + z.im². gammaOf_re : (gammaOf ρ).re = ρ.im; gammaOf_im : (gammaOf ρ).im = 1/2 − ρ.re (from ZeroSummability.lean — PUBLIC lemmas there ✓). So normSq (gammaOf ρ) = ρ.im² + (1/2 − ρ.re)². Those lemmas exist (gammaOf_re, gammaOf_im in Zeta23.WeilEF namespace).\n\n6. zeroMult coercion: zeroMult ρ for ρ : {ρ // IsNontrivialZero ρ} — how does the current liCoeff use it? `(zeroMult ρ : ℂ)` — zeroMult takes ℂ: `def zeroMult (ρ : ℂ) : ℕ`. So zeroMult ρ means zeroMult (ρ:ℂ)? With ρ : subtype, `zeroMult ρ` — there's a coercion; current code works so ✓.\n\n7. The sum type mismatch: zero_sum_inv_sq zetaSeam : Summable (fun ρ : (zetaZeros zetaSeam).carrier => ...). The subtype (zetaZeros zetaSeam).carrier vs {ρ // IsNontrivialZero ρ}: carrier = {ρ | IsNontrivialZero ρ} (rfl per zetaZeroConfig_carrier? — that's for zetaZeroConfig = zetaZeros zetaSeam ✓ same object). {ρ // ρ ∈ {ρ | IsNontrivialZero ρ}} — membership in setOf is defeq to the predicate ✓ so the subtypes are defeq. `show` should convert. If not, use an Equiv.\n\nLet me now write the Scratch.lean development. I'll write it directly as the final form for LiSkeleton (then paste). First draft in Scratch:\n\n```lean\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 ρ̄) with\nf ρ = 1 − (1−1/ρ)ⁿ. Manifestly real-valued; absolutely summable\n(liSummable below) — the correct Keiper–Li coefficient. -/\ndef liSummand (n : ℕ) (ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℂ :=\n  (zeroMult ρ : ℂ) / 2 * ((1 - (1 - 1 / (ρ : ℂ)) ^ n) + (1 - (1 - 1 / (star (ρ : ℂ))) ^ n))\n\nlemma star_summand (n : ℕ) (z : ℂ) :\n    1 - (1 - 1 / (star z)) ^ n = star (1 - (1 - 1 / z) ^ n) := by\n  simp [map_sub, map_one, map_pow, map_div, map_natCast] -- hope simp closes\n```\n\nHmm, star (1 - (1 - 1/z)^n): star is the ring endomorphism; the expression uses: 1 (Nat cast? no — literal 1 : ℂ), sub, div, pow (ℕ). simp lemmas: `map_sub (starRingEnd ℂ)`, `map_one`, `map_div₀`, `map_pow`. `starRingEnd ℂ` applied: star (1 - (1 - 1/z)^n) = star 1 - star((1 - 1/z)^n) = 1 - (star(1 - 1/z))^n = 1 - (1 - star(1/z))^n = 1 - (1 - 1/star z)^n ✓. So:\n\nstar (1 - (1 - 1/z)^n) = 1 - (1 - 1/(star z))^n — the lemma direction reversed. Write:\n```lean\nlemma summand_star (n : ℕ) (z : ℂ) :\n    (1 : ℂ) - (1 - 1 / (star z)) ^ n = star ((1 - (1 - 1 / z) ^ n)) := by\n  rw [map_sub, map_one, map_pow, map_sub, map_one, map_div, map_one]\n```\nmap_div for starRingEnd: `map_div₀ (f : α →+* β) (a b) : f (a / b) = f a / f b`. Should work. Then:\n\n```lean\nlemma liSummand_eq (n : ℕ) (ρ : {ρ : ℂ // IsNontrivialZero ρ}) :\n    liSummand n ρ = (zeroMult ρ : ℂ) * (((1 - (1 - 1 / (ρ : ℂ)) ^ n).re) : ℂ) := by\n  rw [liSummand, summand_star]\n  have h : (1 - (1 - 1 / (ρ : ℂ)) ^ n) + star (1 - (1 - 1 / (ρ : ℂ)) ^ n)\n      = 2 * (((1 - (1 - 1 / (ρ : ℂ)) ^ n).re) : ℂ) := Complex.add_conj _\n  -- (mult/2) * (2 * re) = mult * re\n  rw [h]; ring\n```\n`Complex.add_conj : z + star z = 2 * (z.re : ℂ)` ✓ (I believe it's `Complex.add_conj (z : ℂ) : z + star z = 2 * (z.re : ℂ)`).\n\nNow the norm bound. Let me define things: for the analytic lemma I'll work with z : ℂ directly:\n\n```lean\nlemma re_li_bound {n : ℕ} (hn : 1 ≤ n) {z : ℂ} (hzre : z.re ∈ Set.Icc 0 1) (hz : 2 * n ≤ ‖z‖) :\n    |(1 - (1 - 1 / z) ^ n).re| ≤ 2 * n ^ 2 / ‖z‖ ^ 2 := by\n  ...\n```\n\nProof plan:\n- set w := 1 - 1/z.\n- hw1 : w - 1 = -(1/z) — ring.\n- hgeom : w^n - 1 = (w - 1) * ∑ j in range n, w^j := geom_sum_mul w n — actually `geom_sum_mul (x : α) (n : ℕ) : (x - 1) * ∑ i ∈ range n, x ^ i = x ^ n - 1` ✓.\n- So 1 - w^n = -(w-1) * S = (1/z) * S with S := ∑ j in range n, w^j.\n- f.re = Re((1/z)·S) = Re((1/z)·n) + Re((1/z)(S−n)) = n·z.re/‖z‖² + Re((S−n)/z).\n- Bound A: |n·z.re/‖z‖²| ≤ n/‖z‖² (|z.re| ≤ 1 from hzre ⊆ [0,1]).\n- Bound B: |S − n| ≤ n²/‖z‖:\n  S − n = ∑_{j<n} (w^j − 1) = ∑_{j<n} (w−1)·(∑_{i<j} w^i).\n  |w^j − 1| = |w−1|·|∑_{i<j} w^i| ≤ |w−1|·∑_{i<j}|w|^i ≤ |w−1|·j·(max 1 |w|)^{n-1}... hmm |Σ_{i<j} w^i| ≤ Σ_{i<j} |w|^i ≤ j·max(1,|w|)^j — for j ≤ n−1: ≤ j·max(1,|w|)^{n-1} (if j ≤ n−1, max^j ≤ max^{n-1} since max ≥ 1 ✓).\n  Sum over j: |S−n| ≤ |w−1|·max(1,|w|)^{n-1}·Σ_{j<n} j = |w−1|·max(1,|w|)^{n-1}·n(n−1)/2.\n  |w−1| = 1/‖z‖; max(1,|w|) ≤ 1+1/‖z‖ ≤ 1+1/(2n); (1+1/(2n))^{n-1} ≤ (1+1/(2n))^n ≤ 2.\n  So |S−n| ≤ (1/‖z‖)·2·(n²/2) = n²/‖z‖ ✓.\n- |Re f| ≤ n/‖z‖² + n²/‖z‖·(1/‖z‖) = (n+n²)/‖z‖² ≤ 2n²/‖z‖² ✓ (n ≤ n² for n ≥ 1).\n\nSub-facts to prove in Lean:\n- ‖1/z‖ = 1/‖z‖: `norm_inv`.\n- |w| ≤ 1 + 1/‖z‖: w = 1 − 1/z: |w| ≤ 1 + |1/z| ✓ triangle.\n- (1 + 1/(2n))^n ≤ 2: as discussed — (1+x)^n ≤ exp(nx): from `Real.add_one_le_exp : 1 + x ≤ Real.exp x` (for all x? the Mathlib version: `Real.add_one_le_exp (x : ℝ) : 1 + x ≤ Real.exp x` ✓ I think it holds for all real x). pow: (1+x)^n ≤ (exp x)^n = exp(n·x) — `Real.exp_nat_mul : Real.exp (n * x) = (Real.exp x) ^ n`? The direction: Real.exp_nat_mul states exp (n*x) = (exp x)^n I believe ✓. With x = 1/(2n): exp(n·(1/(2n))) = exp(1/2) ≤ 2: exp(1/2) ≤ 2 ⟸ exp(1/2)^2 = exp 1 ≤ 4 ⟸ e ≤ 4: `Real.exp_one_lt_d9 : Real.exp 1 < 2.7182818286` ✓ so exp(1/2) ≤ 2 via sq: (exp(1/2))² = exp(2·(1/2)) = exp(1) ≤ 4 ⟹ exp(1/2) ≤ 2 (nonneg). ✓\n- Re((1/z)·n) = n·z.re/‖z‖²: (1/z).re = z.re/‖z‖²: `Complex.inv_re : (z⁻¹.re) = z.re / ‖z‖^2`? I believe there's `Complex.inv_re (z : ℂ) : (z⁻¹).re = z.re / Complex.normSq z` or `Complex.div_re`. One-div: 1/z = z⁻¹ ✓. And (n·(1/z)).re = n·(1/z).re (nat cast real). normSq z = ‖z‖²: `Complex.normSq_eq_norm_sq`? There's `Complex.normSq_eq_abs : normSq z = (Complex.abs z)^2` and abs = ‖z‖ (`Complex.abs_eq_norm`? ‖z‖ = Complex.abs z defeq? `Complex.norm_eq_abs` ✓).\n\n- The geom sum bound |Σ_{i<j} w^i| ≤ Σ_{i<j}|w|^i: `norm_sum_le`; Σ_{i<j} |w|^i ≤ j·max^j: each term |w|^i ≤ max(1,|w|)^j for i < j (pow_le_pow_left₀ with max ≥ |w| ≥ 0 and i ≤ j−1 < j... need i ≤ j: i < j ⟹ i ≤ j−1, and |w|^i ≤ max^i ≤ max^j ✓ since max ≥ 1).\n  Hmm wait: for j, bound Σ_{i ∈ range j} |w|^i ≤ j·max(1,|w|)^j: i < j ⟹ |w|^i ≤ max(1,|w|)^i ≤ max(1,|w|)^j ✓ (pow monotone, base ≥ 1, i ≤ j).\n\n- Σ_{j ∈ range n} j = n(n−1)/2: `Finset.sum_range_id`? There's `Finset.sum_range_id_mul_two : (∑ i ∈ range n, i) * 2 = n * (n - 1)`. In ℝ: Σ j = n(n−1)/2. ✓\n\nThen the final assembly. This is a decent chunk — let me estimate: ~200–300 lines with careful norm estimates. The `nlinarith`/`gcongr` tactics will help.\n\nLet me also think about whether to prove with ‖z‖ or normSq — use ‖z‖ consistently; ‖z‖² means (‖z‖)^2.\n\nThe comparison step:\n```lean\nlemma normSq_gammaOf_le (z : ℂ) (hzre : z.re ∈ Set.Icc 0 1) (hgam : 1 ≤ z.im^2) :\n    1 + Complex.normSq (gammaOf z) ≤ 9/4 * ‖z‖^2\n```\nnormSq (gammaOf z) = z.im² + (1/2 − z.re)² (via gammaOf_re/gammaOf_im).\n1 + z.im² + (1/2−z.re)² ≤ 1 + z.im² + 1/4 (|1/2 − z.re| ≤ 1/2 since z.re ∈ [0,1]).\n≤ 5/4 + z.im². And 9/4·‖z‖² = 9/4·(z.re² + z.im²) ≥ 9/4·z.im².\nNeed 5/4 + z.im² ≤ 9/4·z.im² ⟺ 5/4 ≤ 5/4·z.im² ⟺ 1 ≤ z.im² ✓ hgam.\n‖z‖² = z.re² + z.im²: `Complex.sq_norm`? ‖z‖² = normSq z: `Complex.normSq_eq_norm_sq`? I recall `Complex.sq_abs_sub_sq_re_add_sq_im`... simplest: ‖z‖^2 = z.re^2 + z.im^2 — there is `Complex.normSq_apply : normSq z = z.re^2 + z.im^2` and `Complex.norm_eq_abs : ‖z‖ = Complex.abs z` and `Complex.sq_abs : (Complex.abs z)^2 = normSq z` — `Complex.sq_abs (z) : (Complex.abs z)^2 = Complex.normSq z`? I think `Complex.sq_abs` exists (abs z ^ 2 = normSq z). OK.\n\nAnd |γ| ≥ 1 from 2n ≤ ‖z‖: γ² = ‖z‖² − z.re² ≥ 4n² − 1 ≥ 3 ≥ 1 ✓.\n\nAssembly:\n```lean\ntheorem liSummable (n : ℕ) : Summable (liSummand n) := by\n  cases Nat.eq_zero_or_pos n with\n  | inl h => -- n = 0: summand = 0\n      subst h; simp [liSummand] -- (1 - (1-1/z)^0) = 0\n  | inr hn =>\n  -- main case n ≥ 1\n  ...\n```\n\nThen the dominator D with if-then-else and finite support:\n\n```lean\n  let D : {ρ // IsNontrivialZero ρ} → ℝ := fun ρ =>\n    if 2 * n ≤ ‖(ρ : ℂ)‖ then (9/2) * n^2 * (zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf ρ))\n    else ‖liSummand n ρ‖\n  have hD : Summable D := by\n    have hbase := (WeilEF.zero_sum_inv_sq zetaSeam).mul_left ((9/2) * (n:ℝ)^2)\n    -- D = Dbase + (D − Dbase), D−Dbase finite support\n    ...\n  exact Summable.of_norm_bounded hD (fun ρ => ...)\n```\n\nWait — `zero_sum_inv_sq zetaSeam` has family over `(zetaZeros zetaSeam).carrier` — defeq to our subtype? zetaZeroConfig = zetaZeros zetaSeam and zetaZeroConfig_carrier : zetaZeroConfig.carrier = {ρ | IsNontrivialZero ρ} := rfl. So (zetaZeros zetaSeam).carrier = {ρ | IsNontrivialZero ρ} definitionally. The subtype {x // x ∈ {ρ | IsNontrivialZero ρ}} vs {ρ // IsNontrivialZero ρ}: `Set.mem_setOf_eq : a ∈ {x | p x} = p a` — defeq ✓. So `show Summable (fun ρ : {ρ // IsNontrivialZero ρ} => (zeroMult ρ : ℝ)/(1+normSq (gammaOf ρ)))` from hbase should work by defeq (maybe with a `show` or `convert`/`exact`). \n\nAnd mult coercion: zero_sum_inv_sq's family has `(zeroMult ρ : ℝ)` — with ρ : carrier subtype, zeroMult ρ — zeroMult : ℂ → ℕ, coercion ρ → ℂ ✓.\n\nFinite support of D − Dbase: supp ⊆ {ρ | ‖(ρ:ℂ)‖ < 2n} — finite: \n```lean\nhave hfin : {ρ : {ρ // IsNontrivialZero ρ} | ¬ (2 * n ≤ ‖(ρ : ℂ)‖)}.Finite\n```\nThe set maps into closedBall (0:ℂ) (2n) ∩ riemannZetaZeros via the coercion: subtype injective. IsNontrivialZero ρ ⟹ riemannZeta ρ = 0 ⟹ (ρ:ℂ) ∈ riemannZetaZeros. And ‖ρ‖ < 2n ⟹ ρ ∈ closedBall. Mathlib: `IsCompact.inter_riemannZetaZeros_finite (hS : IsCompact S) : (S ∩ riemannZetaZeros).Finite`. closedBall compact ✓ (isCompact_closedBall). Then the subtype set is finite via Set.Finite.preimage on the injective coe function — `Set.Finite.preimage` needs the map injective on... `Set.Finite.preimage (hf : s.Finite) (hinj : Set.InjOn f (f ⁻¹' s))`? There's `Set.Finite.preimage (hs : s.Finite) (hf : InjOn f (f ⁻¹' s)) : (f ⁻¹' s).Finite` — hmm actually the standard: inj + image finite ⟹ preimage finite: `Set.Finite.of_finite_image`? There's `Set.Finite.of_finite_image (hf : (f '' s).Finite) (hinj : InjOn f s) : s.Finite` ✓ use that with f = coe.\n\nThen summable_of_finite_support: `summable_of_finite_support (hf : (Function.support f).Finite) : Summable f`? I believe `summable_of_finite_support` exists ✓. support (D − Dbase) ⊆ {ρ | D ρ ≠ Dbase ρ} ⊆ {ρ | ¬(2n ≤ ‖ρ‖)} ✓.\n\nThen `Summable.of_norm_bounded hD (fun ρ => ...)`: the bound ‖liSummand n ρ‖ ≤ D ρ:\n- if 2n ≤ ‖ρ‖: ‖liSummand n ρ‖ = ‖(zeroMult : ℂ)/2 · (f + f̄)‖ — via liSummand_eq: = ‖(zeroMult : ℂ) · (f.re : ℂ)‖ = (zeroMult ρ : ℝ)·|f.re| ≤ mult·(2n²/‖ρ‖²) ≤ mult·(2n²)·(9/4)/(1+‖γ‖²) = D ✓. Hmm wait: mult/‖ρ‖² ≤ mult·(9/4)/(1+‖γ‖²) ⟺ 1+‖γ‖² ≤ (9/4)‖ρ‖² ✓ step 3. So ‖liSummand‖ ≤ 2n²·mult/‖ρ‖² ≤ (9/2)n²·mult/(1+‖γ‖²) = D ✓.\n- else: D = ‖liSummand‖, le_refl ✓.\n\nNote `Summable.of_norm_bounded` signature check: in current Mathlib: `theorem Summable.of_norm_bounded {f : α → E} {g : α → ℝ} (hg : Summable g) (h : ∀ i, ‖f i‖ ≤ g i) : Summable f` — I'm fairly confident ✓.\n\nzeroMult as a real: need (zeroMult ρ : ℝ) ≥ 0 for the mul_left — `Nat.cast_nonneg`.\n\nAlso `WeilEF.zero_sum_inv_sq` — namespace: Zeta23.WeilEF.zero_sum_inv_sq with `open Zeta23` → WeilEF.zero_sum_inv_sq ✓ (the Scratch axiom check used `WeilEF.zero_sum_inv_sq` after `open Zeta23` ✓ worked).\n\nAlright — also the def replacement in LiSkeleton. The current:\n```lean\ndef liCoeff (n : ℕ) : ℂ :=\n  tsum fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>\n    (zeroMult ρ : ℂ) * (1 - (1 - 1 / (ρ : ℂ)) ^ n)\n```\nbecomes:\n```lean\ndef liCoeff (n : ℕ) : ℂ := tsum (liSummand n)\n```\nplus the liSummand def + liSummable theorem + the honesty-note rewrite.\n\nWhere to put the proof: directly in LiSkeleton.lean §1. But develop in Scratch first. Actually — since Scratch.lean currently has the axiom check (committed), I'll write the development there, iterate with `lake env lean Scratch.lean`, then move the final code into LiSkeleton.lean and rebuild the package.\n\nOne concern: iteration speed — Scratch.lean imports all of Mathlib + Zeta23; each `lake env lean Scratch.lean` run takes ~30–60s? The imports are precompiled so it's just the file elaboration. Fine.\n\nLet me write the initial development. I'll be careful about details:\n\n- `geom_sum_mul : (x - 1) * ∑ i ∈ Finset.range n, x ^ i = x ^ n - 1` — for CommRing. ℂ ✓.\n- w^j − 1 = (w−1)·∑_{i<j} w^i: same lemma at j.\n- S − n = ∑_{j<n} (w^j − 1): S = ∑_{j<n} w^j, n = ∑_{j<n} 1: `Finset.sum_sub_distrib`? (Σ a − Σ b = Σ (a−b)): `Finset.sum_sub_distrib : ∑ (f i - g i) = ∑ f i - ∑ g i` ✓ (recent Mathlib name; older: sum_sub_distrib ✓). And ∑_{j<n} 1 = n: `Finset.sum_const` + `Finset.card_range` ✓ (nsmul).\n- Re((1/z)·S): f = 1 − w^n = (1/z)·S — as complex equality. Then f.re = ((1/z)·S).re.\n  ((1/z)·S) = (1/z)·n + (1/z)·(S−n). ((1/z)·n).re = n·(1/z).re (n real, nat cast: Complex.re_ofNat? (n : ℂ) has re = n: `Complex.natCast_re`? simp handles).\n  (1/z).re = z.re/‖z‖²: `Complex.inv_re`? Let me think — in Mathlib: `Complex.inv_re : (z⁻¹).re = z.re / (Complex.abs z)^2`? or normSq form. There's `Complex.div_re` for division. For 1/z: simp [Complex.div_re, Complex.normSq_apply, Complex.norm_eq_abs] should reduce (1/z).re to z.re/(z.re²+z.im²). I'll compute inside the proof with simp + field_simp.\n  \n  Actually simpler: write the bound via |Re(w)| ≤ ‖w‖ directly where possible:\n  |f.re| ≤ |n·(1/z).re| + |((1/z)·(S−n)).re| ≤ n·|(1/z).re| + ‖(1/z)·(S−n)‖ (|re| ≤ norm: `Complex.abs_re_le_norm`).\n  ‖(1/z)(S−n)‖ = ‖S−n‖/‖z‖ ≤ n²/‖z‖/‖z‖ = n²/‖z‖².\n  |(1/z).re| = |z.re|/‖z‖² ≤ 1/‖z‖² (|z.re| ≤ 1 — from IsNontrivialZero: 0 < re < 1 ✓).\n  So |f.re| ≤ n/‖z‖² + n²/‖z‖² = (n+n²)/‖z‖² ≤ 2n²/‖z‖² ✓ (n ≤ n² for n ≥ 1: `Nat.le_self_pow`? n ≤ n*n for n ≥ 1 ✓ nlinarith).\n\n- |(1/z).re| = |z.re|/‖z‖²: (1/z).re = z.re/‖z‖² — the identity 1/z = conj(z)/‖z‖²: re(1/z) = re(conj z)/‖z‖² = z.re/‖z‖². In Lean: `Complex.inv_re` — I need to check the exact form; there's `Complex.inv_re (z : ℂ) : (z⁻¹).re = z.re / (z.re^2 + z.im^2)`? or via normSq. I'll just prove inline: (1/z) = star z / normSq z: `Complex.inv_def : z⁻¹ = star z / ‖z‖²`? There is `Complex.inv_def : z⁻¹ = (star z) / (normSq z)` — yes I believe `Complex.inv_def` exists (z⁻¹ = star z / normSq z, as complex division by real). Then (z⁻¹).re = (star z).re / normSq z = z.re / normSq z ✓ simp [Complex.inv_def, Complex.div_re? ...]. And normSq z = ‖z‖² for the final form.\n\nOK. Enough planning — write it. First version in Scratch.lean. I'll write the whole thing and iterate on errors. Given its size, let me write carefully.\n\nAlso — where does `liSummand`/`liCoeff`/`liSummable` live: in LiSkeleton.lean §1 replacing the current liCoeff. The namespace is NguyenRH1 with `open Zeta23 Complex Filter Topology` — note: open Complex brings `Complex.re` as `re`? Careful with name clashes — current file already uses Complex open. I'll qualify Complex.re explicitly.\n\nOne more check — current liCoeff's users: `Sf` (line 2122): `Sf (n : ℕ) : ℝ := SInfty n + 1 - (liCoeff n).re`. And LiBasePoints + LiSkeleton theorems. Since I keep the name/type, fine.\n\nLet me write the Scratch development now.","signature":""},{"type":"text","text":"`zetaZeroConfig_carrier` is `rfl` — the subtypes are definitionally equal, so `zero_sum_inv_sq zetaSeam` applies directly. Also noted: `riemannZeta_conj` exists in ZetaReflect. Now developing the proof in Scratch."},{"type":"tool_use","id":"Write_83","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 * ((1 - (1 - 1 / (ρ : ℂ)) ^ n) + (1 - (1 - 1 / (star (ρ : ℂ))) ^ n))\n\nlemma summand_star (n : ℕ) (z : ℂ) :\n    (1 : ℂ) - (1 - 1 / (star z)) ^ n = star ((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_star, Complex.add_conj]\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 h1 : ((1 : ℝ) + 1 / (2 * n)) ^ n ≤ Real.exp (n * (1 / (2 * n))) := by\n    have h := Real.add_one_le_exp (1 / (2 * (n : ℝ)))\n    calc ((1 : ℝ) + 1 / (2 * n)) ^ n\n        ≤ (Real.exp (1 / (2 * n))) ^ n := by\n          gcongr\n          · linarith\n          · exact h\n      _ = Real.exp (n * (1 / (2 * n))) := by\n          rw [← Real.exp_nat_mul]\n  have h2 : (n : ℝ) * (1 / (2 * n)) = 1 / 2 := by field_simp\n  rw [h2] at h1\n  have h3 : Real.exp (1 / 2 : ℝ) ≤ 2 := by\n    have hsq : (Real.exp (1 / 2 : ℝ)) ^ 2 ≤ (2 : ℝ) ^ 2 := by\n      rw [← Real.exp_nat_mul]\n      have : Real.exp (2 * (1 / 2 : ℝ)) = Real.exp 1 := by ring_nf\n      rw [this]\n      have h := Real.exp_one_lt_d9\n      norm_num at h ⊢; linarith\n    nlinarith [Real.exp_pos (1 / 2 : ℝ)]\n  exact h1.trans h3\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  set w : ℂ := 1 - 1 / z with hw\n  -- kernel identity: 1 − wⁿ = (1/z)·S, S = Σ_{j<n} w^j\n  have hgeom : w ^ n - 1 = (w - 1) * ∑ j ∈ Finset.range n, w ^ j := geom_sum_mul 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 : (1 : ℂ) - w ^ n = -(w - 1) * ∑ j ∈ Finset.range n, w ^ j := by\n      rw [← hgeom]; ring\n    rw [this, hw1]; ring\n  set S : ℂ := ∑ j ∈ Finset.range n, w ^ j\n  -- S = n + (S − n); Re(f) = n·Re(1/z) + Re((S−n)/z)\n  have hS : S = (n : ℂ) + (S - n) := by ring\n  -- |S − n| ≤ n²/‖z‖\n  have hwnorm : ‖w‖ ≤ 1 + 1 / ‖z‖ := by\n    have : w = 1 - z⁻¹ := by rw [hw, div_eq_mul_inv, one_mul]\n    rw [this]\n    calc ‖(1 : ℂ) - z⁻¹‖ ≤ ‖(1 : ℂ)‖ + ‖z⁻¹‖ := norm_sub_le _ _\n      _ = 1 + 1 / ‖z‖ := by rw [norm_one, norm_inv]\n  have hwmax : max 1 ‖w‖ ≤ 1 + 1 / (2 * n) := by\n    have h1 : 1 / ‖z‖ ≤ 1 / (2 * n) := by\n      apply one_div_le_one_div_of_le (by positivity : (0:ℝ) < 2 * n)\n      exact_mod_cast hz\n    have h2 : ‖w‖ ≤ 1 + 1 / (2 * n) := hwnorm.trans (by linarith)\n    apply max_le\n    · linarith\n    · exact h2\n  have hSn : ‖S - n‖ ≤ n ^ 2 / ‖z‖ := by\n    have hSn1 : S - n = ∑ j ∈ Finset.range n, (w ^ j - 1) := by\n      rw [Finset.sum_sub_distrib]\n      simp [Finset.sum_const, Finset.card_range]\n    rw [hSn1]\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 ^ j - 1 = (w - 1) * ∑ i ∈ Finset.range j, w ^ i := geom_sum_mul w j\n      rw [hgeomj, norm_mul, hw1, 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 hjn : i ≤ n - 1 := by\n                have hij : i < j := Finset.mem_range.mp hi\n                have hjn' : j ≤ n := le_of_lt (Finset.mem_range.mp hj)\n                omega\n              exact pow_le_pow_left₀ (by positivity)\n                (le_trans (le_max_right 1 ‖w‖) hwmax) i (by omega)\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          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]; congr 1; rw [Finset.mul_sum]\n          apply Finset.sum_congr rfl; 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 := by\n            have h := pow_one_add_inv_two_mul_le n hn\n            calc (1 + 1 / (2 * n : ℝ)) ^ (n - 1)\n                ≤ (1 + 1 / (2 * n : ℝ)) ^ n := by\n                  apply pow_le_pow_right₀ (by positivity)\n                  · have : 1 ≤ (1 : ℝ) + 1 / (2 * n) := by positivity\n                    exact this\n                  · omega\n              _ ≤ 2 := h\n          have h3 : (1 / ‖z‖) * (1 + 1 / (2 * n : ℝ)) ^ (n - 1) * (n * (n - 1) / 2)\n              ≤ (1 / ‖z‖) * 2 * (n ^ 2 / 2) := by\n            apply mul_le_mul_of_nonneg_left _ (by positivity)\n            apply mul_le_mul_of_nonneg_left hpow (by positivity)\n            · have : (n : ℝ) * (n - 1) / 2 ≤ n ^ 2 / 2 := by\n                have hn1 : (1 : ℝ) ≤ n := by exact_mod_cast hn\n                nlinarith\n              linarith\n          calc (1 / ‖z‖) * (1 + 1 / (2 * n : ℝ)) ^ (n - 1) * (n * (n - 1) / 2)\n              ≤ (1 / ‖z‖) * 2 * (n ^ 2 / 2) := h3\n            _ = n ^ 2 / ‖z‖ := by ring\n  -- assemble\n  have hfre : (1 - w ^ n).re = n * z.re / ‖z‖ ^ 2 + (((S - n) / z).re) := by\n    rw [hf, hS]\n    have h1 : ((1 / z) * ((n : ℂ) + (S - n))) = (n : ℂ) * (1 / z) + (S - n) / z := by\n      field_simp; ring\n    rw [h1]\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_def]\n        simp [Complex.div_re, Complex.normSq_apply, Complex.norm_eq_abs,\n          Complex.sq_abs]\n      rw [Complex.add_re] at *\n      simp [hinv]\n    rw [Complex.add_re, 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, abs_pow]\n    apply div_le_div_of_nonneg_right (by positivity)\n    calc |z.re| ≤ 1 := abs_le.mpr ⟨by linarith, hzre1⟩\n      _ ≤ _ := by linarith\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      apply div_le_div_of_nonneg_right hSn (by positivity)\n    rw [div_pow] at *\n    calc |((S - n) / z).re| ≤ ‖(S - n) / z‖ := h1\n      _ ≤ (n ^ 2 / ‖z‖) / ‖z‖ := h2\n      _ = n ^ 2 / ‖z‖ ^ 2 := by ring\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    _ ≤ 2 * n ^ 2 / ‖z‖ ^ 2 := by\n        have hn1 : (n : ℝ) ≤ n ^ 2 := by\n          have : (1 : ℝ) ≤ n := by exact_mod_cast hn\n          nlinarith\n        field_simp at *\n        nlinarith\n\nend NguyenRH1\n"},"extra_content":null}]