[{"type":"thinking","thinking":"`LogOfAnalyticFunction` gives exactly what's needed:\n- J_B analytic on ball(0,R), J_B(0) = 0\n- deriv J_B = B′/B on closedBall(0,r)\n- **Re(J_B z) = log‖B z‖ − log‖B 0‖** on ball(0,R) — the exact relation for the BC step.\n\nSo the chain: with B = g (the zero-removed ζ): Re J_g(z) = log|g(z)| − log|g(0)|. Upper bound: log|g(z)| ≤ A' log|t| + B' (from the |ζ| bound + product clearance), −log|g(0)| ≤ C log|t| (center lower bound). So Re J_g ≤ M := (A'+C) log|t| + B''. Then BorelCaratheodoryDeriv (f = J_g, f(0) = 0 ✓): ‖deriv J_g z‖ ≤ 16MR²/(R−r)³. And deriv J_g = g′/g = ζ′/ζ − Σ mult/(s−ρₖ) — wait: g = ζ/∏(s−ρₖ)^{mₖ}: logDeriv g = logDeriv ζ − Σ mₖ/(s−ρₖ) ✓.\n\nNote: the lemmas are stated for functions on discs centered at 0 — so apply to the translated/scaled function. The SetOfZeros/Blaschke stuff: actually for the Davenport argument I DON'T need the Blaschke factors — the simpler g = ζ/∏(s−ρₖ)^{mₖ} division suffices (the Blaschke form is for |factor| ≤ 1 control, but the crude clearance bound works too). So maybe I don't even need DiskBound/BlaschkeB — just:\n1. g := ζ(s) / ∏(s−ρₖ)^{mₖ} — analytic & nonvanishing on the disc (zeros removed) ✓ elementary (each factor removal kills the pole... wait: ζ has zeros at ρₖ with multiplicity mₖ = analyticOrderNatAt ζ ρₖ; dividing by (s−ρₖ)^{mₖ} removes them — analyticity of the quotient at ρₖ needs the order argument — `ZeroFactorization` lemma exists (line 214) ✓ or build directly from analyticOrderAt).\n2. |g| on outer circle ≤ |ζ|/∏|s−ρₖ|^{mₖ} ≤ C|t|²/clearance^m.\n3. log|g(s₀)| ≥ ... (center lower bound).\n4. LogOfAnalyticFunction + borelCaratheodory'/BorelCaratheodoryDeriv.\n5. deriv J_g = g′/g = ζ′/ζ − Σ mₖ/(s−ρₖ) via logDeriv product rules (need: logDeriv (ζ/∏) = logDeriv ζ − Σ... — logDeriv_div, logDeriv_prod, logDeriv (s−ρ)^m = m/(s−ρ): `logDeriv_pow`? there might be `logDeriv_fun_pow`? these exist in some form — check during implementation).\n\nThis is a clean assembly path using LogOfAnalyticFunction + borelCaratheodory' (or Deriv). The BlaschkeB/ZerosBound pieces are only needed if I want the Jensen zero count — but the count comes from the perimeter ZeroCountProp instead ✓ (cleaner, and it's the honest Trudgian constant).\n\nGeometry final: center s₀ = 2+it; R = 5/2 (disc σ ∈ [−1/2, 9/2]); collection radius r_c: zeros with |γ−t|<1 have |ρ−s₀| ≤ √((2)²+1) = √5 ≤ 2.24; collect zeros with |ρ−s₀| ≤ 2.3 (say); clearance on outer circle ≥ 2.5−2.3 = 0.2. Inner (application) radius r_a = 3/2 (cover σ ∈ [1/2, 7/2]). BC derivative factor: 16·R²/(R−r_a)³ = 16·(25/4)/(1)³ = 100.\n\nThe |ζ| bound on B(2+it, 5/2): σ ∈ [−1/2, 9/2], via the B₂-representation: ζ(s) = 1/2 + 1/(s−1) + s(s+1)∫₁^∞ B̃₂(x)x^{−s−2}dx (valid σ > −1, s ≠ 1): |ζ(s)| ≤ 1/2 + 1/|s−1| + |s||s+1|/(8(σ+1)). For σ ≥ −1/2: /(σ+1) ≤ 2: |ζ| ≤ 1/2 + 1/9 + |s||s+1|/4 ≤ ... |s| ≤ |t|+5: |s||s+1| ≤ (|t|+5)(|t|+6): |ζ| ≤ 0.61 + (|t|+5)(|t|+6)/4 ≤ C(1+|t|)² ✓.\n\nSo the new-build pieces for ii′-5:\n1. `zeta_rep_level2`: ζ(s) = 1/2 + 1/(s−1) + s(s+1)∫₁^∞ B̃₂(x)x^{−s−2}dx for re s > −1, s ≠ 1 — from Zeta23's ζ₀(N) rep via one more IBP. The B̃₂ function (x−⌊x⌋)²/2 − (x−⌊x⌋)/2 hmm — define B̃₂(x) = ∫₀^x B̃₁(t)dt... need: B̃₂ continuous, periodic, B̃₂(0) = 0, |B̃₂| ≤ 1/8, HasDerivAt B̃₂ (B̃₁ x) off integers. The IBP on each [n, n+1] + telescope + tail. This is the biggest new build (~0.5–1 session).\n   Hmm wait — alternatively skip the IBP and use TWO evaluations of the B₁ rep?? The B₁ rep only works σ > 0. No. The IBP is needed. OR — actually, maybe simpler: use the B₁ rep at the SHIFTED function: bound |ζ| on the disc by applying B₁ to... no.\n   Actually — hmm, ANOTHER thought: avoid σ < 0 entirely by choosing R < 2 and NOT collecting all |γ−t|<1 zeros, but collecting fewer zeros... The R-sum is FIXED (|γ−t|<1). The zeros of the sum with |ρ−s₀| > R − δ sit outside the outer circle — but they're INSIDE the sum regardless. The Blaschke removal must remove exactly the sum's zeros (else (log g)′ ≠ ζ′/ζ − Σ...). If R < collection distance, the far zeros aren't removable by the disc method. So no — collection must fit inside R. Confirmed need the left dip. B₂-level it is.\n\n2. The right-region R-bound assembly (the Davenport argument) — the main theorem (~1 session).\n3. FE-reflection to σ ∈ [−5/2, 1/2] (~0.5 session): logDeriv algebra + digamma_stirling + cot/tan bounds... wait — with the Λ-route there's NO cot at all: ζ′/ζ(s) = −ζ′/ζ(1−s) + log π − (1/2)(ψ((1−s)/2) + ψ(s/2)) — only digamma terms ✓ and ψ(s/2) via the +2 recurrence into the Zeta23 bound's range. NO trig needed!! (The cot cancels in the symmetric ΓR form.) \n   Hmm wait — let me double check the ΓR logDeriv reflection: ΓR(s)·ΓR(1−s)... the reflection formula is for Γ, not ΓR: ΓR(s)ΓR(1−s) hmm = π^{−s/2}Γ(s/2)·π^{−(1−s)/2}Γ((1−s)/2) = π^{−1/2}·Γ(s/2)Γ(1−s/2) = π^{−1/2}·π/sin(πs/2) = √π/sin(πs/2). So logDeriv ΓR(s) + logDeriv ΓR(1−s) = −logDeriv[sin(πs/2)] = −(π/2)cot(πs/2) — the cot DOES appear if I expand via reflection. But my derivation DIDN'T use reflection for ΓR — it used Λ-FE only: ζ′/ζ(s) = −logDeriv Λ(1−s) − logDeriv ΓR(s), and logDeriv Λ(1−s) = logDeriv ΓR(1−s) + logDeriv ζ(1−s). So ζ′/ζ(s) = −logDeriv ΓR(1−s) − ζ′/ζ(1−s) − logDeriv ΓR(s) = −ζ′/ζ(1−s) − [ΓR′/ΓR(1−s) + ΓR′/ΓR(s)]. The bracket is what it is — just two digamma evaluations (each bounded via the recurrence+digamma_stirling) — NO need to simplify via reflection into cot. ✓ The bound: |ΓR′/ΓR(1−s) + ΓR′/ΓR(s)| ≤ |ψ((1−s)/2)|/2 + |ψ(s/2)|/2 + log π·... wait: ΓR′/ΓR(w) = −(log π)/2 + (1/2)ψ(w/2) ✓ so bracket = −log π + (1/2)(ψ((1−s)/2)+ψ(s/2)): |·| ≤ log π + (1/2)(|ψ((1−s)/2)| + |ψ(s/2)|) ≤ log π + (1/2)(C log|t| + C' log|t|) ✓.\n\n4. Constant folding.\n\nTotal estimate: 2–3 sessions as D-064 said. This session (022): design doc D-067 + possibly the start of the B₂-rep build. \n\nHmm — wait, actually, let me reconsider whether the reflection step's identity is even needed in that form. The ii′-6 assembly needs the R-bound on:\n- horizontals: σ ∈ [−5/2, 3] hmm — actually D-036's horizontals: |I_II|, |I_IV| with the (6.12) stepping for σ ∈ [3, 2√n]... the R-bound enters for σ ∈ [−5/2, 3].\n- Actually wait — for σ ∈ [3/2, 3] do we even need the disc? |ζ′/ζ| direct Dirichlet bound works for σ ≥ 3/2 hmm — no: the R-bound is about ζ′/ζ MINUS the near-zero sum; on σ ≥ 3/2, |ζ′/ζ| ≤ |ζ′/ζ(3/2)| directly ✓ but the near-zero sum Σ1/(s−ρ) still needs bounding — trivially: each |s−ρ| ≥ |σ−β| ≥ 1/2 hmm σ = 3/2: |s−ρ| ≥ 1/2: Σ ≤ 2·C₀ — fine directly. So for σ ≥ 3/2 the R-bound is DIRECT (no disc needed). The disc is needed for σ ∈ [1/2, 3/2] hmm — and the reflection covers σ ∈ [−5/2, 1/2] using the disc region re(1−s) ∈ [1/2, 7/2] — but wait for re(1−s) ∈ [3/2, 7/2] the direct bound applies instead. Consistent either way.\n\nFine. The design is DONE modulo implementation details. Write D-067 now, journal, STATE, commit. Then next session starts the build.\n\nActually — let me also sanity-check the ONE risky existing-piece claim: `digamma_stirling` gives ‖ψ(w) − log w + 1/(2w)‖ ≤ 3/w.im² for re w > 0, |im w| ≥ 1/2. Our applications: ψ((1−s)/2) with re((1−s)/2) = (1−σ)/2 ∈ [1/4, 7/4] for σ ∈ [−5/2, 1/2] ✓ > 0; |im| = |t|/2 ≥ 5 ≥ 1/2 ✓. ψ(s/2+2) (recurrence shift): re = σ/2+2 ∈ [3/4, 9/4] ✓ > 0; |im| = |t|/2 ≥ 5 ✓. Both fine. And |log w| ≤ log|w| + π ≤ log|t| + C ✓.\n\nOne more: the recurrence ψ(w) = ψ(w+1) − 1/w — Mathlib: `Complex.digamma_add_one`? D-066 inventory said `digamma_apply_add_one` ✓ exists in Mathlib. Two applications: ψ(w) = ψ(w+2) − 1/w − 1/(w+1) ✓.\n\nAnd the logDeriv-FE derivation: Λ(1−s) = Λ(s) (completedRiemannZeta_one_sub ✓) — deriv of both sides: need deriv (fun s => Λ(1−s)) s = −Λ′(1−s) ✓ chain rule (deriv_comp / hasDerivAt...). And logDeriv Λ(s) = logDeriv ΓR(s) + logDeriv ζ(s) for s with ζ(s) ≠ 0, s ∉ {0,1}, ΓR(s) ≠ 0: logDeriv (ΓR·ζ) = logDeriv ΓR + logDeriv ζ via `logDeriv_mul` (needs both nonvanishing + differentiable ✓). But Λ = ΓR·ζ only off {0} ∪ ΓR-poles (the RvM.completedRiemannZeta_eq_Gammaℝ_mul needs s ≠ 0, ΓR s ≠ 0) — at our s (re ∈ [−5/2, 1/2], |t| ≥ 10, ζ(s) ≠ 0): s ≠ 0 ✓; ΓR s ≠ 0 ⟺ s ∉ {−2n} ✓ (|t| ≥ 10). ✓. So logDeriv ζ s = logDeriv Λ s − logDeriv ΓR s — valid. Similarly at 1−s: re(1−s) ∈ [1/2, 7/2]: need ζ(1−s) ≠ 0 for logDeriv ζ(1−s)... hmm! logDeriv ζ (1−s) = ζ′/ζ(1−s) — at a zero of ζ(1−s) it's a pole — the identity R(s) = −R(1−s) + ... is stated for s with ζ(s) ≠ 0; then 1−s: ζ(1−s) ≠ 0? As computed earlier: ζ(1−s) = 0 ⟹ (1−s nontrivial zero) ⟹ s = 1−ρ₀... and then ζ(s) = 0 too (FE) — contradiction ✓. So under the hypothesis ζ(s) ≠ 0: ζ(1−s) ≠ 0 ✓ (for s in the strip σ ∈ [−5/2, 1/2], |t| ≥ 10 — plus the case re(1−s) ≥ 1 handled by Λ zeros being nontrivial). Need the FE step \"ζ(1−s) = 0 ⟹ ζ(s) = 0\" hmm direction: if 1−s is a nontrivial zero then s is a zero: ζ(s) = ζ(1−(1−s)) = χ₀(1−(1−s))... use Λ: Λ(s) = Λ(1−s) = 0 ✓ and Λ(s) = ΓR(s)ζ(s) with ΓR(s) ≠ 0 ⟹ ζ(s) = 0 ✓. Clean via Λ.\n\nOK. Design complete. Write D-067.","signature":""},{"type":"text","text":"All pieces verified. The design is complete and — importantly — it avoids the two feared builds (no complex Stirling for Γ, no Hadamard). Writing the design doc D-067 now."},{"type":"tool_use","id":"Write_174","name":"Write","input":{"file_path":"D:\\Python\\Quantum\\research\\derivations\\D-067-ii-prime-5-design.md","content":"# D-067 — ii′-5 design: the R-bound in Lean (route b″, Stirling-free)\nDate: 2026-08-22 | Session: 022 | Task: 5.1 tier ii′-5 (D-064 §4 R3)\nStatus: DESIGN COMPLETE (inventory verified live against the vendored\nMathlib + Zeta23). Implementation sub-stages ii′-5a..e below.\n\n## 0. Target and context\n\nTier-ii′ goal (D-064 §5 graph [R3]): formalize the R-bound input to the\nii′-6 assembly — D-056's Theorem R:\n\n  R(s) := ζ′/ζ(s) − Σ_{|γ−t|<1} mult(ρ)/(s−ρ),\n  |R(s)| ≤ A·log(|t|+2) + B₀   (A = 10.5, B₀ = 48; σ ∈ [−5/2, 3], |t| ≥ 10)\n\nD-056's pen-and-paper proof uses the ξ Hadamard partial fractions —\nRULED OUT for Lean (D-066: no Weierstrass/order theory in Mathlib).\nD-064's prescription: the Davenport Ch.-15 LOCAL route (disc +\nBorel–Carathéodory). This design pins the exact route, geometry, and\nconstants, and — critically — ELIMINATES the two feared builds:\n\n* **No complex Stirling for Γ.** The vertical-decay bound |Γ(a+ib)| ~\n  |b|^{a−1/2}e^{−π|b|/2} is NOT needed anywhere (see §2/§3).\n* **No Hadamard product for ξ.** The zero-sum in R(s) is handled by the\n  disc Blaschke-removal, and the left-strip half by FE-reflection with\n  EXACT zero-sum cancellation (§3).\n\n## 1. Geometry and the key obstruction\n\nThe disc argument needs |ζ| polynomially bounded on a disc covering both\nthe application region and the near zeros. Zeros ρ = β+iγ with |γ−t| < 1\nsit at distance up to √(c²+1) from any center c+it (β → 0⁺), and\n√(c²+1) > c ALWAYS — so every covering disc dips left of σ = 0, where\nthe Dirichlet series and Zeta23's `ZetaUpperBnd` (σ ≥ 1−A/log|t| only,\nFromPNTPlus/ZetaBounds.lean:1402) are useless, and the FE bound would\nneed Γ's vertical decay (§0, avoided). Resolution: keep the dip shallow\n(σ ≥ −1/2) and bound |ζ| there by ONE extra Euler–Maclaurin level (§2).\n\n**Chosen geometry (right region).** Center s₀ = 2+it, outer radius\nR = 5/2 (disc ⊆ {σ ≥ −1/2}), zero-collection radius r_c = 2.3\n(all |γ−t|<1 zeros: |ρ−s₀| ≤ √5 ≈ 2.236 < 2.3; clearance on the outer\ncircle ≥ 0.2), application radius r_a = 3/2 (covers σ ∈ [1/2, 7/2] —\nthe range the FE-reflection needs, §3).\n\n**Lean statement shape (target):** for s = σ+it, σ ∈ [−5/2, 3],\n|t| ≥ 10, riemannZeta s ≠ 0:\n  ‖logDeriv riemannZeta s − Σ_{ρ ∈ nearZeros t} (zeroMult ρ)/(s−ρ)‖\n    ≤ 10.5 * Real.log (|t|+2) + 48\nwith nearZeros t the finset of nontrivial zeros in the open window\n(finiteness: ii′-4's zerosIn_finite pattern; the mult-weighted count\nbound via the perimeter or ZerosBound — pinned at implementation).\n\n## 2. The |ζ| polynomial bound on σ ≥ −1/2 (NEW BUILD, ~1 session)\n\nOne extra Euler–Maclaurin level over Zeta23's existing B₁ machinery:\n\n  ζ(s) = 1/2 + 1/(s−1) + s(s+1)·∫₁^∞ B̃₂(x)·x^{−s−2} dx\n         (re s > −1, s ≠ 1)\n\nwith B̃₂(x) = ∫₀ˣ B̃₁, periodic, B̃₂(0) = 0, |B̃₂| ≤ 1/8 (B̃₂(x) =\n((x−⌊x⌋)²−(x−⌊x⌋))/2 on each period). Derivation: Zeta23 has\n`riemannZeta0 N s = riemannZeta s` (re s > 0, `Zeta0EqZeta`) with the\nB₁-integral; IBP once (per unit interval + telescope; B̃₂ continuous so\nthe boundary terms at integers vanish; tail converges for re s > −1);\nextend to −1 < re s ≤ 0 by the identity principle (both sides analytic\nthere; agree on re s > 0). Then on the disc B(2+it, 5/2):\n\n  |ζ(s)| ≤ 1/2 + 1/|s−1| + |s||s+1|/(8(σ+1)) ≤ C(1+|t|)²  (σ ≥ −1/2).\n\nPieces in Zeta23/FromPNTPlus: EulerMaclaurin.lean (`B1`,\n`abs_B1_le_half`, `integral_deriv_mul_add_const` IBP helper),\nZetaBounds.lean (`Zeta0EqZeta`, integrability lemmas). New: B̃₂ def +\nproperties + the IBP step + the identity-principle extension.\n\n## 3. The two-half plan\n\n### Right half: σ ∈ [1/2, 7/2], |t| ≥ 10 (the Davenport disc, ~1–1.5 sess)\nOn B(2+it, 5/2):\n1. |ζ| ≤ C(1+|t|)² (§2).\n2. Collect the zeros {ρₖ} of ζ in B(s₀, 2.3) with multiplicities\n   mₖ = analyticOrderNatAt ζ ρₖ (= zeroMult); count-with-multiplicity\n   ≤ 3·C0hat(t+3)-style bound (three unit windows of ii′-4's\n   ZeroCountProp; mult ≤ count via the window bound applied to\n   multiplicities — or ZerosBound/Jensen; pin at implementation).\n   g(s) := ζ(s)/∏ₖ(s−ρₖ)^{mₖ} — analytic, NONVANISHING on B(s₀, 2.3+);\n   the removal analyticity via Zeta23 `ZeroFactorization`\n   (StrongPNTPrefix.lean:214) or direct order arguments.\n3. Outer circle: |g| ≤ C(1+|t|)²/(0.2)^m ⟹ log|g| ≤ A′log|t| + B′.\n4. Center: |ζ(2+it)| ≥ 1/ζ(2) (via 1/ζ = Σμ(n)n^{−s}, ‖1/ζ‖ ≤ ζ(2) —\n   Mathlib LSeries moebius; name check at build time) and\n   ∏|s₀−ρₖ| ≤ 2.3^m ⟹ −log|g(s₀)| ≤ C′log|t|.\n5. `LogOfAnalyticFunction` (StrongPNTPrefix:124): J_g analytic,\n   J_g(s₀) = 0 (after the 0-centered translation), deriv J_g = g′/g,\n   and Re J_g = log|g| − log|g(s₀)| ≤ M := (A′+C′)log|t| + B″.\n6. `BorelCaratheodoryDeriv` (StrongPNTPrefix:108): ‖deriv J_g‖ ≤\n   16M R²/(R−r_a)³ = 100M on B(s₀, 3/2).\n7. deriv J_g = ζ′/ζ − Σₖ mₖ/(s−ρₖ) (logDeriv quotient/product rules).\n   R(s) = (log g)′(s) + Σ_{collected, |γ−t|≥1} mₖ/(s−ρₖ); extras:\n   each |s−ρₖ| ≥ |t−γₖ| ≥ 1 ⟹ |extras| ≤ count ≤ C₀-bound.\n\n### Left half: σ ∈ [−5/2, 1/2], |t| ≥ 10 (FE-reflection, ~0.5 sess)\nVia Λ = ΓR·ζ (Zeta23 `RvM.completedRiemannZeta_eq_Gammaℝ_mul`, valid\nsince ΓR(s) ≠ 0 off {−2n} and s ≠ 0) and Λ(1−s) = Λ(s)\n(`completedRiemannZeta_one_sub`):\n\n  ζ′/ζ(s) = −ζ′/ζ(1−s) − [ΓR′/ΓR(1−s) + ΓR′/ΓR(s)].\n\nUnder riemannZeta s ≠ 0 also ζ(1−s) ≠ 0 (Λ-vanishing ⟺ IsNontrivialZero,\n`completedRiemannZeta_eq_zero_iff`, + the FE). Substituting R(1−s):\n\n  R(s) = −R(1−s) − [ΓR′/ΓR(1−s) + ΓR′/ΓR(s)]\n         + [Σ_{|γ−t|<1} m/(s−ρ)] − [Σ_{|γ′+t|<1} m′/(1−s−ρ′)]\n\nand the two sums CANCEL EXACTLY: zeros with γ′ near −t are ρ′ = 1−ρ with\nγ near t (FE symmetry), multiplicities match (mult_reflect — Zeta23\nseam), and 1/(1−s−(1−ρ)) = −1/(s−ρ).\n\nThe ΓR-bracket: ΓR′/ΓR(w) = −(log π)/2 + ½ψ(w/2) (Zeta23\n`RvM.logDeriv_Gammaℝ` — exists, used in XiPrime/ZeroCount/Y.lean).\nBoth digamma arguments have positive real part:\n- (1−s)/2: re ∈ [1/4, 7/4], |im| = |t|/2 ≥ 5 — direct.\n- s/2: re ∈ [−5/4, 1/4] — shift by +2 via the digamma recurrence\n  (Mathlib `digamma_apply_add_one` twice; two rational terms O(1/|t|)),\n  landing in re ∈ [3/4, 9/4].\nBound: `Zeta23.StirlingVert.digamma_stirling` (0 < re, 1/2 ≤ |im|):\n‖ψ(w) − log w + 1/(2w)‖ ≤ 3/w.im² — already proved in Zeta23. ⟹\n|ΓR-bracket| ≤ log π + C·log|t| + O(1).\n\nSo |R(s)| ≤ |R(1−s)| + C·log|t| + O(1), and the right-half bound closes\nit. NOTE: this also SUBSUMES D-056's Lemma D (the digamma remainder) —\nnever needed separately; `digamma_stirling` is strictly stronger.\n\n### Constants fold (~0.25 sess, with E-support if wanted)\nTrace the constants through §2–§3 to the A = 10.5, B₀ = 48 form (the\npaper's values; the Lean proof can carry its own traced constants —\nthey only need to fit under Bn FAlt in ii′-6, which has huge slack —\nD-056 §3 sensitivity: 26×). Decision at build time: match D-056's\nnumbers or take the natural traced ones (must stay ≤ paper claims).\n\n## 4. Inventory of existing machinery (all verified live, session 022)\n\nMathlib: `Complex.borelCaratheodory` (unused — Zeta23's derivative\nversion is the one), `completedRiemannZeta_one_sub`,\n`riemannZeta_ne_zero_of_one_lt_re`, `digamma_apply_add_one`,\n`riemannZeta_neg_two_mul_nat_add_one`, LSeries vonMangoldt/moebius.\nZeta23: FromPNTPlus/StrongPNTPrefix.lean — `BorelCaratheodoryDeriv`\n(‖deriv f‖ ≤ 16MR²/(R−r)³), `LogOfAnalyticFunction` (J_B with Re J_B =\nlog‖B‖−log‖B(0)‖, deriv J_B = B′/B), `ZeroFactorization`, `ZerosBound`;\nFromPNTPlus/ZetaBounds.lean — `Zeta0EqZeta` (B₁-level ζ rep, re > 0),\n`ZetaUpperBnd`; GammaFacts/StirlingVert.lean — `digamma_stirling`;\nGammaFacts/Series.lean — digamma series + Weierstrass for 1/Γ (unused);\nRvM/CountByIntegral.lean — `completedRiemannZeta_eq_Gammaℝ_mul`,\n`completedRiemannZeta_eq_zero_iff`; XiPrime/ZeroCount/Y.lean —\n`norm_digamma_le` (‖ψ(w)‖ ≤ ‖w‖+8), `RvM.logDeriv_Gammaℝ`.\nii′-4 (this project): `ZeroCountProp`, `zeroWindow_finite`,\n`zeroMult_neg_two`, `two_le_C0hat`.\n\n## 5. Sub-stage plan\n\n| # | Content | Depends | Est. |\n|---|---------|---------|------|\n| ii′-5a | this design doc | — | done (session 022) |\n| ii′-5b | B̃₂ + IBP level-2 ζ rep + |ζ| ≤ C(1+|t|)² on σ ≥ −1/2 | ζ₀ | ~1 sess |\n| ii′-5c | right-half Davenport disc (g, J_g, BC, R-bound σ∈[1/2,7/2]) | 5b, ii′-4 | ~1–1.5 sess |\n| ii′-5d | FE-reflection to σ∈[−5/2,1/2] + digamma bracket | 5c | ~0.5 sess |\n| ii′-5e | constants fold to A = 10.5, B₀ = 48 + audit | 5d | ~0.25 sess |\n\nRisks: (a) the B̃₂ IBP is fiddly but elementary (mitigation: per-interval\nwork is exactly EulerMaclaurin.lean's pattern); (b) the mult-weighted\nzero count may want a Jensen detour (ZerosBound exists); (c) logDeriv\nproduct-rule glue for the quotient g — standard.\n"},"extra_content":null}]