← Session 27 — ii′-5c/5d: Davenport disc + FE-reflection bounds
Now the NGUYEN.md checklist update (ii′-5d entry).
tool: Edit
input
{
"file_path": "D:\\Python\\Quantum\\NGUYEN.md",
"old_string": " **Capstone: logDeriv_riemannZeta_sub_nearZeros_le** \u2014 the LOOSE\n R-bound \u2016\u03b6\u2032/\u03b6(s) \u2212 \u03a3_{|\u03b3\u2212t|<1} m/(s\u2212\u03c1)\u2016 \u2264 100000\u00b7(log|t|)\u00b2 on\n \u03c3 \u2208 [1/2, 7/2], |t| \u2265 10, \u03b6 s \u2260 0 (no perimeter hypothesis \u2014\n Jensen count input). Build GREEN (8753 jobs, LiDisc now root-\n imported); 32 new decls audited: 3 standard axioms only.\n- [ ] ii\u2032-6 L0 assembly: sides identity + bridge |\u03bb_n(T)| \u2264 2\u00b7FAlt(T)\n (hRH) + |Sf n| \u2264 Bn FAlt n on [10\u2075, N\u2081].",
"new_string": " **Capstone: logDeriv_riemannZeta_sub_nearZeros_le** \u2014 the LOOSE\n R-bound \u2016\u03b6\u2032/\u03b6(s) \u2212 \u03a3_{|\u03b3\u2212t|<1} m/(s\u2212\u03c1)\u2016 \u2264 100000\u00b7(log|t|)\u00b2 on\n \u03c3 \u2208 [1/2, 7/2], |t| \u2265 10, \u03b6 s \u2260 0 (no perimeter hypothesis \u2014\n Jensen count input). Build GREEN (8753 jobs, LiDisc now root-\n imported); 32 new decls audited: 3 standard axioms only.\n- [x] ii\u2032-5d FE-reflection to \u03c3 \u2208 [\u22125/2, 1/2] + left-plane uniform\n digamma bound.\n \u2192 COMPLETE (session 025, LiReflect.lean, ~640 lines, 26 decls\n audited clean): `logDeriv_zeta_fe` (the pointwise logDeriv FE);\n `sum_nearZeros_neg_reflect` (the EXACT zero-sum cancellation under\n \u03c1 \u21a6 1\u2212\u03c1: nearZeros(\u2212t) = image, zeroMult invariant via Zeta23\n analyticOrderAt_zeta_one_sub); `logDeriv_Gamma\u211d_shift` (the +4 \u0393R\n shift putting both digamma arguments in re > 0) + digamma_stirling\n \u27f9 \u0393R-bracket \u2264 4(log|t|)\u00b2; capstone\n **logDeriv_riemannZeta_sub_nearZeros_le_left** \u2264 200000\u00b7(log|t|)\u00b2\n on \u03c3 \u2208 [\u22125/2, 1/2], |t| \u2265 10; PLUS the 5e input\n **norm_digamma_sub_log_le_of_two_le_abs_im** (\u2016\u03c8(w) \u2212 log w\u2016 \u2264 3\n for 2 \u2264 |im w|, uniform in the shift chain: digamma_add_natCast\n + first-order EM + arctan-FTC). Build GREEN (8761 jobs, LiReflect\n root-imported). DEFERRED to session 026 first item:\n zeroMult(\u22122n) = 1 for ALL n (5e's entirety at trivial zeros).\n- [ ] ii\u2032-6 L0 assembly: sides identity + bridge |\u03bb_n(T)| \u2264 2\u00b7FAlt(T)\n (hRH) + |Sf n| \u2264 Bn FAlt n on [10\u2075, N\u2081]."
}
raw content_json (database row)
[{"type":"text","text":"Now the NGUYEN.md checklist update (ii′-5d entry)."},{"type":"tool_use","id":"Edit_158","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\NGUYEN.md","old_string":" **Capstone: logDeriv_riemannZeta_sub_nearZeros_le** — the LOOSE\n R-bound ‖ζ′/ζ(s) − Σ_{|γ−t|<1} m/(s−ρ)‖ ≤ 100000·(log|t|)² on\n σ ∈ [1/2, 7/2], |t| ≥ 10, ζ s ≠ 0 (no perimeter hypothesis —\n Jensen count input). Build GREEN (8753 jobs, LiDisc now root-\n imported); 32 new decls audited: 3 standard axioms only.\n- [ ] ii′-6 L0 assembly: sides identity + bridge |λ_n(T)| ≤ 2·FAlt(T)\n (hRH) + |Sf n| ≤ Bn FAlt n on [10⁵, N₁].","new_string":" **Capstone: logDeriv_riemannZeta_sub_nearZeros_le** — the LOOSE\n R-bound ‖ζ′/ζ(s) − Σ_{|γ−t|<1} m/(s−ρ)‖ ≤ 100000·(log|t|)² on\n σ ∈ [1/2, 7/2], |t| ≥ 10, ζ s ≠ 0 (no perimeter hypothesis —\n Jensen count input). Build GREEN (8753 jobs, LiDisc now root-\n imported); 32 new decls audited: 3 standard axioms only.\n- [x] ii′-5d FE-reflection to σ ∈ [−5/2, 1/2] + left-plane uniform\n digamma bound.\n → COMPLETE (session 025, LiReflect.lean, ~640 lines, 26 decls\n audited clean): `logDeriv_zeta_fe` (the pointwise logDeriv FE);\n `sum_nearZeros_neg_reflect` (the EXACT zero-sum cancellation under\n ρ ↦ 1−ρ: nearZeros(−t) = image, zeroMult invariant via Zeta23\n analyticOrderAt_zeta_one_sub); `logDeriv_Gammaℝ_shift` (the +4 ΓR\n shift putting both digamma arguments in re > 0) + digamma_stirling\n ⟹ ΓR-bracket ≤ 4(log|t|)²; capstone\n **logDeriv_riemannZeta_sub_nearZeros_le_left** ≤ 200000·(log|t|)²\n on σ ∈ [−5/2, 1/2], |t| ≥ 10; PLUS the 5e input\n **norm_digamma_sub_log_le_of_two_le_abs_im** (‖ψ(w) − log w‖ ≤ 3\n for 2 ≤ |im w|, uniform in the shift chain: digamma_add_natCast\n + first-order EM + arctan-FTC). Build GREEN (8761 jobs, LiReflect\n root-imported). DEFERRED to session 026 first item:\n zeroMult(−2n) = 1 for ALL n (5e's entirety at trivial zeros).\n- [ ] ii′-6 L0 assembly: sides identity + bridge |λ_n(T)| ≤ 2·FAlt(T)\n (hRH) + |Sf n| ≤ Bn FAlt n on [10⁵, N₁]."},"extra_content":null}]