[{"type":"thinking","thinking":"DL-1 committed (4c36802). Now DL-2: the V_left bound. Components:\n\n(i) **Kernel lemma**: ‖kFun n (3+it)‖ ≤ e^{5/2}+1 for t² ≥ n.\n   |kFun n (3+it)| = |(3+it)/(2+it)|ⁿ − 1| ≤ |(3+it)/(2+it)|ⁿ + 1.\n   |(3+it)/(2+it)|² = (9+t²)/(4+t²) = 1 + 5/(4+t²).\n   So |(3+it)/(2+it)|ⁿ = (1+5/(4+t²))^{n/2} ≤ exp(5n/(2(4+t²))) ≤ e^{5/2} (t² ≥ n ⟹ 5n/(2(4+t²)) ≤ 5n/(2t²)·... wait: 4+t² ≥ t² ≥ n ⟹ 5n/(2(4+t²)) ≤ 5n/(2n) = 5/2 ✓).\n   The Lean form: ‖((3+it)/(2+it))ⁿ‖ = ‖(3+it)/(2+it)‖ⁿ = ((9+t²)/(4+t²))^{n/2}... in ℂ norm: ‖(3+it)/(2+it)‖ = √(9+t²)/√(4+t²) = ((9+t²)/(4+t²))^{1/2} (nonneg). Then ‖·‖ⁿ = ((1+5/(4+t²))^{1/2})ⁿ = (1+5/(4+t²))^{n/2}.\n   Bound: (1+x)^{n/2} ≤ exp(nx/2) with x = 5/(4+t²) (1+x ≤ e^x). So ≤ exp(n·5/(2(4+t²))) ≤ e^{5/2}.\n   \n   In Lean: this needs norm computation of the complex ratio + real power bounds. The existing kernel lemmas (kFun_shift_norm_le_exp_four_add_one etc. in LiContour) did similar — let me clone the pattern from kFun_shift_norm_le_exp_four_add_one (LiContour:503). Let me read it to clone.\n\n(ii) **C_zeta3 Dirichlet bound**: ‖ζ′/ζ(3+it)‖ ≤ 0.165. The dirichletC2 pattern: norm_logDeriv_zeta_le_dirichlet (re ≥ 2) : ‖ζ′/ζ s‖ ≤ dirichletC2 where dirichletC2 = ∑' ‖LSeries.term Λ 2 n‖. For re ≥ 3: ‖ζ′/ζ s‖ ≤ ∑'‖LSeries.term Λ 3 n‖ =: dirichletC3 — a new def + a clone of the dirichlet lemma's proof at 3. Then dirichletC3 ≤ 0.165 — the CERTIFIED evaluation: dirichletC3 = Σ Λ(m)/m³ — bounding this in Lean by 0.165 needs a finite partial sum + tail bound proof. Partial sum to K (say 200) + tail ≤ ∫_K^∞ log x/x³ dx·... — in Lean, a partial sum over a Finset of Λ-terms (computable — but Λ is ArithmeticFunction.vonMangoldt — the sum Σ_{m≤200} Λ(m)/m³ is a finite computation — then bound the tail. This could be heavy: the tail bound via an integral comparison (the LiTightR antitone-integral machinery exists!) or a cruder telescoping bound.\n   \n   Cruder route avoiding the big partial sum: Σ_{m≥2} Λ(m)/m³ ≤ Σ_{m≥2} (log m)/m³ ≤ small-constant by a simple integral comparison: Σ_{m≥2} log m/m³ ≤ log 2/8 + ∫_2^∞ log x/x³ dx = 0.0866 + [log 2/(2·4) + 1/(4·4)] = 0.0866 + 0.0866 + 0.0625 = 0.2357 — too loose (0.2357 > 0.165). Tighter: Σ_{m=2}^{10} Λ(m)/m³ exactly + tail ∫_{10}^∞: (2log10+1)/(4·81)·... = (2·2.303+1)/324 = 0.0173; partial Σ_{2}^{10}: log2/8+log3/27+log5/125+log7/343+log2/16(log4... wait Λ(4) = log2, Λ(8) = log2, Λ(9) = log3: Σ_{2..10} = log2(1/8+1/16+1/32+1/256(16=2⁴ is ≤10? 16>10 no)) — m ∈ {2,...,10}: Λ: log2, log3, log2, log5, 0, log7, log2, log3, 0 → log2/8 + log3/27 + log2/16 + log5/125 + log7/343 + log2/256 + log3/729 = 0.0866+0.0407+0.0433+0.0129+0.00567+0.00271+0.00151 = 0.19342?? That EXCEEDS 0.165!! Wait — log2/16 = 0.0433 (m=4), log2/256 = 0.00271 (m=8). Sum: 0.08664+0.04069+0.04332+0.01288+0.005674+0.002708+0.001507 = 0.19342. But the true total is 0.16482?? CONTRADICTION — let me recompute: Λ(2) = log 2 = 0.6931; /8 = 0.08664. Λ(3) = log 3 = 1.0986; /27 = 0.04069. Λ(4) = log 2 = 0.6931; /64!! 4³ = 64, not 16!! /64 = 0.010830. I made an arithmetic error (used 4² = 16 as the denominator — wrong, it's m³ = 64). Λ(5)/125 = 0.012877. Λ(6) = 0. Λ(7)/343 = 0.005673. Λ(8) = log2/512 = 0.001354. Λ(9) = log3/729 = 0.001507. Λ(10) = 0. Sum: 0.08664+0.04069+0.01083+0.01288+0.00567+0.00135+0.00151 = 0.15956. Tail from 11: ∫_{10}^∞ (2log x+1)/(4x²)·... the certified tail (2log(K−1)+1)/(4(K−1)²) at K = 11: (2·2.303+1)/(4·100) = 5.606/400 = 0.01401. So C_zeta3 ≈ 0.15956+0.01401+ε... hmm 0.15956+tail-true(~0.0053) = 0.1648 ✓ consistent with the mpmath value 0.1648227. For a Lean bound: partial(10) + tail(11) = 0.15956+0.01401 = 0.17357 — too loose vs 0.165!! Need partial to larger K: K = 26 (tail (2log25+1)/(4·625) = 7.4376/2500 = 0.00298): partial(25) = true − Σ_{26+} ≈ 0.16482 − 0.005 = 0.1598?? no — partial(25) ≈ 0.16482 − Σ_{m≥26}Λ/m³ ≈ 0.16482 − (log26/17576 + ...) ≈ 0.16482 − 0.0004 ≈ 0.1644. +0.00298 = 0.1674 — still > 0.165!! K = 101: tail (2·4.615+1)/4e4 = 10.23/40000 = 0.000256; partial(100) ≈ 0.16482 − 0.0001 ≈ 0.1647; sum = 0.16496 ≤ 0.165 ✓ tight. K = 201: tail (2·5.3+1)/160800 = 0.0000721; partial ≈ 0.16479; sum ≈ 0.16486 ✓.\n\n   So the Lean certification needs a partial sum to K ≈ 100–200 with a certified tail. In Lean: Σ_{m=2}^{100} Λ(m)/m³ as a finite rational computation — 99 terms, each Λ(m)·... — ArithmeticFunction.vonMangoldt is defined via the Möbius function convolution (Λ = μ ⋆ log) — computing it for m ≤ 100 in Lean: `decide`/native_decide could evaluate... that's 100 terms of ℂ arithmetic — `norm_num` won't do it (log values!). Hmm — Λ(m) is log p for prime powers — Real.log p is NOT a rational. So the partial sum is a sum of Real.log p terms — can't be evaluated by norm_num to a decimal.\n\n   Better Lean route: bound Σ Λ(m)/m³ WITHOUT computing logs: \n   Σ_{m≥2} Λ(m)/m³ ≤ Σ_{m≥2} (log m)/m³ — then bound Σ log m/m³ via grouping + integral comparison with certified log evaluations at a few points... still messy.\n   \n   ALTERNATIVE cleaner route: use a DIFFERENT bound for ‖ζ′/ζ(3+it)‖ that avoids the constant evaluation entirely: ‖ζ′/ζ(3+it)‖ ≤ ΣΛ(m)/m³ ≤ ΣΛ(m)/m²·(1/... no.\n   \n   Hmm — what about: Σ Λ(m)/m³ ≤ (1/8)Σ Λ(m)/m²·... no: 1/m³ ≤ (1/8)(1/m²)?? no — 1/m³ ≤ 1/(8m²) ⟺ m ≥ 8... not uniform.\n   \n   Split: Σ_{m≥2} Λ(m)/m³ = Σ_{m=2}^{7} Λ(m)/m³ + Σ_{m≥8} Λ(m)/m³. First sum: the values involve log 2, log 3, log 5, log 7 — bound by certified rational log bounds (Real.log_two_lt_d9, log 3/5/7 via exp comparisons — small, 4 numbers ✓ the LiBasePoints machinery does exactly this). Second: Σ_{m≥8} Λ(m)/m³ ≤ Σ_{m≥8} (log m)/m³ ≤ ∫_7^∞ log x/x³ dx = (log 7 + 1/2)/(2·49)·... = (log 7)/(2·49) + 1/(4·49)·... wait ∫_7^∞ log x/x³ dx = [−log x/(2x²) − 1/(4x²)]_7^∞ = log 7/(2·49) + 1/(4·49) = log7/98 + 1/196 ≈ 1.9459/98 + 0.0051 = 0.01986+0.0051 = 0.02496. And the discrete sum ≤ integral + first term: Σ_{m≥8} log m/m³ ≤ log 8/512 + ∫_8^∞ log x/x³ dx = 0.00406 + (log 8)/(2·64)+1/(4·64) = 0.00406+0.01624+0.00391 = 0.02421. Hmm — so second ≈ 0.0242. First: log2(1/8+1/64+1/512) + log3(1/27+1/729) + log5/125 + log7/343: 0.6931·(0.125+0.015625+0.0019531) = 0.6931·0.142578 = 0.098831; 1.0986·(0.037037+0.0013717) = 1.0986·0.038409 = 0.042205; 1.6094/125 = 0.012875; 1.9459/343 = 0.005673. First ≈ 0.159584. Total ≈ 0.1838 — still > 0.165!! The integral tail bound is too lossy (the true tail from 8 is ~0.0053 but the integral comparison gives 0.0242 — 4.6× too big because log x/x³ drops fast).\n\n   Tighter tail: Σ_{m≥8} log m/m³ — integral comparison with a SHIFT: for decreasing f: Σ_{m≥K} f(m) ≤ f(K) + ∫_K^∞ f — that gave 0.0242. Better: Σ_{m≥K} f(m) ≤ ∫_{K−1}^∞ f for decreasing f: ∫_7^∞ log x/x³ dx = log7/98+1/196 = 0.02496. Worse. The issue: the integrand drops by factor 8 per doubling; the integral comparison loses ~f(K)·(1+1/(2K))·... ~ f(8)·3 — inherently lossy for fast-decreasing sums. To get 0.005-ish need the partial sum to m ~ 30–100 with certified log values at ~10 primes — that's ~20 certified log bounds (Real.log_two_lt_d9 exists; log 3, 5, 7, 11, 13, 17, 19, 23, 29, 31 via the exp-comparison machinery — each ~10 lines in the LiBasePoints style). Tedious but mechanical. Tail from 101: ∫_{100}^∞ log x/x³ = log100/20000+1/40000 = 0.00023+0.000025 = 0.000255; plus the discrete-vs-integral gap: use Σ_{m≥101} f ≤ ∫_{100}^∞ f = 0.000255 ✓. Partial(100): the true value 0.16457 + tail 0.000255 = 0.16482 ≤ 0.165 ✓✓.\n\n   So the Lean C_zeta3 proof: Σ_{m=2}^{100} Λ(m)/m³ ≤ [certified rational R₁₆₄₅₇+ε] + tail ≤ 0.00026. The partial sum: Σ over prime powers ≤ 100: primes 2,3,5,7,11,...,97 (25 primes) + prime powers 4,8,16,32,64 (2ⁿ), 9,27,81 (3ⁿ), 25 (5²), 49 (7²) — 35 terms, each Λ = log p. So Σ = Σ_{p≤100} c_p·log p with c_p = Σ_{k: p^k ≤ 100} 1/p^{3k} (c_2 = 1/8+1/64+1/512+1/4096+1/32768 = 0.14261; c_3 = 1/27+1/729+1/19683 = 0.03851; c_5 = 1/125+1/15625 = 0.008064; c_7 = 1/343+1/16807 = 0.002975; other primes c_p = 1/p³). Bound each log p ≤ certified rational (the LiBasePoints route: log p ≤ log-bound via e^{bound} ≥ p comparisons). The log values needed: log 2..log 97 — 25 primes. Certified upper bounds to ~1e-4 each: log 2 ≤ 0.6932 (d9 ✓); log 3 ≤ 1.0987; log 5 ≤ 1.6095; log 7 ≤ 1.9460; log 11 ≤ 2.3980; log 13 ≤ 2.5650; log 17 ≤ 2.8333; log 19 ≤ 2.9445; log 23 ≤ 3.1356; log 29 ≤ 3.3674; log 31 ≤ 3.4341; log 37 ≤ 3.6110; log 41 ≤ 3.7137; log 43 ≤ 3.7613; log 47 ≤ 3.8502; log 53 ≤ 3.9704; log 59 ≤ 4.0776; log 61 ≤ 4.1110; log 67 ≤ 4.2048; log 71 ≤ 4.2628; log 73 ≤ 4.2906; log 79 ≤ 4.3696; log 83 ≤ 4.4189; log 89 ≤ 4.4887; log 97 ≤ 4.5748. Each needs an exp comparison in Lean (e^{bound} ≥ p — via the partial-sum/exp machinery — 25 little proofs or a systematic norm_num-able route: e^{bound} ≥ p with bound rational: Real.sum_le_exp_of_nonneg gives a LOWER bound on exp; then log p ≤ bound ⟺ p ≤ e^{bound} ⟸ (p : ℝ) ≤ Σ₀ᴷ boundⁱ/i! — a finite rational inequality — norm_num CAN check these (the partial sums are rational with huge denominators but norm_num handles them — session-012 did exactly this pattern: `le_trans (by norm_num [Finset.sum_range_succ]) (Real.sum_le_exp_of_nonneg ...)`). So each log p ≤ bound is ~3 lines. 25 × 3 lines ≈ 75 lines. The tail: Σ_{m≥101} Λ(m)/m³ ≤ Σ_{m≥101} (log m)/m³ ≤ ∫_{100}^∞ log x/x³ dx = (log 100)/20000 + 1/40000 — needs the antitone-integral machine (LiTightR's AntitoneOn.tsum_comp_add_le_integral pattern) or a dyadic/telescoping elementary bound: Σ_{m≥101} log m/m³ ≤ Σ_{j≥0} Σ_{100·2^j ≤ m < 100·2^{j+1}} log m/m³ ≤ Σ_j (count)·log(100·2^{j+1})/(100·2^j)³ = Σ_j 100·2^j·(log100 + (j+1)log2)/(100³·8^j) = (1/100²)·Σ_j (log100+(j+1)log2)/4^j = (1/100²)·[log100·(4/3) + log2·(4/3 + 4/9... Σ(j+1)/4^j = 1/(1−1/4)²·(1/4)... = (1/4)/(9/16) = 16/9·... = (4/3)²/... Σ_{j≥0}(j+1)/4^j = 1/(1−1/4)² = 16/9]. = (1/10000)·[1.3333·log100 + 1.7778·log2] = (1/10000)·[1.3333·4.6052+1.7778·0.6931] = (1/10000)·[6.1403+1.2322] = 0.000737. Hmm — cruder (0.000737 vs 0.000255) but ELEMENTARY (geometric series, no integral machine). Total: partial ≤ 0.16457-ish + 0.00074 = 0.16531 — EXCEEDS 0.165!! Ugh. The dyadic tail is too lossy by 0.0005.\n   \n   Fix: partial to 200 instead of 100 (adds Σ_{101..200} ≈ log101/1030301·... ~ 0.00018 of true value) and dyadic tail from 200: (1/200²)·[1.3333·log200+1.7778·log2] = (1/40000)·[1.3333·5.2983+1.2322] = (1/40000)·[7.0644+1.2322] = 0.000207. Total ≈ 0.16475+0.000207 = 0.16496 ≤ 0.165 ✓✓ (tight but OK — the certified partial must come in ≤ 0.16476; with log-bound slack 1e-4·Σc_p ≈ 1e-4·0.19 ≈ 2e-5 — fine).\n\n   Hmm — this is getting heavy (25 log bounds + a 35-term rational sum + dyadic tail). ALTERNATIVE: is there a cheaper mathematical bound for ‖ζ′/ζ(3+it)‖ avoiding the constant 0.165?? \n\n   IDEA: use the dirichletC2 machinery at a SHIFTED point: ‖ζ′/ζ(3+it)‖ ≤ ΣΛ(m)/m³ ≤ ΣΛ(m)/(2·m²)·... no. \n   \n   IDEA 2: bound ΣΛ(m)/m³ by (1/2)·ΣΛ(m)/m² + correction: Λ(m)/m³ ≤ Λ(m)/(2m²) for m ≥ 2 ✓!! (1/m³ ≤ 1/(2m²) ⟺ m ≥ 2 ✓). So ΣΛ(m)/m³ ≤ (1/2)·ΣΛ(m)/m² = dirichletC2/2 ≤ 0.57/2 = 0.285. Too big (0.285 > 0.165).\n   \n   IDEA 3: sharpen: ΣΛ(m)/m³ ≤ Λ(2)/8 + Λ(3)/27 + Σ_{m≥4} Λ(m)/(4m²)·... 1/m³ ≤ 1/(4m²) for m ≥ 4: = log2/8 + log3/27 + (1/4)(dirichletC2 − log2/4 − log3/9) = 0.0866+0.0407+(1/4)(0.57−0.1733−0.1221) = 0.1273+0.0687 = 0.1960. Still > 0.165. One more split level (m ≥ 8 → 1/(8m²)): log2/8+log3/27+log2/64+log5/125+log7/343 + (1/8)(dirichletC2 − log2/4−log3/9−log2/16−log5/25−log7/49) = 0.15958 + (1/8)(0.57−0.1733−0.1221−0.0433−0.0644−0.0397) = 0.15958+(1/8)(0.1272) = 0.15958+0.01590 = 0.1755. Still > 0.165. Extend to m ≥ 16: subtract and add (1/16): partial(15) ≈ 0.15958+Λ(8)/512+Λ(9)/729+Λ(11)/1331+Λ(13)/2197 = 0.15958+0.001354+0.001507+0.001802+0.001168 = 0.16541 + (1/16)(dirichletC2 − partial-quadratic) = 0.16541+(1/16)(0.57−0.4493) = 0.16541+0.00754 = 0.1729. WORSE — the partial sum itself already exceeds 0.165 at m = 11!! Because the TRUE total is 0.1648 and the m ≤ 13 partial is already 0.1654?? That can't be — let me recompute partial(13): 0.086640+0.040690+0.010830+0.012877+0.005673+0.001354+0.001507+0.001802+0.001168 = 0.162541. Hmm I added wrong: 0.15958+0.001354 = 0.16093; +0.001507 = 0.16244; +0.001802 = 0.16424; +0.001168 = 0.16541?? 0.16424+0.001168 = 0.16541 — but the TRUE TOTAL is 0.16482 and the tail from 17 is positive?! Let me recheck the true value: mpmath said 0.164822681359. Partial(13) computed: log2/8 = 0.0866403; log3/27 = 0.0406892; log2/64 = 0.0108304; log5/125 = 0.0128755; log7/343 = 0.0056731; log2/512 = 0.0013539; log3/729 = 0.0015072; log11/1331 = 0.0018015; log13/2197 = 0.0011677. Sum: 0.0866403+0.0406892 = 0.1273295; +0.0108304 = 0.1381599; +0.0128755 = 0.1510354; +0.0056731 = 0.1567085; +0.0013539 = 0.1580624; +0.0015072 = 0.1595696; +0.0018015 = 0.1613711; +0.0011677 = 0.1625388. OK partial(13) = 0.16254 ✓ (my running addition was sloppy). Tail from 17: true − partial = 0.16482−0.16254 = 0.00228. So partial(13) + tail-bound ≤ 0.165 needs tail(17) ≤ 0.00246. Dyadic tail from 16: (1/16²)·[1.3333·log16+1.7778·log2]·... — redo the dyadic: Σ_{m≥17} Λ(m)/m³ ≤ Σ_{m≥16}(log m)/m³ ≤ Σ_j 16·2^j·(log(16·2^{j+1}))/(16³·8^j)... = (1/256)·Σ_j (log16+(j+1)log2)/4^j = (1/256)·[(4/3)log16 + (16/9)log2] = (1/256)·[1.3333·2.7726+1.7778·0.6931] = (1/256)·[3.6968+1.2322] = (1/256)·4.929 = 0.01925. Way too lossy. The dyadic bound's constant (count 16·2^j per dyadic block) is terrible.\n\n   The dyadic tail is fundamentally too lossy at small K. The INTEGRAL comparison is much tighter: Σ_{m≥K} f ≤ f(K)+∫_K^∞ f: at K = 17: log17/4913 + log17/(2·289)+1/(4·289) = 0.000576+0.004899+0.000865 = 0.00634. Still too lossy (0.00634 > 0.00246). ∫_{16}^∞ (no +f(K)): log16/(2·256)+1/(4·256) = 0.005412+0.000977 = 0.006389. Same.\n\n   So the tail MUST be ~0.0023 at m = 17 and any elementary bound gives ≥ 0.006. The only way: partial sum further out (K = 100–200) where the integral tail ≤ 0.0003 — needs the ~25 certified log bounds anyway (partial(100) with the c_p-weighted sum: c_2 = 0.14261·log2 ≤ 0.14261·0.6932 = 0.098858; c_3·log3 = 0.03851·1.0987 = 0.042309; c_5·log5 = 0.008064·1.6095 = 0.012978; c_7·log7 = 0.002975·1.9460 = 0.005789; then primes 11..97: log11/1331 ≤ 2.3980/1331 = 0.0018017; log13/2197 ≤ 0.0011677; log17/4913 ≤ 2.8333/4913 = 0.0005767; log19/6859 ≤ 0.0004292; log23/12167 ≤ 0.0002578; log29/24389 ≤ 0.0001381; log31/29791 ≤ 0.0001153; log37/50653 ≤ 0.0000713; log41/68921 ≤ 0.0000539; log43/79507 ≤ 0.0000473; log47/103823 ≤ 0.0000371; log53/148877 ≤ 0.0000267; log59/205379 ≤ 0.0000199; log61/226981 ≤ 0.0000181; log67/300763 ≤ 0.0000140; log71/357911 ≤ 0.0000119; log73/389017 ≤ 0.0000110; log79/493039 ≤ 0.0000089; log83/571787 ≤ 0.0000077; log89/704969 ≤ 0.0000064; log97/912673 ≤ 0.0000050. Sum: 0.098858+0.042309+0.012978+0.005789+0.0018017+0.0011677+0.0005767+0.0004292+0.0002578+0.0001381+0.0001153+0.0000713+0.0000539+0.0000473+0.0000371+0.0000267+0.0000199+0.0000181+0.0000140+0.0000119+0.0000110+0.0000089+0.0000077+0.0000064+0.0000050 = 0.164617. Tail from 101: ∫_{100}^∞ log x/x³ dx = log100/(2·10000)+1/(4·10000) = 0.000230+0.000025 = 0.000255; plus the integral-vs-discrete: Σ_{m≥101} log m/m³ ≤ ∫_{100}^∞ ✓ (antitone from 100 ✓ since log x/x³ decreasing for x > e^{1/3} ✓). Total ≤ 0.164617+0.000255 = 0.164872 ≤ 0.165 ✓✓ (slack 0.000128 — tight but real).\n\n   So the Lean C_zeta3 proof needs: (a) the LSeries bound dirichletC3 := ∑'‖LSeries.term Λ 3 n‖ with ‖ζ′/ζ s‖ ≤ dirichletC3 for re ≥ 3 (clone of the dirichletC2 pattern); (b) dirichletC3 ≤ Σ_{m=2}^{100} Λ(m)/m³ + 0.000255... — the tail from 101 via the antitone-integral machine (LiTightR has AntitoneOn.tsum_comp_add_le_integral — the session-035 banked pattern) with ∫ log x/x³ = −(2log x+1)/(4x²); (c) the partial sum ≤ 0.1647 via 25 certified log bounds + rational arithmetic.\n\n   Effort estimate: (a) is a clone (~40 lines); (b) the tail ~80 lines (the integral machine + the antiderivative); (c) ~150 lines (25 log bounds à 3–4 lines + the sum assembly). Total ~270 lines. Feasible but chunky. \n\n   ALTERNATIVE (much cheaper!): charge C_zeta3 via dirichletC2 with a SPLIT that keeps it ≤ 0.165: ΣΛ(m)/m³ ≤ Σ_{m≤15} Λ(m)/m³ + (1/16)·Σ_{m≥16} Λ(m)/m². The second: Σ_{m≥16} Λ(m)/m² = dirichletC2 − Σ_{m=2}^{15} Λ(m)/m². dirichletC2 ≤ 0.57?? — WAIT, what is the CHARGED bound on dirichletC2 in Lean? dirichletC2 is DEFINED as the tsum; is there a Lean proof dirichletC2 ≤ 0.57? From D-071 §4.4: \"2^{−(2√n−2)}·0.57\" — the 0.57 appears in IIMaj's def (0.57 literal) — so somewhere there's a certified dirichletC2 ≤ 0.57? The E-021/E-023 world has |ζ′/ζ(2)| = 0.569960993. In Lean — the dirichletC2_le_one lemma (5f piece 1: dirichletC2 ≤ 1!). From session-035: \"piece 1 dirichletC2_le_one\". So Lean has dirichletC2 ≤ 1 (not 0.57). Hmm — so charging via dirichletC2 gives ≤ 1·(1/16)·... let me redo: ΣΛ(m)/m³ ≤ Σ_{m≤15}Λ(m)/m³ + (1/16)·dirichletC2 ≤ 0.16254 (partial, needs the certified logs for 2,3,5,7,11,13 — only SIX primes!) + (1/16)·1 = 0.16254+0.0625 = 0.225. Too big.\n   \n   Two-level split with the SAME idea: Σ_{m≤15}Λ/m³ + (1/16)Σ_{16≤m≤255}Λ/m² + (1/256)Σ_{m≥256}Λ/m² — the middle is ≤ (1/16)(dirichletC2 − partial²₁₅) — still needs dirichletC2 ≤ something-tight. With dirichletC2 ≤ 1: (1/16)(1−0.4493) = 0.0344; total 0.16254+0.0344+0.0039 = 0.2009. No.\n\n   The dirichletC2 ≤ 1 bound is too weak; the tight dirichletC2 ≤ 0.57 isn't in Lean. Hmm — actually is it? The IIMaj def uses 0.57 as a LITERAL — meaning when IIMaj was built, someone certified |ζ′/ζ| ≤ 0.57 somewhere? IIMaj's 0.57 comes from the paper's I_I analysis — was it ever Lean-proved that dirichletC2 ≤ 0.57? Probably not (IIMaj is a definition — the 0.57 is baked; the JUSTIFICATION would be needed in ii′-6-c for I_I! Note: the I_I bound in the eventual SfBoundProp proof needs |ζ′/ζ(2√n+it)| ≤ 2^{−(2√n−2)}·0.57 — that requires dirichletC2 ≤ 0.57 in Lean — NOT YET PROVED (it's inside the ii′-6-c workload). So certifying dirichletC2 ≤ 0.57 is ALREADY on the critical path for ii′-6-c/I_I. Hmm — and C_zeta3 = 0.165 could piggyback on the same machinery (dirichletC2 ≤ 0.57 via partial-sum + tail; then C_zeta3 via the m ≥ 8 split: partial(7) + (1/8)(dirichletC2 − log2/4 − log3/9 − log2/16·... wait Λ(4)/4² = log2/16 ✓): Σ_{m≥8}Λ/m³ ≤ (1/8)Σ_{m≥8}Λ/m²·... 1/m³ ≤ 1/(8m²) for m ≥ 8 ✓. Σ_{m≥8}Λ/m² = dirichletC2 − (log2/4+log3/9+log2/16+log5/25+log7/49) ≤ 0.57−(0.1733+0.1221+0.0433+0.0644+0.0397) = 0.57−0.4428 = 0.1272. C_zeta3 ≤ 0.15958+(1/8)(0.1272) = 0.15958+0.0159 = 0.1755 > 0.165. Extend split to m ≥ 16: partial(15) = 0.16254; (1/16)(0.57 − Σ_{m=2}^{15}Λ/m²): Σ_{m=2}^{15}Λ/m² = log2/4+log3/9+log2/16+log5/25+log7/49+log2/64+log3/81+log11/121+log13/169 = 0.17329+0.12207+0.04332+0.06438+0.03968+0.01083+0.01356+0.01982+0.01518 = 0.50213. (1/16)(0.57−0.50213) = (1/16)(0.06787) = 0.004242. Total: 0.16254+0.004242 = 0.16678 — still > 0.165!! Split at 32: partial(31): 0.16254+log17/4913+log19/6859+log23/12167+log29/24389+log31/29791+log2/16384(2^4·... Λ(16) = log2/4096 = 0.0001692; Λ(25) = log5/15625 = 0.0001030; Λ(27) = log3/19683 = 0.0000558; Λ(32) = log2/32768 = 0.0000212) = 0.16254+0.0005767+0.0004292+0.0002578+0.0001381+0.0001153+0.0001692+0.0001030+0.0000558+0.0000212 = 0.16421. (1/32)(0.57 − Σ_{2}^{31}Λ/m²): Σ_{2}^{31}Λ/m² ≈ 0.50213+0.0016677(17²=289: log17/289 = 0.009804)+log19/361 = 0.008157+log23/529 = 0.005928+log29/841 = 0.004004+log31/961 = 0.003574+log2/1024 = 0.000677+log5/625 = 0.002575+log3/729 = 0.001507+log2/4096 = 0.000169 = 0.50213+0.03650 = 0.53863. (1/32)(0.57−0.53863) = 0.000980. Total: 0.16421+0.00098 = 0.16519 > 0.165. STILL short by 0.00019 — because dirichletC2 ≤ 0.57 is itself 0.00004 above the true 0.56996 and the split-bound is lossy. ARGH.\n\n   OK so the dirichletC2-piggyback doesn't reach 0.165 either. The honest route is the direct dirichletC3 partial-sum + tail (the ~270-line build). OR — reconsider the CHARGED constant: does VLeftBound NEED 0.165? The charge feeds the fold: VLeftBound = ((√n+1)/2)·13.19·C — with C = 0.165 it's 1.088(√n+1). If we charge a LOOSER C, say 0.175 (reachable via the m ≥ 16 split with a tight-enough dirichletC2?) — 0.1755 above (still needs dirichletC2 ≤ 0.57, itself a partial-sum build at 2!). Or C = 0.18: partial(7)-style + (1/8)·(dirichletC2 − ...) with dirichletC2 ≤ 0.57: 0.15958+(1/8)(0.1272)·... = 0.1755 ≤ 0.18 ✓! So with dirichletC2 ≤ 0.57 in hand, C_zeta3 ≤ 0.1755 → charge 0.176: VLeftBound = ((√n+1)/2)·13.19·0.176 = 1.1607·(√n+1) — 6.7% bigger than the 0.165 version. Margin cost: the dog-leg charge grows by 2·0.073·(√n+1)/2·... ≈ +0.073√n — at n = 10⁵: +23; at N₁: +0.073·3e12·2/2 = +2.2e11 vs margin 2.458e26 — NEGLIGIBLE. So the fold is indifferent to C = 0.165 vs 0.176!\n\n   DECISION: charge C_zeta3 = 0.176 via the m ≥ 8 split, IF dirichletC2 ≤ 0.57 is cheap to get. But dirichletC2 ≤ 0.57 is itself a partial-sum build (ΣΛ(m)/m² ≤ 0.57: partial to ~40 + tail: partial(40) ≈ 0.53863+log37/1369 = 0.002637+log41/1681 = 0.002209+log43/1849 = 0.002035+log47/2209 = 0.001743+log2/256(16)… wait already counted 16: partial(48) ≈ 0.53863+0.002637+0.002209+0.002035+0.001743+log2/16384·… let me just: true 0.56996; tail from 48 ≈ ∫_{47}^∞ log x/x² = (log47+1)/47 = 0.06276 — too lossy; partial to ~200: true−~0.001 + tail (log200+1)/200 = 0.0315 — still lossy by 0.03!! The ∫ log x/x² tail is horribly lossy for the same reason. Hmm — so even dirichletC2 ≤ 0.57 needs care: Σ_{m≥K}Λ(m)/m² ≤ (log K+1)/K via ∫_{K}^∞ — at K = 200: 0.0315 — blows the 0.00004 budget. Need partial to ~2000 with the dyadic/integral tail (log K+1)/K·(1+o) — at K = 2000: 0.0043 — still too big vs 0.00004 slack!! IMPOSSIBLE to certify dirichletC2 ≤ 0.57 via these crude tails (the true value is 0.56996 — slack to 0.57 is 3.9e-5; the tail bound (log K+1)/K needs K ~ 2e5 to get under 4e-5 — 200,000-term partial sum in Lean?! NO).\n\n   WAIT — this means the I_I bound's 0.57 in IIMaj CANNOT be certified in Lean via partial sums either!! How was IIMaj's 0.57 justified?? IIMaj is a DEFINITION — its 0.57 comes from the paper analysis; the Lean SfBoundProp proof will need ‖ζ′/ζ(2√n+it)‖ ≤ 2^{−(2√n−2)}·0.57 — the 0.57 there is |ζ′/ζ(2+it)|'s sup — for the I_I proof the same certification problem arises. Hmm — but wait: dirichletC2 is DEFINED as the tsum; the I_I proof needs dirichletC2 ≤ 0.57?? OR it can use dirichletC2 DIRECTLY as the constant (IIMaj's 0.57 is just an upper bound used for the MARGIN — the margin needs Bn ≤ something with 0.57-certified... no wait — IIMaj is a defined majorant with the 0.57 literal; for the FOLD to prove |I_I| ≤ IIMaj, someone must show the true |I_I| ≤ IIMaj — that proof needs |ζ′/ζ| ≤ 2^{−(2√n−2)}·C with C = 0.57 certified... OR IIMaj could be REDEFINED with dirichletC2 as the constant... but the margin/convexity/base-point machinery uses the numeric 0.57...\n\n   Hmm — hold on. Let me reconsider: is dirichletC2 ≤ 0.57 really hard? The issue is only the TAIL. Better tail bounds exist: Σ_{m>K} Λ(m)/m² ≤ 2·(log K)/K·... no. Use a weighted comparison: Σ_{m>K} Λ(m)/m² ≤ Σ_{m>K} (log m)/m² ≤ ∫_{K−1}^∞ log x/x² dx·(antitone from K−1 ✓) = (log(K−1)+1)/(K−1). At K = 10⁴: 10.21/9999 = 0.001021 — still > 3.9e-5. K = 3e5: 13.6/3e5 = 4.5e-5 ≈ the slack — K ~ 4e5. NO.\n\n   Use the CHEBYSHEV/psixy bound: Σ_{m≤x} Λ(m) ≤ A·x with explicit A (e.g., A = 1.04 — the explicit Chebyshev: ψ(x) ≤ 1.04x for all x? There are elementary bounds ψ(x) ≤ 1.1x provable by hand (the binomial-coefficient method!). Then Σ_{m>K} Λ(m)/m² = ∫_K^∞ dψ/t² ≤ A·(log K + 1)/K·... via Abel summation: Σ_{m>K} Λ(m)/m² ≤ sup_{x≥K}(ψ(x)/x)·(1+o)·... ≈ A·(log K + 1)/K·... — same order. The (log K)/K decay is inherent to the Λ-weighted tail — can't beat it without PNT-strength input.\n\n   Hmm OK — so how does one certify dirichletC2 ≤ 0.57 in Lean feasibly? Answer: you DON'T need the true 0.57 — you need any certified constant that keeps the fold working. IIMaj's 0.57 is baked into Bn/margin machinery — changing it to a bigger certified C_I (e.g., 0.6 via partial(200)+tail(0.0315+... no still lossy). Partial(2000) in Lean: 2000-term sum — the terms are Λ-weighted rational logs... 2000 terms with ~50 distinct logs — the SUM in Lean is a Finset.sum of ℂ/rationals — computable by norm_num? 2000 terms is a LOT for norm_num (the denominators...). RationalRat-style: the sum Σ c_p log p ≤ Σ c_p·(certified log upper) — the assembly is linear in the log bounds ✓ same 25-ish log bounds + 2000 rational coefficients... the coefficient list c_p for p ≤ 2000 has 303 primes — 303 log bounds?! NO WAY.\n\n   RETHINK. The clean solution: bound the Λ-sum via a PRIME-FREE majorant: Λ(m) ≤ log m, and bound Σ_{m>K} log m/m² via the antitone-integral machine — (log K+1)/K — the SAME lossy tail. OR — charge the V_left zeta factor differently: don't bound |ζ′/ζ(3+it)| by a constant at all — use the dirichletC3 tsum as the constant ITSELF (define dirichletC3 := the tsum; VLeftBound(n) := ((√n+1)/2)·(e^{5/2}+1)·dirichletC3) and prove dirichletC3 ≤ 0.165 SEPARATELY for the fold/numerics... but Bn/margin need a RATIONAL constant (convexity ψ-analysis, base points) — dirichletC3 can't stay symbolic in the margin.\n\n   Hmm wait — actually, CAN it? The margin machinery needs the horizontal charge as explicit closed forms (for the ψ-blocks and base-point evaluations). VLeftBound ∝ √n with coefficient (13.19/2)·C_zeta3 — if C_zeta3 stays a named constant with a certified rational bound 0.165, the fold uses 0.165 — the certification must exist SOMEWHERE. The question is just the cheapest correct route.\n\n   CHEAPEST CORRECT ROUTE: the direct partial sum to K = 100 with the 25 certified log bounds (~150 lines) + the antitone-integral tail at 100 (0.000255, ~60 lines via the LiTightR machine). That's the ~270-line build I scoped. It's a day of Lean work at our session pace — acceptable, and it's reusable (the same pattern certifies dirichletC2 ≤ 0.57 IF the I_I proof needs it — partial(100) at 2: Σ_{m≤100}Λ/m² ≈ 0.5627? + tail (log100+1)/100 = 0.056 — NO: 0.5627+0.056 = 0.619 > 0.57 — the m² tail at 100 is 0.056 — 1400× the slack. So dirichletC2 ≤ 0.57 is INFEASIBLE by partial sums. The I_I proof will need a different route for its constant... — BUT WAIT: IIMaj's 0.57 is for |ζ′/ζ(2√n+it)| ≤ 2^{−(X_R−2)}·|ζ′/ζ(2)| — |ζ′/ζ(2)| = dirichletC2 = 0.56996 < 0.57. The fold needs 0.57 certified. If that's infeasible by partial sums, alternatives: (i) redefine IIMaj with 0.5700+X for a feasible X — same problem; (ii) certify dirichletC2 ≤ 0.6: partial(100) 0.5627+0.056 = 0.619 > 0.6; partial(500): true≈0.56996−~0.002+tail (log500+1)/500 = 0.0144: 0.568+0.0144 = 0.582 ≤ 0.6 ✓ — but partial(500) has 95 primes — 95 log bounds, no. (iii) Use a CHEBYSHEV-type tail: Σ_{m>K}Λ(m)/m² ≤ (A+ε)(log K)/K·... same (log K)/K shape. (iv) Abel-summation with the EXPLICIT ψ(x) ≤ 1.02x (provable?): Σ_{m>K} Λ(m)/m² = Σ (∫_m^∞ dt/t²)·... = ∫_K^∞ ψ(x)/x³·... dx ≤ A∫_K^∞ x/x³ = A/K = 1.02/100 = 0.0102 — better than 0.056 but still > 0.00004. Doesn't fix.\n\n   Hmm — so dirichletC2 ≤ 0.57 is genuinely painful. BUT — does the fold actually need it? Look at IIMaj's ROLE: I_I's contribution to Bn is IIMaj(n) = 2(√n+1)(e^{√n/2}+1)·0.57·2^{−(2√n−2)} — ASTRONOMICALLY small (2^{−2√n} dominates: at n = 8e4, 2^{−564}·e^{141}·... ≈ 2^{−564+203}·... = 2^{−361}·2900 ≈ 1e-105). The 0.57 could be 5.7 or 57 and IIMaj would STILL be negligible (57× more: 1e-103)! SO: the fold is utterly indifferent to the 0.57 — we can charge dirichletC2 ≤ 1 (ALREADY PROVED, session-035's dirichletC2_le_one!) and REDEFINE IIMaj's 0.57 → 1.0 or keep 0.57 with a comment... NO — the I_I proof will charge |ζ′/ζ| ≤ 2^{−(2√n−2)}·dirichletC2 ≤ 2^{−(2√n−2)}·1 — so IIMaj's honest constant is dirichletC2 ≤ 1. Redefine IIMaj with 1 instead of 0.57: IIMaj grows 1.75× — still ~1e-105 — margin impact ZERO (below all precisions). THAT's the cheap fix for I_I.\n\n   SAME IDEA FOR C_zeta3!! Charge C_zeta3 = 1 (via the m ≥ 2 comparison to dirichletC2 ≤ 1!): ΣΛ(m)/m³ ≤ ΣΛ(m)/(2m²)·... m ≥ 2: 1/m³ ≤ 1/(2m²) ⟺ m ≥ 2 ✓: ΣΛ(m)/m³ ≤ (1/2)·dirichletC2 ≤ (1/2)·1 = 0.5. C_zeta3 = 0.5 → VLeftBound = ((√n+1)/2)·13.19·0.5 = 3.2975·(√n+1) — 3× the 0.165 version. Margin impact: the dog-leg charge grows by 2·(3.2975−1.088)(√n+1) ≈ +4.42√n — at n = 8e4: +1250 vs margin 14,419 (8.7% — eats into it but survives: margin(8e4) → ~13,170); at 10⁵: +1400 vs 90,317 ✓; at N₁: +1.3e13 vs 2.458e26 ✓✓. The fold SURVIVES with C_zeta3 = 0.5 comfortably (base margins stay positive with huge slack — E-034's margin(8e4) would drop from 14,419 to ~13,170, still > 0 ✓ and hbase2: 13,170 < 90,317−1400·... ✓ fine).\n\n   Hmm — but wait, the directive says \"Create a rational certified constant C_zeta4 such that −ζ′(4)/ζ(4) ≤ C_zeta4\" and \"DO NOT bake 1.1 into the formal proof until interval/rational certification is completed\" — the SPIRIT is a certified constant; 0.5 via (1/2)·dirichletC2 ≤ 0.5 IS a certified rational constant (with dirichletC2 ≤ 1 already in Lean). The cost is a slightly bigger VLeftBound. BUT it changes the E-034 fold numbers — I should re-run the fold model with C = 0.5 to confirm margins (quick — modify E-034's C_ZETA3 and re-run the fold part; or compute by hand: margin(8e4): Bn += 2·(3.2975−1.088)(√8e4+1)/1 ≈ 2·2.2095·283.84 = 1254: 14419−1254 = 13,165 ✓; margin(10⁵): 2·2.2095·317.23 = 1402: 90317−1402 = 88,915 ✓; margin(N₁): fine).\n\n   Better middle ground: C_zeta3 = 0.34 via m ≥ 3 split: ΣΛ/m³ ≤ Λ(2)/8 + (1/3)Σ_{m≥3}Λ/m²·... 1/m³ ≤ 1/(3m²) for m ≥ 3 ✓: = log2/8 + (1/3)(dirichletC2 − log2/4) ≤ 0.0866+(1/3)(1−0.1733) = 0.0866+0.2756 = 0.3622. Hmm 0.3622 — worse than 0.5·... no wait 0.3622 < 0.5 ✓ better! Even better m ≥ 4 split: log2/8+log3/27 + (1/4)(1−0.1733−0.1221) = 0.12733+0.17615 = 0.3035. m ≥ 8: +log2/64+log5/125+log7/343 + (1/8)(1−0.4428) = 0.15958+0.06965 = 0.2292 ✓ better still. m ≥ 16: partial(15) 0.16254 + (1/16)(1−0.50213) = 0.16254+0.03110 = 0.1936. m ≥ 32: 0.16421+(1/32)(1−0.53863) = 0.16421+0.01442 = 0.1786. m ≥ 64: partial(63): +log37/50653+log41/68921+log43/79507+log47/103823+log53/148877+log59/205379+log61/226981+log2/262144+... ≈ 0.16421+0.00045 = 0.16466; (1/64)(1−0.55) = 0.00703: total 0.1717. The partial sums need the log bounds for primes up to the split point only — m ≥ 16 split needs logs of 2,3,5,7,11,13 (SIX primes, all cheap: log_two (d9), log 3,5,7,11,13 via exp comparisons ~3 lines each) → C_zeta3 = 0.1936 → charge 0.194: VLeftBound = ((√n+1)/2)·13.19·0.194 = 1.2797·(√n+1). Cost vs 0.165: +0.19√n per side → +0.38√n total: at 8e4: +108; margin(8e4) → 14,311 ✓; at 10⁵: +121 → 90,196 ✓. NEGLIGIBLE cost, and the certification needs only SIX log bounds + dirichletC2 ≤ 1 + the m ≥ 16 comparison. \n\n   EVEN BETTER: I realize the m ≥ 16 split has a subtlety: Σ_{m≥16} Λ(m)/m³ ≤ (1/16)·Σ_{m≥16} Λ(m)/m²·... uses 1/m³ ≤ 1/(16m²) for m ≥ 16 ✓. And Σ_{m≥16}Λ/m² ≤ dirichletC2 − Σ_{m=2}^{15}Λ/m² — needs LOWER bounds on the dropped partial sum (log₂/4 + ... ≥ 0.50213 certified — needs the six logs LOWER-bounded (the d9 lower bounds exist for log 2; for 3,5,7,11,13 need lower bounds too — or simpler: drop the subtraction: Σ_{m≥16}Λ/m² ≤ dirichletC2 ≤ 1 directly: then C_zeta3 ≤ 0.16254 + (1/16)·1 = 0.16254+0.0625 = 0.2250 → charge 0.225: VLeftBound = ((√n+1)/2)·13.19·0.225 = 1.4835·(√n+1). Cost vs 0.194: +0.20√n/side — similar scale. But the SUBTRACTED version (0.194) needs lower bounds on the six logs — the exp-machine gives both directions cheaply (e^{bound} ≥ p for upper, e^{bound} ≤ p via lower partial sums for lower — session-012 did both). The effort difference is small; take the 0.194 version? Or simplest-first: take C_zeta3 = 0.225 (NO log lower bounds, only the partial UPPER sum Σ_{m≤15}Λ/m³ ≤ 0.16254-certified... wait the partial upper sum needs the six log UPPER bounds only ✓).\n\n   Hmm, actually — hold on, let me reconsider the effort/feasibility of the FULL honest 0.165 once more. The partial(100) needs 25 prime logs. Each log p ≤ bound: `have : Real.log p ≤ B := by rw [Real.log_le_iff_le_exp (by norm_num)]; exact le_trans (by norm_num) (exp_lower_bound...)` hmm the route: log p ≤ B ⟺ p ≤ e^B ⟸ (p:ℝ) ≤ Σ₀ᴷ Bⁱ/i! ≤ e^B: Real.sum_le_exp_of_nonneg gives Σ ≤ exp; need (p:ℝ) ≤ Σ — a rational inequality checkable by norm_num [Finset.sum_range_succ] with K ~ 7–10 per prime (bigger p needs bigger K). 25 × ~4 lines = 100 lines. The sum assembly: Σ_{m≤100}Λ/m³ = Σ c_p·log p (grouping by prime) ≤ Σ c_p·B_p — the GROUPING itself (proving the finite sum equals the c_p-weighted form) is the painful part in Lean (Finset manipulations over 100 terms with the vonMangoldt values — vonMangoldt m is defined via the Möbius convolution — evaluating Λ(12) = log 2 in Lean requires... `ArithmeticFunction.vonMangoldt` computes via μ ⋆ log — norm_num can't evaluate it symbolically (Real.log). We'd need lemmas Λ(p^k) = log p (Mathlib: vonMangoldt_prime_pow?) and the sum split — each Λ(m) value needs a little proof. 100 little proofs?! NO.\n\n   So the m ≥ 16 split (six primes) is the sweet spot: Σ_{m=2}^{15} Λ(m)/m³ — the m values 2..15: Λ nonzero at 2,3,4,5,7,8,9,11,13 — NINE terms, each Λ value: log 2 (×3: m=2,4,8), log 3 (×2: 3,9), log 5, log 7, log 11, log 13 — the vonMangoldt evaluations: Mathlib has vonMangoldt_prime (Λ(p) = log p) and vonMangoldt_prime_pow (Λ(p^k) = log p) and the zero cases (Λ(6) = 0, Λ(10) = 0, Λ(12) = 0, Λ(14) = 0, Λ(15) = 0 — non-prime-powers: Mathlib vonMangoldt_eq_zero_iff?). Feasible: ~9 little evaluations + six log bounds + the comparison + dirichletC2 ≤ 1 + subtraction. TOTAL ~80–120 lines. C_zeta3 = 0.194 charged (or 0.225 without subtraction — the subtraction needs 6 LOWER log bounds: Σ_{2}^{15}Λ/m² ≥ 0.50213: with lower bounds the total is 0.16254+(1−0.50213)/16 = 0.19364 → charge 0.194; without subtraction (Σ_{m≥16}Λ/m² ≤ dirichletC2 ≤ 1): 0.2250 → charge 0.225).\n\n   DECISION: go with C_zeta3 = 0.194 (subtracted, six primes both directions) — the extra cost is the six lower bounds (same machinery, ~20 more lines) and it shaves VLeftBound from 1.4835 to 1.2797. Actually — you know what, let me check the margin sensitivity to decide if the 0.194 vs 0.225 matters: ΔVLeftBound per side = (1.4835−1.2797)(√n+1) = 0.2038(√n+1); total ΔBn ≈ 0.41√n: at 8e4: 116; at 10⁵: 129; at N₁: 1.2e12 — all negligible vs margins (14k/90k/2.5e26). The fold is INDIFFERENT. So take the SIMPLEST: C_zeta3 = 0.225 (no subtraction, six upper log bounds only). Hmm — but \"0.225\" vs the true 0.1648 (37% fat) vs 0.194 (18% fat)... the directive cares about certified constants, not tightness. E-034's VLeftBound was computed with 0.165 — the fold numbers there used 1.088·(√n+1). With 0.225 the VLeftBound is 1.4835(√n+1) — the fold margins change slightly (recompute: margin(8e4): Bn += 2·(1.4835−1.088)·283.84·... wait — E-034's DogLegRight used C = 0.165: VLeft = 1.0884(√n+1). With C = 0.225: VLeft = 1.48347(√n+1): ΔVLeft = 0.3951(√n+1) per side: ΔBn = 0.7902(√n+1): margin(8e4): 14419 − 0.7902·283.84 = 14419−224 = 14,195; margin(10⁵): 90317−251 = 90,066; margin(N₁): 2.458e26−2.4e12 ≈ same. All fine ✓.\n\n   Hmm — but the purist in me: the directive's E-034 gate was run with C = 0.165 — the Lean charge 0.225 deviates from the validated fold. The honest thing: re-run the E-034 fold with the Lean-charged C before finalizing DL-2 (cheap — one script tweak + rerun of the fold portion). I'll do that as part of DL-2's validation (update E-034's C_ZETA3 to the Lean-charged value... or better: parameterize E-034's fold at C = 0.225 and record the margins).\n\n   Actually — WAIT. Let me reconsider using dirichletC3 as the direct constant with a bound via the SAME six-prime partial + tail-at-16-with-INTEGRAL: Σ_{m≥16} log m/m³ ≤ log16/4096 + ∫_{16}^∞ log x/x³ = 0.000677+0.006389 = 0.00707 — partial(15) = 0.16254: total 0.16961 → charge 0.17!! VLeftBound = ((√n+1)/2)·13.19·0.17 = 1.1212(√n+1) — only 3% above the E-034 value! The tail-at-16 via the antitone-integral machine (∫log x/x³ = −(2log x+1)/(4x²)) — the LiTightR machine exists (AntitoneOn.tsum_comp_add_le_integral) and the antiderivative is elementary (hasDerivAt: d/dx[−(2log x+1)/(4x²)] = log x/x³ ✓ verifiable). The sum Σ_{m≥16} log m/m³ ≤ log16/4096·... hmm the machine: Σ_{m≥K} f(m) ≤ f(K)+∫_K^∞ f for antitone f: f(x) = log x/x³ antitone for x > e^{1/3} ✓ 16 ✓. So C_zeta3 ≤ Σ_{m=2}^{15}Λ/m³ + Σ_{m≥16}(log m)/m³ ≤ 0.16254 + 0.00707 = 0.16961 → charge 0.17. The Λ ≤ log comparison is free. The partial(15) needs the six prime log UPPER bounds + the nine Λ-evaluations ✓ same as before. The tail needs the integral machine (~40 lines). C_zeta3 = 0.17 — nearly the E-034 constant (0.165) and simpler than 0.194's subtraction. \n\n   Even better: the m ≥ 16 tail bound Σ_{m≥16} log m/m³: actually the Λ-sum Σ_{m≥16}Λ(m)/m³ ≤ Σ_{m≥16}(log m)/m³ ✓ (Λ(m) ≤ log m — Mathlib: vonMangoldt_le_log? there should be — Λ(m) = log p ≤ log m for m = p^k ✓; Mathlib: ArithmeticFunction.vonMangoldt_le_log or applyBound — check). \n\n   FINAL DECISION for DL-2: C_zeta3 := 0.17 charged, via:\n   (a) dirichletC3 := ∑'‖LSeries.term Λ 3 n‖ + the bound ‖logDeriv ζ s‖ ≤ dirichletC3 for 3 ≤ re s (clone of norm_logDeriv_zeta_le_dirichlet at 2 — check its proof to clone);\n   (b) dirichletC3 ≤ Σ_{m=2}^{15} Λ(m)/m³ + Σ_{m≥16} (log m)/m³ — the tsum split (tsum_split_finset or the fiber machine — LiCircleBound has tsum_split_finset ✓);\n   (c) Σ_{m=2}^{15}Λ(m)/m³ ≤ 0.16255 certified (six prime logs + nine Λ-evaluations);\n   (d) Σ_{m≥16}(log m)/m³ ≤ 0.00707 (antitone-integral machine);\n   (e) dirichletC3 ≤ 0.17 ⟹ VLeft zeta factor ≤ 0.17.\n\n   Hmm — wait, actually for (b): dirichletC3 = ∑'‖LSeries.term Λ 3 n‖ = Σ_{m≥2}Λ(m)/m³ (the LSeries term at 3 is Λ(m)/m^3 in norm — need the identification: ‖LSeries.term Λ 3 m‖ = Λ(m)/m³ for m ≥ 2, and the m = 0,1 terms are 0 (Λ(1) = 0, term at 0 = 0) ✓. The split: tsum = Σ_{m=2}^{15} + Σ_{m≥16} ✓.\n\n   This is still a chunky build (~150-250 lines). Acceptable for DL-2? The sub-stage map says DL-2 = left vertical lift bound. Let me scope DL-2 fully:\n   (i) kernel lemma ‖kFun n (3+it)‖ ≤ e^{5/2}+1 for t² ≥ n (~40 lines, clone LiContour patterns).\n   (ii) dirichletC3 + the split + certified 0.17 (~200 lines).\n   (iii) the VIntegral bound assembly: ‖VIntegral (Jlag n) 3 T U‖ ≤ (U−T)·(e^{5/2}+1)·0.17 for T² ≥ n, 0 < T ≤ U (interval-integral norm bound: ‖∫_a^b f‖ ≤ ∫_a^b‖f‖ ≤ (b−a)·sup — the intervalIntegral.norm_integral_le_of_norm_le_const or similar; the product bound ‖kFun‖·‖ζ′/ζ‖ ≤ (e^{5/2}+1)·0.17 ✓; plus the VIntegral's I• factor: ‖I • x‖ = ‖x‖ ✓). (~50 lines)\n   (iv) the (U−T) = T_cut/2 ≤ (√n+1)/2 accounting — at the DL-5 assembly (not here).\n   \n   Let me check norm_logDeriv_zeta_le_dirichlet's proof to clone (LiCircleBound ~203-230) before writing. Also check Mathlib's vonMangoldt_le_log and vonMangoldt prime/pow evaluations.\n\nAlso — the e^{5/2}+1 kernel lemma: look at how kFun_shift_norm_le_exp_four_add_one was proved (the normSq core norm_one_add_one_div_le) to clone for the 3+it case.\n\nLet me read the LiContour kernel lemma proof and the dirichlet lemma.","signature":""},{"type":"text","text":"DL-1 committed (`4c36802`). Now DL-2. Key scoping insight first: the fold is indifferent to C_zeta3's exact value, so I'll charge **0.17** (six-prime partial sum + antitone-integral tail — avoids an infeasible 25-prime certification). Reading the two patterns to clone: the LiContour kernel proof and the dirichlet bound."},{"type":"tool_use","id":"Read_197","name":"Read","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiContour.lean","offset":449,"limit":105},"extra_content":null}]