{
  "file_path": "D:\\Python\\Quantum\\research\\journal\\session-022.md",
  "content": "# Session 022 \u2014 2026-08-22 \u2014 ii\u2032-5a DESIGN (D-067) + ii\u2032-5b COMPLETE (the |\u03b6| disc bound)\n\n## Directive\nWork tier ii\u2032 sub-stage ii\u2032-5 (STATE.md NEXT ACTION): the R-bound\n(D-064 R3, D-056 A = 10.5/B\u2080 = 48) \u2014 the long pole of the remaining\nii\u2032 map. Session split into 5a (design) and 5b (the |\u03b6| polynomial\nbound), both complete. Commits: de6ab52 (5a design), ab2df3f (5b WIP1:\nB\u0303\u2082 + IBP identity), f607489 (5b complete: representation + disc bound).\n\n## ii\u2032-5a \u2014 design D-067 (route b\u2033)\nFull machinery inventory against vendored Mathlib/Zeta23 (everything\nverified live \u2014 StrongPNTPrefix's BorelCaratheodoryDeriv/\nLogOfAnalyticFunction/ZeroFactorization, ZetaBounds' Zeta0EqZeta/\nZetaUpperBnd, StirlingVert's digamma_stirling, RvM product forms).\nTWO major route decisions:\n1. **No complex Stirling for \u0393 needed.** The naive route needs\n   |\u0393(a+ib)| ~ |b|^{a\u22121/2}e^{\u2212\u03c0|b|/2} (vertical decay) for the FE-side\n   |\u03b6| bound \u2014 a heavy build. ELIMINATED by (i) keeping the disc dip\n   shallow (\u03c3 \u2265 \u22121/2) and covering it with ONE extra Euler\u2013Maclaurin\n   level (B\u0303\u2082), and (ii) reaching the left strip \u03c3 \u2208 [\u22125/2, 1/2] by\n   FE-reflection of the R-bound itself: R(s) = \u2212R(1\u2212s) + digamma\n   bracket \u2014 the zero sums cancel EXACTLY (1/(1\u2212s\u2212(1\u2212\u03c1)) = \u22121/(s\u2212\u03c1)).\n2. **No Hadamard.** (already known \u2014 disc Blaschke removal instead).\nAlso found: Zeta23's `digamma_stirling` (\u2016\u03c8(w) \u2212 log w + 1/(2w)\u2016 \u2264\n3/w.im\u00b2, re w > 0, |im| \u2265 1/2) SUBSUMES D-056's Lemma D \u2014 the digamma\nremainder never needs separate formalization.\nGeometry note: every disc covering the |\u03b3\u2212t|<1 zeros dips left of\n\u03c3 = 0 (\u221a(c\u00b2+1) > c for any center c+it) \u2014 hence the B\u0303\u2082 level is\nunavoidable; chosen R = 5/2 about 2+it.\n\n## ii\u2032-5b \u2014 LiRBound.lean COMPLETE (~640 lines, all green)\n- **b2Fun** (the periodic Bernoulli primitive (u\u00b2\u2212u)/2, u = Int.fract x):\n  periodicity (fract_add_one), range [\u22121/8, 0], continuity for FREE via\n  `ContinuousOn.comp_fract''` (endpoint-matched composition), HasDerivAt\n  (fract x \u2212 1/2) off \u2124, b2Fun = 0 at integers.\n- **integral_b1_cpow_eq** (the level-2 identity, re s > 0): per-unit-\n  interval IBP (integral_mul_deriv_eq_deriv_mul_of_hasDerivAt \u2014 the\n  ContinuousOn+Ioo-derivatives variant, exactly fitting B\u0303\u2082's corners),\n  boundary terms vanish at integers, sum to [1,N], N\u2192\u221e via\n  intervalIntegral_tendsto_integral_Ioi.\n- **hasDerivAt_b2Integral** (re s > \u22121): clone of Zeta23's\n  hasDerivAt_Zeta0Integral via hasDerivAt_integral_of_dominated_loc_of_\n  deriv_le, with \u03b5 = (\u03c3+1)/2 and bound x^{\u2212(\u03c3+3)/2}|log x| (their\n  integrable_log_over_pow).\n- **riemannZeta_eq_level2** (re s > \u22121, s \u2260 1 \u2014 in two im-region\n  variants): \u03b6(s) = 1/2 + 1/(s\u22121) \u2212 s(s+1)\u222b\u2081^\u221e B\u0303\u2082(x)x^{\u2212s\u22122}dx.\n  KEY TRICK: instead of proving {re > \u22121} \u2216 {1} connected (the\n  point-avoidance path grind), use the CONVEX regions\n  W\u00b1 = {re > \u22121, \u00b1im > 5} \u2014 convex \u27f9 preconnected, and they contain\n  every application disc (|t| \u2265 10 \u27f9 disc B(2+it, 5/2) has |im| \u2265 7.5).\n  Convexity of half-planes via `convex_Ioi.linear_preimage reCLM`.\n- **norm_riemannZeta_le_disc**: \u2016\u03b6(s)\u2016 \u2264 (3/4)|t|\u00b2 on B(2+it, 5/2),\n  |t| \u2265 10 \u2014 from the representation + \u2016\u222bB\u0303\u2082x^{\u2212s\u22122}\u2016 \u2264 (1/8)/(\u03c3+1)\n  (norm_integral_le_integral_norm + rpow integral) + norm triangle\n  bookkeeping.\nFull build GREEN (8752 jobs); axiom audit (27 decls): 3 standard axioms\nonly, no sorryAx.\n\n## Lean gotchas banked this session (additions to journal-011/019/020/021)\n- `set x := e` variables are OPAQUE to linarith (no hypothesis); keep\n  `h_def : x = e := rfl` and rewrite where needed.\n- `IntegrableOn.mono'` does not exist \u2014 use `Integrable.mono'` (work\n  directly on the restrict measure; IntegrableOn f s \u03bc IS Integrable\n  on the restrict, defeq for `exact`).\n- `IntegrableOn.congr_fun h _ measurableSet_Ioi` \u2014 use `apply` form so\n  unification instantiates the target function (refine ?_ leaves it\n  uninstantiated). And WATCH Nat casts: Zeta23's Ioi (\u21911) vs my Ioi 1 \u2014\n  `rw [Nat.cast_one]` before congr-rewrites.\n- `add_le_add_left`/`add_le_add_right` in current Mathlib: _left is the\n  RIGHT-addition form (h : b \u2264 c) (a) : b + a \u2264 c + a.\n- `Ico_mem_nhds` (not Set.Ico_mem_nhds); `natCast_floor_eq_intCast_floor`\n  is ROOT-namespace (not Nat.).\n- `ContinuousOn.comp_fract'' (h : ContinuousOn f (Icc 0 1)) (hf : f 0 = f 1)`\n  : Continuous (f \u2218 fract) \u2014 the endpoint-matching periodic-continuity\n  machine (Topology/Algebra/Order/Floor.lean).\n- `intervalIntegral.intervalIntegrable_iff'` + integrableOn_of_bounded\n  with `by fun_prop` measurability (B1 is @[fun_prop]-marked in Zeta23).\n- `hasDerivAt_ofReal_cpow_const (hx : x \u2260 0) (hr : r \u2260 0)` and the\n  continuity-only `continuousAt_ofReal_cpow_const x y (Or.inr hx0)`.\n- `HasDerivAt.congr_deriv (h) (e : f' = g')` for derivative-value\n  adjustments; `HasDerivAt.const_cpow (hf) (h0 : c \u2260 0 \u2228 f x \u2260 0)`.\n- \u2102 equations: linarith/nlinarith do NOT apply \u2014 use\n  sub_eq_zero/neg_eq_iff_eq_neg/neg_inj chains (journal-011 knew this;\n  it keeps biting in new contexts).\n- `AnalyticAt.congr (hf : AnalyticAt f x) (h : f =\u1da0[\ud835\udcdd x] g)` direction;\n  `.symm` via `EventuallyEq.symm` as a TERM.\n\n## Status\nii\u2032-5b COMPLETE (D-067 estimate ~1 sess \u2713). Next: ii\u2032-5c \u2014 the\nDavenport disc argument proper (g = \u03b6/\u220f(s\u2212\u03c1\u2096)^m\u2096, LogOfAnalyticFunction\n+ BorelCaratheodoryDeriv + the perimeter zero count + the center lower\nbound via 1/\u03b6 = \u03a3\u03bc(n)n^{\u2212s}) giving the R-bound on \u03c3 \u2208 [1/2, 7/2].\nThen 5d (FE-reflection), 5e (constants fold).\n"
}

{
  "type": "create",
  "filePath": "D:\\Python\\Quantum\\research\\journal\\session-022.md",
  "content": "# Session 022 \u2014 2026-08-22 \u2014 ii\u2032-5a DESIGN (D-067) + ii\u2032-5b COMPLETE (the |\u03b6| disc bound)\n\n## Directive\nWork tier ii\u2032 sub-stage ii\u2032-5 (STATE.md NEXT ACTION): the R-bound\n(D-064 R3, D-056 A = 10.5/B\u2080 = 48) \u2014 the long pole of the remaining\nii\u2032 map. Session split into 5a (design) and 5b (the |\u03b6| polynomial\nbound), both complete. Commits: de6ab52 (5a design), ab2df3f (5b WIP1:\nB\u0303\u2082 + IBP identity), f607489 (5b complete: representation + disc bound).\n\n## ii\u2032-5a \u2014 design D-067 (route b\u2033)\nFull machinery inventory against vendored Mathlib/Zeta23 (everything\nverified live \u2014 StrongPNTPrefix's BorelCaratheodoryDeriv/\nLogOfAnalyticFunction/ZeroFactorization, ZetaBounds' Zeta0EqZeta/\nZetaUpperBnd, StirlingVert's digamma_stirling, RvM product forms).\nTWO major route decisions:\n1. **No complex Stirling for \u0393 needed.** The naive route needs\n   |\u0393(a+ib)| ~ |b|^{a\u22121/2}e^{\u2212\u03c0|b|/2} (vertical decay) for the FE-side\n   |\u03b6| bound \u2014 a heavy build. ELIMINATED by (i) keeping the disc dip\n   shallow (\u03c3 \u2265 \u22121/2) and covering it with ONE extra Euler\u2013Maclaurin\n   level (B\u0303\u2082), and (ii) reaching the left strip \u03c3 \u2208 [\u22125/2, 1/2] by\n   FE-reflection of the R-bound itself: R(s) = \u2212R(1\u2212s) + digamma\n   bracket \u2014 the zero sums cancel EXACTLY (1/(1\u2212s\u2212(1\u2212\u03c1)) = \u22121/(s\u2212\u03c1)).\n2. **No Hadamard.** (already known \u2014 disc Blaschke removal instead).\nAlso found: Zeta23's `digamma_stirling` (\u2016\u03c8(w) \u2212 log w + 1/(2w)\u2016 \u2264\n3/w.im\u00b2, re w > 0, |im| \u2265 1/2) SUBSUMES D-056's Lemma D \u2014 the digamma\nremainder never needs separate formalization.\nGeometry note: every disc covering the |\u03b3\u2212t|<1 zeros dips left of\n\u03c3 = 0 (\u221a(c\u00b2+1) > c for any center c+it) \u2014 hence the B\u0303\u2082 level is\nunavoidable; chosen R = 5/2 about 2+it.\n\n## ii\u2032-5b \u2014 LiRBound.lean COMPLETE (~640 lines, all green)\n- **b2Fun** (the periodic Bernoulli primitive (u\u00b2\u2212u)/2, u = Int.fract x):\n  periodicity (fract_add_one), range [\u22121/8, 0], continuity for FREE via\n  `ContinuousOn.comp_fract''` (endpoint-matched composition), HasDerivAt\n  (fract x \u2212 1/2) off \u2124, b2Fun = 0 at integers.\n- **integral_b1_cpow_eq** (the level-2 identity, re s > 0): per-unit-\n  interval IBP (integral_mul_deriv_eq_deriv_mul_of_hasDerivAt \u2014 the\n  ContinuousOn+Ioo-derivatives variant, exactly fitting B\u0303\u2082's corners),\n  boundary terms vanish at integers, sum to [1,N], N\u2192\u221e via\n  intervalIntegral_tendsto_integral_Ioi.\n- **hasDerivAt_b2Integral** (re s > \u22121): clone of Zeta23's\n  hasDerivAt_Zeta0Integral via hasDerivAt_integral_of_dominated_loc_of_\n  deriv_le, with \u03b5 = (\u03c3+1)/2 and bound x^{\u2212(\u03c3+3)/2}|log x| (their\n  integrable_log_over_pow).\n- **riemannZeta_eq_level2** (re s > \u22121, s \u2260 1 \u2014 in two im-region\n  variants): \u03b6(s) = 1/2 + 1/(s\u22121) \u2212 s(s+1)\u222b\u2081^\u221e B\u0303\u2082(x)x^{\u2212s\u22122}dx.\n  KEY TRICK: instead of proving {re > \u22121} \u2216 {1} connected (the\n  point-avoidance path grind), use the CONVEX regions\n  W\u00b1 = {re > \u22121, \u00b1im > 5} \u2014 convex \u27f9 preconnected, and they contain\n  every application disc (|t| \u2265 10 \u27f9 disc B(2+it, 5/2) has |im| \u2265 7.5).\n  Convexity of half-planes via `convex_Ioi.linear_preimage reCLM`.\n- **norm_riemannZeta_le_disc**: \u2016\u03b6(s)\u2016 \u2264 (3/4)|t|\u00b2 on B(2+it, 5/2),\n  |t| \u2265 10 \u2014 from the representation + \u2016\u222bB\u0303\u2082x^{\u2212s\u22122}\u2016 \u2264 (1/8)/(\u03c3+1)\n  (norm_integral_le_integral_norm + rpow integral) + norm triangle\n  bookkeeping.\nFull build GREEN (8752 jobs); axiom audit (27 decls): 3 standard axioms\nonly, no sorryAx.\n\n## Lean gotchas banked this session (additions to journal-011/019/020/021)\n- `set x := e` variables are OPAQUE to linarith (no hypothesis); keep\n  `h_def : x = e := rfl` and rewrite where needed.\n- `IntegrableOn.mono'` does not exist \u2014 use `Integrable.mono'` (work\n  directly on the restrict measure; IntegrableOn f s \u03bc IS Integrable\n  on the restrict, defeq for `exact`).\n- `IntegrableOn.congr_fun h _ measurableSet_Ioi` \u2014 use `apply` form so\n  unification instantiates the target function (refine ?_ leaves it\n  uninstantiated). And WATCH Nat casts: Zeta23's Ioi (\u21911) vs my Ioi 1 \u2014\n  `rw [Nat.cast_one]` before congr-rewrites.\n- `add_le_add_left`/`add_le_add_right` in current Mathlib: _left is the\n  RIGHT-addition form (h : b \u2264 c) (a) : b + a \u2264 c + a.\n- `Ico_mem_nhds` (not Set.Ico_mem_nhds); `natCast_floor_eq_intCast_floor`\n  is ROOT-namespace (not Nat.).\n- `ContinuousOn.comp_fract'' (h : ContinuousOn f (Icc 0 1)) (hf : f 0 = f 1)`\n  : Continuous (f \u2218 fract) \u2014 the endpoint-matching periodic-continuity\n  machine (Topology/Algebra/Order/Floor.lean).\n- `intervalIntegral.intervalIntegrable_iff'` + integrableOn_of_bounded\n  with `by fun_prop` measurability (B1 is @[fun_prop]-marked in Zeta23).\n- `hasDerivAt_ofReal_cpow_const (hx : x \u2260 0) (hr : r \u2260 0)` and the\n  continuity-only `continuousAt_ofReal_cpow_const x y (Or.inr hx0)`.\n- `HasDerivAt.congr_deriv (h) (e : f' = g')` for derivative-value\n  adjustments; `HasDerivAt.const_cpow (hf) (h0 : c \u2260 0 \u2228 f x \u2260 0)`.\n- \u2102 equations: linarith/nlinarith do NOT apply \u2014 use\n  sub_eq_zero/neg_eq_iff_eq_neg/neg_inj chains (journal-011 knew this;\n  it keeps biting in new contexts).\n- `AnalyticAt.congr (hf : AnalyticAt f x) (h : f =\u1da0[\ud835\udcdd x] g)` direction;\n  `.symm` via `EventuallyEq.symm` as a TERM.\n\n## Status\nii\u2032-5b COMPLETE (D-067 estimate ~1 sess \u2713). Next: ii\u2032-5c \u2014 the\nDavenport disc argument proper (g = \u03b6/\u220f(s\u2212\u03c1\u2096)^m\u2096, LogOfAnalyticFunction\n+ BorelCaratheodoryDeriv + the perimeter zero count + the center lower\nbound via 1/\u03b6 = \u03a3\u03bc(n)n^{\u2212s}) giving the R-bound on \u03c3 \u2208 [1/2, 7/2].\nThen 5d (FE-reflection), 5e (constants fold).\n",
  "structuredPatch": [],
  "originalFile": null
}