[{"type":"thinking","thinking":"I was computing the bracket bound's decay for the 2·IIMaj convexity option. The key decision: how to handle the IIMaj coefficient in Bn (I_I + dog-leg's V_right) for the convexity proof.\n\nThe cleanest resolution: charge V_right ≤ IIMaj/4 via a DIRECT dirichlet-series bound at re = 2√n (log2-leading + 3^{−(2√n−2)} tail with dirichletC2 ≤ 1), which gives dog-leg total = I_I + 2·(IIMaj/4) = 1.5·IIMaj — and the convexity works with the existing 4/3-bracket (1.5·(4/3)/(4n) = 1/(2n) strictly ✓).\n\nSo the plan for ii′-6-a2 (small pieces):\n1. **DL-6 (small Lean build, ~100-150 lines)**: the direct I_I/V_right zeta bound — dirichletCX-style: ‖ζ′/ζ(2√n+it)‖ ≤ (log2 + 9·(4/9)^{√n})·2^{−2√n} ≤ 2.28·2^{−2√n} = 0.57·2^{−(2√n−2)} for n ≥ 5. Then:\n   - V_right re-charge: V_right ≤ ((√n+1)/2)·(e^{√n/2}+1)·0.57·2^{−(2√n−2)}·(1/1)?? — hmm — let me recompute. The V_right provable bound with the direct zeta: ‖V_right‖ ≤ (U−T)·(e^{√n/2}+1)·‖ζ′/ζ(2√n+it)‖ ≤ ((√n+1)/2)·(e^{√n/2}+1)·(0.6931+9(4/9)^{√n})·2^{−2√n} — and IIMaj/4 = (1/4)·2(√n+1)(e+1)·0.57·2^{−(2√n−2)} = ((√n+1)/2)(e+1)·0.57·2^{−(2√n−2)} = ((√n+1)/2)(e+1)·2.28·2^{−2√n}. And the direct gives ((√n+1)/2)(e+1)·(0.6931+9(4/9)^{√n})·2^{−2√n} ≤ ((√n+1)/2)(e+1)·2.28·2^{−2√n} ⟺ 0.6931+9(4/9)^{√n} ≤ 2.28 ✓ (n ≥ 5 ✓). So V_right ≤ IIMaj/4 ✓ via the direct bound.\n2. But wait — DL-5's hVr2 already charged V_right ≤ IIMaj/2 (provable with dirichletC2 ≤ 1 via the (6.10) route — that gives dog-leg total 2·IIMaj in Bn, breaking convexity). To keep 1.5·IIMaj, I need to UPGRADE hVr2 to IIMaj/4 via the direct route — OR add a new lemma `vIntegral_Jlag_right_norm_le_quarter` (V_right ≤ IIMaj/4 via the direct bound) and use THAT in the Bn's dog-leg charge (overriding DL-5's IIMaj/2 for the fold).\n\nActually — simpler: build the direct bound as a small DL-6, then a new capstone `vIntegral_Jlag_right_norm_le_quarter` proving ‖VIntegral (Jlag n) (2√n) T U‖ ≤ (U−T)·(e^{√n/2}+1)·(0.57·2^{−(2√n−2)}) = (U−T)·(IIMaj's per-length form) — and then V_right ≤ ((√n+1)/2)·(that) = IIMaj/4. The fold uses IIMaj/4.\n\nThen the dog-leg total: 2·(VLeft + 8.38 + IIMaj/4) + I_I = 2·VLeft + 16.76 + IIMaj/2 + IIMaj = 2·VLeft + 16.76 + 1.5·IIMaj ✓ convexity works with the 4/3-bracket (1.5·IIMaj″ < 1.5·(4/3)/(4n) = 2/(4n) = 1/(2n) strict ✓✓).\n\nSo the pieces:\n- **DL-6** (the direct dirichlet bound at 2√n + the V_right quarter re-charge). THEN ii′-6-a2's Bn charge uses DogLegRight = VLeft + 8.38 + IIMaj/4.\n\nLet me plan DL-6 carefully:\n\n**DL-6-i: the direct zeta bound at 2√n.**\n\n```\ndef dirichletCX (n : ℕ) : ℝ :=\n  ∑' m : ℕ, ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (2 * Real.sqrt n : ℂ) m‖\n```\n\nHmm — the cast: (2·√n : ℝ) : ℂ. And norm_logDeriv_zeta_le_dirichletCX {n : ℕ} {t : ℝ} : ‖logDeriv ζ (2√n+it)‖ ≤ dirichletCX n — the clone (same LSeries machinery, needs 1 < (2√n+it).re = 2√n for the LSeries identity — √n ≥ ... n ≥ 5 gives 2√n ≥ 4.47 > 1 ✓).\n\nThe split: dirichletCX n = Λ(2)/2^{2√n} + Σ_{m≥3}Λ(m)/m^{2√n}. The tail ≤ 3^{−(2√n−2)}·dirichletC2.\n\nTermwise: for m ≥ 3: ‖term Λ (2√n) m‖ = Λ(m)/m^{2√n} = Λ(m)/(m²·m^{2√n−2}) ≤ Λ(m)/(m²·3^{2√n−2}) = 3^{−(2√n−2)}·‖term Λ 2 m‖ — the m^{2√n−2} ≥ 3^{2√n−2} via rpow_le_rpow (3 ≤ m, exponent 2√n−2 ≥ 0 for n ≥ 1 ✓ — need 2√n ≥ 2 ⟺ n ≥ 1 ✓).\n\nHmm wait — actually, the exponent on m: the term at (2√n : ℂ) has n ^ s.re = m^{2√n} (rpow with real exponent 2√n) — and I want to compare with 3^{2√n−2}: m^{2√n} = m²·m^{2√n−2} (rpow_add: 2√n = 2 + (2√n−2) ✓ exponent arithmetic ✓) — and m^{2√n−2} ≥ 3^{2√n−2} for m ≥ 3 (Real.rpow_le_rpow: 0 ≤ 3 ≤ m, 0 ≤ 2√n−2 ✓ need 2√n ≥ 2 ⟺ n ≥ 1 ✓).\n\nAnd Σ_{m≥3} ≤ 3^{−(2√n−2)}·Σ_{m≥3}‖term Λ 2 m‖ ≤ 3^{−(2√n−2)}·dirichletC2 ≤ 3^{−(2√n−2)}·1.\n\nThe m ∈ {0,1,2} part: tsum_split_finset with s = {0,1,2}: the finset sum = term(0) + term(1) + term(2) = 0 + 0 + Λ(2)/(2^{2√n}) — term(0) = 0 (LSeries term at 0), term(1) = Λ(1)/1 = 0 (vonMangoldt_apply_one) ✓ term(2) = Λ(2)/2^{2√n} = log 2·2^{−2√n} ✓ (norm: ‖Λ(2)/2^{2√n}‖ = Λ(2)/2^{2√n} with Λ(2) = log 2 ≥ 0 ✓).\n\nThen: dirichletCX n ≤ log2·2^{−2√n} + 3^{−(2√n−2)} — and ≤ 0.57·2^{−(2√n−2)}:\nlog2·2^{−2√n} + 3^{−(2√n−2)} ≤ 0.57·2^{−(2√n−2)} = 0.57·4·2^{−2√n} = 2.28·2^{−2√n}\n⟺ log2·2^{−2√n} + 3^{−(2√n−2)} ≤ 2.28·2^{−2√n}\n⟺ log2 + 3^{−(2√n−2)}·2^{2√n} ≤ 2.28\n⟺ log2 + 9·(2²/3²)^{√n}·... = log2 + 9·(4/9)^{√n} ≤ 2.28\n⟸ 9·(4/9)^{√n} ≤ 2.28 − 0.6932 = 1.5868\n⟸ (4/9)^{√n} ≤ 0.17631.\n\nFor n ≥ 5: √n ≥ √5 ≥ 2.236: (4/9)^{√n} ≤ (4/9)^{2.236}: (4/9)^{2.236} = e^{2.236·log(4/9)} = e^{−1.8134} ≤ 0.17631 ⟺ e^{1.8134} ≥ 1/0.17631 = 5.672: e^{1.8134} ≥ Σ₀⁶(1.8134^i/i!) = 1+1.8134+1.6443+0.9942+0.4508+0.1635+0.0494 = 6.1156 ≥ 5.672 ✓ — certified by partial sums ✓ (norm_num-able? 1.8134^i/i! rationals ✓ ~6 terms ✓).\n\nHmm — cleaner: (4/9)^{√n} for √n ≥ 2.236: (4/9)^{√n} = e^{√n·log(4/9)}: log(4/9) = 2log2 − log9 = 2·0.6931 − 2.1972 = −0.8110. So (4/9)^{√n} ≤ e^{−0.8110·2.236} = e^{−1.8134}. Certified: e^{1.8134} ≥ 5.672 ⟹ e^{−1.8134} ≤ 1/5.672 = 0.17631 ✓✓.\n\nSo DL-6-i's capstone:\n```\ntheorem norm_logDeriv_zeta_le_iimZeta {n : ℕ} (hn : 5 ≤ n) {t : ℝ} :\n    ‖logDeriv riemannZeta (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ ≤\n      (0.57 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) := ...\n```\n(0.57·2^{−(2√n−2)} = 2.28·2^{−2√n} ✓ the IIMaj zeta form.)\n\n**DL-6-ii: the V_right quarter charge.**\n```\ntheorem vIntegral_Jlag_right_norm_le_quarter {n : ℕ} {T U : ℝ}\n    (hn : 16 ≤ n) (hT0 : (0 : ℝ) < T) (hTU : T ≤ U) (hTn : (n : ℝ) ≤ T ^ 2) :\n    ‖VIntegral (Jlag n) (2 * Real.sqrt (n : ℝ)) T U‖ ≤\n      (U - T) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *\n        ((0.57 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2))) := by\n```\n— same structure as vIntegral_Jlag_right_norm_le but with the direct zeta bound (0.57·2^{−(2√n−2)}) instead of 2^{−(2√n−2)}·dirichletC2. Then with U−T ≤ (√n+1)/2: V_right ≤ ((√n+1)/2)(e+1)·0.57·2^{−(2√n−2)} = IIMaj/4 ✓ (IIMaj/4 = (1/4)·2(√n+1)(e+1)·0.57·2^{−X} = ((√n+1)/2)(e+1)·0.57·2^{−X} ✓ EXACT).\n\nSo the fold's DogLegRight := VLeft + 8.38 + IIMaj/4, and Bn's IIMaj coefficient = 1 (I_I) + 2·(1/4) = 1.5 ✓.\n\nHmm wait — but DL-5's hVr2 charged IIMaj/2 — the dogLegUpper lemmas use IIMaj/2. For the fold I want the IIMaj/4 version. Two options:\n(A) Upgrade DL-5's dogLegUpper to use IIMaj/4 (edit hVr2's charge → IIMaj/4 via DL-6-ii). DL-5's lemmas then state dogLegUpper = VLeft + 8.38 + IIMaj/4 ✓ cleaner for ii′-6-c's direct use.\n(B) Keep DL-5 as-is (IIMaj/2) and add the quarter version separately for the fold.\n\n(A) is cleaner — edit DL-5's hVr2 to use the quarter bound (after DL-6-ii exists). The E-034 fold's VRightBound should then go back to IIMaj/4 (it was IIMaj/2 for the DL-4 charge — update to IIMaj/4 with the direct-route note, re-run).\n\nAnd Bn's IIMaj coefficient becomes 1 (I_I) + 2·(1/4) = 1.5 ✓ convexity works with the EXISTING 4/3-bracket — but the 4/3-bracket strengthening is on the PAUSED branch (wip/c-1.5-margin-redo)! Master's iimaj_bracket_bound is < 2. For 1.5·IIMaj″ < 1/(2n) I need IIMaj″ < 1/(3n) (bracket < 4/3). So I need to cherry-pick JUST the bracket strengthening (< 2 → < 4/3) + IIMaj_deriv2_lt_three onto master — those are independent of the c = 1.5 k-shift work (the bracket strengthening is a one-line constant change + the lt_three lemma ~15 lines).\n\nWait — actually for 1.5·IIMaj″ < 1/(2n) STRICT: 1.5·bracket/(4n) < 1/(2n) ⟸ bracket < 4/3 ✓ (1.5·(4/3)/(4n) = 2/(4n) = 1/(2n) — and the bracket bound is STRICT < 4/3 ⟹ 1.5·IIMaj″ < 1.5·(4/3)/(4n) = 1/(2n) ✓ STRICT ✓ — the final linarith: margiñ″ ≥ 1/(2n) + nonnegs − 1.5·IIMaj″ ≥ 1/(2n) − 1.5·IIMaj″ > 0? — hmm: 1/(2n) − 1.5·IIMaj″ > 1/(2n) − 1/(2n) = 0 ⟸ 1.5·IIMaj″ < 1/(2n) ✓ STRICT ✓ works.\n\nSo the ii′-6-a2 plan (small pieces):\n1. DL-6-i: the direct zeta bound (dirichletCX split + tail + assembly ≤ 0.57·2^{−(2√n−2)}).\n2. DL-6-ii: vIntegral_Jlag_right_norm_le_quarter (V_right ≤ (U−T)·(e+1)·0.57·2^{−(2√n−2)}).\n3. DL-5 upgrade: hVr2 charge → IIMaj/4 via DL-6-ii; dogLegUpper → VLeft + 8.38 + IIMaj/4.\n4. Cherry-pick bracket < 4/3 + IIMaj_deriv2_lt_three onto master (independent lemmas).\n5. ii′-6-a2 proper: Bn redefinition (DogLegRight = ((√n+1)/2)(e^{5/2}+1)/2 + 8.38 + IIMaj/4) + margin lockstep + convexity re-proof + base points + endpoint + audit.\n6. E-034 re-validation at VRightBound = IIMaj/4.\n\nHmm — also for step 5's Bn: the I_I piece in the FOLD — does the fold's Bn need I_I ≤ IIMaj proved via the direct route? Yes — in ii′-6-c, the I_I side bound will use DL-6-i's norm_logDeriv_zeta_le_iimZeta (≤ 0.57·2^{−(2√n−2)}) + the kernel e^{√n/2}+1 + length 2T = 2(√n+1): |I_I| ≤ 2(√n+1)(e+1)·0.57·2^{−(2√n−2)} = IIMaj ✓ — provable ✓.\n\nOK — let me start DL-6-i. The dirichletCX definition + split + tail + capstone. Key subtleties:\n- The LSeries point: ((2·√n : ℝ) : ℂ) with .re = 2√n ✓.\n- norm_logDeriv_zeta_le_dirichletCX: clone of the dirichletC3 clone (with (2√n : ℂ) and re = 2√n > 1 for n ≥ 1).\n- The split: tsum_split_finset (LiCircleBound has it) with s = {0,1,2} — hmm — tsum_split_finset (hf : Summable f) (s : Finset ι) : ∑' f = ∑_{i ∈ s} f i + ∑' (if i ∈ s then 0 else f i) ✓ — the tail part ∑' (if i ∈ {0,1,2} then 0 else f i) = ∑'_{m ≥ 3} f(m)-ish (need the reindex: ∑'_{m≥3} f = ∑' if-zeroed ✓ via tsum_subtype or just bound the if-zeroed tail directly).\n- The tail bound: ∑' (if i ∈ {0,1,2} then 0 else ‖term Λ (2√n) i‖) ≤ 3^{−(2√n−2)}·dirichletC2 — termwise: for i ∉ {0,1,2} (i ≥ 3): ‖term Λ (2√n) i‖ ≤ 3^{−(2√n−2)}·‖term Λ 2 i‖ ✓ the comparison; for i ∈ {0,1,2}: 0 ≤ anything ✓. Then Summable.tsum_le_tsum termwise hsum-tail hsumC2-scaled + tsum_mul_left.\n\nLet me also double-check the term comparison for the tail: ‖term Λ (2√n) m‖ ≤ 3^{−(2√n−2)}·‖term Λ 2 m‖ for m ≥ 3:\n‖term Λ (2√n) m‖ = Λ(m)/m^{2√n} (rpow, m ≥ 1) — and 3^{−(2√n−2)}·Λ(m)/m² — so need Λ(m)/m^{2√n} ≤ 3^{−(2√n−2)}·Λ(m)/m² ⟺ m²/m^{2√n} ≤ 3^{−(2√n−2)} ⟺ m^{2√n−2} ≥ 3^{2√n−2} ✓ (rpow_le_rpow: 0 ≤ 3 ≤ m, 0 ≤ 2√n−2 (n ≥ 1) ✓).\n\nThe m = 2 term: ‖term Λ (2√n) 2‖ = Λ(2)/2^{2√n} = log2·2^{−2√n} — hmm — need vonMangoldt at 2 = log 2: Mathlib: `ArithmeticFunction.vonMangoldt_prime (hp : p.Prime) : Λ p = Real.log p` ✓ — Nat.prime_two ✓.\n\nNow write DL-6-i (~150 lines).","signature":""},{"type":"text","text":"Resuming with the key decision resolved: charge V_right at **IIMaj/4** via a direct dirichlet-series bound at re = 2√n (log2-leading + 3^{−(2√n−2)} tail with dirichletC2 ≤ 1 — no 95-prime build needed), giving the convexity-safe 1.5·IIMaj total. Building **DL-6-i** (the direct zeta bound)."},{"type":"tool_use","id":"TodoWrite_417","name":"TodoWrite","input":{"todos":[{"content":"DL-6-i: dirichletCX split + tail + capstone norm_logDeriv_zeta_le_iimZeta (≤ 0.57·2^{−(2√n−2)}, n ≥ 5)","status":"in_progress","activeForm":"Building the direct zeta bound at 2√n"},{"content":"DL-6-ii: vIntegral_Jlag_right_norm_le_quarter (V_right ≤ (U−T)·(e+1)·0.57·2^{−(2√n−2)} = IIMaj/4-charge)","status":"pending","activeForm":"Re-charging V_right at IIMaj/4"},{"content":"DL-5 upgrade: hVr2 → IIMaj/4 via DL-6-ii; dogLegUpper → VLeft + 8.38 + IIMaj/4; E-034 re-validation at IIMaj/4","status":"pending","activeForm":"Upgrading DL-5 to the quarter charge"},{"content":"Cherry-pick bracket < 4/3 + IIMaj_deriv2_lt_three onto master (from wip branch, k-shift excluded)","status":"pending","activeForm":"Cherry-picking the bracket strengthening"},{"content":"ii′-6-a2: Bn dog-leg redefinition + margin lockstep + convexity re-proof + base points + audit + commit","status":"pending","activeForm":"Executing the Bn redefinition"}]},"extra_content":null},{"type":"tool_use","id":"Edit_418","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDogLeg.lean","old_string":"end NguyenRH1\n\nend","new_string":"/-! ## 8. The direct Dirichlet bound at re = 2√n (DL-6) — the I_I /\nV_right zeta factor WITHOUT certifying dirichletC2 ≤ 0.57.\n\nThe I_I charge in IIMaj is 0.57·2^{−(2√n−2)} = 2.28·2^{−2√n} (the\n(6.10)-route constant |ζ′/ζ(2)|). Proving dirichletC2 ≤ 0.57 directly\nneeds a ~100-prime partial-sum build (the antitone-integral tail is too\nfat). AVOIDED here: the DIRECT Dirichlet-series bound at re = 2√n gives\nlog2-leading + a 3^{−(2√n−2)} tail (dirichletC2 ≤ 1), which is ≤\n0.57·2^{−(2√n−2)} for n ≥ 5 — the IIMaj charge exactly. -/\n\n/-- The Dirichlet majorant at s = 2√n (summable since 2√n > 1). -/\ndef dirichletCX (n : ℕ) : ℝ :=\n  ∑' m : ℕ, ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ))\n    ((2 * Real.sqrt (n : ℝ) : ℝ) : ℂ) m‖\n\n/-- ‖ζ′/ζ(2√n+it)‖ ≤ dirichletCX n for n ≥ 1 (the LSeries majorant). -/\nlemma norm_logDeriv_zeta_le_dirichletCX {n : ℕ} (hn : 1 ≤ n) {t : ℝ} :\n    ‖logDeriv riemannZeta (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ ≤\n      dirichletCX n := by\n  have h1 : (1 : ℝ) ≤ Real.sqrt (n : ℝ) := Real.one_le_sqrt.mpr (by exact_mod_cast hn)\n  have hs1 : (1 : ℝ) < (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I).re := by\n    simp\n    linarith\n  have h1' : -logDeriv riemannZeta (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)\n      = LSeries (fun n => (ArithmeticFunction.vonMangoldt n : ℂ))\n        (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) := by\n    have h2 := ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div hs1\n    rw [logDeriv, Pi.div_apply, h2]\n    ring\n  have hsumX : Summable (fun m : ℕ =>\n      ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ))\n        (((2 * Real.sqrt (n : ℝ)) : ℝ) : ℂ) m‖) := by\n    rw [summable_norm_iff]\n    apply ArithmeticFunction.LSeriesSummable_vonMangoldt\n    rw [show (((2 * Real.sqrt (n : ℝ) : ℝ) : ℂ).re) = 2 * Real.sqrt (n : ℝ) from by simp]\n    linarith\n  have hsumS : Summable (fun m : ℕ =>\n      ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ))\n        (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) m‖) := by\n    rw [summable_norm_iff]\n    exact ArithmeticFunction.LSeriesSummable_vonMangoldt hs1\n  have hle : ‖LSeries (fun n => (ArithmeticFunction.vonMangoldt n : ℂ))\n      (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ ≤ dirichletCX n := by\n    show ‖∑' m : ℕ, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ))\n      (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) m‖ ≤ _\n    calc ‖∑' m : ℕ, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ))\n          (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) m‖\n        ≤ ∑' m : ℕ, ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ))\n            (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) m‖ :=\n          norm_tsum_le_tsum_norm hsumS\n      _ ≤ ∑' m : ℕ, ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ))\n            (((2 * Real.sqrt (n : ℝ)) : ℝ) : ℂ) m‖ :=\n          Summable.tsum_le_tsum (fun m => LSeries.norm_term_le_of_re_le_re _ (by\n            simp\n            linarith) m) hsumS hsumX\n      _ = dirichletCX n := rfl\n  calc ‖logDeriv riemannZeta (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖\n      = ‖LSeries (fun n => (ArithmeticFunction.vonMangoldt n : ℂ))\n          (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ := by\n        rw [← h1', norm_neg]\n    _ ≤ dirichletCX n := hle\n\n/-- Termwise tail comparison: for m ≥ 3, the term at 2√n is ≤\n3^{−(2√n−2)}·(the term at 2). -/\nlemma norm_term_vonMangoldt_X_le_three_pow {n : ℕ} (hn : 1 ≤ n) {m : ℕ} (hm : 3 ≤ m) :\n    ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ))\n        (((2 * Real.sqrt (n : ℝ)) : ℝ) : ℂ) m‖ ≤\n      (3 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) *\n        ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (2 : ℂ) m‖ := by\n  have hXre : ((((2 * Real.sqrt (n : ℝ)) : ℝ) : ℂ).re) = 2 * Real.sqrt (n : ℝ) := by simp\n  have h2re : ((2 : ℂ).re) = 2 := rfl\n  simp only [LSeries.norm_term_eq, hXre, h2re]\n  split\n  · norm_num\n  · next hm0 =>\n    have hΛ : ‖(ArithmeticFunction.vonMangoldt m : ℂ)‖ =\n        ArithmeticFunction.vonMangoldt m :=\n      Complex.norm_of_nonneg ArithmeticFunction.vonMangoldt_nonneg\n    rw [hΛ]\n    have hm2 : (0 : ℝ) < (m : ℝ) := by exact_mod_cast (by omega : 0 < m)\n    have hsqrt2 : (2 : ℝ) ≤ 2 * Real.sqrt (n : ℝ) := by\n      have h1 : (1 : ℝ) ≤ Real.sqrt (n : ℝ) := Real.one_le_sqrt.mpr (by exact_mod_cast hn)\n      linarith\n    have hexp_nn : (0 : ℝ) ≤ 2 * Real.sqrt (n : ℝ) - 2 := by linarith\n    have e : ArithmeticFunction.vonMangoldt m / (m : ℝ) ^ (2 * Real.sqrt (n : ℝ)) =\n        (1 / (m : ℝ) ^ (2 * Real.sqrt (n : ℝ) - 2)) *\n          (ArithmeticFunction.vonMangoldt m / (m : ℝ) ^ (2 : ℝ)) := by\n      rw [show (2 * Real.sqrt (n : ℝ)) = (2 * Real.sqrt (n : ℝ) - 2) + 2 by ring,\n        Real.rpow_add hm2]\n      field_simp [hm2.ne']\n    rw [e]\n    have hle : (1 : ℝ) / (m : ℝ) ^ (2 * Real.sqrt (n : ℝ) - 2) ≤\n        (3 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) := by\n      rw [Real.rpow_neg (by norm_num : (0 : ℝ) ≤ 3), ← one_div]\n      apply one_div_le_one_div_of_le (Real.rpow_pos_of_pos (by norm_num : (0 : ℝ) < 3) _)\n      exact Real.rpow_le_rpow (by norm_num : (0 : ℝ) ≤ 3)\n        (by exact_mod_cast hm : (3 : ℝ) ≤ (m : ℝ)) hexp_nn\n    have hpos : (0 : ℝ) ≤ ArithmeticFunction.vonMangoldt m / (m : ℝ) ^ (2 : ℝ) :=\n      div_nonneg ArithmeticFunction.vonMangoldt_nonneg\n        (Real.rpow_nonneg (by positivity : (0 : ℝ) ≤ (m : ℝ)) _)\n    exact mul_le_mul_of_nonneg_right hle hpos\n\n/-- The split: dirichletCX n = log 2·2^{−2√n} + (the m ≥ 3 tail). -/\nlemma dirichletCX_le {n : ℕ} (hn : 1 ≤ n) :\n    dirichletCX n ≤ Real.log 2 * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ))) +\n      (3 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) * dirichletC2 := by\n  have hsumX : Summable (fun m : ℕ =>\n      ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ))\n        (((2 * Real.sqrt (n : ℝ)) : ℝ) : ℂ) m‖) := by\n    rw [summable_norm_iff]\n    apply ArithmeticFunction.LSeriesSummable_vonMangoldt\n    rw [show (((2 * Real.sqrt (n : ℝ) : ℝ) : ℂ).re) = 2 * Real.sqrt (n : ℝ) from by simp]\n    have h1 : (1 : ℝ) ≤ Real.sqrt (n : ℝ) := Real.one_le_sqrt.mpr (by exact_mod_cast hn)\n    linarith\n  have hsplit := tsum_split_finset hsumX {0, 1, 2}\n  have hsum2 : Summable (fun m : ℕ =>\n      ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (2 : ℂ) m‖) := by\n    rw [summable_norm_iff]\n    exact ArithmeticFunction.LSeriesSummable_vonMangoldt (by norm_num)\n  have hfin : ∑ i ∈ ({0, 1, 2} : Finset ℕ),\n      ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ))\n        (((2 * Real.sqrt (n : ℝ)) : ℝ) : ℂ) i‖ =\n      Real.log 2 * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ))) := by\n    have hXre : ((((2 * Real.sqrt (n : ℝ)) : ℝ) : ℂ).re) = 2 * Real.sqrt (n : ℝ) := by simp\n    rw [Finset.sum_insert (by norm_num), Finset.sum_insert (by norm_num),\n      Finset.sum_singleton]\n    simp only [LSeries.norm_term_eq, hXre]\n    have h0 : (0 : ℝ) = (0 : ℝ) := rfl\n    rw [if_pos rfl, if_neg (by norm_num : (1 : ℕ) ≠ 0), if_neg (by norm_num : (2 : ℕ) ≠ 0)]\n    simp [ArithmeticFunction.vonMangoldt_apply_one]\n    have hΛ2 : ‖(ArithmeticFunction.vonMangoldt 2 : ℂ)‖ = Real.log 2 := by\n      have h1 : ArithmeticFunction.vonMangoldt 2 = Real.log 2 :=\n        ArithmeticFunction.vonMangoldt_prime Nat.prime_two\n      rw [h1]\n      exact Complex.norm_of_nonneg (Real.log_two_gt_d9.le)\n    rw [hΛ2]\n    have e : (2 : ℝ) ^ (2 * Real.sqrt (n : ℝ)) = (2 : ℝ) ^ (2 * Real.sqrt (n : ℝ)) := rfl\n    rw [show Real.log 2 / (2 : ℝ) ^ (2 * Real.sqrt (n : ℝ)) =\n        Real.log 2 * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ))) by\n      rw [Real.rpow_neg (by norm_num : (0 : ℝ) ≤ 2)]\n      field_simp [Real.rpow_pos_of_pos (by norm_num : (0 : ℝ) < 2)\n        (2 * Real.sqrt (n : ℝ)).ne']]\n    ring\n  have htail : (∑' i : ℕ, (if i ∈ ({0, 1, 2} : Finset ℕ) then 0\n      else ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ))\n        (((2 * Real.sqrt (n : ℝ)) : ℝ) : ℂ) i‖)) ≤\n      (3 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) * dirichletC2 := by\n    have hterm : ∀ m : ℕ, (if m ∈ ({0, 1, 2} : Finset ℕ) then 0\n        else ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ))\n          (((2 * Real.sqrt (n : ℝ)) : ℝ) : ℂ) m‖) ≤\n        (3 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) *\n          ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (2 : ℂ) m‖ := by\n      intro m\n      by_cases hm : m ∈ ({0, 1, 2} : Finset ℕ)\n      · rw [if_pos hm]\n        positivity\n      · rw [if_neg hm]\n        have hm3 : 3 ≤ m := by omega\n        exact norm_term_vonMangoldt_X_le_three_pow hn hm3\n    have hsum_tail : Summable (fun m : ℕ => (if m ∈ ({0, 1, 2} : Finset ℕ) then 0\n        else ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ))\n          (((2 * Real.sqrt (n : ℝ)) : ℝ) : ℂ) m‖)) := by\n      apply Summable.of_norm_bounded hsumX.norm\n      intro m\n      by_cases hm : m ∈ ({0, 1, 2} : Finset ℕ) <;> simp [hm]\n    calc (∑' m : ℕ, (if m ∈ ({0, 1, 2} : Finset ℕ) then 0\n          else ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ))\n            (((2 * Real.sqrt (n : ℝ)) : ℝ) : ℂ) m‖))\n        ≤ ∑' m : ℕ, (3 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) *\n            ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (2 : ℂ) m‖ :=\n          Summable.tsum_le_tsum hterm hsum_tail (hsum2.mul_left _)\n      _ = (3 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) * dirichletC2 := by\n          rw [dirichletC2, tsum_mul_left]\n  calc dirichletCX n\n      = ∑ i ∈ ({0, 1, 2} : Finset ℕ),\n          ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ))\n            (((2 * Real.sqrt (n : ℝ)) : ℝ) : ℂ) i‖ +\n        ∑' i : ℕ, (if i ∈ ({0, 1, 2} : Finset ℕ) then 0\n          else ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ))\n            (((2 * Real.sqrt (n : ℝ)) : ℝ) : ℂ) i‖) := hsplit\n    _ ≤ Real.log 2 * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ))) +\n        (3 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) * dirichletC2 :=\n        add_le_add (le_of_eq hfin) htail\n\n/-- **The I_I zeta charge WITHOUT dirichletC2 ≤ 0.57** (DL-6 capstone):\nfor n ≥ 5, ‖ζ′/ζ(2√n+it)‖ ≤ 0.57·2^{−(2√n−2)} — the IIMaj zeta form,\nvia the direct log2-leading + 3^{−(2√n−2)} tail (dirichletC2 ≤ 1) with\nthe certified (4/9)^{√n} ≤ 0.17631 bound at √n ≥ √5. -/\ntheorem norm_logDeriv_zeta_le_iimZeta {n : ℕ} (hn : 5 ≤ n) {t : ℝ} :\n    ‖logDeriv riemannZeta (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ ≤\n      (0.57 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) := by\n  have hn1 : 1 ≤ n := by omega\n  have h1 := norm_logDeriv_zeta_le_dirichletCX hn1 (t := t)\n  have h2 := dirichletCX_le hn1\n  have hC2 : dirichletC2 ≤ 1 := dirichletC2_le_one\n  have hC2nn : (0 : ℝ) ≤ dirichletC2 := dirichletC2_nonneg\n  -- the (4/9)^{√n} ≤ 0.17631 certification at √n ≥ √5\n  have hsqrt5 : (2.236 : ℝ) ≤ Real.sqrt (n : ℝ) := by\n    have hnR : (5 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn\n    have h1 : Real.sqrt 5 ≤ Real.sqrt (n : ℝ) := Real.sqrt_le_sqrt hnR\n    have h2 : (2.236 : ℝ) ≤ Real.sqrt 5 := by\n      rw [Real.le_sqrt (by norm_num) (by norm_num)]\n      norm_num\n    linarith\n  have h49 : (4 / 9 : ℝ) ^ Real.sqrt (n : ℝ) ≤ (0.17631 : ℝ) := by\n    have hlog : Real.log (4 / 9) = 2 * Real.log 2 - Real.log 9 := by\n      rw [Real.log_div (by norm_num : (4 : ℝ) ≠ 0) (by norm_num : (9 : ℝ) ≠ 0),\n        Real.log_pow, Real.log_pow]\n      push_cast\n      ring\n    have hlog49 : Real.log (4 / 9) ≤ (-0.811 : ℝ) := by\n      rw [hlog]\n      have h1 := Real.log_two_lt_d9\n      have h2 : Real.log 9 = 2 * Real.log 3 := by\n        rw [show (9 : ℝ) = 3 ^ 2 by norm_num, Real.log_pow]\n        push_cast\n        ring\n      have h3 : (2.1972 : ℝ) ≤ Real.log 3 := by\n        rw [show (2.1972 : ℝ) = Real.log (Real.exp 2.1972) by rw [Real.log_exp]]\n        apply Real.log_le_log (Real.exp_pos _)\n        rw [show Real.exp 2.1972 = Real.exp 2 * Real.exp 0.1972 by\n          rw [← Real.exp_add]; norm_num]\n        calc (3 : ℝ) ≤ 2.7182818283 * 1.2179 := by norm_num\n          _ ≤ Real.exp 2 * Real.exp 0.1972 :=\n            mul_le_mul Real.exp_one_gt_d9.le\n              (le_trans (by norm_num [Finset.sum_range_succ])\n                (Real.sum_le_exp_of_nonneg (by norm_num : (0 : ℝ) ≤ 0.1972) 6))\n              (by norm_num) (Real.exp_pos _).le\n      linarith [h3]\n    have h1 : (4 / 9 : ℝ) ^ Real.sqrt (n : ℝ) =\n        Real.exp (Real.sqrt (n : ℝ) * Real.log (4 / 9)) := by\n      rw [Real.rpow_def_of_pos (by norm_num : (0 : ℝ) < 4 / 9)]\n    rw [h1]\n    have h2 : Real.sqrt (n : ℝ) * Real.log (4 / 9) ≤ (-1.8135 : ℝ) := by\n      have hlogneg : Real.log (4 / 9) < 0 :=\n        Real.log_neg (by norm_num : (0 : ℝ) < 4 / 9) (by norm_num : (4 / 9 : ℝ) < 1)\n      have h1 : Real.sqrt (n : ℝ) * Real.log (4 / 9) ≤ 2.236 * (-0.811) := by\n        apply mul_le_mul_of_nonpos_right _ hlogneg.le\n        · rw [show (2.236 : ℝ) * (-0.811) = -(-2.236 * 0.811) by ring]\n          apply Real.rpow_le_rpow (by norm_num : (0 : ℝ) ≤ 4 / 9)\n          · -- 2.236 ≤ √n and log(4/9) ≤ −0.811: the product ≤ 2.236·(−0.811)\n            sorry\n          · sorry\n        sorry\n      sorry\n    sorry\n  sorry\n\nend NguyenRH1\n\nend"},"extra_content":null}]