[{"type":"thinking","thinking":"Now I have the Lean definitions:\n- `kFun n s = (s / (s - 1)) ^ n - 1` — this is the kernel. Note: s/(s−1) = 1 + 1/(s−1)... and D-036's |1+1/s|² with σ ≤ −1/2 gives |k_n| ≤ 2 — wait, the contour variable in D-036 is shifted: the Lagarias contour in w-plane vs s-plane. In LiSides, the kernel is (w/(w−1))ⁿ − 1 with w the integration variable; D-036 writes 1+1/s where s = w−1. So |kFun n w| ≤ (|w/(w−1)|)ⁿ + 1, and |w/(w−1)| = |1 + 1/(w−1)|.\n\nFor the L1 bounds:\n- Left vertical of the w-contour at Re w = σ₀+1 = −3/2? D-036 §3 (III) says left vertical σ₀ = −5/2 in the s-variable... Let me not worry — the L1 Lean statements should be about kFun directly:\n  - If Re(w/(w−1))... hmm. Actually |w/(w−1)| ≤ 1 ⟺ Re(w) ≤ 1/2. Because |w| ≤ |w−1| ⟺ Re w ≤ 1/2. So on Re w ≤ 1/2, |kFun n w| ≤ 1 + 1 = 2? Wait |kFun| = |(w/(w−1))ⁿ − 1| ≤ |w/(w−1)|ⁿ + 1 ≤ 2 when |w/(w−1)| ≤ 1. Clean!\n  - |w/(w−1)| ≤ 1 ⟺ |w|² ≤ |w−1|² ⟺ Re w ≤ 1/2. Yes.\n  - On horizontals (Im w = ±T, Re w ∈ [−3/2, ...]): |w/(w−1)|² = (σ²+T²)/((σ−1)²+T²) = 1 + (2σ−1)/((σ−1)²+T²). For σ ≤ ... the bound e⁴+1 comes from |1+1/s| ≤ 1+4/(16+n) with s = w−1, σ_s ∈ [−3,3]: |1+1/s|² = 1 + (2σ_s+1)/|s|². For the e⁴ bound: n·log(1+4/(16+n)) ≤ 4·n/(16+n) ≤ 4. So |kFun| ≤ e⁴+1.\n  - Right vertical σ₁ = 2√n (s-variable, so w-variable Re w = 2√n+1?): |kFun| ≤ e^{√n/2}+1.\n\nHmm — but what precisely should the Lean statements be? The D-064 graph says \"kernel bounds |k_n| ≤ 2, e⁴+1, e^{√n/2}+1\". These are real-analysis estimates on kFun. In Lean:\n\n1. `kFun_norm_le_two_of_re_le_half`: Re w ≤ 1/2 → ‖kFun n w‖ ≤ 2. (Elementary: ‖w/(w−1)‖ ≤ 1.)\n   Wait — need w ≠ 1 for kFun to be well-defined... it's a function ℂ → ℂ with division; at w = 1 junk. Re w ≤ 1/2 ⟹ w ≠ 1. Fine.\n   Hmm, actually ‖w/(w−1)‖ ≤ 1 ⟺ ‖w‖ ≤ ‖w−1‖ ⟺ re w ≤ 1/2 (via normSq). Then ‖(w/(w−1))ⁿ − 1‖ ≤ ‖w/(w−1)‖ⁿ + 1 ≤ 1 + 1 = 2. But wait: if ‖w/(w−1)‖ ≤ 1 then ‖·‖ⁿ ≤ 1 (pow_le_one). Yes.\n\n2. The e⁴+1 bound: on the horizontal segments, σ ∈ [−3/2?, 2], |Im w| = T ≥ ... In s = w−1 variable, D-036 has −3 ≤ Re s ≤ 3 i.e. −2 ≤ Re w ≤ 4, and |1+1/s|² = 1 + (2σ_s+1)/|s|² with |s|² ≥ 16+n... The exact Lean statement should mirror what ii′-6 assembly needs. Hmm. What's the cleanest usable form?\n\nSomething like: for w with |Im w| ≥ some bound and Re w in a range, ‖w/(w−1)‖ ≤ 1 + 4/(16+n)?? Hmm — D-036: |1+1/s| ≤ 1 + (σ+1)/(σ²+T²). With s = σ + iT, |s|² = σ²+T² ≥ T² ≥ n (T ≥ √n). Then |1+1/s| ≤ 1 + 4/n... wait D-036 says (1+4/(16+n))ⁿ ≤ e⁴ — because T² ≥ n gives |s|² ≥ n+... hmm hmm. Actually: |1+1/s| ≤ 1 + (σ+1)/|s|² (since |1+1/s|² = 1 + (2σ+1)/|s|² ≤ (1 + (σ+1)/|s|²... no: (1+x)² = 1+2x+x² ≥ 1+2x ⟹ 1+x ≥ √(1+2x). So |1+1/s| = √(1+(2σ+1)/|s|²) ≤ 1 + (σ+1/2)/|s|²? Since √(1+u) ≤ 1+u/2: √(1+(2σ+1)/|s|²) ≤ 1 + (2σ+1)/(2|s|²) = 1 + (σ+1/2)/|s|². For σ ≤ 3: ≤ 1 + 3.5/|s|². |s|² ≥ T² ≥ n when on the horizontal |Im s| = T ≥ √n. So |1+1/s| ≤ 1 + 4/n for n large (3.5/n ≤ 4/n). Then (1+4/n)ⁿ ≤ e⁴. So |kFun| ≤ e⁴ + 1. The \"16+n\" in D-036 is a slightly different bookkeeping (|s|² ≥ 16+n perhaps from σ²+T² with T² ≥ n and σ² ≥ ... no — T ≥ √n+... whatever). The Lean statement should pick a clean form.\n\n3. Right vertical: σ₁ = 2√n (s-var): |1+1/s| ≤ 1 + (σ₁+1/2)/|s|²... for σ large: |1+1/s| ≤ 1 + 1/(|s|)... |s| ≥ σ₁ = 2√n ⟹ |1+1/s| ≤ 1 + 1/(2√n) (since |1+1/s| ≤ 1 + 1/|s|). Then (1+1/(2√n))ⁿ ≤ e^{n/(2√n)} = e^{√n/2}. So |kFun| ≤ e^{√n/2}+1. Clean statement: Re s ≥ 2√n ... hmm need to map to w = s+1.\n\nOK. So the L1 Lean content is three norm bounds on kFun (or on w/(w−1)). All elementary real analysis: normSq manipulations, (1+x/n)ⁿ ≤ e^x (Mathlib: `Real.add_one_le_exp`? no — need (1+x)ⁿ ≤ exp(nx) for x ≥ 0 or x > −1: one_add_le_exp? The standard: 1+x ≤ e^x ⟹ (1+x)ⁿ ≤ e^{nx} for 1+x ≥ 0. Mathlib has Real.add_one_le_exp : x + 1 ≤ exp x. Then pow_le_pow_left for ≤ and exp.)\n\nAnd zeroMult(−2) = 1: `zeroMult ρ = analyticOrderNatAt riemannZeta ρ` (from Rfun_residue_at's proof: `(zeroMult ρ : ℂ) = (analyticOrderNatAt riemannZeta ρ : ℂ) := rfl` — so zeroMult is analyticOrderNatAt riemannZeta). To prove analyticOrderNatAt riemannZeta (−2) = 1:\n\nRoute (D-066): FE + Gammaℝ_eq_zero_iff + ζ(3) ≠ 0.\n- Λ(s) := completedRiemannZeta s = ΓR(s)·ζ(s) (Mathlib: completedRiemannZeta = Gammaℝ s * riemannZeta s? Actually `completedRiemannZeta s = Gammaℝ (s/2)... hmm. Mathlib: `Complex.completedRiemannZeta s = Gammaℝ (s/2) * ...`? Let me recall: Mathlib defines `completedRiemannZeta s = riemannZeta s * Gammaℝ (s/2)`? Actually I think `completedRiemannZeta s = Gammaℝ (s/2) * riemannZeta s`? Hmm, Mathlib's `Complex.completedRiemannZeta` is defined as `s ↦ Gammaℝ (s/2) * riemannZeta s`? Not sure of exact form; there might be a completedRiemannZeta₀ (the \"wrong ξ\" noted in D-066: \"completedRiemannZeta₀ noted as the wrong ξ\").\n- ζ(−2) = 0 trivially (riemannZeta_neg_two_mul_nat? Mathlib: `riemannZeta_neg_nat`? There's `riemannZeta_neg_two_mul_nat : riemannZeta (-2 * n) = 0`? Hmm — Mathlib has `riemannZeta_neg_two_mul_nat` I believe: riemannZeta (-2 * k) = 0 for k ≥ 1 via Bernoulli values. Actually `riemannZeta_neg_nat` — zeta at negative integers = −B_{k+1}/(k+1), and B_{odd ≥ 3} = 0. So ζ(−2) = −B₃/3 = 0. But the ORDER: analyticOrderNatAt ζ (−2) = 1 needs deriv ζ (−2) ≠ 0 or the FE argument.\n- FE argument: Λ(s) = ΓR(s)ζ(s) entire, Λ(s) = Λ(1−s) (completedRiemannZeta_one_sub). At s = −2: ΓR has a simple pole at −2 (ΓR(s) = π^{−s/2}Γ(s/2); Γ(s/2) pole at s = −2 is simple with residue 2·(−1)¹/1!·π^{...}). Mathlib: does it have pole order of Gammaℝ at −2? There's `Complex.Gammaℝ_eq_zero_iff`?? Wait D-066 says \"Gammaℝ_eq_zero_iff (zeros of ΓR = {−2n})\" — hmm, that must be about 1/Gammaℝ or... Actually maybe Mathlib's Gammaℝ is defined such that... no, Γ(s/2)π^{−s/2} has no zeros. Let me check Mathlib for the actual lemma name. Hmm, \"Gammaℝ_eq_zero_iff\" — maybe it states Gammaℝ s = 0 ↔ False? That'd be trivially named weirdly. OR maybe it's `Complex.Gamma_eq_zero_iff`? Hmm, Gamma has no zeros: `Gamma_ne_zero`... Actually I'm not sure these exist with those exact names; D-066 says verified to exist in session 019. Let me grep the Mathlib source in the .lake packages to confirm exact names.\n\nFor analyticOrderNatAt: the route via meromorphic order: order of ζ at −2 = order of Λ at −2 − order of ΓR at −2 = 0 − (−1) = 1. In Lean, working with analyticOrderNatAt riemannZeta (−2) = 1: need (i) ζ(−2) = 0 (so order ≥ 1, given order ≠ ⊤ i.e. ζ not locally zero), (ii) deriv ζ (−2) ≠ 0 (so order ≤ 1)? analyticOrderNatAt characterization: for f analytic at z₀ with f z₀ = 0, analyticOrderNatAt f z₀ = the unique n with f = (z−z₀)ⁿ·g, g(z₀) ≠ 0. order = 1 ⟺ f(z₀) = 0 ∧ deriv f z₀ ≠ 0 (for analytic f). Mathlib might have `analyticOrderNatAt_eq_one`? Probably not directly. There are lemmas like analyticOrderNatAt_eq_of... Hmm.\n\nAlternative via FE directly computing deriv: deriv ζ (−2) = ... messy.\n\nCleaner: use Λ = ΓR·ζ. At −2, ΓR has a simple pole: (s+2)·ΓR(s) analytic at −2 with value ≠ 0 (residue). Λ analytic everywhere, Λ(−2) = Λ(3) = ΓR(3)ζ(3) ≠ 0 (ΓR(3) = π^{−3/2}Γ(3/2) ≠ 0 — Mathlib Gammaℝ_ne_zero_of_re_pos? re 3 > 0 ✓; ζ(3) ≠ 0 — is that in Mathlib? ζ(3) > 1 via the LSeries... `riemannZeta_ne_zero_of_one_lt_re`? For re s > 1, ζ(s) ≠ 0 via Euler product — Mathlib HAS `riemannZeta_ne_zero_of_one_lt_re` I believe (Euler product nonvanishing). Yes, Mathlib has that.)\n\nSo: define via orders of meromorphic functions... Does Mathlib have meromorphic order machinery connecting to analyticOrderNatAt? Zeta23's zeroMult uses analyticOrderNatAt. There's `MeromorphicAt.order` in Mathlib (newer versions). With MeromorphicNFAt etc. The product rule for analyticOrderNatAt: analyticOrderNatAt (f*g) z = analyticOrderNatAt f z + analyticOrderNatAt g z when both analytic and nonzero-germs. But ΓR is NOT analytic at −2 (pole). So ζ = Λ · (1/ΓR) where 1/ΓR IS analytic at −2 with a simple zero (pole of ΓR = zero of 1/ΓR). Hmm — is 1/Gammaℝ analytic everywhere? 1/Γ is entire (Weierstrass) — Mathlib: does it have differentiability of Inv ∘ Gamma? There might be `differentiable_one_div_Gamma`? Hmm. For Gammaℝ... not sure.\n\nThis could be a rabbit hole. Let me scope what ii′-4 NEEDS zeroMult(−2) = 1 for: the ii′-6 assembly split Sz = {nontrivial} ∪ {−2}: the trivial-zero contribution to the sum is zeroMult(−2)·(1−(−2/(−2−1))ⁿ) = zeroMult(−2)·(1−(2/3)ⁿ), and |1−(2/3)ⁿ| ≤ 1 (since (2/3)ⁿ ∈ (0,1)). With zeroMult(−2) = 1 the contribution is ≤ 1. If zeroMult(−2) stays symbolic, the bound would need zeroMult(−2) ≤ something — so the assembly needs the value.\n\nSTATE.md says: \"the trivial-zero residue value 1−(2/3)ⁿ at −2 — needs zeroMult(−2) = 1 (trivial-zero simplicity, deferred from ii′-1b(iii): route via the FE + Gammaℝ_eq_zero_iff + ζ(3) ≠ 0, D-066 §6 note)\".\n\nSo the deliverables for ii′-4:\n\n**L3** (`exists_zero_avoiding_T`): \nStatement (Lean): given the unit-window zero-count hypothesis (perimeter, Trudgian) — e.g. `ZeroCountProp`: for all t ≥ some bound, the number of nontrivial zeros ρ with Im ρ ∈ [t, t+1] is ≤ C0hat-equivalent... Hmm. What exact form? The pigeonhole in D-036 §2: \"Zeros in [√n, √n+1]: ≤ C₀(√n+1)\". C₀(t) bounds zeros in [t−1, t+1] (unit window around t)? D-036 §2 says \"Zeros in [√n, √n+1]: ≤ C₀(√n+1)\" — so C₀(u) bounds the count in ANY unit interval ending near u... In D-056 §2, Ĉ₀(t) = 0.433 log(t+2) + 0.886 log log(t+2) + 2.9 is the \"unit-interval zero-count majorant\". Let me read D-056 §2 for its precise statement.\n\nThen pigeonhole: given ≤ M zeros with ordinates in [a, a+1], there exists T ∈ [a, a+1] with distance ≥ 1/(3M)... wait D-036: gap ≥ 1/(C₀+1) among C₀+2 points (endpoints + zeros); T at gap center ⟹ clearance ≥ 1/(2(C₀+1)); D-036 uses d_min ≥ 1/(3C₀(√n+1)) (safer). The Lean statement: \n\n```\ntheorem exists_zero_avoiding_T {n : ℕ} (hn : ...) :\n  ∃ T : ℝ, Real.sqrt n ≤ T ∧ T ≤ Real.sqrt n + 1 ∧\n    ∀ ρ : ℂ, IsNontrivialZero ρ → ρ.im ∈ ... → |ρ.im - T| ≥ 1 / (3 * C0hat (Real.sqrt n + 1))\n```\n\nBut this needs the zero count as a hypothesis. Perimeter: \"TrudgianN (FAlt form, named hyp)\". So L3 takes a hypothesis like:\n\n```\ndef ZeroCountBound : Prop := ∀ t : ℝ, 2 ≤ t →\n  (Nat.card {ρ : ℂ // IsNontrivialZero ρ ∧ t ≤ ρ.im ∧ ρ.im ≤ t + 1}) ≤ C0hat (t + 1)  -- or similar\n```\n\nHmm, Nat.card of a subtype — needs Fintype. Might be cleaner: for any finite... Actually the pigeonhole proof: suppose the finite set of zeros in window has cardinal ≤ M. Lean: the set of zeros with im in [t,t+1] is finite (from IsCompact.inter_riemannZetaZeros_finite? ii′-1a used `IsCompact.inter_riemannZetaZeros_finite` — Zeta23 has finiteness of zeros in compact sets!). So the Finset exists; the count bound is the perimeter hypothesis.\n\nThe pigeonhole lemma itself: given a Finset of reals S ⊆ [a, a+1] with S.card ≤ M (real M, via Nat.card ≤ ⌊M⌋ or card ≤ M as reals), there exists T ∈ [a, a+1] such that ∀ x ∈ S, |x − T| ≥ 1/(3·max M 1)... Let me think about the cleanest pigeonhole.\n\nStandard: sort the points x₁ ≤ ... ≤ x_k in [a,b]. Consider the k+1 gaps: a→x₁, x₁→x₂, ..., x_k→b (gaps between consecutive including endpoints). Sum of gaps = b−a = 1. So some gap ≥ 1/(k+1). Take T = midpoint of that gap: distance to all points ≥ 1/(2(k+1)). With k ≤ M: 1/(2(k+1)) ≥ 1/(2(M+1)) ≥ 1/(3M) when M ≥ 2 (since 2(M+1) ≤ 3M ⟺ M ≥ 2). C0hat(t) ≥ 2.9 > 2. ✓.\n\nIn Lean, pigeonhole over sorted finset: there might be an existing pigeonhole (Finset.exists_... pigeonhole principles exist for card > card * ...). The gap argument: consider the sorted list; gaps... This is some honest real-analysis grunt work but elementary. Approach: let the sorted elements be x₀ ≤ x₁ ≤ ... ≤ x_{k−1}. Define gap candidates: x₀ − a, x_i+1 − x_i, b − x_{k−1}. Sum telescopes: (x₀ − a) + Σ(x_{i+1} − x_i) + (b − x_{k−1}) = b − a = 1. If all gaps < 1/(k+1), sum < (k+1)/(k+1) = 1 — contradiction. So some gap ≥ 1/(k+1); its midpoint T works: points before the gap are ≤ left end, points after ≥ right end.\n\nLean formalization of this: use Finset.sort to get a sorted list, or work with Finset.orderIsoOfFin... There's `Finset.exists_between`? Hmm. Alternative approach avoiding sorting: consider the k+1 intervals formed... Actually simplest Lean route: \n\nLet S = sorted list of the k ordinates (with multiplicities? zeros distinct as points; ordinates could coincide — use list with possible duplicates; distance argument still works with multiset/sorted list).\n\nAlternative cleaner formulation: define f : Fin (k+1) → ℝ of \"gap midpoints\"? Hmm.\n\nActually, maybe cleaner: use the interval-halving... no. Let me think of the Lean-est route:\n\nTake the k+1 closed intervals... Actually here's a slicker pigeonhole avoiding sort: For j = 0..k, consider candidate points T_j = a + (2j+1)/(2(k+1)) — the k+1 midpoints of the k+1 equal sub-intervals of [a, a+1] of width 1/(k+1). Each zero ordinate x ∈ [a, a+1] can be \"close\" (|x − T_j| < 1/(2(k+1))) to at most one T_j. With k zeros and k+1 candidates, one candidate T_j has NO zero within 1/(2(k+1)). This is a strict pigeonhole: map each zero to the (unique if exists) j with x in the open ball... uniqueness: |x − T_j| < 1/(2(k+1)) and |x − T_l| < 1/(2(k+1)) ⟹ |T_j − T_l| < 1/(k+1) ⟹ j = l. So define a partial map from zeros to candidates; injective; k ≤ k+1... wait need k zeros ≤ k+1 candidates minus... an injection from a k-element set to a (k+1)-element set isn't a contradiction. Need: each zero kills AT MOST one candidate ⟹ zeros kill ≤ k candidates ⟹ ≥ 1 of the k+1 candidates survives. Yes! That works — it's not a contradiction argument, it's a counting argument: the set of \"bad\" candidates has card ≤ k < k+1.\n\nLean: Bad = {j : Fin (k+1) // ∃ x ∈ S, |x − T_j| < 1/(2(k+1))}. Map Bad → S choosing a witness: injective? If j₁, j₂ both map to same x: |T_{j₁} − T_{j₂}| ≤ |T_{j₁} − x| + |x − T_{j₂}| < 1/(k+1) ⟹ j₁ = j₂. So the choice map is injective ⟹ card Bad ≤ card S = k < k+1 ⟹ ∃ j ∉ Bad. This is Finset.card_le_card_of_injOn or Fintype card argument. Doable in Lean but fiddly.\n\nvs. the sorted-gap argument: also fiddly. Both are ~100-200 lines of Lean. The candidates approach might be cleaner with Fin (k+1) and explicit T_j.\n\nHmm — wait. Is there an even simpler formulation that suffices for the ASSEMBLY? What does ii′-6 actually need? \"for each n in range, ∃ T ∈ [√n, √n+1], zero-avoiding with clearance δ\" where δ = 1/(3·C0hat(√n+1)) or so. Plus the border-nonvanishing for rectInt'_Jlag (ζ ≠ 0 on border — the clearance gives that: zeros off the horizontal lines ±T and off verticals by strip arguments).\n\nAlso L3 for the MOMENTS (ii′-3b): zero-avoiding T at ARBITRARY height (T → ∞ sequence): \"T-zero-avoiding (perimeter N(T) + pigeonhole — ii′-4's L3)\". So L3 should be general: for any a ≥ some lower bound, ∃ T ∈ [a, a+1] with clearance ≥ 1/(3·C0hat(a+1)) from all zero ordinates in [a, a+1]. General in a. Then ii′-6 instantiates a = √n.\n\nSo the count hypothesis form: `ZeroCountBound : Prop := ∀ t : ℝ, (2 ≤ t) → Nat.card {ρ : ℂ // IsNontrivialZero ρ ∧ ρ.im ∈ Set.Icc t (t+1)} ≤ ⌊C0hat (t+1)⌋₊`? or as a real inequality `(… : ℝ) ≤ C0hat (t+1)`. Nat.card needs Finite instance — from Zeta23's compact-finiteness. There's the question of whether zeros in Icc form a Finite type: Zeta23 ii′-1a used `IsCompact.inter_riemannZetaZeros_finite` — so Zeta23 has `riemannZetaZeros` as a set and compact-intersection finiteness. IsNontrivialZero — how's it defined? Probably re ∈ (0,1) ∧ riemannZeta ρ = 0 or via the RvM set. The set {ρ | IsNontrivialZero ρ ∧ t ≤ im ≤ t+1} is contained in a compact box (re bounded in [0,1], im in [t,t+1]) → finite.\n\nOK. And what about C0hat vs the ACTUAL Trudgian unit-window count? D-056 §2 derived Ĉ₀(t) = 0.433 log(t+2) + 0.886 log log(t+2) + 2.9 as a majorant for zeros in a unit window. The perimeter declaration (Trudgian N(T)/S(T)) would give this via N(t+1)−N(t) ≤ ... Actually the perimeter hypothesis for L3 should be stated cleanly as a named Prop, like:\n\n```\n/-- Unit-window zero count (Trudgian 2014 N(T)/S(T) consequence, D-056 §2). -/\ndef ZeroCountProp : Prop :=\n  ∀ t : ℝ, 2 ≤ t →\n    (Nat.card {ρ : ℂ // IsNontrivialZero ρ ∧ t ≤ ρ.im ∧ ρ.im ≤ t + 1} : ℝ) ≤ C0hat (t + 1)\n```\n\nHmm wait — C0hat at what argument. D-036 §2: \"Zeros in [√n, √n+1]: ≤ C₀(√n+1)\" — so count in [t, t+1] ≤ C₀(t+1). With Ĉ₀ the declared form. Then L3:\n\n```\ntheorem exists_zero_avoiding_T (hZC : ZeroCountProp) {a : ℝ} (ha : 2 ≤ a) :\n    ∃ T : ℝ, a ≤ T ∧ T ≤ a + 1 ∧\n      ∀ ρ : ℂ, IsNontrivialZero ρ → a ≤ ρ.im → ρ.im ≤ a + 1 →\n        |ρ.im - T| ≥ 1 / (3 * C0hat (a + 1))\n```\n\nwith proof by the candidates pigeonhole: M = C0hat(a+1), k = Nat.card ≤ M, k+1 candidates T_j = a + (2j+1)/(2(k+1))... wait but the clearance from the candidates argument is 1/(2(k+1)) ≥ 1/(2(M+1)) ≥ 1/(3M) iff 2(M+1) ≤ 3M iff M ≥ 2 ✓ (C0hat ≥ 2.9). But k here is a natural; the candidates count k+1; clearance 1/(2(k+1)) — and we need it ≥ 1/(3M): 1/(2(k+1)) ≥ 1/(2(M+1)) ≥ 1/(3M)... 2(M+1) ≤ 3M ⟺ M ≥ 2 ✓. But also need 1/(2(M+1)) vs target 1/(3M): 3M ≥ 2M+2 ⟺ M ≥ 2 ✓. Good.\n\nAlternatively simplify: clearance target 1/(3*C0hat(a+1)) as stated. The proof: Bad candidates ≤ k < k+1. \n\nHmm, k+1 candidates with k = Nat.card. If the zero set in window is empty (k=0): 1 candidate, trivially fine.\n\nLean mechanics for the candidates argument:\n- Let S : Finset ℂ or work with the subtype. Let k = Nat.card {zeros in window}. Need a Finset enumeration: since the subtype is Finite, get a Finset via Set.toFinset.\n- Bad : Finset (Fin (k+1)) := {j | ∃ x ∈ window-zeros, |x.im − T j| < 1/(2(k+1))} — via Finset.filter (decidable pred — classical).\n- Choose map: Bad → window-zeros... injOn argument then card Bad ≤ k = card of zeros... = Nat.card. Then card (Fin (k+1)) = k+1 > k ≥ card Bad ⟹ ∃ j ∉ Bad (Finset.exists_mem_not_mem_of_card_lt? there's Finset.exists_ne_of_card_lt or similar: if card s < card univ then ∃ x ∉ s — `Finset.exists_not_mem_of_card_lt`? something like that exists).\n- The inequality |T_j − T_l| < 1/(k+1) ⟹ j = l: T_j = a + (2j+1)·w/2 where w = 1/(k+1): |T_j − T_l| = |j − l|·w... for j ≠ l, |T_j − T_l| ≥ w = 1/(k+1). Triangle: |T_j − T_l| ≤ |T_j − x| + |x − T_l| < w/2 + w/2 = w. Contradiction ⟹ j = l.\n\nAll real-arithmetic fiddly but elementary. nlinarith/norm_num friendly.\n\n**L1** (kernel bounds): kFun n s = (s/(s−1))ⁿ − 1. Bounds:\n1. `kFun_norm_le_two`: Re s ≤ 1/2 → ‖kFun n s‖ ≤ 2. Proof: ‖s‖ ≤ ‖s−1‖ (normSq: re²+im² ≤ (re−1)²+im² ⟺ 0 ≤ 1−2re ⟺ re ≤ 1/2). So ‖s/(s−1)‖ ≤ 1 (s ≠ 1 since re ≤ 1/2 < 1). ‖(s/(s−1))ⁿ‖ ≤ 1ⁿ = 1. ‖kFun‖ ≤ 1 + 1 = 2. Note n = 0: kFun 0 s = 1−1 = 0 ≤ 2 ✓.\n2. `kFun_norm_le_exp_add_one` type bounds: for the horizontals: if |Im s| ≥ ... hmm — the D-036 statement is on |1+1/s| in the s-variable (s = w−1 shift). In kFun terms: kFun n w with w/(w−1) = 1 + 1/(w−1). So |1+1/(w−1)| where w−1 =: s. The horizontal bound: |Im(w−1)| = |Im w| = T, Re(w−1) ∈ [−3,3]: |1+1/s|² = 1 + (2σ+1)/|s|² ≤ 1 + (2·3+1)/T² ≤ 1+7/n? Hmm wait — need |1+1/s| ≤ 1 + c/n to get (1+c/n)ⁿ ≤ e^c. √(1+7/n) ≤ 1 + 7/(2n) = 1+3.5/n ⟹ ^n ≤ e^{3.5} ≤ e⁴. So on Re(w−1) ∈ [−3, 3] and |Im w|² ≥ n: ‖kFun n w‖ ≤ e^{3.5}+1 ≤ e⁴+1. D-036's \"e⁴+1\". In Lean state as e.g. `kFun_norm_le_exp4_add_one` with appropriate hypotheses (need n ≥ 1? (1+x/n)ⁿ ≤ e^x needs... 1 + 3.5/n ≤ e^{3.5/n} then ^n ≤ e^{3.5}. For n ≥ 1 fine; n = 0: kFun = 0 ✓).\n   Wait — also need to double check the exact side geometry in ii′-6's assembly (which rectangle). The D-036 rectangle is in the s-plane with left σ₀ = −5/2... the w-plane rectangle (integration variable of Jlag) is shifted by +1: Re w ∈ [−3/2, 2√n+1]?? Hmm — D-036 §3 (I) right vertical σ₁ = 2√n in s-plane ⟹ w-plane right edge Re w = 2√n + 1. The L1 statements should be parameterized to cover the assembly's rectangle. Since ii′-6 isn't built yet, provide the three bounds as standalone lemmas with explicit hypotheses on w:\n   - re w ≤ 1/2 ⟹ ‖kFun n w‖ ≤ 2. [covers left vertical: Re w = −3/2]\n   - |im w| ≥ √n ∧ −2 ≤ re w − ... hmm. Let me state in terms of s = w−1: define nothing new; state: (hre : −3 ≤ w.re − 1 ∧ w.re − 1 ≤ 3) (him : (n:ℝ) ≤ w.im²)?? Let me use: (hn : 1 ≤ n) (hre : |(w−1).re| ≤ 3) (him : n ≤ (w−1).im^2)... hmm (w−1).im = w.im. Cleaner: state about s directly: `lemma kFun_shift_norm_le_exp_add_one {n} {s : ℂ} (hre : |s.re| ≤ 3) (him : (n:ℝ) ≤ s.im^2) : ‖kFun n (s+1)‖ ≤ Real.exp 4 + 1`? Since kFun n (s+1) = ((s+1)/s)ⁿ − 1 = (1 + 1/s)ⁿ − 1 (needs s ≠ 0 — from him and n ≥ 1, s.im² ≥ 1 so s ≠ 0). \n   - Right vertical: (hσ : 2√n ≤ s.re): |1+1/s| ≤ 1 + 1/|s| ≤ 1 + 1/(2√n) ⟹ ^n ≤ e^{√n/2} ⟹ ‖kFun n (s+1)‖ ≤ e^{√n/2}+1.\n\n   Hmm wait — for the horizontal e⁴ bound I should double check against what ii′-6 will need: horizontals at Im w = ±T, Re w from −3/2 to 2√n+1 — i.e. s from −5/2 to 2√n. Re s ∈ [−5/2, 2√n]: |s.re| ≤ 3 doesn't cover re s up to 2√n! For re s > 3, D-036 uses the stepping argument (6.12) — that's a |ζ′/ζ| argument, not a kFun argument. For kFun on re s ∈ [3, 2√n]: |1+1/s| ≤ 1 + 1/|s| ≤ 1 + 1/3 ⟹ |kFun| ≤ (4/3)ⁿ+1 — NOT ≤ e⁴+1! Hmm. But wait — D-036 §3 (II),(IV) horizontals: \"|k_n| ≤ (1+4/(16+n))ⁿ + 1 ≤ e⁴ + 1 (−3 ≤ σ ≤ 3); σ ∈ [3, 2√n]: stepping (6.12): each unit step right gains factor 2 on |ζ′/ζ| while |k_n(s+1)+1|/|k_n(s)+1| ≤ e ⟹ geometric sum...\" — so for σ > 3 they use a different decomposition: k_n(s+1)+1 = (1+1/(s+1))ⁿ... the +1: kFun n (s+1) + 1 = ((s+1)/s)ⁿ. So on the right part, they bound |((s+1)/s)ⁿ| = |1+1/s|ⁿ ≤ (1+1/σ)ⁿ ≤ e^{n/σ} ≤ e^{n/3}?? That's huge... hmm no wait: |k_n(s+1)+1|/|k_n(s)+1| ≤ e — the RATIO is ≤ e per unit step: (1+1/(σ+1))ⁿ/(1+1/σ)ⁿ... that's ≤ 1 actually? No — (1+1/s)ⁿ DECREASES as σ increases. Ratio < 1. Hmm, \"≤ e\" is loose. And |k_n(s)+1| = |1+1/s|ⁿ at σ = 3: ≤ (1+1/3)ⁿ = (4/3)ⁿ. That's not ≤ e⁴ either for large n!\n\n   Hmm wait — I think I'm misreading. Let me re-read D-036 §3 (II),(IV): \"|1+1/s| ≤ 1 + (σ+1)/(σ²+T²) ⟹ |k_n| ≤ (1+4/(16+n))ⁿ + 1 ≤ e⁴ + 1 (−3 ≤ σ ≤ 3)\". The bound 1 + (σ+1)/(σ²+T²): for σ ∈ [−3,3], (σ+1)/(σ²+T²) ≤ 4/T² ≤ 4/n. For σ > 3: (σ+1)/(σ²+T²) ≤ (σ+1)/σ² ≤ 4/9 at σ=3 decreasing — actually (σ+1)/(σ²+T²) ≤ (σ+1)/σ² for σ ≥ 1: ≤ (σ+1)/σ² ≤ 4/3/3 = 4/9? at σ=3: 4/9. So 1+(σ+1)/(σ²+T²) ≤ 1+4/9 — constant! (1+4/9)ⁿ blows up. So the e⁴+1 bound is only valid on σ ∈ [−3,3] where (σ+1)/T² ≤ 4/n... wait for σ ∈ [−3,3]: σ+1 ≤ 4, σ²+T² ≥ T² ≥ n. So |1+1/s| ≤ 1+4/n ⟹ ≤ e⁴. For σ ∈ [3, 2√n]: the stepping argument on the PRODUCT |k_n(s)+1|·|ζ′/ζ| — the kFun piece alone isn't ≤ e⁴+1 there. So in the assembly, the horizontal integral over [3, 2√n] is handled by the stepping argument coupling kFun growth (≤ e per step... but (1+1/σ)ⁿ at σ=3 is (4/3)ⁿ ~ e^{0.29n} — huge!). \n\n   Hmm wait, that can't be right. (1+1/3)ⁿ = (4/3)ⁿ = e^{0.288n} — vs e⁴. That would be catastrophic for the bound. Let me recompute: |1+1/s| for σ = 3, t = T: |1+1/s|² = 1 + (2σ+1)/|s|² = 1 + 7/(9+T²) ≈ 1+7/n. NOT (1+1/3)²! I conflated |1+1/s| with 1+1/|s|: 1+1/|s| is the triangle bound, very loose for large |s|. The tight bound: |1+1/s|² = 1 + (2σ+1)/(σ²+T²). For ANY σ ∈ [−3, 2√n], 2σ+1 ≤ 4√n+1 and σ²+T² ≥ T² ≥ n: |1+1/s|² ≤ 1 + (4√n+1)/n = 1 + 4/√n + 1/n. Hmm — (1 + (4√n+1)/n)^{n/2} = exp((n/2)·log(1+(4√n+1)/n)) ≈ exp((n/2)·(4√n/n)) = exp(2√n). So |kFun| ≤ e^{2√n}+1 on the WHOLE horizontal — that's the e^{√n/2}-style bound, not e⁴. But D-036 says for σ ∈ [−3,3]: (σ+1)/(σ²+T²) — using |1+1/s| ≤ 1+(σ+1)/(σ²+T²) (a different inequality: |1+1/s| ≤ ... hmm 1+(σ+1)/(σ²+T²) with σ ≤ 3 gives ≤ 1+4/n ⟹ e⁴ ✓). For σ ∈ [3, 2√n] they couple with |ζ′/ζ| decay via stepping.\n\n   OK so the precise L1 statements (as in D-036):\n   (a) |k_n| ≤ 2 on Re s ≤ −1/2 (i.e. |1+1/s| ≤ 1). In w-plane: Re w ≤ 1/2.\n   (b) |k_n| ≤ e⁴+1 on horizontals with |Re s| ≤ 3 (well, −3 ≤ σ ≤ 3), |t| ≥ √n. \n   Hmm — but the horizontal in the assembly spans σ from −5/2 to 2√n... the e⁴+1 only covers [−3,3] (which contains [−5/2, 3] fine). For σ ∈ [3, 2√n], what bound on |kFun| does the assembly use? From D-036: the stepping gives |k_n(s+1)+1| ≤ e·|k_n(s)+1| per step — i.e., working with (1+1/s)ⁿ directly = kFun+1. |kFun n (s+1) + 1| = |1+1/s|ⁿ. At σ ≥ 3, t = T ≥ √n: |1+1/s|² = 1 + (2σ+1)/(σ²+T²) ≤ 1 + (2σ+1)/T²... for σ up to 2√n: 2σ+1 ≤ 4√n+1, /T² ≤ (4√n+1)/n ≈ 4/√n. So |1+1/s| ≤ (1+4/√n)^{1/2}·… ≤ e^{2/√n} ⟹ |1+1/s|ⁿ ≤ e^{2√n}. Hmm so |kFun+1| ≤ e^{2√n} on that range. But D-036's stepping: \"each unit step right gains factor 2 on |ζ′/ζ| while |k_n(s+1)+1|/|k_n(s)+1| ≤ e\" — hmm the ratio |1+1/(s+1)|ⁿ/|1+1/s|ⁿ: for σ ≥ 3... |1+1/(s+1)|/|1+1/s|: at large T both ≈ 1 + σ/|s|² vs 1+(σ+1)/|s+1|² — the ratio ≈ 1 + O(1/T²) per step, and there are 2√n steps: total ≈ (1+c/n)^{2√n} ≈ e^{2c/√n} ≈ 1. So the stepping ratio ≤ e is very loose; fine.\n   \n   So for the assembly (ii′-6), the horizontal piece on [3, 2√n] needs: |kFun n (s+1) + 1| = |1+1/s|ⁿ ≤ e^{2√n} — hmm wait but that's what combines with the geometric |ζ′/ζ| decay 2^{−(σ−2)} per step. e^{2√n}·2^{−2√n} → 0 fast. OK.\n\n   The exact forms needed will be finalized in ii′-6; for ii′-4, D-064 says provide: |k_n| ≤ 2, e⁴+1, e^{√n/2}+1. The e^{√n/2}+1 is for the right vertical σ₁ = 2√n: |1+1/s| ≤ 1 + 1/|s| ≤ 1 + 1/(2√n) (triangle, tight enough here since |s| ≥ σ = 2√n and... |1+1/s| ≤ 1+1/|s| ✓) ⟹ ⁿ ≤ e^{n/(2√n)} = e^{√n/2} ⟹ |k_n| ≤ e^{√n/2}+1 ✓.\n\nSo L1 = three lemmas about kFun:\n1. `‖kFun n w‖ ≤ 2` for re w ≤ 1/2. (w ≠ 1 automatic)\n2. `‖kFun n (s+1)‖ ≤ exp 4 + 1` for |s.re| ≤ 3? hmm — D-036: −3 ≤ σ ≤ 3 and |t| ≥ √n... wait need (σ+1) ≤ 4 ⟸ σ ≤ 3 and σ²+T² ≥ n ⟸ T² ≥ n. But also for the LEFT horizontals the assembly starts at σ = −5/2 — covered. Statement: (hn : 1 ≤ n) (hσ : s.re ≤ 3) (hT : (n:ℝ) ≤ s.im^2)?? But σ+1 could be negative (σ < −1) — the inequality |1+1/s| ≤ 1 + (σ+1)/(σ²+T²)... hmm wait: |1+1/s|² = 1 + (2σ+1)/|s|². And (1+(σ+1)/|s|²)² = 1 + 2(σ+1)/|s|² + (σ+1)²/|s|⁴ = 1 + (2σ+2)/|s|² + ... ≥ 1 + (2σ+1)/|s|² ✓ (since (2σ+2) > (2σ+1) and the extra term ≥ 0 — need σ+1 ≥ 0? no: (1+x)² with x = (σ+1)/|s|²: 1+2x+x² ≥ 1+(2σ+1)/|s|² ⟺ 2x+x² ≥ (2σ+1)/|s|² ⟺ (2σ+2)/|s|² + x² ≥ (2σ+1)/|s|² ⟺ 1/|s|² + x² ≥ 0 ✓ always). So |1+1/s| ≤ |1+(σ+1)/|s|²|... need 1+(σ+1)/|s|² ≥ 0 for the sqrt comparison: |1+1/s|² ≤ (1+(σ+1)/|s|²)² and 1+(σ+1)/|s|² ≥ 0 gives |1+1/s| ≤ 1+(σ+1)/|s|² (since |1+1/s| ≥ 0). Is 1+(σ+1)/|s|² ≥ 0? |s|² ≥ n ≥ 1, |σ+1| ≤ 4 → (σ+1)/|s|² ≥ −4 ≥ ... hmm 1 − 4 = −3 < 0 if |s|² = 1. But |s|² = σ²+T² ≥ T² ≥ n ≥ 10⁵ in the assembly... for the lemma state n ≥ 1: |s|² ≥ 1, (σ+1)/|s|² with σ ≥ −3: ≥ −2/1 = −2. 1−2 = −1. Hmm — but if σ = −3 then σ² ≥ 9 so |s|² ≥ 9+n... Let me just require |s.re| ≤ 3 (i.e. −3 ≤ σ ≤ 3) then |s|² ≥ T² ≥ n and (σ+1)/|s|² ≥ −2/n... 1+(σ+1)/|s|² ≥ 1 − 2/n ≥ 0 for n ≥ 2. OK fine — the Lean lemma can assume 2 ≤ n or just prove 0 ≤ 1+(σ+1)/(σ²+T²) from (σ+1) ≥ −(σ²+T²)... (σ+1) ≥ −2 (σ ≥ −3) and σ²+T² ≥ 9... when σ = −3: σ² ≥ 9 so σ²+T² ≥ 9 ≥ 2 ✓. Actually general: σ²+T² + σ + 1 ≥ σ² + σ + 1 = (σ+1/2)²+3/4 > 0 ✓ ALWAYS. So 1+(σ+1)/(σ²+T²) = (σ²+T²+σ+1)/(σ²+T²) > 0 always. \n   Then: |1+1/s| ≤ 1+(σ+1)/(σ²+T²) ≤ 1 + 4/n (for σ ≤ 3, σ²+T² ≥ n) ⟹ (…)^n ≤ (1+4/n)ⁿ ≤ (e^{4/n})ⁿ = e⁴ (needs 1+4/n ≤ e^{4/n}: add_one_le_exp ✓; then pow_le_pow_left 0 ≤ ...). ⟹ ‖kFun‖ ≤ e⁴+1.\n3. `‖kFun n (s+1)‖ ≤ exp(√n/2) + 1` for 2√n ≤ s.re: |1+1/s| ≤ 1+1/|s| ≤ 1+1/(2√n) ⟹ ^n ≤ e^{√n/2}.\n\nAll three are honest real-analysis bounds. Doable: normSq lemmas for ℂ, div norm, pow bounds, exp comparison. Each maybe 40–100 lines.\n\nAlso D-036's \"Trivial zeros: only ρ = −2 inside; |(1+1/(−2))ⁿ − 1| = 1 − 2^{−n} ≤ 1\" — in kFun terms: kFun n (−2+1) = kFun n (−1) = (−1/−2)ⁿ − 1 = (1/2)ⁿ − 1? Wait: kFun n w = (w/(w−1))ⁿ − 1; at w = −1: (−1/−2)ⁿ − 1 = (1/2)ⁿ − 1 — hmm but the zero-sum term is (1−(ρ/(ρ−1))ⁿ) at ρ = −2: 1 − ((−2)/(−3))ⁿ = 1 − (2/3)ⁿ. kFun n (ρ) = (ρ/(ρ−1))ⁿ − 1 = −(1 − (ρ/(ρ−1))ⁿ). At ρ = −2: kFun n (−2) = (2/3)ⁿ − 1, |kFun n (−2)| = 1 − (2/3)ⁿ ≤ 1. So L1 includes `kFun_neg_two`: kFun n (−2) = (2/3)ⁿ − 1 and ‖·‖ ≤ 1. Elementary.\n\nAnd zeroMult(−2) = 1 (the simplicity). This is the one analytically deep piece. Route: FE + ΓR pole simple + Λ(3) ≠ 0.\n\nLet me now check what Zeta23/Mathlib give us:\n- zeroMult = analyticOrderNatAt riemannZeta (from Rfun_residue_at: `(zeroMult ρ : ℂ) = (analyticOrderNatAt riemannZeta ρ : ℂ) := rfl` — so zeroMult is presumably `def zeroMult (ρ : ℂ) : ℕ := analyticOrderNatAt riemannZeta ρ` in LiSides or Zeta23. Grep later.\n- Mathlib: `riemannZeta_neg_two_mul_nat`? or `riemannZeta_neg_nat`? For ζ(−2) = 0. \n- Mathlib `Complex.completedRiemannZeta s = Complex.Gammaℝ (s/2) * riemannZeta s`? I think completedRiemannZeta is defined as `s (s-1) π^(-s/2) Γ(s/2) ζ(s) / ...`? No — that's Λ with the s(s−1) factor: completedRiemannZeta in Mathlib = `Gammaℝ (s/2) * riemannZeta s`? Hmm. Actually Mathlib: `Complex.completedRiemannZeta s = Complex.Gammaℝ (s / 2) * riemannZeta s`? I recall `completedRiemannZeta_residue_one`: the residue at s = 1 is 1? and `completedRiemannZeta_one_sub : completedRiemannZeta (1 − s) = completedRiemannZeta s`. And completedRiemannZeta₀ = `completedRiemannZeta s / (s * (s − 1))`? or minus the pole terms. D-066 noted \"completedRiemannZeta₀ noted as the wrong ξ\".\n\nFor the order argument: analyticOrderNatAt riemannZeta (−2) = 1.\nCharacterization: for f analytic at z₀, analyticOrderNatAt f z₀ = n ⟺ f z₀ = 0 ∧ ... hmm. Mathlib API: `analyticOrderNatAt` — let me check what exists: `analyticOrderNatAt_eq_iff`? `analyticOrderNatAt_nonneg`? There is `analyticOrderNatAt_eq_one_iff`? Unlikely. Probably: `analyticOrderNatAt f z = n ↔ ∃ g, AnalyticAt ℂ g z ∧ g z ≠ 0 ∧ f =ᶠ[𝓝 z] (fun w => (w − z)^n * g w)` or via `analyticOrderNatAt_eq_natCast`... There's also the relation: analyticOrderNatAt f z = 0 ⟺ f z ≠ 0. And if f z = 0 and analytic and not identically zero near z: order = Fintype... The practical route: \n\norder(ζ, −2) = order(Λ/ΓR, −2). Using: (i) ζ(−2) = 0 ⟹ order ≥ 1 (needs order ≠ ⊤: ζ not ≡ 0 near −2 — ζ(3) ≠ 0 and identity... analyticOrderNatAt_ne_top_of_... hmm — ii′-1b has `zeta_order_ne_top_of_ne` (lemma at line 121 in LiSides!): \"zeta_order_ne_top_of_ne {ρ : ℂ} (hρ : ρ ≠ 1) : analyticOrderNatAt riemannZeta ρ ≠ ⊤\" — already proved via zetaA identity principle. So order at −2 is a nat.)\n\n(ii) order ≤ 1: need deriv ζ (−2) ≠ 0? Or show ζ(s)/(s+2) has nonzero limit... The cleanest: use Λ = ΓR·ζ and (s+2)·ΓR(s) analytic at −2 with value = Res(ΓR, −2) ≠ 0. Then ζ(s) = Λ(s)·[(s+2)/((s+2)ΓR(s))]·(1/(s+2))... hmm: ζ(s)·(s+2) = Λ(s)·(s+2)/ΓR(s)·... no: ζ = Λ/ΓR ⟹ (s+2)·ζ(s) = Λ(s) · (s+2)/ΓR(s) = Λ(s) · ((s+2)·ΓR(s))⁻¹·... wait (s+2)/ΓR(s) = (s+2)·(1/ΓR(s)). Since ΓR has a simple pole at −2, 1/ΓR has a simple zero: (s+2)/ΓR(s) → 1/Res. So (s+2)⁻¹·ζ(s)... hmm I want: ζ(s) = (s+2)⁻¹ · [Λ(s) · (s+2)/ΓR(s) ... no. Let me redo: ζ(s) = Λ(s)/ΓR(s). Define H(s) := (s+2)·ΓR(s) (analytic at −2, H(−2) = Res ≠ 0). Then 1/ΓR(s) = (s+2)/H(s). So ζ(s) = Λ(s)·(s+2)/H(s) = (s+2)·[Λ(s)/H(s)]. So ζ(s) = (s+2)·G(s) with G(s) = Λ(s)/H(s) analytic at −2 (H(−2) ≠ 0) and G(−2) = Λ(−2)/H(−2) ≠ 0 since Λ(−2) = Λ(3) ≠ 0. ⟹ analyticOrderNatAt ζ (−2) = 1. \n\nIn Lean: need\n- `AnalyticAt ℂ (fun s => (s + 2) * Gammaℝ (s/2)...` wait — completedRiemannZeta uses Gammaℝ(s/2)?? Let me get Mathlib's actual def: I believe `completedRiemannZeta (s) = Gammaℝ (s/2) * riemannZeta s`? Hmm no. Let me check: Mathlib's `Complex.completedRiemannZeta`: \"completed Riemann zeta function Λ(s) = π^{−s/2} Γ(s/2) ζ(s)\"... and Gammaℝ(s) = π^{−s/2}Γ(s/2). So completedRiemannZeta s = Gammaℝ s * riemannZeta s. YES — Gammaℝ already includes the s/2 inside Gamma. So Λ(s) = Gammaℝ s · ζ(s). Poles of Gammaℝ at s = −2n (Gamma poles at −n). Good: at s = −2, Gammaℝ simple pole.\n\nMathlib API for Gammaℝ pole: is there `Gammaℝ_eq_zero_iff`?? D-066 listed it: \"`Gammaℝ_eq_zero_iff` (zeros of ΓR = {−2n})\" — zeros of Gammaℝ?? ΓR has no zeros... OH WAIT. Maybe it's about `riemannZeta` zeros: `riemannZeta_eq_zero_iff`... Hmm, D-066 wrote \"Gammaℝ_eq_zero_iff (zeros of ΓR = {−2n} — also the future trivial-zero simplicity input)\". Hmm, maybe the lemma is about Gamma: `Complex.Gamma_eq_zero_iff : Gamma s = 0 ↔ False`? and Gammaℝ... I bet D-066 means the lemma characterizing when the COMPLETED zeta vanishes or something. Whatever — I'll check Mathlib directly in the .lake packages when implementing.\n\nFor the pole: need AnalyticAt of (s+2)·Gammaℝ s at −2 and value ≠ 0. Mathlib: `Complex.Gammaℝ` analyticity: `AnalyticAt ℂ Gammaℝ s` for s ∉ {−2n}? There's `differentiable_Gammaℝ`? Hmm. And the residue of Gamma at −n = (−1)ⁿ/n!. Mathlib might not have Gamma residues... This is where it could get heavy. Alternative avoiding Gamma pole machinery: use the FE in asymmetric form? The trivial-zero simplicity might have a slicker route:\n\nζ(1−s) = χ-type... Or use: `riemannZeta_neg_nat` gives VALUES (via Bernoulli) but not the derivative.\n\nAlternative: deriv ζ (−2) ≠ 0 via FE differentiation: Λ(s) = Λ(1−s) doesn't directly give deriv of ζ.\n\nHmm, what about Zeta23? It's a full RH formalization repo — does it have trivial-zero simplicity? D-066 inventory mentions Zeta23: \"completedRiemannZeta s = 0 ↔ IsNontrivialZero s (CountByIntegral.lean), seam mult_reflect, WeilEF.zero_sum_inv_sq\" — no trivial-zero simplicity mentioned. Let me grep Zeta23 for it when implementing.\n\nMathlib DOES have (I believe): `Complex.differentiable_one_div_Gamma`? Hmm. Actually I recall Mathlib has `Complex.Gammaℝ_ne_zero_of_re_pos` (D-066 ✓) and `Complex.differentiableAt_Gammaℝ` (for s not a nonpositive even?). For 1/Gammaℝ analyticity at the pole — probably NOT in Mathlib. \n\nBuilding \"H(s) = (s+2)·Gammaℝ(s) analytic at −2 with H(−2) ≠ 0\" from scratch: Gammaℝ s = π^{−s/2}·Γ(s/2). (s+2)Γ(s/2): Γ(s/2) = Γ(s/2+1)/(s/2) = 2Γ(s/2+1)/s... pole at s = −2 comes from Γ(s/2+1) pole at s/2+1 = 0 i.e. s = −2: Γ(s/2+1) = Γ(s/2+2)/(s/2+1) = 2Γ(s/2+2)/(s+2). So (s+2)Γ(s/2) = (s+2)·Γ(s/2+2)/((s/2)(s/2+1))·... let me use Γ(z) = Γ(z+2)/(z(z+1)): Γ(s/2) = Γ(s/2+2)/((s/2)(s/2+1)) = 4Γ(s/2+2)/(s(s+2)). So (s+2)Γ(s/2) = 4Γ(s/2+2)/s. At s = −2: 4Γ(1)/(−2) = −2 ≠ 0. And analyticity: Γ(s/2+2) analytic near −2 (s/2+2 near 1, Γ analytic at 1 ✓ — Mathlib: differentiableAt_Gamma for nonneg-int-avoiding points), divided by s (analytic, ≠ 0 at −2 ✓). So H(s) = π^{−s/2}·4Γ(s/2+2)/s is analytic at −2 with H(−2) = π¹·4·1/(−2) = −2π ≠ 0. The Γ functional equation Γ(z+2) = (z+1)zΓ(z) — Mathlib has `Complex.Gamma_add_one`. This is all buildable but fiddly (~1-2 sessions of Lean grunt just for this?). Hmm.\n\nWait — maybe Mathlib has more: is there `analyticOrderNatAt` API for products/inverses of meromorphic functions? Mathlib recently (2024-2025) got MeromorphicAt order theory: `MeromorphicAt.order`, `MeromorphicAt.order_mul`, `order_inv`... and relations between analyticOrderNatAt and meromorphic order? If MeromorphicAt.order (ΓR) (−2) = −1 is provable via `MeromorphicAt.order` of Gamma... Mathlib might have the meromorphic order of Gamma at poles? Probably not directly.\n\nGiven the estimate \"ii′-4: 1 session\" in D-064, and zeroMult(−2)=1 potentially being a mini-rabbit-hole, the pragmatic sub-staging (per §8.5 sub-stage rule):\n- ii′-4a: L3 pigeonhole (exists_zero_avoiding_T) — self-contained real analysis + the perimeter Prop declaration.\n- ii′-4b: L1 kernel bounds (three kFun lemmas + trivial residue value).\n- ii′-4c: zeroMult(−2) = 1 (trivial-zero simplicity).\n\nIf 4c turns into a swamp, it can be split further. Let me also check whether Zeta23 already has something about analyticOrderNatAt riemannZeta at trivial zeros or Gamma poles. Quick grep in the zeta-23-lean repo.\n\nAlso — where do the new lemmas live? D-064 §5: \"Module: NguyenRH1/LiContour.lean (+ LiResidue.lean for R1 machinery, LiCrux.lean for R2, LiRBound.lean for R3)\". So create `LiContour.lean` for L3+L1. New file = allowed under freeze protocol (\"only new files + root imports are touched\").\n\nWhere's the perimeter zero-count Prop declared? Options: declare `ZeroCountProp` in LiContour.lean (or LiSkeleton — freeze protocol says no edits to existing proofs; ADDING a def to LiSkeleton might be OK? \"no edits to existing Lean proofs except the liCoeff correctness fix\" — adding new declarations to an existing file changes the file but not existing proofs. Safer to put everything new in LiContour.lean.)\n\nLet me now check: (1) zeroMult definition location; (2) Zeta23 trivial-zero/order lemmas; (3) Mathlib Gammaℝ pole API. Then write the session plan.\n\nLet me grep.","signature":""},{"type":"text","text":"I have the full picture now. Let me check the remaining pieces: where `zeroMult` is defined, and what Zeta23/Mathlib provide for the trivial-zero simplicity route."},{"type":"tool_use","id":"Grep_45","name":"Grep","input":{"-n":true,"output_mode":"content","path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1","pattern":"def zeroMult|zeroMult.*:="},"extra_content":null},{"type":"tool_use","id":"Bash_46","name":"Bash","input":{"command":"cd D:/Python/Quantum/research/lean && ls && ls zeta-23-lean 2>/dev/null | head -20","description":"Locate vendored zeta-23-lean repo"},"extra_content":null}]