{
  "file_path": "D:\\Python\\Quantum\\research\\journal\\session-019.md",
  "content": "# Session 019 \u2014 2026-08-21 \u2014 ii\u2032-3 DESIGN (D-066, route \u03b24) + piece (B) PROVED\n\n## Directive\nContinue tier ii\u2032 per D-064: sub-stage ii\u2032-3 (Lagarias (4.10), the long\npole). STATE.md: design note first (read EF_lit_zeta + WeilEF interface),\nthen Lean.\n\n## Work done\n**(1) Route investigation COMPLETE (D-066, commit 62a1ddf).** Read:\nEF_lit_zeta's exact statement (Zeta23/ExplicitFormula.lean \u2014 the\nliterature-form Weil EF for k \u2208 C\u00b2_c, h = paperFT k entire of exp type);\nits proof structure (WeilEF/Main.lean \u2014 full-line contour identity);\nLagarias's own \u00a74 proof (archived PDF pp. 14\u201317: Lemma 4.1 via the\nHadamard product, (4.10) by coefficient comparison, (4.19)\u2013(4.22) digamma\npartial fractions); Mathlib infrastructure inventory.\n\nRoute verdicts:\n- **\u03b21 (Hadamard product) OUT as scoped in D-064**: the guessed seed\n  `MeromorphicOn.extract_zeros_poles` is finite-only (FactorizedRational /\n  CanonicalDecomposition); Mathlib has NO Weierstrass infinite product,\n  NO minimum-modulus theorem, NO order theory.\n- **\u03b22 (EF reuse) OUT**: the moment kernels (1/2+iz)^{\u2212k} are not entire \u2014\n  the zero power sums are outside EF_lit's test-function class.\n- **\u03b24 ADOPTED**: prove the moment identity (M) \u03c3_k = \u2212g^{(k\u22121)}(0)/(k\u22121)!\n  directly by the ii\u2032-1b rectangle-residue machinery (w^{\u2212k}\u00b7g(w), k \u2265 2;\n  paired kernel g(w)/(2w(1\u2212w)) for k = 1), expanding limit killed by the\n  R-bound (SHARED with ii\u2032-5 \u2014 the key dependency insight), vertical lines\n  vanishing by push-off (no poles right of Re 1; decay). Factorization\n  (4.10-a) \u27fa (M) + (A) archimedean + (B) \u03b6-piece, with the FE reflection\n  g^{(k\u22121)}(0) = (\u22121)^k g^{(k\u22121)}(1) (Mathlib completedRiemannZeta_one_sub).\n  Sanity gates all check numerically (\u03c3\u2081 Davenport value; \u03c4\u2080 via\n  digamma_one_half; \u03c8\u2032(1/2) = \u03c0\u00b2/8\u00b72 etc.).\n- **Resequenced pipeline** (supersedes D-064's ii\u2032-3-first ordering):\n  ii\u2032-3a (pieces A+B, no contour deps) \u2192 ii\u2032-4 (L3+L1) \u2192 ii\u2032-5 (R-bound)\n  \u2192 ii\u2032-3b (moments) \u2192 ii\u2032-3c (assembly \u2192 crux sf_eq_resW1) \u2192 ii\u2032-6 \u2192 7.\n- Key object note: Mathlib's `completedRiemannZeta\u2080` is the WRONG \u03be (its\n  zeros are shifted \u2014 \u039b\u2080 = \u039b + 1/s \u2212 1/(s\u22121)); the right object is\n  xiL := (s(s\u22121)/2)\u00b7completedRiemannZeta (entire; zeros = IsNontrivialZero\n  via Zeta23 CountByIntegral + factor nonvanishing).\n- Mathlib inventory verified live: TendstoLocallyUniformlyOn.differentiableOn\n  (Weierstrass), Complex.digamma_one_half \u2713 (\u03c4\u2080!), digamma_apply_add_one,\n  Gamma\u211d_def/one/ne_zero_of_re_pos/eq_zero_iff, LSeries_vonMangoldt_eq_\n  deriv_riemannZeta_div (\u2212\u03b6\u2032/\u03b6 Dirichlet series), BohrMollerup\n  tendsto_log_gamma (the digamma-series seed for piece A's j \u2265 1).\n\n**(2) Piece (B) PROVED (LiZetaCoeff.lean, ~250 lines)**:\n`hLiExt s := (1 \u2212 hLi(1+s))/s` extended by \u2212deriv hLi 1 at 0 \u2014 the\nanalytic-at-0 form of 1/s + \u03b6\u2032/\u03b6(1+s):\n- `hLiExt_tendsto` (slope limit), `hLiExt_analyticAt_zero` (removable\n  singularity, the zetaA pattern), `hLiExt_mul_id` (exact global identity\n  s\u00b7hLiExt s = 1 \u2212 hLi(1+s)), `iteratedDeriv_hLi_one_add` (comp bridge via\n  iteratedDeriv_comp_sub_const at c = \u22121),\n- **`iteratedDeriv_hLiExt`**: iteratedDeriv j hLiExt 0 = \u2212(j!)\u00b7lcoeff j \u2014\n  the Taylor coefficients of 1/s + \u03b6\u2032/\u03b6(1+s) at 0 are \u2212c_j. Proof: Leibniz\n  (iteratedDeriv_mul) with the identity factor collapsing the sum to i = 1,\n  then factorial bookkeeping.\n- `hLiExt_eq_near_zero`: hLiExt s = 1/s + \u03b6\u2032/\u03b6(1+s) on \ud835\udcdd[\u2260] 0 (the\n  reading as the actual meromorphic function).\n\n## Lean notes (hard-won this session, additions to the handoff list)\n- `HasDerivAt.comp` at a composed point: write the outer hypothesis's\n  point SYNTACTICALLY as `g x` (e.g. `1 + 0`), not its reduced form \u2014\n  else the elaborator solves ?g := const.\n- `1 + 0` is NOT defeq to `1` for \u2102/\u211d (OfNat/HAdd don't compute) \u2014 nhds\n  targets need `simpa using` bridges, not `exact`.\n- `tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within`: source filter\n  stays arbitrary (\ud835\udcdd[\u2260] 0), first premise Tendsto f l (\ud835\udcdd a) \u2014 use\n  `.mono_left nhdsWithin_le_nhds`.\n- `iteratedDeriv_succ'` : iteratedDeriv (n+1) f = iteratedDeriv n (deriv f)\n  (deriv INSIDE; `iteratedDeriv_succ` is the other order).\n- `iteratedDeriv_const` : = if n = 0 then c else 0 (no side hypothesis).\n- `deriv_id'' : deriv (fun x => x) = fun x => 1` (function equality,\n  not pointwise \u2014 don't apply it to an argument).\n- `ContDiffAt \u2102 (j+1)` lives at order \u2115\u221e: the \u2191?n = \u2191j + 1 unification\n  leaves beta-redex artifacts downstream \u2014 pin iteratedDeriv_mul's\n  conclusion with an explicit type ascription (clean Finset.range (j+2)).\n- `add_eq_left : a + b = a \u2194 b = 0` (add_eq_right is the other one).\n- `iteratedDeriv_comp_sub_const m f c` produces the LAMBDA\n  fun z => f (z \u2212 c) (not the \u2218 form).\n\n## State at stop\nii\u2032-3a piece (B) COMPLETE. Remaining in ii\u2032-3a: piece (A) \u2014 the archimedean\n\u03c4-evaluation (\u03c4\u2080 via digamma_one_half; j \u2265 1 via the digamma series built\nfrom BohrMollerup's logGammaSeq + termwise derivation + the odd-m\nreindexing to lagariasA). Then ii\u2032-4 (L3+L1), ii\u2032-5 (R-bound), ii\u2032-3b\n(moments), ii\u2032-3c (assembly).\n"
}

{
  "type": "create",
  "filePath": "D:\\Python\\Quantum\\research\\journal\\session-019.md",
  "content": "# Session 019 \u2014 2026-08-21 \u2014 ii\u2032-3 DESIGN (D-066, route \u03b24) + piece (B) PROVED\n\n## Directive\nContinue tier ii\u2032 per D-064: sub-stage ii\u2032-3 (Lagarias (4.10), the long\npole). STATE.md: design note first (read EF_lit_zeta + WeilEF interface),\nthen Lean.\n\n## Work done\n**(1) Route investigation COMPLETE (D-066, commit 62a1ddf).** Read:\nEF_lit_zeta's exact statement (Zeta23/ExplicitFormula.lean \u2014 the\nliterature-form Weil EF for k \u2208 C\u00b2_c, h = paperFT k entire of exp type);\nits proof structure (WeilEF/Main.lean \u2014 full-line contour identity);\nLagarias's own \u00a74 proof (archived PDF pp. 14\u201317: Lemma 4.1 via the\nHadamard product, (4.10) by coefficient comparison, (4.19)\u2013(4.22) digamma\npartial fractions); Mathlib infrastructure inventory.\n\nRoute verdicts:\n- **\u03b21 (Hadamard product) OUT as scoped in D-064**: the guessed seed\n  `MeromorphicOn.extract_zeros_poles` is finite-only (FactorizedRational /\n  CanonicalDecomposition); Mathlib has NO Weierstrass infinite product,\n  NO minimum-modulus theorem, NO order theory.\n- **\u03b22 (EF reuse) OUT**: the moment kernels (1/2+iz)^{\u2212k} are not entire \u2014\n  the zero power sums are outside EF_lit's test-function class.\n- **\u03b24 ADOPTED**: prove the moment identity (M) \u03c3_k = \u2212g^{(k\u22121)}(0)/(k\u22121)!\n  directly by the ii\u2032-1b rectangle-residue machinery (w^{\u2212k}\u00b7g(w), k \u2265 2;\n  paired kernel g(w)/(2w(1\u2212w)) for k = 1), expanding limit killed by the\n  R-bound (SHARED with ii\u2032-5 \u2014 the key dependency insight), vertical lines\n  vanishing by push-off (no poles right of Re 1; decay). Factorization\n  (4.10-a) \u27fa (M) + (A) archimedean + (B) \u03b6-piece, with the FE reflection\n  g^{(k\u22121)}(0) = (\u22121)^k g^{(k\u22121)}(1) (Mathlib completedRiemannZeta_one_sub).\n  Sanity gates all check numerically (\u03c3\u2081 Davenport value; \u03c4\u2080 via\n  digamma_one_half; \u03c8\u2032(1/2) = \u03c0\u00b2/8\u00b72 etc.).\n- **Resequenced pipeline** (supersedes D-064's ii\u2032-3-first ordering):\n  ii\u2032-3a (pieces A+B, no contour deps) \u2192 ii\u2032-4 (L3+L1) \u2192 ii\u2032-5 (R-bound)\n  \u2192 ii\u2032-3b (moments) \u2192 ii\u2032-3c (assembly \u2192 crux sf_eq_resW1) \u2192 ii\u2032-6 \u2192 7.\n- Key object note: Mathlib's `completedRiemannZeta\u2080` is the WRONG \u03be (its\n  zeros are shifted \u2014 \u039b\u2080 = \u039b + 1/s \u2212 1/(s\u22121)); the right object is\n  xiL := (s(s\u22121)/2)\u00b7completedRiemannZeta (entire; zeros = IsNontrivialZero\n  via Zeta23 CountByIntegral + factor nonvanishing).\n- Mathlib inventory verified live: TendstoLocallyUniformlyOn.differentiableOn\n  (Weierstrass), Complex.digamma_one_half \u2713 (\u03c4\u2080!), digamma_apply_add_one,\n  Gamma\u211d_def/one/ne_zero_of_re_pos/eq_zero_iff, LSeries_vonMangoldt_eq_\n  deriv_riemannZeta_div (\u2212\u03b6\u2032/\u03b6 Dirichlet series), BohrMollerup\n  tendsto_log_gamma (the digamma-series seed for piece A's j \u2265 1).\n\n**(2) Piece (B) PROVED (LiZetaCoeff.lean, ~250 lines)**:\n`hLiExt s := (1 \u2212 hLi(1+s))/s` extended by \u2212deriv hLi 1 at 0 \u2014 the\nanalytic-at-0 form of 1/s + \u03b6\u2032/\u03b6(1+s):\n- `hLiExt_tendsto` (slope limit), `hLiExt_analyticAt_zero` (removable\n  singularity, the zetaA pattern), `hLiExt_mul_id` (exact global identity\n  s\u00b7hLiExt s = 1 \u2212 hLi(1+s)), `iteratedDeriv_hLi_one_add` (comp bridge via\n  iteratedDeriv_comp_sub_const at c = \u22121),\n- **`iteratedDeriv_hLiExt`**: iteratedDeriv j hLiExt 0 = \u2212(j!)\u00b7lcoeff j \u2014\n  the Taylor coefficients of 1/s + \u03b6\u2032/\u03b6(1+s) at 0 are \u2212c_j. Proof: Leibniz\n  (iteratedDeriv_mul) with the identity factor collapsing the sum to i = 1,\n  then factorial bookkeeping.\n- `hLiExt_eq_near_zero`: hLiExt s = 1/s + \u03b6\u2032/\u03b6(1+s) on \ud835\udcdd[\u2260] 0 (the\n  reading as the actual meromorphic function).\n\n## Lean notes (hard-won this session, additions to the handoff list)\n- `HasDerivAt.comp` at a composed point: write the outer hypothesis's\n  point SYNTACTICALLY as `g x` (e.g. `1 + 0`), not its reduced form \u2014\n  else the elaborator solves ?g := const.\n- `1 + 0` is NOT defeq to `1` for \u2102/\u211d (OfNat/HAdd don't compute) \u2014 nhds\n  targets need `simpa using` bridges, not `exact`.\n- `tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within`: source filter\n  stays arbitrary (\ud835\udcdd[\u2260] 0), first premise Tendsto f l (\ud835\udcdd a) \u2014 use\n  `.mono_left nhdsWithin_le_nhds`.\n- `iteratedDeriv_succ'` : iteratedDeriv (n+1) f = iteratedDeriv n (deriv f)\n  (deriv INSIDE; `iteratedDeriv_succ` is the other order).\n- `iteratedDeriv_const` : = if n = 0 then c else 0 (no side hypothesis).\n- `deriv_id'' : deriv (fun x => x) = fun x => 1` (function equality,\n  not pointwise \u2014 don't apply it to an argument).\n- `ContDiffAt \u2102 (j+1)` lives at order \u2115\u221e: the \u2191?n = \u2191j + 1 unification\n  leaves beta-redex artifacts downstream \u2014 pin iteratedDeriv_mul's\n  conclusion with an explicit type ascription (clean Finset.range (j+2)).\n- `add_eq_left : a + b = a \u2194 b = 0` (add_eq_right is the other one).\n- `iteratedDeriv_comp_sub_const m f c` produces the LAMBDA\n  fun z => f (z \u2212 c) (not the \u2218 form).\n\n## State at stop\nii\u2032-3a piece (B) COMPLETE. Remaining in ii\u2032-3a: piece (A) \u2014 the archimedean\n\u03c4-evaluation (\u03c4\u2080 via digamma_one_half; j \u2265 1 via the digamma series built\nfrom BohrMollerup's logGammaSeq + termwise derivation + the odd-m\nreindexing to lagariasA). Then ii\u2032-4 (L3+L1), ii\u2032-5 (R-bound), ii\u2032-3b\n(moments), ii\u2032-3c (assembly).\n",
  "structuredPatch": [],
  "originalFile": null
}