← Session 27 — ii′-5c/5d: Davenport disc + FE-reflection bounds
thinking (113 chars)
Now session closure: journal-026, STATE.md, NGUYEN.md, db session registration, commit. Let me write the journal.
Now the session journal and STATE update.
tool: Write
input
{
"file_path": "D:\\Python\\Quantum\\research\\journal\\session-026.md",
"content": "# Session 026 \u2014 2026-08-22 \u2014 ii\u2032-5e prep (zeroMult(\u22122n) = 1, ALL n) + D-068 (5e design)\n\n## Directive\nContinue tier ii\u2032-5 per STATE.md: session 026 first item \u2014 generalize\nii\u2032-4c's zeroMult_neg_two to all trivial zeros \u2014 then the ii\u2032-5e design.\nUser: \"yes\" (to the queued plan).\n\n## Outcome 1: zeroMult(\u22122n) = 1 for ALL n \u2265 1 \u2014 COMPLETE (commit 0d9887a)\nNew file `NguyenRH1/LiTrivialZeros.lean` (~290 lines, 8 decls, all\naxiom-audited: 3 standard axioms only, zero sorryAx), root-imported;\nfull build GREEN (8762 jobs).\n\nBuild path:\n1. `gamma_mul_prod`: the product-form \u0393 recurrence\n \u0393(z)\u00b7\u220f_{j<n}(z+j) = \u0393(z+n) for z avoiding {0,\u2026,\u2212(n\u22121)} \u2014 clean\n induction on `Complex.Gamma_add_one` (empty-product base, no\n side conditions at n = 0; the multiplied form avoids division\n side-conditions entirely).\n2. The cofactor `HfunT n s = 2\u00b7\u03c0^{\u2212s/2}\u00b7\u0393(s/2+n+1)/trivQ n s` with\n trivQ n s = \u220f_{j<n}(s/2+j): analytic at \u22122n (\u0393(s/2+n+1) analytic via\n re(s/2+n+1) \u2208 (1/2, 3/2) on the unit ball \u2014 away from the Gamma\n poles; trivQ a polynomial with trivQ(\u22122n) = \u220f(\u2212n+j) \u2260 0) and\n HfunT(\u22122n) = 2\u03c0\u207f\u00b7\u0393(1)/trivQ(\u22122n) \u2260 0.\n3. The punctured identity `HfunT_eq`: (s+2n)\u00b7\u0393R(s) = HfunT n s on\n ball(\u22122n, 1) \u2216 {\u22122n} \u2014 the recurrence side conditions\n (\u2200 k \u2264 n, s/2 \u2260 \u2212k) from the ball geometry (s/2 = \u2212k \u27f9 s = \u22122k at\n distance 2|n\u2212k| \u2265 2 from \u22122n unless k = n = the puncture).\n4. `zeroMult_neg_two_mul`: \u03b6 = (s+2n)\u00b7(\u039b/HfunT n) near \u22122n with\n \u039b(\u22122n) = \u039b(1+2n) = \u0393R(1+2n)\u00b7\u03b6(1+2n) \u2260 0 (FE + \u0393R-ne-zero-of-re_pos\n + riemannZeta_ne_zero_of_one_lt_re) \u27f9 analyticOrderAt = 1 via\n analyticOrderAt_eq_natCast (the ii\u2032-4c pattern verbatim).\n\n## Outcome 2: D-068 \u2014 ii\u2032-5e DESIGN COMPLETE\nThe partial-fraction identity assembly plan. TWO CORRECTIONS to the\nD-067 \u00a76 sketch found by the pre-build survey:\n- (C1) the circle series bound is O((log R)\u00b3), not O((log R)\u00b2) \u2014 the\n correct split is by the RADIAL distance ||s|\u2212|\u03c1|| with the \u03b3-gap\n needed only in the critical annulus [R\u00b12] (the naive |s\u2212\u03c1| \u2265 1 bound\n over the \u224d R log R annulus zeros gives O(R log R) \u2014 fatal; recorded\n with the fix).\n- (C2) the near-axis left-plane digamma bound is a SEPARATE build\n (5d's bound needs 2 \u2264 |im w| for the slit-plane FTC; the circle's\n near-real-axis left part has w = s/2 with |im w| possibly < 2):\n recurrence + separated reciprocal sum \u03a3 1/|w+j| \u2264 C\u00b7log(m+1)\n (1-separated real parts + dist(w,\u2212\u2115) \u2265 1/4 \u27f9 \u2264 2 per unit bin) +\n \u03c8(w+m) via StirlingVert (|im| \u2265 1/2) or compactness (|im| < 1/2,\n re \u2208 [1,2]). Also the right-half re \u2265 2 mild case via the Weierstrass\n series (Zeta23 DigammaSeries.digamma_series \u2014 exists).\nSub-stage map 5e-i..v: (i) \u00d72-rescaled \u03b3-gap circles R_k \u2208 [4k+2.5,\n4k+3] (the 5c \u00d710-trick verbatim; R/2 \u2208 [2k+1.25, 2k+1.5] \u27f9 dist \u2265 1/4\nto \u2124 automatically); (ii) the C2 digamma bound; (iii) the zero series\n(summability via the ii\u2032-1a dominator + zero_sum_inv_sq; analytic off\nthe zeros via locally-uniform limits; isolation at each zero);\n(iv) F entire by principal-part splits (NO removable-singularity\ntheorem, NO Hadamard \u2014 at 1 via ii\u2032-1b's zetaA logDeriv; at 0 and \u22122n\nvia the digamma series splits + zeroMult_neg_two_mul); (v) circle\nbound O((log R)\u00b3) + max-modulus squeeze \u27f9 F \u2261 const (no Liouville\nneeded). Capstone: \u2203 B : \u2102, the identity for s off\n{zeros} \u222a {0,1} \u222a {\u22122n}. Plus the 5f preview (D-056's six-piece\nanalysis; the perimeter ZeroCountProp's FIRST use in the R-chain).\n\n## Banked gotchas (session 026 additions)\n- `DifferentiableAt.analyticAt` does NOT exist in this Mathlib \u2014 for a\n pointwise-analyticity goal use `by fun_prop` (AnalyticAt is\n fun_prop-enabled) or DifferentiableOn + analyticOnNhd on a ball.\n- Gamma\u211d_eq_zero_iff gives s = `-(2 * \u2191m)` (negation OUTSIDE), not\n `-2 * \u2191m` \u2014 match patterns accordingly.\n- `riemannZeta_neg_two_mul_nat_add_one (n)` : \u03b6(\u22122\u00b7(\u2191n+1)) = 0 with\n the +1 in \u2102 \u2014 for \u03b6(\u22122n), apply at n\u22121 and rewrite\n \u2191(n\u22121)+1 = \u2191n via \u2190 Nat.cast_add_one + Nat.sub_add_cancel.\n- `lt_trichotomy` exists (le_or_lt does NOT in this Mathlib).\n- field_simp may close the goal entirely (again) \u2014 check before a\n trailing ring (second occurrence; journal-024 had the first).\n- Finset.analyticAt_fun_prod : (\u2200 i \u2208 s, AnalyticAt \ud835\udd5c (f i) x) \u2192\n AnalyticAt \ud835\udd5c (fun x => \u220f i \u2208 s, f i x) x.\n\n## Status / next\nii\u2032-5e prep (5e-0) + design (D-068) COMPLETE. Next: **ii\u2032-5e-i**\n(\u03b3-gap circles via the \u00d72-rescaled midpoint pigeonhole), then 5e-ii\n(near-axis digamma bound), 5e-iii (series), 5e-iv (F entire),\n5e-v (capstone). Then ii\u2032-5f (tight analysis \u2192 10.5/48, D-056),\nii\u2032-3b, ii\u2032-3c, ii\u2032-6, ii\u2032-7.\n"
}
raw content_json (database row)
[{"type":"thinking","thinking":"Now session closure: journal-026, STATE.md, NGUYEN.md, db session registration, commit. Let me write the journal.","signature":""},{"type":"text","text":"Now the session journal and STATE update."},{"type":"tool_use","id":"Write_211","name":"Write","input":{"file_path":"D:\\Python\\Quantum\\research\\journal\\session-026.md","content":"# Session 026 — 2026-08-22 — ii′-5e prep (zeroMult(−2n) = 1, ALL n) + D-068 (5e design)\n\n## Directive\nContinue tier ii′-5 per STATE.md: session 026 first item — generalize\nii′-4c's zeroMult_neg_two to all trivial zeros — then the ii′-5e design.\nUser: \"yes\" (to the queued plan).\n\n## Outcome 1: zeroMult(−2n) = 1 for ALL n ≥ 1 — COMPLETE (commit 0d9887a)\nNew file `NguyenRH1/LiTrivialZeros.lean` (~290 lines, 8 decls, all\naxiom-audited: 3 standard axioms only, zero sorryAx), root-imported;\nfull build GREEN (8762 jobs).\n\nBuild path:\n1. `gamma_mul_prod`: the product-form Γ recurrence\n Γ(z)·∏_{j<n}(z+j) = Γ(z+n) for z avoiding {0,…,−(n−1)} — clean\n induction on `Complex.Gamma_add_one` (empty-product base, no\n side conditions at n = 0; the multiplied form avoids division\n side-conditions entirely).\n2. The cofactor `HfunT n s = 2·π^{−s/2}·Γ(s/2+n+1)/trivQ n s` with\n trivQ n s = ∏_{j<n}(s/2+j): analytic at −2n (Γ(s/2+n+1) analytic via\n re(s/2+n+1) ∈ (1/2, 3/2) on the unit ball — away from the Gamma\n poles; trivQ a polynomial with trivQ(−2n) = ∏(−n+j) ≠ 0) and\n HfunT(−2n) = 2πⁿ·Γ(1)/trivQ(−2n) ≠ 0.\n3. The punctured identity `HfunT_eq`: (s+2n)·ΓR(s) = HfunT n s on\n ball(−2n, 1) ∖ {−2n} — the recurrence side conditions\n (∀ k ≤ n, s/2 ≠ −k) from the ball geometry (s/2 = −k ⟹ s = −2k at\n distance 2|n−k| ≥ 2 from −2n unless k = n = the puncture).\n4. `zeroMult_neg_two_mul`: ζ = (s+2n)·(Λ/HfunT n) near −2n with\n Λ(−2n) = Λ(1+2n) = ΓR(1+2n)·ζ(1+2n) ≠ 0 (FE + ΓR-ne-zero-of-re_pos\n + riemannZeta_ne_zero_of_one_lt_re) ⟹ analyticOrderAt = 1 via\n analyticOrderAt_eq_natCast (the ii′-4c pattern verbatim).\n\n## Outcome 2: D-068 — ii′-5e DESIGN COMPLETE\nThe partial-fraction identity assembly plan. TWO CORRECTIONS to the\nD-067 §6 sketch found by the pre-build survey:\n- (C1) the circle series bound is O((log R)³), not O((log R)²) — the\n correct split is by the RADIAL distance ||s|−|ρ|| with the γ-gap\n needed only in the critical annulus [R±2] (the naive |s−ρ| ≥ 1 bound\n over the ≍ R log R annulus zeros gives O(R log R) — fatal; recorded\n with the fix).\n- (C2) the near-axis left-plane digamma bound is a SEPARATE build\n (5d's bound needs 2 ≤ |im w| for the slit-plane FTC; the circle's\n near-real-axis left part has w = s/2 with |im w| possibly < 2):\n recurrence + separated reciprocal sum Σ 1/|w+j| ≤ C·log(m+1)\n (1-separated real parts + dist(w,−ℕ) ≥ 1/4 ⟹ ≤ 2 per unit bin) +\n ψ(w+m) via StirlingVert (|im| ≥ 1/2) or compactness (|im| < 1/2,\n re ∈ [1,2]). Also the right-half re ≥ 2 mild case via the Weierstrass\n series (Zeta23 DigammaSeries.digamma_series — exists).\nSub-stage map 5e-i..v: (i) ×2-rescaled γ-gap circles R_k ∈ [4k+2.5,\n4k+3] (the 5c ×10-trick verbatim; R/2 ∈ [2k+1.25, 2k+1.5] ⟹ dist ≥ 1/4\nto ℤ automatically); (ii) the C2 digamma bound; (iii) the zero series\n(summability via the ii′-1a dominator + zero_sum_inv_sq; analytic off\nthe zeros via locally-uniform limits; isolation at each zero);\n(iv) F entire by principal-part splits (NO removable-singularity\ntheorem, NO Hadamard — at 1 via ii′-1b's zetaA logDeriv; at 0 and −2n\nvia the digamma series splits + zeroMult_neg_two_mul); (v) circle\nbound O((log R)³) + max-modulus squeeze ⟹ F ≡ const (no Liouville\nneeded). Capstone: ∃ B : ℂ, the identity for s off\n{zeros} ∪ {0,1} ∪ {−2n}. Plus the 5f preview (D-056's six-piece\nanalysis; the perimeter ZeroCountProp's FIRST use in the R-chain).\n\n## Banked gotchas (session 026 additions)\n- `DifferentiableAt.analyticAt` does NOT exist in this Mathlib — for a\n pointwise-analyticity goal use `by fun_prop` (AnalyticAt is\n fun_prop-enabled) or DifferentiableOn + analyticOnNhd on a ball.\n- Gammaℝ_eq_zero_iff gives s = `-(2 * ↑m)` (negation OUTSIDE), not\n `-2 * ↑m` — match patterns accordingly.\n- `riemannZeta_neg_two_mul_nat_add_one (n)` : ζ(−2·(↑n+1)) = 0 with\n the +1 in ℂ — for ζ(−2n), apply at n−1 and rewrite\n ↑(n−1)+1 = ↑n via ← Nat.cast_add_one + Nat.sub_add_cancel.\n- `lt_trichotomy` exists (le_or_lt does NOT in this Mathlib).\n- field_simp may close the goal entirely (again) — check before a\n trailing ring (second occurrence; journal-024 had the first).\n- Finset.analyticAt_fun_prod : (∀ i ∈ s, AnalyticAt 𝕜 (f i) x) →\n AnalyticAt 𝕜 (fun x => ∏ i ∈ s, f i x) x.\n\n## Status / next\nii′-5e prep (5e-0) + design (D-068) COMPLETE. Next: **ii′-5e-i**\n(γ-gap circles via the ×2-rescaled midpoint pigeonhole), then 5e-ii\n(near-axis digamma bound), 5e-iii (series), 5e-iv (F entire),\n5e-v (capstone). Then ii′-5f (tight analysis → 10.5/48, D-056),\nii′-3b, ii′-3c, ii′-6, ii′-7.\n"},"extra_content":null}]