{
  "file_path": "D:\\Python\\Quantum\\research\\journal\\session-029.md",
  "content": "# Session 029 \u2014 2026-08-23 \u2014 ii\u2032-5e-iv COMPLETE: F entire (LiFEntire.lean)\n\n## Directive\nContinue the route per STATE.md: ii\u2032-5e-iv (D-068 \u00a74) \u2014 F entire by\nprincipal-part splits. User: \"let's work on the remaining route.\"\n\n## Outcome: 5e-iv COMPLETE (commits 58e03e2 + closure; LiFEntire.lean,\n~1130 lines, 30 decls, all audited clean: 3 standard axioms only; full\nbuild GREEN 8766 jobs, LiFEntire root-imported)\n\nThe difference function `Fexpr s := logDeriv \u03b6 s \u2212 seriesFun s + 1/s +\n1/(s\u22121) \u2212 (log \u03c0)/2 + \u03c8(s/2)/2` extends to an ENTIRE function. Since\nMathlib lacks a general removable-singularity theorem AND the pointwise\nvalues of Fexpr at the excluded points are junk (0/0-forms), the\nextension is packaged as the punctured-limit function\n`Gentire s := limUnder (\ud835\udcdd[\u2260] s) Fexpr`:\n\n- **good points** (`\u00acbadPoint s`, where badPoint = nontrivial \u2228 0 \u2228 1 \u2228\n  \u22122n): Fexpr analytic there (`Fexpr_analyticAt_of_not_bad`) \u27f9\n  continuous \u27f9 the punctured limit is the value (`gentire_eq_Fexpr`,\n  via tendsto_nhds_limUnder + tendsto_nhds_unique); and a whole ball of\n  good points exists (`exists_ball_good_of_not_bad`: the \u03b6 \u2260 0\n  continuity ball \u2229 {0,1}-avoidance) \u27f9 Gentire =\u1da0 Fexpr there \u27f9\n  analytic.\n- **bad points**: an explicit analytic witness W per case with punctured\n  agreement Fexpr =\u1da0[\ud835\udcdd[\u2260] s] W; the limUnder uniqueness gives Gentire\n  s = W s, and a small ball is bad-point-free off the center \u27f9\n  Gentire =\u1da0[\ud835\udcdd s] W (full nhd) \u27f9 analytic at s.\n\nThe four witness cases (D-068 \u00a70's residue bookkeeping verified at\neach):\n- **nontrivial \u03c1\u2080** (`Fexpr_eventually_nontrivial`): the NF witness\n  `logDeriv_zeta_sub_mult_div_eventually` (the LiSides NF block:\n  logDeriv \u03b6 \u2212 m/(s\u2212\u03c1\u2080) =\u1da0 logDeriv h punctured, h the order normal\n  form factor) + 5e-iii's `seriesFun_sub_polar_analyticAt`; the\n  elementary terms analytic since re \u03c1\u2080 \u2208 (0, 1).\n- **s = 1** (`Fexpr_eventually_one`): logDeriv \u03b6 = logDeriv zetaA \u2212\n  1/(s\u22121) punctured (zetaA = (s\u22121)\u03b6 analytic, zetaA 1 = 1 \u2014\n  `logDeriv_zeta_eq_logDeriv_zetaA_sub`).\n- **s = 0** (`Fexpr_eventually_zero`): \u03c8(s/2)/2 + 1/s = \u2212\u03b3/2 +\n  \u00bd\u00b7digammaSeriesPart(s/2) punctured; the series part analytic on\n  ball(0, 1/2) by the M-test (`digammaSeriesPart_analyticOn`, majorant\n  1/(j+1)\u00b2); logDeriv \u03b6 analytic at 0 (\u03b6(0) = \u22121/2).\n- **s = \u22122n** (`Fexpr_eventually_neg_two_mul`): logDeriv \u03b6 \u2212 1/(s+2n)\n  analytic (NF + `zeroMult_neg_two_mul` via the new\n  `riemannZeta_neg_two_mul`); \u03c8(s/2)/2 + 1/(s+2n) = \u00bd\u00b7H_n(s/2)\n  punctured where H_n = the digamma series with the j = n\u22121 term\n  dropped (`digammaSeriesPartSub`, analytic on ball(\u2212n, 1/2) by the\n  eventually M-test, majorant (2n+1)/(j+1)\u00b2 for j \u2265 2n+1;\n  `digammaSeriesPart_eq_sub_add_single` the tsum split).\n\nSupporting infrastructure:\n- `analyticAt_digamma`: \u03c8 analytic off {0} \u222a \u2212\u2115 (finite-min avoiding\n  ball; \u0393 differentiable + nonzero there; DifferentiableOn \u2192\n  analyticOnNhd \u2192 the deriv/div form of logDeriv \u0393).\n- `zeta_zero_classification`: every zero of \u03b6 is nontrivial, 0, or \u22122n\n  (re \u2265 1 by Mathlib's one_le_re nonvanishing; re \u2264 0 by\n  Gamma\u211d_eq_zero_iff + Zeta23's completedRiemannZeta_eq_zero_iff \u2014 the\n  LiDisc argument globalized).\n\n**Capstone `gentire_analyticAt_and_eq`**: (\u2200 s, AnalyticAt \u2102 Gentire s)\n\u2227 (\u2200 s \u2209 bad set, Gentire s = Fexpr s) \u2014 exactly the input 5e-v needs\n(circle bound on the \u03b3-gap circles \u2014 all good points \u2014 then the\nmax-modulus squeeze \u27f9 Gentire \u2261 const =: B).\n\n## Banked gotchas (session 029 additions)\n- **AnalyticAt.comp HOU ambiguity**: `(analyticAt_digamma h).comp h1`\n  with hg : AnalyticAt \u2102 g (s/2) \u2014 the `f x` pattern unifies to the\n  WRONG solution (f := HDiv.hDiv s, x := 2). Pin f:\n  `AnalyticAt.comp (f := fun s : \u2102 => s / 2) hg h1`. And the middle\n  value must be normalized FIRST when it's a non-defeq arithmetic form\n  ((\u22122\u2191n)/2 vs \u2212\u2191n): build hg at the unreduced point via\n  `rw [show \u22122\u2191n/2 = \u2212\u2191n by ring]` inside the have, then comp.\n- **AnalyticAt.div with ascribed hg0**: `apply AnalyticAt.div\n  analyticAt_const _ (h : 0 \u2212 1 \u2260 0)` mis-unifies g (HOU on g x = 0\u22121).\n  Pin g: `(g := fun s : \u2102 => s \u2212 1)`.\n- **Pi-form defeq is reliable for exact** ((f \u2212 g) x \u2261 f x \u2212 g x via\n  Pi.sub_apply etc.) but NOT for rw-pattern matching and NOT for apply\n  conclusions involving HOU \u2014 the apply-form\n  `apply AnalyticAt.div f g h` on a lambda goal works, the raw term\n  `f.div g h` ascription to a lambda type mostly works.\n- **`Complex.norm_ofReal` does NOT exist** \u2014 it's `RCLike.norm_ofReal`\n  (\u2200-form; fine in rw). `RCLike.norm_natCast`, `RCLike.norm_ofNat` same\n  \u2200-form class. `Complex.norm_intCast` exists (\u2192 \u2124-norm; chain\n  Int.norm_eq_abs).\n- **Cast-leaf elaboration**: `((k + (n:\u2124)) : \u2102)` elaborates with the\n  coercion pushed to the LEAVES (\u2191k + \u2191\u2191n), not a single outer cast \u2014\n  the expected type propagates through +. To force one outer cast pin\n  the inner type: `(((k + (n:\u2124)) : \u2124) : \u2102)`. Same for\n  `show (k:\u2102) + ((n:\u2124):\u2102) = (((k:\u211d)+(n:\u211d)):\u2102)`-style rewrites \u2014 the\n  LHS must match the goal's atom EXACTLY (elaborated forms differ by\n  coercion insertion points). The ROBUST alternative for\n  \u2016cast-expr\u2016 bounds: `Complex.abs_re_le_norm` + a simp-computed re\n  (Complex.add_re/sub_re/mul_re + natCast_re/ofNat_re) \u2014 no norm-of-cast\n  matching needed.\n- **`ContinuousAt.eventually_ne (hg2 : g x \u2260 y)`** has {y} implicit \u2014\n  pin the result type by ascription (`have hz0 : \u2200\u1da0 w in \ud835\udcdd 0, \u03b6 w \u2260 0\n  := ...`) or the by-block's norm_num sees a metavariable.\n- **`EventuallyEq` vs raw `\u2200\u1da0`**: `Tendsto.congr'`/`AnalyticAt.congr`\n  want the EventuallyEq wrapper; a raw `\u2200\u1da0 y in l, f y = g y`\n  hypothesis is defeq but dot-notation (.symm) fails \u2014 bridge with\n  `have h' : f =\u1da0[l] g := h`. And `rw [Metric.eventually_nhds_iff_ball]`\n  does NOT see through the =\u1da0 wrapper \u2014 `show \u2200\u1da0 ...` first.\n- **`subst hye` with hye : y = s eliminated s** (the outer lemma\n  variable!) when both are locals \u2014 use `rw [hye]` on the goal instead\n  (or name the target: subst y).\n- `nhdsNE_neBot` is an @[instance] (NormedField namespace) \u2014 \ud835\udcdd[\u2260] s in\n  \u2102 is NeBot automatically; no haveI needed.\n- `simp only [if_pos h]`/`if_neg` rewrites under binders (rw can't);\n  `simp at hd` on `\u2016(1:\u2102) \u2212 0\u2016 < 1/2` needs the explicit norm_one\n  chain \u2014 prefer `rw [show \u2016(1:\u2102)\u22120\u2016 = 1 by simp] at hd; linarith`.\n- file-end convention: `end NguyenRH1` then `end` (noncomputable\n  section wraps the namespace) \u2014 confirmed again.\n\n## Status / next\nii\u2032-5e-iv COMPLETE. Next: **ii\u2032-5e-v** (D-068 \u00a75): the circle bound\n|Gentire| \u2264 C(log R_k)\u00b3 on 5e-i's \u03b3-gap circles |s| = R_k (inputs: 5c's\n\u2016\u03b6\u2032/\u03b6 \u2212 near\u2016 \u2264 100000(log|t|)\u00b2 on \u03c3 \u2208 [1/2, 7/2], 5d's left version \u2264\n200000(log|t|)\u00b2, the Dirichlet bound for re \u2265 2 (Zeta23 LSeries\nvonMangoldt), 5e-ii's digamma bounds, 5e-i's circle gaps for the series\nradial split (log R)\u00b3/c) + the difference-quotient max-modulus squeeze\n\u27f9 Gentire \u2261 Gentire 0 =: B \u27f9 the capstone \u2203 B identity. Then ii\u2032-5f\n(D-056's tight analysis \u2192 10.5/48) \u2192 ii\u2032-3b \u2192 ii\u2032-3c \u2192 ii\u2032-6 \u2192 ii\u2032-7.\n"
}

{
  "type": "create",
  "filePath": "D:\\Python\\Quantum\\research\\journal\\session-029.md",
  "content": "# Session 029 \u2014 2026-08-23 \u2014 ii\u2032-5e-iv COMPLETE: F entire (LiFEntire.lean)\n\n## Directive\nContinue the route per STATE.md: ii\u2032-5e-iv (D-068 \u00a74) \u2014 F entire by\nprincipal-part splits. User: \"let's work on the remaining route.\"\n\n## Outcome: 5e-iv COMPLETE (commits 58e03e2 + closure; LiFEntire.lean,\n~1130 lines, 30 decls, all audited clean: 3 standard axioms only; full\nbuild GREEN 8766 jobs, LiFEntire root-imported)\n\nThe difference function `Fexpr s := logDeriv \u03b6 s \u2212 seriesFun s + 1/s +\n1/(s\u22121) \u2212 (log \u03c0)/2 + \u03c8(s/2)/2` extends to an ENTIRE function. Since\nMathlib lacks a general removable-singularity theorem AND the pointwise\nvalues of Fexpr at the excluded points are junk (0/0-forms), the\nextension is packaged as the punctured-limit function\n`Gentire s := limUnder (\ud835\udcdd[\u2260] s) Fexpr`:\n\n- **good points** (`\u00acbadPoint s`, where badPoint = nontrivial \u2228 0 \u2228 1 \u2228\n  \u22122n): Fexpr analytic there (`Fexpr_analyticAt_of_not_bad`) \u27f9\n  continuous \u27f9 the punctured limit is the value (`gentire_eq_Fexpr`,\n  via tendsto_nhds_limUnder + tendsto_nhds_unique); and a whole ball of\n  good points exists (`exists_ball_good_of_not_bad`: the \u03b6 \u2260 0\n  continuity ball \u2229 {0,1}-avoidance) \u27f9 Gentire =\u1da0 Fexpr there \u27f9\n  analytic.\n- **bad points**: an explicit analytic witness W per case with punctured\n  agreement Fexpr =\u1da0[\ud835\udcdd[\u2260] s] W; the limUnder uniqueness gives Gentire\n  s = W s, and a small ball is bad-point-free off the center \u27f9\n  Gentire =\u1da0[\ud835\udcdd s] W (full nhd) \u27f9 analytic at s.\n\nThe four witness cases (D-068 \u00a70's residue bookkeeping verified at\neach):\n- **nontrivial \u03c1\u2080** (`Fexpr_eventually_nontrivial`): the NF witness\n  `logDeriv_zeta_sub_mult_div_eventually` (the LiSides NF block:\n  logDeriv \u03b6 \u2212 m/(s\u2212\u03c1\u2080) =\u1da0 logDeriv h punctured, h the order normal\n  form factor) + 5e-iii's `seriesFun_sub_polar_analyticAt`; the\n  elementary terms analytic since re \u03c1\u2080 \u2208 (0, 1).\n- **s = 1** (`Fexpr_eventually_one`): logDeriv \u03b6 = logDeriv zetaA \u2212\n  1/(s\u22121) punctured (zetaA = (s\u22121)\u03b6 analytic, zetaA 1 = 1 \u2014\n  `logDeriv_zeta_eq_logDeriv_zetaA_sub`).\n- **s = 0** (`Fexpr_eventually_zero`): \u03c8(s/2)/2 + 1/s = \u2212\u03b3/2 +\n  \u00bd\u00b7digammaSeriesPart(s/2) punctured; the series part analytic on\n  ball(0, 1/2) by the M-test (`digammaSeriesPart_analyticOn`, majorant\n  1/(j+1)\u00b2); logDeriv \u03b6 analytic at 0 (\u03b6(0) = \u22121/2).\n- **s = \u22122n** (`Fexpr_eventually_neg_two_mul`): logDeriv \u03b6 \u2212 1/(s+2n)\n  analytic (NF + `zeroMult_neg_two_mul` via the new\n  `riemannZeta_neg_two_mul`); \u03c8(s/2)/2 + 1/(s+2n) = \u00bd\u00b7H_n(s/2)\n  punctured where H_n = the digamma series with the j = n\u22121 term\n  dropped (`digammaSeriesPartSub`, analytic on ball(\u2212n, 1/2) by the\n  eventually M-test, majorant (2n+1)/(j+1)\u00b2 for j \u2265 2n+1;\n  `digammaSeriesPart_eq_sub_add_single` the tsum split).\n\nSupporting infrastructure:\n- `analyticAt_digamma`: \u03c8 analytic off {0} \u222a \u2212\u2115 (finite-min avoiding\n  ball; \u0393 differentiable + nonzero there; DifferentiableOn \u2192\n  analyticOnNhd \u2192 the deriv/div form of logDeriv \u0393).\n- `zeta_zero_classification`: every zero of \u03b6 is nontrivial, 0, or \u22122n\n  (re \u2265 1 by Mathlib's one_le_re nonvanishing; re \u2264 0 by\n  Gamma\u211d_eq_zero_iff + Zeta23's completedRiemannZeta_eq_zero_iff \u2014 the\n  LiDisc argument globalized).\n\n**Capstone `gentire_analyticAt_and_eq`**: (\u2200 s, AnalyticAt \u2102 Gentire s)\n\u2227 (\u2200 s \u2209 bad set, Gentire s = Fexpr s) \u2014 exactly the input 5e-v needs\n(circle bound on the \u03b3-gap circles \u2014 all good points \u2014 then the\nmax-modulus squeeze \u27f9 Gentire \u2261 const =: B).\n\n## Banked gotchas (session 029 additions)\n- **AnalyticAt.comp HOU ambiguity**: `(analyticAt_digamma h).comp h1`\n  with hg : AnalyticAt \u2102 g (s/2) \u2014 the `f x` pattern unifies to the\n  WRONG solution (f := HDiv.hDiv s, x := 2). Pin f:\n  `AnalyticAt.comp (f := fun s : \u2102 => s / 2) hg h1`. And the middle\n  value must be normalized FIRST when it's a non-defeq arithmetic form\n  ((\u22122\u2191n)/2 vs \u2212\u2191n): build hg at the unreduced point via\n  `rw [show \u22122\u2191n/2 = \u2212\u2191n by ring]` inside the have, then comp.\n- **AnalyticAt.div with ascribed hg0**: `apply AnalyticAt.div\n  analyticAt_const _ (h : 0 \u2212 1 \u2260 0)` mis-unifies g (HOU on g x = 0\u22121).\n  Pin g: `(g := fun s : \u2102 => s \u2212 1)`.\n- **Pi-form defeq is reliable for exact** ((f \u2212 g) x \u2261 f x \u2212 g x via\n  Pi.sub_apply etc.) but NOT for rw-pattern matching and NOT for apply\n  conclusions involving HOU \u2014 the apply-form\n  `apply AnalyticAt.div f g h` on a lambda goal works, the raw term\n  `f.div g h` ascription to a lambda type mostly works.\n- **`Complex.norm_ofReal` does NOT exist** \u2014 it's `RCLike.norm_ofReal`\n  (\u2200-form; fine in rw). `RCLike.norm_natCast`, `RCLike.norm_ofNat` same\n  \u2200-form class. `Complex.norm_intCast` exists (\u2192 \u2124-norm; chain\n  Int.norm_eq_abs).\n- **Cast-leaf elaboration**: `((k + (n:\u2124)) : \u2102)` elaborates with the\n  coercion pushed to the LEAVES (\u2191k + \u2191\u2191n), not a single outer cast \u2014\n  the expected type propagates through +. To force one outer cast pin\n  the inner type: `(((k + (n:\u2124)) : \u2124) : \u2102)`. Same for\n  `show (k:\u2102) + ((n:\u2124):\u2102) = (((k:\u211d)+(n:\u211d)):\u2102)`-style rewrites \u2014 the\n  LHS must match the goal's atom EXACTLY (elaborated forms differ by\n  coercion insertion points). The ROBUST alternative for\n  \u2016cast-expr\u2016 bounds: `Complex.abs_re_le_norm` + a simp-computed re\n  (Complex.add_re/sub_re/mul_re + natCast_re/ofNat_re) \u2014 no norm-of-cast\n  matching needed.\n- **`ContinuousAt.eventually_ne (hg2 : g x \u2260 y)`** has {y} implicit \u2014\n  pin the result type by ascription (`have hz0 : \u2200\u1da0 w in \ud835\udcdd 0, \u03b6 w \u2260 0\n  := ...`) or the by-block's norm_num sees a metavariable.\n- **`EventuallyEq` vs raw `\u2200\u1da0`**: `Tendsto.congr'`/`AnalyticAt.congr`\n  want the EventuallyEq wrapper; a raw `\u2200\u1da0 y in l, f y = g y`\n  hypothesis is defeq but dot-notation (.symm) fails \u2014 bridge with\n  `have h' : f =\u1da0[l] g := h`. And `rw [Metric.eventually_nhds_iff_ball]`\n  does NOT see through the =\u1da0 wrapper \u2014 `show \u2200\u1da0 ...` first.\n- **`subst hye` with hye : y = s eliminated s** (the outer lemma\n  variable!) when both are locals \u2014 use `rw [hye]` on the goal instead\n  (or name the target: subst y).\n- `nhdsNE_neBot` is an @[instance] (NormedField namespace) \u2014 \ud835\udcdd[\u2260] s in\n  \u2102 is NeBot automatically; no haveI needed.\n- `simp only [if_pos h]`/`if_neg` rewrites under binders (rw can't);\n  `simp at hd` on `\u2016(1:\u2102) \u2212 0\u2016 < 1/2` needs the explicit norm_one\n  chain \u2014 prefer `rw [show \u2016(1:\u2102)\u22120\u2016 = 1 by simp] at hd; linarith`.\n- file-end convention: `end NguyenRH1` then `end` (noncomputable\n  section wraps the namespace) \u2014 confirmed again.\n\n## Status / next\nii\u2032-5e-iv COMPLETE. Next: **ii\u2032-5e-v** (D-068 \u00a75): the circle bound\n|Gentire| \u2264 C(log R_k)\u00b3 on 5e-i's \u03b3-gap circles |s| = R_k (inputs: 5c's\n\u2016\u03b6\u2032/\u03b6 \u2212 near\u2016 \u2264 100000(log|t|)\u00b2 on \u03c3 \u2208 [1/2, 7/2], 5d's left version \u2264\n200000(log|t|)\u00b2, the Dirichlet bound for re \u2265 2 (Zeta23 LSeries\nvonMangoldt), 5e-ii's digamma bounds, 5e-i's circle gaps for the series\nradial split (log R)\u00b3/c) + the difference-quotient max-modulus squeeze\n\u27f9 Gentire \u2261 Gentire 0 =: B \u27f9 the capstone \u2203 B identity. Then ii\u2032-5f\n(D-056's tight analysis \u2192 10.5/48) \u2192 ii\u2032-3b \u2192 ii\u2032-3c \u2192 ii\u2032-6 \u2192 ii\u2032-7.\n",
  "structuredPatch": [],
  "originalFile": null
}