[{"type":"thinking","thinking":"The user wants to plan tier ii′: closing the Lean-verified contour bound `SfBoundProp`. This is a significant planning task. Let me think deeply about this.\n\nThe goal: prove in Lean 4 (Mathlib):\n```\nSfBoundProp : ∀ n : ℕ, 100000 ≤ n → (n : ℝ) ≤ (3 * 10^12 - 1 : ℝ)^2 → |Sf n| ≤ Bn FAlt (n : ℝ)\n```\n\nwhere `Sf n := SInfty n + 1 - (liCoeff n).re` and `Bn FAlt n` is the explicit traced bound.\n\nPer D-062 §3 triage, the proof decomposes into layers:\n\n- **L0**: Rectangle contour identity for `k_n(w−1)(−ζ′/ζ)`: residues at zeros give the truncated zero sum; assembling Sf = S_∞ + 1 − λ_n from the contour output. **Mathlib-partial**: meromorphic residue machinery on rectangles is thin in current Mathlib; this is the main formalization lift.\n- **L1**: Kernel bounds: |k_n| ≤ 2, ≤ e⁴+1, ≤ e^{√n/2}+1; stepping (6.12); trivial residue ≤ 1. **Mathlib-tractable**.\n- **L2**: Reference-point R-bound (D-056 Thm R: |R(s)| ≤ 10.5 log(|t|+2) + 48): partial fractions for ζ′/ζ (Hadamard product of ξ), digamma Lemma D, unit-interval grouping. **Mathlib-tractable modulo L4**.\n- **L3**: Zero-avoiding T ∈ [√n, √n+1] (pigeonhole gap center). **Mathlib-tractable modulo L4**.\n- **L4**: Trudgian 2014 explicit N(T), S(T) bounds — decided PERIMETER.\n- **L5**: Bridge: zeros with |γ| ≤ T ≤ T₀ on the line ⟹ each zero term ≤ 2 — uses RHUpTo, already perimeter.\n- **L6**: M₀ ≤ 1.3352 on |t| ≤ 10 — grid-verified E-023; computational perimeter after E-023b.\n- **L7**: liCoeff summability — folds into L0.\n\nThe user asks:\n1. What does it take to accomplish this task?\n2. Break it down into sub-stages to work on one at a time.\n3. What is the possibility this can be done?\n4. Think deep, analyze, find ways to close the Lean-verified contour bound issue.\n\nLet me think deeply about the actual mathematical and formalization content.\n\n### What is the actual mathematics that needs formalizing?\n\nThe contour argument (D-036, D-037 §4, Lagarias Thm 6.1 variant B):\n\n1. **Setup**: For n ≥ 10⁵, consider the rectangle with vertices at σ₀ = −5/2, σ₁ = 2√n, Im = ±T, where T ∈ [√n, √n+1] is chosen zero-avoiding. Integrand: `k_n(w−1)(−ζ′/ζ(w))` where `k_n(s) = (1+1/s)^n − 1`.\n\n2. **Residue theorem**: The integral over the rectangle equals 2πi × sum of residues at poles inside:\n   - At each nontrivial zero ρ with |γ| ≤ T: residue contributes `k_n(ρ−1)` × (order), giving the truncated zero sum `Σ'_{|γ|≤T} [1 − (ρ/(ρ−1))^n]·(−1)` (note `k_n(ρ−1) = (ρ/(ρ−1))^n − 1`).\n   - At s = 0 (pole of ζ′/ζ? No — ζ has no pole at 0... wait, let me think. ζ′/ζ has poles at zeros of ζ and at s = 1 (pole of ζ). Actually also trivial zeros are inside or on boundary... σ₀ = −5/2 so trivial zeros at −2, −4 are inside. Hmm, wait, trivial zeros at −2 and −4 are inside the rectangle (σ from −5/2 to 2√n). So their residues also contribute.\n   - At s = 1: pole of ζ, residue of ζ′/ζ is −1, contributing `k_n(0)·1 = (1+1/0)^n...` wait, `k_n(w−1)` at w = 1 is `k_n(0)` which is singular. Hmm, but k_n(s) = (1+1/s)^n − 1 has a pole at s = 0 of order n. And ζ′/ζ at s = 1 has residue −1 (since ζ has a pole, ζ′/ζ ~ −1/(s−1)). The product k_n(w−1)(−ζ′/ζ(w)) at w=1: k_n(w−1) ~ (w−1)^{−n}, −ζ′/ζ ~ 1/(w−1). So the product has a pole of order n+1 at w = 1. The residue there is a complicated expression — but this is exactly what produces the S_∞ archimedean terms... \n\n   Actually wait. In Lagarias's setup (BL Thm 2): λ_n = S_∞ − S_f + 1 where the contour integral identity directly gives S_f = S_∞ + 1 − λ_n. The way D-062 phrased it: \"the D-036 contour computation (Lagarias Thm 6.1 variant B) produces the identity AND the bound in one stroke, so SfBoundProp as stated is exactly what the contour argument proves directly.\"\n\n   The identity: S_f(n) = Σ_{|γ|≤T}′ [1 − (ρ/(ρ−1))ⁿ]·(−1) + (1/2πi)(I_I+I_II+I_III+I_IV) + triv(−2) where I_I..I_IV are the four sides, and the residue at w=1 contributes the S_∞-related terms... hmm, actually let me not over-reconstruct; the point is the identity is established in D-036/D-037 and the residues at w=1 (high-order pole) yield polynomial-in-n terms involving log and constants that combine into the S_∞ + 1 − λ_n structure.\n\n   Actually, from D-037: `S_f(n) = Σ_{|γ|≤T}′ [1 − (ρ/(ρ−1))ⁿ]·(−1) + (1/2πi)(I_I+I_II+I_III+I_IV) + triv(−2)`. And `Sf n := SInfty n + 1 − (liCoeff n).re`. And λ_n = Σ′_ρ [1−(1−1/ρ)ⁿ] (full sum over all zeros). So the identity is: SInfty + 1 − λ_n = −Σ_{|γ|≤T}′[1−(ρ/(ρ−1))ⁿ] + contour terms + trivial-zero terms. Hmm, and the full zero sum λ_n = Σ′_ρ[1−(1−1/ρ)ⁿ] — note 1−1/ρ = (ρ−1)/ρ, so (1−1/ρ)ⁿ... and 1−(ρ/(ρ−1))ⁿ is a different expression. The relation: pairing ρ ↔ 1−ρ. This is standard Li-coefficient theory.\n\n   OK, the point for planning: the identity involves:\n   - The full zero sum (liCoeff, defined as a tsum over zeros — summability = L7)\n   - The truncated zero sum (finite, from residues)\n   - The tail of the zero sum beyond T — bounded by 2N(tail)... wait no. Actually the identity as stated in D-037 has the truncated sum on the RHS plus the contour integrals. The full λ_n appears on the LHS. So the identity must account for the tail Σ_{|γ|>T}. Hmm — how does that work?\n\n   Let me think again. In Lagarias Thm 6.1 variant B (D-036): the contour at finite T gives:\n   ∫rectangle k_n(w−1)(−ζ′/ζ) = 2πi [Σ_{|γ|≤T} residues + residue at w=1 + trivial-zero residues]\n   \n   And separately, λ_n is defined by the convergent sum over ALL zeros. The identity S_f = S_∞ + 1 − λ_n is BL Thm 2. Lagarias's variant B computes S_f(n) (which is a sum over zeros, the \"finite part\" of the BL decomposition) by truncating at T: the zero sum Σ_ρ [1−(ρ/(ρ−1))ⁿ]... \n\n   Hmm, actually in BL Thm 2, λ_n = S_∞ − S_f + 1 where S_f is itself a sum over zeros (the finite part). The contour method evaluates this zero sum by truncation + explicit remainder. The tail beyond T for the S_f sum: terms ~ n/|ρ|² (since 1−(ρ/(ρ−1))ⁿ ≈ ... for large ρ, (ρ/(ρ−1))ⁿ = (1+1/(ρ−1))ⁿ ≈ 1 + n/(ρ−1) + O(n²/ρ²), so 1 − that ≈ −n/(ρ−1) + O(n²/ρ²), and Σ_{|γ|>T} n/|ρ|² ~ n log T / T ≤ √n-ish small. Hmm wait, but actually D-037's identity as quoted includes \"Σ_{|γ|≤T}′ [1 − (ρ/(ρ−1))ⁿ]·(−1)\" — so the contour directly produces the truncated version of the S_f zero sum, and the tail of S_f's zero sum must be bounded separately (that's part of the B(n) accounting, presumably in the \"zeros ≤ 2N(T)\" term plus a tail term... actually D-037 says \"|Σ| ≤ 2N(T) ≤ 2F(T) + 2S_bnd(T)\" using RH-to-T₀ — that's the truncated sum bound, each term ≤ 2. The tail of the S_f sum: bounded by Σ_{|γ|>T} |1−(ρ/(ρ−1))ⁿ| ≤ Σ n·|ρ|⁻¹-ish... \n\n   Hmm, I'm not going to fully reconstruct D-036's exact accounting here. For the plan, what matters is the STRUCTURE of what must be formalized, at the level of the D-062 triage. But let me look at what I know:\n\n   From D-037 §4 (what I read):\n   - Rectangle σ₀ = −5/2, σ₁ = 2√n, Im = ±T, T ∈ [√n, √n+1] zero-avoiding\n   - Integrand k_n(w−1)(−ζ′/ζ(w)), k_n(s) = (1+1/s)ⁿ − 1\n   - Identity: S_f(n) = Σ_{|γ|≤T}′ [1 − (ρ/(ρ−1))ⁿ]·(−1) + (1/2πi)(I_I+I_II+I_III+I_IV) + triv(−2)\n   - Trudgian N(T) bounds, C₀ unit-interval counts\n   - R-bound: |ζ′/ζ(w) − Σ_{|γ−t|<1} 1/(w−ρ)| ≤ A log(|t|+2) + B₀\n   - Pieces: zeros ≤ 2N(T); left vertical via |k_n| ≤ 2 and |ζ′/ζ| bound; etc.\n   - B(n) = 2F(T) + 4T[(2/3)Ĉ₀(T) + 10.5 log(T+2) + 48] + 40·1.3352 + 2(e⁴+1)·[7Ĥ(T) + 3.3] + IIMaj(n) + 1\n\n### What's in Mathlib?\n\nThis is the crux of feasibility. What does current Mathlib (v4.33.0-rc2 era, mid-2026... well, the project uses v4.33.0-rc2) have?\n\n1. **riemannZeta**: Mathlib has `riemannZeta` with analytic continuation, functional equation, the pole at 1, trivial zeros. As of recent versions, Mathlib has:\n   - `riemannZeta` defined for all s via Hurwitz zeta\n   - Functional equation (completedRiemannZeta, the ξ function as `completedRiemannZeta`)\n   - `riemannZeta_residue_one` / the simple pole at s=1 with residue 1\n   - Trivial zeros: `riemannZeta_neg_two_mul_nat` (ζ(−2n) = 0)\n   - Log derivative ζ′/ζ: there's `logDeriv`, and for ζ there might be some API. zeta-23-lean repo itself has counting functions vs Mathlib riemannZeta — the R3 resource. The zeta-23-lean project (v1.0) formalized zero-counting functions. That's OUR inherited library — it has N(T)-related machinery? Let me recall: R3 \"zeta-23-lean repo (tag v1.0): Lean 4 formalization, counting functions vs Mathlib riemannZeta\". D-007 audited it. So zeta-23-lean has SOME zero-counting infrastructure on top of Mathlib. That's relevant — L3/L4 might partially exist there. Actually the zeta-23 challenge was about... hmm, \"counting functions vs Mathlib riemannZeta\". I should check what's actually in it during planning execution.\n\n2. **Contour integration / residue theorem**: Mathlib has:\n   - `circleIntegral`, Cauchy integral formula for circles, `Complex.circleIntegral_sub_inv_smul_of_differentiable_on_off_countable`...\n   - Rectangle integrals: Mathlib has `Complex.integral_boundary_rect_of_hasFDerivAt_real_off_countable` (Cauchy's theorem for rectangles), and `Complex.windingNumber`... There's the \"Cauchy integral formula for a rectangle\" — I recall `Complex.integral_boundary_rect_eq_zero_of_differentiable_on_off_countable` and versions with the winding number. For RESIDUES at multiple poles on rectangles: Mathlib has been developing `MellinTransform` and residue machinery for PNT... Actually, the Prime Number Theorem formalization (PNT+ project by Kontorovich et al.) developed exactly this: rectangle contours, ζ′/ζ bounds, residue computations! PNT+ is a separate project, not in Mathlib core, but parts have been upstreamed. By 2026, how much is in Mathlib? Uncertain. The PNT+ project (Kontorovich, Bordg, Do, etc.) formalized PNT with explicit contours around ζ′/ζ. If PNT+ is available as a dependency, L0 gets dramatically easier — they have `RectangleIntegral`, residue computations for ζ′/ζ with poles at zeros and at 1.\n\n   Hmm, but adding PNT+ as a dependency is a big decision (version compatibility with v4.33.0-rc2). Alternatively, port the needed lemmas.\n\n3. **Zeros of ζ**: Mathlib has `riemannZeta` zeros API? There's `Complex.riemannZeta` and... I believe Mathlib has the nontrivial zeros set? Not sure there's much. zeta-23-lean defines its own zero-counting.\n\n4. **Hadamard factorization of ξ**: Does Mathlib have entire-function product theory? There's some: `Complex.Prod`... Mathlib has Weierstrass products? There's `MellinCalculus`... Actually Mathlib does have the Hadamard product for ξ? I recall work on `riemannXi`... not sure. The partial-fraction expansion ζ′/ζ(s) = B + log... − Σ ... (the R-bound reference-point formula) requires:\n   - ζ′/ζ(s) = log Γ(s/2)-related terms + Σ_ρ [1/(s−ρ) + 1/ρ] + const (Hadamard)\n   - The digamma bound (Lemma D in D-056, proved in D-039/D-056 with |r| ≤ 1.2/|w|² remainder)\n   - Reference-point trick (D-056 repair: bound R(s) by comparing at a reference point to avoid the O(|t| log t) hole)\n   \n   Mathlib has `Complex.Gamma` log derivative = digamma? Mathlib has `Complex.digamma`? There's `Real.Gamma`... As of recent Mathlib, there IS `Complex.digamma` I believe (added for Gamma function API). And the product formula... uncertain.\n\n5. **Convexity/margin machinery**: DONE (tier i/ii).\n\n### Feasibility assessment\n\nLet me think about each layer's real difficulty:\n\n**L0 (contour identity)** — The hardest. Needs:\n- Rectangle residue theorem for meromorphic functions with finitely many poles inside (partially in Mathlib; the rectangle version with winding number exists; multiple-pole version needs assembling)\n- Identification of poles of k_n(w−1)(−ζ′/ζ(w)): at zeros ρ (simple, residue −k_n(ρ−1)·ord... for simple zeros), at w = 1 (pole of order n+1 — residue = a specific finite combination, computable via the Taylor expansion of the regular part), at trivial zeros −2, −4 (simple)\n- The residue at w=1 computation: order n+1 pole — in Lean this is `(n)!⁻¹ · lim dⁿ/dwⁿ [(w−1)^{n+1} · integrand]` — messy but doable? Actually there's a trick: Lagarias variant B might handle s=1 differently (the k_n kernel is designed so that... hmm, k_n(w−1) = (1+1/(w−1))ⁿ − 1 = (w/(w−1))ⁿ − 1. At w = 1 this has a pole of order n. And −ζ′/ζ has a simple pole with residue +1 (since ζ has a pole, ζ′/ζ ~ −1/(s−1), so −ζ′/ζ ~ +1/(s−1)). So product pole order n+1. The residue yields the archimedean/S_∞-side terms. In D-037's accounting, the identity is S_f = truncated zero sum + contour sides + triv(−2) — the w=1 residue must equal −(S_∞-side) exactly? No wait — S_f(n) := S_∞(n) + 1 − λ_n. And BL Thm 2 gives λ_n = S_∞ − S_f + 1. The contour identity must reproduce this. The residue at w=1 of order n+1 gives exactly the terms that turn \"Σ over ALL zeros\" into \"S_∞ + 1 − λ_n\"... \n\n  Hmm, actually maybe the cleaner formalization route: prove the identity in the form\n  S_f(n) = Σ_{|γ|≤T} [residue terms] + (1/2πi)∮sides\n  where S_f is DEFINED as SInfty + 1 − liCoeff.re (as in the Lean code). The identity to prove is an equation between a tsum-defined quantity and contour data. The natural proof: (a) λ_n as zero sum (definition of liCoeff in Mathlib? Is there `liCoeff` in Mathlib?? The Lean code references `liCoeff n` — where is that defined? In NguyenRH1! Let me recall — `Sf (n : ℕ) : ℝ := SInfty n + 1 - (liCoeff n).re`. `liCoeff` must be defined somewhere in NguyenRH1 or Mathlib. Probably NguyenRH1 defines `liCoeff n := ∑' ρ, (1 - (1 - 1/ρ)^n)` over the zero set — and L7 (summability) is flagged. So liCoeff is our own definition over the nontrivial zeros (defined via some enumeration or as a tsum over the zero set as a subtype).\n\n  So the contour identity proof needs:\n  (i) The residue computation at each zero inside (simple poles — clean)\n  (ii) The residue at w = 1 (order n+1 pole — the hard residue; but its value is EXACTLY `S_∞(n) + 1 − [tail of zero sum]`... no. Let me think about what the w=1 residue actually equals.\n\n  From Lagarias Thm 6.1: he computes exactly this residue. k_n(w−1) = Σ_{j=1}^n C(n,j) (w−1)^{−j}. So the integrand is Σ_j C(n,j) (w−1)^{−j} · (−ζ′/ζ(w)). Near w = 1: −ζ′/ζ(w) = 1/(w−1) − γ + O(w−1) (the Laurent series with Stieltjes constants: ζ′/ζ(s) = −1/(s−1) + γ + ...). So (w−1)^{−j}(−ζ′/ζ) has residue = coefficient of (w−1)^{j−1} in −ζ′/ζ = the Stieltjes-ish coefficient: for j=1: 1; for j≥2: (−1)^j γ_{j−2}/(j−2)!? The residue at w=1 is then Σ_{j=1}^n C(n,j)·a_j where a_1 = 1 and a_j = coefficient. And Lagarias identifies this with the archimedean sum S_∞(n) = Σ_j (−1)^j C(n,j) a_j... with the a_j = (1−2^{−j})ζ(j) relation via the Laurent coefficients of −ζ′/ζ at 1 being expressed through η(j) = (1−2^{1−j})ζ(j)... There are standard identities here (D-037 §3 uses Lagarias (4.11): S_∞(n) = Σ_{j=1}^n (−1)^j C(n,j) a_j, a₁ = (log 4π + γ)/2, a_j = (1−2^{−j})ζ(j)).\n\n  So the w=1 residue equals S_∞(n) ± const, and the trivial-zero residues are computable constants. The identity assembly: \n  (1/2πi)∮ = [Σ_{|γ|≤T} −(1−(ρ/(ρ−1))ⁿ)... signs] + [S_∞(n) piece] + [trivial pieces]\n  and rearranging with λ_n = full zero sum gives S_f = S_∞ + 1 − λ_n = [truncated sum] + [sides] + [trivial] + [tail of zero sum with sign].\n  \n  Wait — but then where does the TAIL of the zero sum enter B(n)? |λ_n − truncated|: the tail Σ_{|γ|>T} [1−(1−1/ρ)ⁿ]. Bound: |1−(1−1/ρ)ⁿ| = |1−((ρ−1)/ρ)ⁿ| ≤ n/|ρ| · (something) for large ρ — standard: |(1−w)ⁿ − 1| ≤ n|w|·e^{n|w|} or ≤ 2n|w| for |w| ≤ 1/n. With w = 1/ρ: ≤ 2n/|ρ|. Tail ≤ 2n Σ_{|γ|>T} 1/|ρ|² ~ 2n·(log T)/T ≈ 2√n log T. Hmm, that's significant — is there such a term in B(n)? B(n) = 2F(T) + 4T[...] + ... The 4T[...] terms ~ 4T·(2/3)C₀ ~ T·log T-ish = √n log n-ish. The tail ~ √n log T would be smaller. But I don't see an explicit tail term in B(n)... unless the \"zeros\" term 2F(T) is bounding |Σ_{|γ|≤T}′[1−(ρ/(ρ−1))ⁿ]| ≤ 2N(T) AND the identity as D-037 states it directly has S_f = truncated + sides + triv, with the tail absorbed because... hmm, D-037's identity is EXACT: \"S_f(n) = Σ_{|γ|≤T}′ [1 − (ρ/(ρ−1))ⁿ]·(−1) + (1/2πi)(I_I+I_II+I_III+I_IV) + triv(−2)\". So there's no tail — the identity is exact at finite T. That means S_f's zero-sum definition must be such that truncation is exact — i.e., the contour identity proves S_f (defined via S_∞ + 1 − λ_n) equals the truncated expression exactly. Fine — that's the L0 theorem. The tail is handled inside the identity proof: ∮ sides converge... no, at finite T the identity is exact by residues. The connection between the residue sum and liCoeff requires the FULL zero sum to appear, i.e., the residue computation gives Σ_{|γ|≤T}, and the definition S_f = S_∞ + 1 − λ_n involves the full sum. So the identity proof needs: full sum = truncated + tail, and the tail must be canceled/absorbed by something — presumably the residue at w=1 and the S_∞ identification don't involve the tail... \n\n  Hmm wait, I think I have the structure slightly off. Let me reconsider: probably the actual Lagarias variant-B identity is:\n\n  λ_n = Σ_{|γ|≤T}[1−(1−1/ρ)ⁿ] + tail, and separately the contour gives an exact expression for the truncated sum Σ_{|γ|≤T}[1−(1−1/ρ)ⁿ] = [sides + w=1 residue + trivial residues]. Then S_f = S_∞ + 1 − λ_n = S_∞ + 1 − [that exact expression] − tail. And the w=1 residue = S_∞ + 1 − (constants) so it cancels. Then |S_f| ≤ |sides| + |trivial| + |tail|, and the tail IS one of the bounded pieces. Given B(n) includes \"2F(T)\" as \"the zeros term\", maybe 2F(T) bounds the tail? No — tail ≤ 2nΣ_{|γ|>T}1/|ρ|² — with Σ_{|γ|>T}1/|ρ|² ≤ ∫_T^∞ dN(t)/t² ≤ ~log T/T: tail ≤ 2n·C·log T/T ≈ 2√n·C·log T. And 2F(T) ≈ (T/π)log T = (√n/π)·(½log n). Compare: 2√n C log T vs (√n/π)(log n)/2... these are the same order! So maybe the 2F(T) term actually bounds the TAIL (via Stieltjes-integral zero-counting), and the truncated sum... no wait, D-037 §4 says \"zeros: with RH to height T₀ and n ≤ (T₀−1)², every zero with |γ| ≤ T ≤ T₀ is on the line ⟹ |ρ/(ρ−1)| = 1 ⟹ each term ≤ 2: |Σ| ≤ 2N(T) ≤ 2F(T) + 2S_bnd(T)\". So 2F(T) bounds the TRUNCATED sum (each of N(T) terms ≤ 2). Hmm, so the identity in D-037 has the truncated sum on the RHS — meaning S_f itself equals truncated + sides + triv EXACTLY, with no tail. OK so the exact identity at finite T is what it is; the formalizer must prove exactly that identity. The subtle point: the identity connects liCoeff (full sum) to the truncated sum — the difference IS the tail, and the identity says tail = sides + w=1-residue-excess + triv... i.e., the identity IS nontrivial but exact. Whatever — the exact bookkeeping is in D-036; for the plan, L0 = \"prove the exact identity (D-036 §0)\".\n\n**The w=1 high-order-pole residue**: order n+1 pole. In Lean, computing residues of order n+1... Mathlib has `Complex.residue`?? I don't think Mathlib has a general residue API. PNT+ computes residues via `RectangleIntegral` + explicit local manipulations. For a pole of order n+1 where n is a VARIABLE (n ≥ 10⁵!), you can't just \"compute the residue\" — you need the closed-form identification with S_∞(n) = Σ_j (−1)^j C(n,j) a_j and then the a_j values. This is genuinely intricate: it requires the Laurent coefficients of −ζ′/ζ at s=1 to all orders j ≤ n, identified with (1−2^{−j})ζ(j) up to signs — via the Laurent series of ζ at 1 (Stieltjes constants) — but expressed through the LOGARITHMIC derivative, so there's a recursion (Newton-identity-like) between Stieltjes constants and the log-derivative coefficients. Doable but real work: it's the kind of thing that takes a page of analysis and a formalization of \"logDeriv Laurent coefficients of a function with a simple pole\" lemma.\n\n  ALTERNATIVE ROUTE around the w=1 pole: **change the kernel or the contour to avoid the high-order pole.** Hmm, is there a way? The kernel k_n(w−1) has its pole AT w=1 necessarily (k_n(s) = (1+1/s)ⁿ−1 has pole at s=0). Any kernel with the right interpolation property (k_n(ρ−1) = (ρ/(ρ−1))ⁿ − 1 at zeros) will have the pole where 1+1/s blows up, i.e., s = 0 ⟺ w = 1. So the high-order pole at w=1 is intrinsic to this kernel family. BUT — the residue there is exactly computable in closed form (Lagarias does it), so it's a finite-but-n-dependent explicit quantity. The formalization doesn't need asymptotics; it needs the exact identity. \n\n  ANOTHER ALTERNATIVE: **prove SfBoundProp via a different, contour-free route?** Is there any? |S_f(n)| ≤ B(n) where S_f = S_∞ + 1 − λ_n. Directly bounding |S_f| without the contour: S_f is a zero-sum; the only known way to relate the zero sum to the archimedean data with explicit constants IS the contour argument (that IS BL Thm 2's quantitative version). Alternatively, could we prove the weaker statement needed — λ_n > 0 for n ∈ [10⁵, N₁] — some other way? E.g., direct zero-sum argument: λ_n = Σ[1−(1−1/ρ)ⁿ]; for zeros on the line, each term ≥ 0 individually! (Since |1−1/ρ| = 1 on the line... wait, ρ = 1/2+iγ: 1−1/ρ = (ρ−1)/ρ, |ρ−1| = |ρ| on the line ⟹ |1−1/ρ| = 1, but 1−(1−1/ρ)ⁿ is NOT obviously ≥ 0 — it's 1 − e^{inθ} which has real part 1−cos(nθ) ≥ 0! YES: on the line, each term's real part is 1−cos(nθ_ρ) ≥ 0 where θ_ρ = arg((ρ−1)/ρ).) So IF all zeros with... but λ_n is a sum over ALL zeros, and terms with |γ| large: Re[1−(1−1/ρ)ⁿ] — for ρ on the line this is ≥ 0 ALWAYS. So under FULL RH, λ_n ≥ 0 termwise — trivially. Under RH-only-to-T₀: zeros beyond T₀ could be off-line and contribute negative real parts. The off-line zeros beyond T₀: ρ = σ+iγ with σ possibly ≠ 1/2; |1−1/ρ| vs 1: if σ > 1/2, |1−1/ρ| = |ρ−1|/|ρ| > 1 (since |ρ−1|²−|ρ|² = 1−2σ > 0 ⟺ σ < 1/2... wait: |ρ−1|² = (σ−1)²+γ², |ρ|² = σ²+γ²; |ρ−1|² − |ρ|² = 1−2σ. So σ < 1/2 ⟹ |ρ−1| > |ρ| ⟹ |1−1/ρ| > 1.) Zeros come in symmetric quartets; for σ < 1/2 (equivalently 1−σ > 1/2), |1−1/ρ| > 1, so (1−1/ρ)ⁿ grows exponentially in n and 1−(1−1/ρ)ⁿ ~ −(1−1/ρ)ⁿ has huge NEGATIVE real part along the argument. So off-line zeros high up contribute catastrophically to λ_n for large n — this is WHY the finite-height result needs the contour bound: the margin argument must dominate these hypothetical contributions. Could one bound the off-line contribution directly? |contribution of zero ρ| ≤ 1 + |1−1/ρ|ⁿ ≤ 1 + (|ρ−1|/|ρ|)ⁿ. For zeros beyond T₀ with σ ≤ 1−ε... we have zero-free regions (classical: σ ≤ 1 − c/log|γ|, or explicit Vinogradov–Korobov, or explicit zero-free regions like Mossinghoff–Trudgian: σ ≤ 1 − 1/(R log(|t|+...)) with R ≈ 5.5-ish). With the FUNCTIONAL EQUATION, zeros are symmetric about 1/2, so σ ≤ 1 − δ implies a mirror at 1−σ ≥ δ... the bad zeros have σ < 1/2, factor |1−1/ρ| = |ρ−1|/|ρ| = sqrt(1 + (1−2σ)/|ρ|²) ≤ sqrt(1 + 1/|ρ|²) ≤ 1 + 1/(2|ρ|²). So |1−1/ρ|ⁿ ≤ exp(n/(2|ρ|²)) — for |ρ| > T₀ = 3×10¹² and n ≤ 9×10²⁴: n/(2|ρ|²) ≤ 9×10²⁴/(2·9×10²⁴) = 1/2. Hmm! So |1−1/ρ|ⁿ ≤ e^{n/(2γ²)} ≤ e^{1/2} — the GROWTH is at most e^{1/2} per zero?! That's because n ≤ (T₀−1)² ≈ γ². So each high zero contributes at most ~1 + e^{1/2}... no wait, that's the point — but there are INFINITELY many zeros beyond T₀, and Σ_ρ n/(2|ρ|²) over |γ| > T₀... Σ_{|γ|>T₀} 1/γ² ~ log T₀/T₀ — tiny. And Σ |1−(1−1/ρ)ⁿ| over the tail: using |1−(1−w)ⁿ|... for |1/ρ| small, 1−(1−1/ρ)ⁿ ≈ Σ_{j≥1} C(n,j)(−1)^{j+1}ρ^{−j} — hmm the sum over the tail of the FIRST-order term n/ρ: Σ_{|γ|>T₀} n/ρ doesn't converge absolutely (Σ 1/ρ conditionally converges). With pairing ρ, ρ̄: n·(1/ρ + 1/ρ̄) = 2n·Re(1/ρ) = 2nσ/|ρ|² — absolutely summable. So the tail (paired) ≤ Σ_{pairs, |γ|>T₀} [2nσ/|ρ|² + higher order ≤ C n²/|ρ|⁴-ish]... Σ_{|γ|>T₀} 1/γ² ≈ (1/2π)log T₀/T₀·... ≈ 29/(2π·3×10¹²) ~ 1.5×10⁻¹². Times n = 9×10²⁴: ~ 1.4×10¹³. Hmm, that's big — bigger than the margin (margin at N₁ is 2.46×10²⁶ — no wait, margin(N₁) = 2.458e26 per STATE.md... and S_∞ lower bound ~ ½n log n ~ ½·9×10²⁴·57 ~ 2.6×10²⁶). Tail bound 1.4×10¹³ ≪ 2.6×10²⁶. WAIT. So the tail of the zero sum beyond T₀ is bounded by ~n·(log T₀)/(2π T₀)·2 ≈ tiny compared to S_∞(n) at n = N₁?!\n\n  Hold on, is that right? Σ_{|γ|>T} 1/γ² ≈ ∫_T^∞ (1/2π)log(t/2π) dt/t² = (1/2π)[(log(T/2π)+1)/T]. At T = 3×10¹²: log(3×10¹²/2π) ≈ log(4.77×10¹¹) ≈ 26.9. So Σ ≈ 27.9/(2π·3×10¹²) ≈ 1.48×10⁻¹². Paired first-order tail term: 2n·Σ σ/|ρ|² ≤ 2n·Σ 1/γ² ≈ 2n×1.48×10⁻¹². At n = N₁ ≈ 9×10²⁴: ≈ 2.7×10¹³. And higher-order terms: Σ_j≥2 C(n,j)|ρ|^{−j} ≤ Σ_j (ne/ρ)^j/j! ≤ ... dominated by j=2: n²/γ⁴; Σ_{|γ|>T}1/γ⁴ ~ log T/T³; n²/T³ ~ 8.1×10⁴⁹/2.7×10³⁷ = 3×10¹²·log T — comparable-ish but smaller. OK so order ~10¹³-10¹⁴.\n\n  And the ON-LINE zeros up to T₀ contribute ≥ 0 each (1−cos ≥ 0). So:\n\n  λ_n = Σ_{|γ|≤T₀} [1−cos(nθ_ρ)] + (potential off-line zeros up to T₀: NONE by Platt–Trudgian!) + tail_{|γ|>T₀} ≥ −|tail| ≥ −3×10¹³-ish.\n\n  That's not > 0 — it's ≥ −3×10¹³. The on-line terms are ≥ 0 but most are tiny; their sum: Σ_{|γ|≤T₀}[1−cos(nθ_ρ)] — on AVERAGE ≈ N(T₀) ≈ huge (N(3×10¹²) ≈ (3×10¹²/2π)·log(...) ≈ 1.3×10¹³). But it could be small for particular n if the phases align badly... for SPECIFIC n, no easy lower bound. Hmm, so this direct approach gives λ_n ≥ −tail, useless by itself. The S_∞ − S_f decomposition is fundamentally needed because the archimedean side provides the positive main term. So no, there's no cheap contour-free route. The contour argument is essential. Fine.\n\n  Hmm wait, actually — hold on. Is that really true? λ_n = S_∞(n) − S_f(n) + 1 where S_∞(n) ~ ½n log n is the big positive term and S_f is the zero-side. And S_f as a zero sum: S_f(n) = Σ_ρ [1 − (ρ/(ρ−1))ⁿ]... and Re[1−(ρ/(ρ−1))ⁿ] for ρ ON the line: ρ/(ρ−1) has modulus 1, so = 1−cos ≥ 0. So −S_f's on-line part is ≤ 0, i.e., on-line zeros make S_f SMALLER (λ bigger). The bound |S_f| ≤ B(n) needs to control the on-line part too (≤ 2N(T) as D-037 does) — but on-line zeros actually HELP (their contribution to S_f has positive real part 1−cos... wait sign: S_f = Σ[1−(ρ/(ρ−1))ⁿ]; Re = 1−cos(nφ_ρ) ≥ 0; so S_f ≥ 0-ish from on-line zeros, and λ = S_∞ − S_f + 1 ≤ S_∞ + 1. The DANGER is S_f being very POSITIVE (reducing λ): on-line zeros give S_f up to 2N(T₀) ~ 2.6×10¹³ positive — vs S_∞ ~ 2.6×10²⁶. Fine, dominated.\n\n  So conceptually: at n ~ N₁, S_∞ ~ 2.6×10²⁶ vs all zero-side contributions ~ 10¹³–10¹⁴. MASSIVE slack. The contour bound B(n) with its traced constants is what formalizes \"the zero side is small\". Any sufficiently explicit bound works — the slack is ~10¹²-fold. This means the formalization has ENORMOUS room: crude bounds are fine. This matters for feasibility — we can afford the crudest possible estimates at every step.\n\n### Alternative strategies to close SfBoundProp\n\n**Strategy 1 (frontal, per D-062 triage):** Formalize L0 (contour identity) + L1 (kernel bounds) + L2 (R-bound) + L3 (zero-avoiding T), with L4/L5/L6 as perimeter. This is the plan D-062 sketches: \"multi-session formalization (contour + residue machinery); the honest long pole.\"\n\n**Strategy 2 (PNT+ dependency):** The PNT+ project (Kontorovich et al., \"Prime Number Theorem and...\" — the Lean PNT project at github.com/AlexKontorovich/PrimeNumberTheoremAnd) has already formalized:\n- Rectangle integrals of ζ′/ζ with poles at zeros (they prove the explicit formula ψ(x) = x − Σ x^ρ/ρ − ...)\n- Residue computations including at s=1 and at zeros\n- ζ′/ζ bounds in the critical strip\n- Zero-free region arguments\nIf PNT+ (or its Mathlib-upstreamed parts) is compatible with our toolchain (v4.33.0-rc2), L0's residue infrastructure could be largely imported. Their `Rectangle` API, `ResidueTheoremOnRectangleWithPoles`, `RectangleIntegral` etc. exist in PNT+. Big caveat: dependency pinning/version compat, and PNT+ targets ζ′/ζ with kernel x^s/s-type, not our k_n kernel — but the MACHINERY (rectangle residues with finitely many poles, residue at a zero of ζ, pole at 1) transfers.\n\n**Strategy 3 (circumvent the high-order pole):** The w=1 residue of order n+1 is the ugliest exact-computation piece. Alternative: use a MODIFIED contour/kernel that makes the archimedean side cleaner. E.g., Lagarias's variant A vs B; or BL's original proof; or Akbary–... hmm. OR: avoid identifying the residue with S_∞ at all — instead, prove the inequality directly: we need |Sf n| ≤ Bn where Sf = SInfty + 1 − λ. The identity route computes Sf exactly. Alternative INEQUALITY route: \n  |Sf n| = |S_∞ + 1 − λ_n|. Bound λ_n ≥ (something) and ≤ ... no — we need BOTH sides of λ_n... |S_f| two-sided. λ_n = S_∞ + 1 − S_f; |S_f| ≤ B ⟺ S_∞ + 1 − B ≤ λ_n ≤ S_∞ + 1 + B. We only NEED the lower bound on λ_n for the theorem (λ_n > 0 via margin), but SfBoundProp as stated is two-sided. We could RESTATE the hypothesis the assembly actually consumes... but the assembly is already proved from SfBoundProp; changing it means re-proving the assembly glue (minor). A one-sided version: λ_n ≥ S_∞(n) − B(n) + 1 directly. Contour-wise, the lower bound on λ_n comes from an UPPER bound on S_f... no wait: λ_n = S_∞ − S_f + 1 ≥ S_∞ − |S_f| + 1. We need upper bound on S_f = S_∞ + 1 − λ_n, i.e., lower bound on λ_n... circular-ish. The identity S_f = S_∞ + 1 − λ_n is DEFINITIONAL in the Lean code (Sf := SInfty + 1 − liCoeff.re). So |Sf n| ≤ Bn is |S_∞ + 1 − λ_n| ≤ B. The contour identity proves S_∞ + 1 − λ_n = [truncated zero sum + sides + trivial]. One-sided wouldn't simplify the identity proof materially — the identity is the identity. But the EXACT identity needs the w=1 residue exactly. Hmm — actually does it? |S_f| ≤ B: S_f = [truncated] + [sides] + [trivial] EXACTLY (no w=1 residue remains after the BL bookkeeping... but deriving THAT needs the w=1 residue identified with the S_∞ side). The w=1 residue identification is unavoidable in the frontal route. It's exact finite algebra (Laurent coefficients via Stieltjes recursion), painful but mechanical.\n\n**Strategy 4 (different identity entirely — the η-function route):** Lagarias's a_j = (1−2^{−j})ζ(j) suggests working with η(s) = (1−2^{1−s})ζ(s), whose log-derivative Laurent coefficients at 1 are cleaner? The residue at w=1 for the η-based kernel... The standard trick: −ζ′/ζ(s) = 1/(s−1) − γ − Σ ... Stieltjes. And the identification Σ_j C(n,j) η-related = S_∞. This is bookkeeping, same class.\n\n**Strategy 5 (verify the inequality numerically-certified instead of proving the contour bound):** E-021 computed |S_f(n)| EXACTLY (via the exact S_∞ and λ_n) for n ≤ 10⁴ and found max 13.52 vs bound ~2280. Could we certify |S_f(n)| ≤ B(n) for ALL n ∈ [10⁵, N₁] computationally?? N₁ = 9×10²⁴ — NO, impossible by direct computation. The contour bound's whole point is uniformity in n. What about: for n ∈ [10⁵, N₁], use the ZERO-SUM directly: |S_f(n)| = |Σ_ρ 1−(ρ/(ρ−1))ⁿ| ≤ Σ |...| — infinite sum, needs truncation + tail bound — that IS the contour-free equivalent: truncated sum over |γ| ≤ T (computable for T up to... we have 10⁴ zeros, maybe 10⁶ zeros available? Platt's data? Not to 3×10¹²!). The truncated sum to T₀ = 3×10¹² has ~10¹³ terms — incomputable. So no.\n\n**Strategy 6 (shrink what's needed):** Note SfBoundProp's range starts at 10⁵ (splice with finite verification at 5×10⁵, overlap). The margin at 10⁵ is ~10⁵-scale and B(10⁵) ~ 3.5×10⁵... wait margin = slower − Bn + 1 with margin(10⁵) ≥ 85 501 certified, Bn(10⁵) ≤ 347 000. So we need |S_f(n)| ≤ B(n) with B(10⁵) ≈ 3.4×10⁵ — while TRUE |S_f| values (E-021) are ~13 at n ~ 3000, growing slowly (max 13.52 at n=3298; E-021 says the |S_f| curve vs the traced bound has ~170× slack). At n = 10⁵, true |S_f| maybe ~50–100? vs B ~ 3.4×10⁵. Slack ~10³–10⁴×. At n = N₁: B ~? B(n) ~ 4T·(2/3)C₀(T)·... ~ c·T log²T-ish ~ c·√n·(log n)². At n = 9×10²⁴: √n = 3×10¹², (log n)² ~ 57² ~ 3.2×10³, so B ~ c·10¹⁶-ish; true |S_f| ~ 2N(T)+tail ~ 2.6×10¹³+... The point: slack everywhere. Crude bounds fine.\n\n### Feasibility verdict\n\nThe dominant cost is L0 (the exact contour identity with the order-(n+1) pole residue identified with S_∞(n)) — this is a genuine formalization project: rectangle residue theorem for meromorphic functions with multiple poles INCLUDING a variable-order pole, Laurent coefficients of −ζ′/ζ at 1 to all orders (Stieltjes recursion), exact finite algebra. Plus L2's partial fractions (Hadamard) — does Mathlib have the Hadamard product for ξ? There's been work: Mathlib has `Complex.riemannXi`?? Hmm. Actually I recall Mathlib DOES have `riemannZeta` functional equation and the completed zeta, but the HADAMARD product (Weierstrass factorization of ξ with the zero sum Σ[1/(s−ρ)+1/ρ]) — I believe that's NOT in Mathlib core as of early 2026. The R-bound reference-point proof (D-056) needs the partial-fraction expansion of ζ′/ζ — that's Hadamard. Formalizing Hadamard factorization of ξ from scratch: order-1 entire function, convergence of Σ1/|ρ|², product formula... Mathlib has some entire-function machinery (Hadamard three-circles? Phragmén–Lindelöf? factorization?). There's `Complex.Hadamard`?? I don't think full Weierstrass/Hadamard factorization exists in Mathlib. This is another serious lift. ALTERNATIVE for L2: the R-bound can be proved WITHOUT full Hadamard via the classical route: ζ′/ζ(s) = Σ_{|γ−t|<1} 1/(s−ρ) + O(log t) is usually proved FROM the partial fraction expansion, but there are alternative routes: via the Dirichlet-series/log-derivative bounds + Jensen's formula + Borel–Carathéodory (the standard \"Lemma α\" route in Davenport Ch. 15 uses the partial fractions, but the O(log t) bound for ζ′/ζ − Σ can also be gotten via: log ζ bounds from Borel–Carathéodory on a disc, then Cauchy estimate for the derivative, subtracting the local zero contributions via Jensen/Blaschke). Mathlib has Jensen's formula? There's been formalization of Jensen formula in Mathlib (`Complex.Jensen`?)... I believe Mathlib HAS Jensen's formula (added ~2024 for complex analysis). Borel–Carathéodory: not sure. If not, these are standard and provable from Cauchy estimates — a few hundred lines.\n\nD-056's actual proof uses the reference-point trick + Hadamard partial fractions + digamma Lemma D. To formalize D-056 as-is we'd need partial fractions for ζ′/ζ (Hadamard for ξ). To avoid Hadamard: prove the R-bound via the \"local\" route (Borel–Carathéodory + zero counting C₀). Either way it's work.\n\n**Dependency check needed (sub-stage 0):** survey exactly what Mathlib v4.33.0-rc2 has: rectangle residue theorem (yes: `Complex.integral_boundary_rect...` plus winding-number based residue versions — actually I recall `Complex.rectangleIntegral` and residue-on-rectangle landed via PNT upstreaming efforts by 2024–2025), Jensen's formula (I believe yes), Hadamard factorization (likely no), digamma (yes — `Complex.digamma` exists I think), Stieltjes constants (no — we'd define the needed Laurent coefficients ourselves), riemannZeta Laurent at 1 (Mathlib has the simple pole: `riemannZeta` has `hasSum`...? there's the limit statement `tendsto_riemannZeta_sub...`? Something like residue 1 exists). zeta-23-lean: what's in it (zero counting functions — may provide N(T) infrastructure? D-007 audited: \"counting functions vs Mathlib riemannZeta\" — worth re-examining for L3/L4-adjacent API).\n\nPNT+ as a dependency: check compatibility. If PNT+ pins a different Mathlib version, porting selected files is an option (license Apache 2.0, fine).\n\n### Effort estimate (honest)\n\nThis is the largest single formalization push of the project — bigger than tier (i)+(ii) combined (~1700 lines). Realistic decomposition:\n\n- Sub-stage A (scoping/inventory): Mathlib/PNT+/zeta-23 capability survey; fix the exact target lemma stack; write the proof skeleton with sorries top-down. Deliverable: D-064 (design doc) + LiContour.lean skeleton compiling with named sorries. (1 session)\n- Sub-stage B (L1 kernel + elementary bounds): |k_n| estimates, trivial-zero residues, the easy contour-side estimates. Mathlib-tractable. (1 session)\n- Sub-stage C (L3 zero-avoiding T): pigeonhole gap center from the C₀ count (perimeter N(T) bound as hypothesis — already decided). Finite combinatorics. (0.5–1 session)\n- Sub-stage D (L2 R-bound): choose route (Hadamard vs Borel–Carathéodory local route); formalize. The biggest \"analysis\" chunk after L0. (2–3 sessions)\n- Sub-stage E (L0 part 1: rectangle residue theorem for the needed class + residue at zeros (simple poles)); (1–2 sessions)\n- Sub-stage F (L0 part 2: the w=1 pole of order n+1 — Laurent/Stieltjes identification with S_∞(n); exact finite algebra); (2–3 sessions, the crux)\n- Sub-stage G (L0 part 3: assemble the identity S_f = truncated + sides + trivial; limit/limit-free bookkeeping; L7 summability of liCoeff). (1–2 sessions)\n- Sub-stage H (final assembly: bound each piece by the B(n) terms with the traced constants; plug into lambda_pos_finite_height_verified replacing the hypothesis; axiom audit; paper Appendix B update). (1 session)\n\nTotal: ~9–14 sessions of focused Lean work. Feasibility: I'd say HIGH that it's achievable (it's all \"plain complex analysis, no input obstacles\" per D-062, with Mathlib gaps that are infrastructure-shaped, not mathematics-shaped), with two genuine risk points: (F) the variable-order residue — risk mitigated by doing the exact algebra on paper first (D-036 has it); (D) Hadamard — mitigated by the alternative local route. There's also a \"cheat\" available that dramatically de-risks F: since the slack is 10³–10¹²-fold everywhere, we could replace the EXACT w=1-residue identification by an exact identity proved differently — e.g., compute the w=1 residue as \"Σ_{j=1}^n C(n,j) c_j\" with c_j the Laurent coefficients of −ζ′/ζ (definitionally), then prove |S_∞(n) − that| = 0 via the finite identities... no, that IS the identification. Alternatively bound the residue directly: |residue at 1| ≤ Σ C(n,j)|c_j| and identify Σ(−1)^j C(n,j)a_j = S_∞ separately... the identity S_f = ... + [w=1 residue] is exact; to turn it into |S_f| ≤ B we need to know the w=1 residue EXACTLY equals the S_∞−... no wait. Hmm: S_f := S_∞ + 1 − λ_n. Contour: (1/2πi)∮ = Σ_zeros res + res_{w=1} + Σ_trivial res. Also λ_n = full zero sum. So S_f = S_∞ + 1 − λ_n = S_∞ + 1 − [Σ_{|γ|≤T} + tail]. The contour gives Σ_{|γ|≤T} res = (1/2πi)∮ − res_{w=1} − Σ_triv. Substituting: S_f = S_∞ + 1 − (1/2πi)∮ + res_{w=1} + Σ_triv − tail. So |S_f| ≤ |sides| + |S_∞ + 1 + res_{w=1} + Σ_triv| + |tail|. The term |S_∞ + 1 + res_{w=1} + triv| must be bounded — res_{w=1} is the big negative (−S_∞-ish) — so we need |S_∞(n) + 1 + res_{w=1} + Σ_triv res| ≤ [something small]. I.e., we need the DIFFERENCE (S_∞ + res_{w=1} + trivial) to be SMALL, not the exact identity! Is that easier? res_{w=1} = Σ_j C(n,j) c_j (c_j = Laurent coeffs of −ζ′/ζ). S_∞ = Σ_j (−1)^j C(n,j) a_j (a_j = (1−2^{−j})ζ(j) for j ≥ 2, a₁ = (log 4π+γ)/2). Claim: c_j = −(−1)^j a_j exactly?? — that would make S_∞ + res = 0 + lower-order (the triv residues and the +1 handle the rest). The identification c_j vs a_j is EXACTLY the Stieltjes/η identity — same work whether we need equality or a bound on the difference, because the difference is huge unless exactly canceling (individual terms C(n,j)·c_j are ~C(n,j)·(j−1)!-scale? |c_j| growth: Laurent coefficients of ζ′/ζ — c_j = (−1)^j η(j−1)/(j−1)!-ish bounded-ish... a_j = (1−2^{−j})ζ(j) → 1 as j → ∞. The sums Σ C(n,j)a_j ~ 2ⁿ-scale cancellation! NO WAIT: S_∞(n) = Σ(−1)^j C(n,j) a_j is a FINITE difference — it's ~ ½n log n, achieved via massive cancellation of ~2ⁿ-scale terms. You cannot bound the difference |S_∞ + res| without the EXACT per-j identity — any per-term triangle inequality explodes like 2ⁿ. THIS IS the \"three-way cancellation IS RH\" wall from D-033 (\"arithmetic-side triangle bounds explode\"). So the exact identification c_j = ±a_j is FORCED. No cheat. The good news: the identity is classical and exact (Lagarias 4.11); formalizing it is finite algebra + the Laurent-coefficient recursion for logDeriv at a simple pole. It's the crux but it's well-defined.\n\nHmm, one more idea to de-risk F: **avoid the w=1 residue entirely by subtracting a reference kernel**. Consider two consecutive n: k_{n+1} − k_n = (1/s)k_n... or consider the kernel difference trick: the quantity S_∞(n) satisfies a recurrence; the contour for n and the contour for n−1... This doesn't obviously help.\n\n**Better structural idea (the \"engineered identity\" route):** Instead of proving Lagarias's exact identity with the pole at w=1 of order n+1 head-on, use the BL Thm 2 route via MELLIN inversion rather than the rectangle at finite height... no, finite-height explicitness is the whole point.\n\n**Alternative contour shape:** Take σ₁ = +∞ instead of 2√n (Lagarias variant with the right side at infinity — the k_n kernel decays for σ → +∞ since k_n(w−1) = (1+1/(w−1))ⁿ − 1 ~ n/(w−1)); then no I_II right-side integral; but the w=1 pole remains. No help for F.\n\nSo F's exact-algebra identification is unavoidable in ANY contour route. Accept it. It's a known, bounded piece of classical algebra (Lagarias (4.11) is a one-page identity). Formalization: define c_j via the Laurent recursion for logDeriv of ζ at 1 (Mathlib HAS the Laurent/pole API? For a function f with simple pole at s₀, logDeriv f has Laurent coefficients satisfying a recursion in terms of f's — provable via `Complex.meromorphic` API... Mathlib has `MeromorphicAt` with order, Laurent series?? There's `MeromorphicAt` API (added 2024-2025, by the PNT-adjacent work): `MeromorphicAt.order`, Laurent coefficients? Hmm, partial. We may need to roll our own \"local lemma\": if g analytic near 0 with g(0) ≠ 0 then d/ds log((s−1)g(s)) = 1/(s−1) + g′/g, and g′/g's Taylor coefficients satisfy the recursion — elementary with `AnalyticAt`/`FormalMultilinearSeries` API, which Mathlib has solidly). Then identify with (1−2^{−j})ζ(j) via the Dirichlet series of −ζ′/ζ = Λ-sum and the Taylor generating identity... The cleanest classical proof of Lagarias (4.11): a_j defined by the generating function identity; equivalence via comparing the two expressions for the same integral at INFINITY (not via local Laurent algebra!). I.e., prove the global identity \"S_∞(n) + res_{w=1} + triv + 1 = 0\" ONCE for all n by a soft argument (e.g., both sides are... polynomials in n? The residue Σ_j C(n,j)c_j is a polynomial in n of degree n — no, C(n,j) for j ≤ n with n the variable... it's not polynomial in n in a useful sense for induction... hmm, actually C(n,j)c_j summed IS related to finite differences: Σ_j (−1)^j C(n,j) a_j = Δⁿ a at 0 — the n-th finite difference! And S_∞(n) = (Δⁿ a)(0)-ish. Finite-difference calculus: if we show the w=1 residue equals −(Δⁿ ã)(0) for an explicit sequence ã, the identification reduces to a SEQUENCE identity, provable by generating functions (the two sequences have the same exponential generating function — an identity of analytic functions, provable by ... ugh, still work but maybe cleaner: EGF of a_j: A(x) = Σ a_j x^j/j! — related to log Γ-ish functions; EGF of Laurent coeffs similar; equality of EGFs as analytic functions reduces to equality on a sequence accumulating — circular. OK: equality of EGFs via DIRECT computation of both EGFs in closed form. Lagarias's proof: Σ_j (−1)^j C(n,j)a_j with a_j = (1−2^{−j})ζ(j): Σ_m odd ((1−1/m)ⁿ −1 +n/m) — the double-sum form (D-037 §3 derives it by absolute convergence for j ≥ 2). That's the route D-037 used for the S_∞ LOWER bound (already Lean-proved in tier (i) from the double-sum form!). And the residue side: res_{w=1} = Σ_j C(n,j) c_j — write c_j via −ζ′/ζ = −Λ-dirichlet... For j ≥ 2, c_j: the Taylor coefficients of −ζ′/ζ + 1/(s−1) at s=1 equal... via ζ′/ζ(s) = −Σ Λ(m)m^{−s} for Re s > 1, NO — that's the Dirichlet series, valid far right, not the Taylor at 1. The relation a_j = (1−2^{−j})ζ(j) comes from the FUNCTIONAL EQUATION side / the η trick. Hmm, honestly: Lagarias proves (4.11) using the contour argument itself (evaluate the same integral two ways). The cleanest for us might be: DON'T prove the c_j = a_j identity locally at all. Instead, prove the SINGLE global identity we need — S_∞(n) + 1 + res_{w=1}(n) + triv(n) = 0 for all n — by induction on n! Both sides as sequences in n satisfy the same first-order recurrence (S_∞(n+1) − S_∞(n) has a closed form? S_∞ via double sum: difference computable. res_{w=1}(n+1) − res_{w=1}(n): the kernel k_{n+1} − k_n = (1/s)·... k_{n+1}(s) − k_n(s) = (1+1/s)ⁿ·(1/s) = ((1+1/s)ⁿ)/s. Hmm — residue of that difference at w=1 might telescope. If both sides satisfy the same recurrence and match at n = 1 (base case = one explicit residue computation at fixed small order — order-2 pole, EASY), the identity follows for all n. THIS is a much better formalization route for F: reduce the variable-order residue to (i) a base case (order ≤ 2 pole, computable), (ii) a recurrence step (kernel identity, algebra), (iii) induction. The recurrence for the archimedean side: S_∞(n+1) − S_∞(n) — from the double-sum form (already formalized in tier (i)!): h⁺(m) differences... Σ_m odd [(1−1/m)^{n+1} − (1−1/m)ⁿ + 1/m] = Σ_m odd [−(1/m)(1−1/m)ⁿ + 1/m]... = S_∞-related again — has a closed form in terms of the same structures. Feasible. This turns \"identify two n-indexed families of constants\" into \"check one recurrence + one base case\". MUCH more Lean-friendly. I should put this in the plan as the chosen attack for F.)\n\nHmm wait, but actually the induction needs the contour identity for EACH n anyway (we're proving the identity for all n simultaneously)... no — the plan: for each n, the contour identity gives S_f(n) = sides(n) + [S_∞(n) + 1 + res(n) + triv(n)] + tail-free-exact-truncated... The bracket must vanish identically. Prove \"bracket(n) = 0 ∀n\" by induction: bracket(0) or bracket(1) by direct small-order residue computation; bracket(n+1) − bracket(n) = 0 by kernel algebra + the S_∞ difference formula. The residue difference res(n+1) − res(n) = residue of [k_{n+1}(w−1) − k_n(w−1)](−ζ′/ζ) at w=1 = residue of (1+1/(w−1))ⁿ·(1/(w−1))·(−ζ′/ζ) = coefficient extraction — still involves −ζ′/ζ's full Taylor at 1... same problem! Ugh. Unless: the induction is on the CONTOUR side instead: sides(n+1) − sides(n) = ∫ [k_{n+1} − k_n]·(−ζ′/ζ)/2πi = ∫ (1+1/(w−1))ⁿ/(w−1)·(−ζ′/ζ)... and by residues THIS integral over a contour NOT enclosing w=1 but the zeros... this is getting complicated. The recurrence approach doesn't obviously escape the local algebra.\n\nAlternative for F that DOES escape: **prove the bracket vanishes via the TAIL side.** We have S_f(n) := S_∞ + 1 − λ_n and separately S_f(n) = sides + bracket + truncated (contour). Also λ_n = truncated + tail. So bracket(n) = S_f(n) − sides(n) − truncated(n) — and also S_f(n) = S_∞+1−λ_n. The claim bracket = 0 is equivalent to the exact identity. No escape; the exact identity is a theorem and must be proved. The question is only WHICH proof to formalize: (a) local Laurent algebra at w=1 (Lagarias 4.11 via local recursion + η-identity), or (b) Lagarias's own \"evaluate two ways\" trick, or (c) some generating-function global argument. All have similar weight. (a) is the most mechanical. Fine — accept (a), and note (a) has a nice sub-structure: define c_j recursively from ζ's Laurent at 1 (Stieltjes); prove c_j = (−1)^j (1−2^{−j})ζ(j) + [j=1 adjustment] via the η-function: η(s) := (1−2^{1−s})ζ(s) is entire, η(1) = log 2, and −ζ′/ζ(s) = 1/(s−1) + [log(2)·2^{1−s}/(1−2^{1−s})... let me just compute: log η = log(1−2^{1−s}) + log ζ; differentiate: η′/η = (log 2·2^{1−s})/(1−2^{1−s}) + ζ′/ζ. Hmm so ζ′/ζ = η′/η − log 2/(2^{s−1}−1). Near s=1: η′/η analytic (η(1) = log 2 ≠ 0 — WAIT η(1) = lim (1−2^{1−s})ζ(s) = log 2·1 = log 2 ≠ 0 ✓). And log 2/(2^{s−1}−1) has a simple pole at 1 with known full Laurent expansion (Bernoulli numbers!): 1/(2^{s−1}−1) = 1/((s−1)log 2) − 1/2 + (log 2)(s−1)/12 − ... (Bernoulli). So c_j = [Taylor of η′/η at 1] − [Bernoulli series]. And η′/η at 1: Taylor coefficients of logDeriv of the ENTIRE function η — related to ζ(j) values how? η′/η(s) = Σ ... at s = 1: derivatives of log η. Connection to ζ(j), j ≥ 2: NOT local — ζ(j) are values at OTHER points. The identity \"Taylor coeffs of logDeriv η at 1\" = \"(1−2^{−j})ζ(j)-related\" — hmm, this can't be a pure local identity; it must use the global structure. Lagarias (4.11) indeed comes from the global contour manipulation. OK — so the honest content of F: a global identity. Fine, that's mathematics we already have written in D-036/D-037; the formalizer follows the written proof. Bounded work.\n\nGiven the depth here, the plan should include a **paper-first sub-stage**: re-derive the w=1-residue/S_∞ identity in the cleanest possible form on paper (D-064), specifically optimized for formalization (choosing route (a)/(b)/(c) with Mathlib's API in mind), BEFORE writing Lean. This was the session-012-lesson: design-first worked (FAlt swap caught pre-instantiation).\n\n### The honest answer on \"possibility\"\n\n- Mathematical novelty required: ZERO. All content exists in the archive (D-036/D-037/D-056, Lagarias) with constants traced.\n- Mathlib gaps: real but infrastructure-shaped. Rectangle residue theorem: partially exists; multi-pole version must be assembled. Hadamard factorization of ξ: likely absent — circumvent via local route (Borel–Carathéodory/Jensen) or formalize the needed fragment (Σ[1/(s−ρ)+1/ρ] convergence — needs zero-count input C₀ anyway = perimeter, so the convergence proof can USE the perimeter bound! Nice: with N(T) ≤ F(T) (perimeter), Σ|ρ|⁻² converges by comparison — the Hadamard product's analytic machinery is still needed though: order-1 entire function ξ... Mathlib has `Complex.riemannXi`? There's `completedRiemannZeta` and its entireness I believe. The product formula itself — the honest survey in sub-stage A will tell.)\n- Variable-order pole: the crux, bounded, classical.\n- Scale: ~9–14 sessions by the estimate above. Compare: tier (i)+(ii) took sessions 011–012 (~1700 lines). This is maybe 4–8× that.\n- Success probability: high that it's achievable with sustained effort (no mathematical obstacles, only engineering); the main risks are (1) Mathlib API gaps forcing detours, (2) the w=1 identity formalization being fiddly, (3) PNT+ incompatibility if we try to import. Mitigations: paper-first design stage, local-route alternatives, sorries-first top-down skeleton so the critical path is visible early.\n\nAlso worth noting: what does success BUY? The tag upgrade from \"[PROVED-CONDITIONAL + SfBoundProp hypothesis]\" to \"[Lean-verified modulo published N(T)/S(T) bounds + computational certificates]\" (D-062 §4 consequence). It does NOT change the theorem, the paper's math, or the height. It removes the one named analytic hypothesis. Given paper A is submission-ready NOW with the hypothesis honestly declared, and the referee process may itself comment — the user should know: this is a robustness/self-containment upgrade, not a correctness fix. Also note D-062's decision was that tier ii′ is POST-publication per the mathematician review. The user now wants to do it anyway — fine, their call, maybe they'd rather have the fully-closed form before submission. Worth stating the trade-off honestly: (i) doing it now delays submission by many sessions; (ii) doing it after publication risks the referee asking exactly this. Actually for Experimental Mathematics, a declared-hypothesis machine-verified theorem is quite standard and the perimeter declaration is honest. But the user asked for the plan, not the go/no-go — I'll give the plan and a short note on sequencing choice.\n\n### Plan structure\n\nI'll propose:\n\n**Sub-stage ii′-0 — Capability survey + target stack (D-064).** Inventory: Mathlib v4.33.0-rc2 (rectangle residues, MeromorphicAt/Laurent, Jensen, digamma, riemannZeta API, Γ, Bernoulli), zeta-23-lean contents, PNT+ compatibility check. Fix the exact lemma dependency graph for L0–L3. Choose routes: Hadamard-vs-local for L2; local-Laurent-vs-global for the w=1 identity. Deliverable: D-064 design + `LiContour.lean` skeleton compiling with ~15–25 named sorries (each a claimed lemma with precise statement). Exit criterion: every sorry statement reviewed against D-036/D-037/D-056; no sorry is mathematically unproved in the archive.\n\n**Sub-stage ii′-1 — L1 kernel bounds + trivial residues.** Elementary.\n\n**Sub-stage ii′-2 — L3 zero-avoiding T.** Pigeonhole on the C₀ count (perimeter N-bound as a hypothesis-of-record `TrudgianN`).\n\n**Sub-stage ii′-3 — L2 R-bound.** The analytic heavy lift #1.\n\n**Sub-stage ii′-4 — L0a rectangle residue machinery.** Multi-pole rectangle residue theorem (assemble from Mathlib's rectangle + winding number, or port PNT+ fragment).\n\n**Sub-stage ii′-5 — L0b w=1 pole: the S_∞ identification.** The crux; paper-first (already drafted in ii′-0).\n\n**Sub-stage ii′-6 — L0c identity assembly + L7 summability.**\n\n**Sub-stage ii′-7 — Final bound assembly + theorem swap + audit.** Replace `hSf : SfBoundProp` hypothesis with the proved theorem; rerun full axiom audit (target: 3 standard axioms + 0 sorryAx in the Li chain); update paper Appendix B + tag to the D-062 §4 endpoint form; journal/NGUYEN/ledger updates.\n\nAlso: keep E-023b (acb M₀) as a parallel optional item — needed to make L6 a computational perimeter (currently E-023 grid-verified; declared).\n\nI should also mention the strategic option: **run ii′ while submitting** — paper A is ready; the submission can go out with the declared hypothesis and tier ii′ strengthens a revision. But user said \"regroup to work on tier ii′\" — they may have decided. I'll note the option in one line and let them decide.\n\nPer §8.5 sub-stage rule, each sub-stage ends in a clean committed resumable state. Also note the fork rule doesn't really apply (single path).\n\nOne more consideration: total Lean line estimate. Tier (i)+(ii) ≈ 1100 + 560 + skeleton ~ maybe 3000 lines. Tier ii′: L2 ~ 800–1500, L0a ~ 400–800, L0b ~ 600–1200, rest ~ 800. Total maybe 3000–5000 lines of new Lean. Sessions: 8–14. I'll present ranges honestly and note the two crux points.\n\nI could also propose de-risking: start with ii′-5-crux ON PAPER (the exact identity proof written in formalization-friendly form) since everything hinges on it — actually no, better to start with the skeleton (ii′-0) which includes the paper design for the crux.\n\nFormat: this deserves a well-structured, moderately detailed response — the user asked to \"think deep and analyze... break this down into sub-stages... possibility... plan\". Not too long though. I'll give: (1) what the task actually is (the three real obstacles), (2) feasibility analysis with the key de-risking insights (slack, perimeter reuse, recurrence/pole handling, PNT+ option), (3) the sub-stage plan with exit criteria, (4) probability estimate, (5) strategic note. Then ask if they want to start with ii′-0.\n\nShould I use AskUserQuestion at the end? The user said \"Let me know what you think and your plan on this matter.\" So they want the plan first. I'll end with a simple question about whether to proceed/adjust. A plain closing question is fine.\n\nLength: this is a planning deep-dive the user explicitly requested — medium-long is appropriate, but keep it tight. Use tables sparingly. No need for tool calls now — I have enough from D-062/D-037/STATE. I could do a quick Mathlib inventory via grep of the local Mathlib checkout to firm up feasibility claims... The NguyenRH1 has path-requires to vendored zeta-23-lean and Mathlib — I could grep Mathlib source for key APIs (residue, Jensen, digamma, Hadamard). That would make the feasibility assessment concrete rather than from-memory. Worth doing quickly — it's cheap and derisks the plan. Let me check a few key things:\n\n1. Rectangle residue theorem in Mathlib: search for \"residue\" / \"rectangle\" in Mathlib's Complex analysis.\n2. Jensen's formula.\n3. digamma.\n4. Hadamard / Weierstrass product.\n5. riemannZeta API surface (Laurent at 1, trivial zeros).\n6. PNT+ presence (probably not vendored).\n\nLet me find the Mathlib path first. It's in the .lake/packages of zeta-23-lean or NguyenRH1. Let me glob for it.","signature":""},{"type":"text","text":"Let me ground the feasibility analysis in what's actually available in the vendored Mathlib before proposing the plan."},{"type":"tool_use","id":"Bash_9","name":"Bash","input":{"command":"ls \"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\.lake\\packages\" 2>/dev/null; ls \"D:\\Python\\Quantum\\research\\lean\\zeta-23-lean\\.lake\\packages\" 2>/dev/null","description":"Locate vendored Mathlib package path"},"extra_content":null}]