{
  "file_path": "D:\\Python\\Quantum\\research\\derivations\\D-074-dogleg-repair.md",
  "old_string": "- 2026-08-25 (session 040): **DL-6 COMPLETE** \u2014 the direct Dirichlet\n  bound at re = 2\u221an + the IIMaj/4 V_right re-charge (LiDogLeg.lean\n  +~350 lines, restructured with DL-6 before DL-5; full build GREEN\n  8773 jobs; audit: 36 decls, 3 standard axioms only, 0 sorryAx):",
  "new_string": "- 2026-08-25 (session 040): **ii\u2032-6-a2 COMPLETE** \u2014 the Bn dog-leg\n  redefinition (the freeze-exception protocol): DogLegRight(n) def\n  (DL-5 quarter-charge form: ((\u221an+1)/2)(e^{5/2}+1)/2 + 8.38 +\n  IIMaj(n)/4 per side) + Bn redefined (the horizontal share\n  2(e\u2074+1)(7H\u0302+3.3) \u2192 2(e\u2074+1)(7H\u0302) + 2\u00b7DogLegRight(n); T = \u221an+1\n  UNCHANGED \u2014 the endpoint N\u2081 = (T\u2080\u22121)\u00b2 \u2248 9\u00d710\u00b2\u2074 PRESERVED);\n  marginTilde/marginExpanded/mK lockstep (the dog-leg charge\n  decomposes into EXISTING block shapes: \u221an-linear into mIdb's\n  coefficient +(e^{5/2}+1)/2, I_I/dog-leg IIMaj total \u00d71.5, mK\n  loses the broken 3.3, gains 16.76 \u2014 NO new chain-rule machinery);\n  the cherry-picked 4/3-bracket strengthening landed on master\n  (iimaj_bracket_bound < 4/3 + IIMaj_deriv2_lt_three, from the paused\n  wip branch, k-shift EXCLUDED); **marginTilde_convex RE-PROVED**\n  (1.5\u00b7IIMaj\u2033 < 1.5\u00b7(4/3)/(4n) = 1/(2n) strictly, with the\n  reciprocal bridge 1.5\u00b7(1/(3n)) = 1/(2n)); **base points\n  re-certified** (exp_five_halves_le e^{5/2} \u2264 12.183 via the tight\n  e\u00b3/e^{0.5} route; Bn(8e4) \u2208 [273 000, 332 000], Bn(10\u2075) \u2264 352 000\n  \u27f9 margin(8e4) \u2265 4 001 > 0, margin(8e4) \u2264 66 001 < margin(10\u2075) \u2265\n  80 501 \u2014 hbase + hbase2 hold; the doc comments carry the updated\n  certified/true values); endpoint margins E-034-validated at the\n  dog-leg constants (margin(N\u2081) = 2.458\u00d710\u00b2\u2076 at the ORIGINAL N\u2081).\n  SfBoundProp/lambda endpoints UNCHANGED. Full build GREEN (8773\n  jobs); audit: 41 decls, [propext, Classical.choice, Quot.sound]\n  only, 0 sorryAx. **THE ORIGINAL PLAN NOW RESUMES**: ii\u2032-6-c (the\n  four side bounds; horizontals = the session-038 mid-segment\n  machine + DL-5's dogLegUpper_two_sides) \u2192 ii\u2032-6-d (fold \u27f9\n  sfBoundProp) \u2192 ii\u2032-7 (closure at the ORIGINAL N\u2081 = 9\u00d710\u00b2\u2074 with the\n  paper correction note covering F-A + F-B + the F-D dog-leg repair).\n- 2026-08-25 (session 040): **DL-6 COMPLETE** \u2014 the direct Dirichlet\n  bound at re = 2\u221an + the IIMaj/4 V_right re-charge (LiDogLeg.lean\n  +~350 lines, restructured with DL-6 before DL-5; full build GREEN\n  8773 jobs; audit: 36 decls, 3 standard axioms only, 0 sorryAx):"
}

{
  "filePath": "D:\\Python\\Quantum\\research\\derivations\\D-074-dogleg-repair.md",
  "oldString": "- 2026-08-25 (session 040): **DL-6 COMPLETE** \u2014 the direct Dirichlet\n  bound at re = 2\u221an + the IIMaj/4 V_right re-charge (LiDogLeg.lean\n  +~350 lines, restructured with DL-6 before DL-5; full build GREEN\n  8773 jobs; audit: 36 decls, 3 standard axioms only, 0 sorryAx):",
  "newString": "- 2026-08-25 (session 040): **ii\u2032-6-a2 COMPLETE** \u2014 the Bn dog-leg\n  redefinition (the freeze-exception protocol): DogLegRight(n) def\n  (DL-5 quarter-charge form: ((\u221an+1)/2)(e^{5/2}+1)/2 + 8.38 +\n  IIMaj(n)/4 per side) + Bn redefined (the horizontal share\n  2(e\u2074+1)(7H\u0302+3.3) \u2192 2(e\u2074+1)(7H\u0302) + 2\u00b7DogLegRight(n); T = \u221an+1\n  UNCHANGED \u2014 the endpoint N\u2081 = (T\u2080\u22121)\u00b2 \u2248 9\u00d710\u00b2\u2074 PRESERVED);\n  marginTilde/marginExpanded/mK lockstep (the dog-leg charge\n  decomposes into EXISTING block shapes: \u221an-linear into mIdb's\n  coefficient +(e^{5/2}+1)/2, I_I/dog-leg IIMaj total \u00d71.5, mK\n  loses the broken 3.3, gains 16.76 \u2014 NO new chain-rule machinery);\n  the cherry-picked 4/3-bracket strengthening landed on master\n  (iimaj_bracket_bound < 4/3 + IIMaj_deriv2_lt_three, from the paused\n  wip branch, k-shift EXCLUDED); **marginTilde_convex RE-PROVED**\n  (1.5\u00b7IIMaj\u2033 < 1.5\u00b7(4/3)/(4n) = 1/(2n) strictly, with the\n  reciprocal bridge 1.5\u00b7(1/(3n)) = 1/(2n)); **base points\n  re-certified** (exp_five_halves_le e^{5/2} \u2264 12.183 via the tight\n  e\u00b3/e^{0.5} route; Bn(8e4) \u2208 [273 000, 332 000], Bn(10\u2075) \u2264 352 000\n  \u27f9 margin(8e4) \u2265 4 001 > 0, margin(8e4) \u2264 66 001 < margin(10\u2075) \u2265\n  80 501 \u2014 hbase + hbase2 hold; the doc comments carry the updated\n  certified/true values); endpoint margins E-034-validated at the\n  dog-leg constants (margin(N\u2081) = 2.458\u00d710\u00b2\u2076 at the ORIGINAL N\u2081).\n  SfBoundProp/lambda endpoints UNCHANGED. Full build GREEN (8773\n  jobs); audit: 41 decls, [propext, Classical.choice, Quot.sound]\n  only, 0 sorryAx. **THE ORIGINAL PLAN NOW RESUMES**: ii\u2032-6-c (the\n  four side bounds; horizontals = the session-038 mid-segment\n  machine + DL-5's dogLegUpper_two_sides) \u2192 ii\u2032-6-d (fold \u27f9\n  sfBoundProp) \u2192 ii\u2032-7 (closure at the ORIGINAL N\u2081 = 9\u00d710\u00b2\u2074 with the\n  paper correction note covering F-A + F-B + the F-D dog-leg repair).\n- 2026-08-25 (session 040): **DL-6 COMPLETE** \u2014 the direct Dirichlet\n  bound at re = 2\u221an + the IIMaj/4 V_right re-charge (LiDogLeg.lean\n  +~350 lines, restructured with DL-6 before DL-5; full build GREEN\n  8773 jobs; audit: 36 decls, 3 standard axioms only, 0 sorryAx):",
  "originalFile": "# D-074 \u2014 Zero-free dog-leg repair of the Lagarias horizontal right tail (design + progress anchor)\nDate: 2026-08-25 | Session: 040 (thread START) | Status: **DL-0 COMPLETE (E-034 ALL CHECKS PASS; A\u2013L report \u00a77) \u2014 AWAITING USER GATE before DL-1 (Lean)**\nDirective: **PROJECT_DIRECTIVE_D-074.txt** (repo root, user-authored \u2014 the\npersisted mission; \u00a719's work order = execute \u00a72\u2013\u00a711 then STOP and report\nanswers A\u2013L). This file is the in-archive design/progress anchor (the\nD-073-pattern: nothing lives only in conversation).\nEvidence: E-031 (finding), E-032 (hidden-cancellation diagnostic),\nE-033 (c-repair constants), E-034 (planned dog-leg validation).\nRelated: D-072 (Finding F-D), D-073 (the c-repair side thread \u2014 Lemma 4.1\n+ R(c) are REUSED here), D-071 (honest-Bn machinery).\n\n## 0. Mission and plan-integration (user directives 2026-08-25)\n\n**MISSION (D-074): recover the ORIGINAL finite-height endpoint\nN\u2081 = (T\u2080\u22121)\u00b2 \u2248 9\u00d710\u00b2\u2074.** Keep T_cut = \u221an (the residue cutoff, the RH\nbridge, and \u03bb_n(T_cut) are UNCHANGED); replace ONLY the broken right\nhorizontal tail [3, 2\u221an] (Finding F-D) by a zero-free dog-leg up to\nU = (3/2)\u00b7T_cut, where D-073's repaired stepping applies\n(q = e^{4/9}/2 < 1). The dog-leg rectangle lies entirely in Re w \u2265 3\n(our w-convention; Lagarias's Re(s+1) \u2265 4) \u2014 \u03b6 zero-free + no pole\nUNCONDITIONALLY, so the Cauchy deformation is exact and needs NO new\nperimeter and NO RH above T_cut.\n\n**PROTOCOL DIRECTIVES (user, same date):** (i) the plan is integrated\ninto the standard protocol (NGUYEN.md \u00a75 entry ii\u2032-6-DL + this anchor +\nindex/db registration); (ii) stop-and-go at any time without loss \u2014\ncrash-safe per NGUYEN.md \u00a78: artifacts saved IMMEDIATELY when produced,\na clean committed state at every sub-stage, this file's progress log\n(\u00a71) is the in-thread stop-and-go record, STATE.md updated LAST with an\nexplicit NEXT ACTION; (iii) when this plan completes, the ORIGINAL plan\nresumes and finishes the theorem \u2014 the return map is \u00a78 below.\n\n**BACKGROUND (established; do not re-derive):** Finding F-D (D-072 \u2014\nthe (6.12) stepping is broken at T = \u221an; both ingredient bounds sharp;\nno side-wise fix possible there). E-032 (the T = \u221an per-side claim is\nempirically TRUE via hidden cancellation but envelope-unprovable;\nmid-segment [\u22125/2, 3] honest). D-073 (the repaired stepping Lemma 4.1\n+ explicit R(c); R(1.5) = 5.94 [PROVED, elementary]; E-033 constants).\nThe session-038 honest Bn (bridge 4F, I_III (2/3)Z2) stands \u2014 D-074\nchanges ONLY the horizontal right-tail charge.\n\n**THE DESIGN (our w-convention, rectInt'_Jlag: integrand\nJlag(w) = k_n(w\u22121)\u00b7(\u2212\u03b6\u2032/\u03b6(w)), right tail w = \u03c3+iT_cut, \u03c3 \u2208 [3, 2\u221an],\nT_cut = \u221an + \u03b5 zero-avoiding).** Replace H_low (\u03c3 : 3 \u2192 2\u221an at height\nT_cut) by the dog-leg:\n- V_left (lift at \u03c3 = 3): t : T_cut \u2192 U. Kernel\n  |1+1/(2+it)|\u207f = (1+5/(4+t\u00b2))^{n/2} \u2264 e^{5/2} \u27f9 |k_n| \u2264 e^{5/2}+1;\n  |\u03b6\u2032/\u03b6(3+it)| \u2264 \u03a3\u039b(m)/m\u00b3 = \u2212\u03b6\u2032(3)/\u03b6(3) (abs. convergent, Re 3 > 1);\n  length (\u03b1\u22121)T_cut = \u221an/2 \u27f9 |V_left| \u2264 (\u221an/2)\u00b7(e^{5/2}+1)\u00b7C_zeta3,\n  C_zeta3 = 0.165 certified \u2265 \u2212\u03b6\u2032(3)/\u03b6(3) = 0.16482 (\u2248 1.07\u00b7\u221an at\n  the true constants).\n- H_high (traverse at U = (3/2)\u221an): D-073 Cor 4.2 verbatim \u2014\n  |H_high| \u2264 R(1.5) = 5.94 (geometric stepping, q = e^{4/9}/2,\n  certified e^{4/9} < 2).\n- V_right (drop at X_R = 2\u221an): kernel \u2264 e^{\u221an/2}+1,\n  |\u03b6\u2032/\u03b6| \u2264 0.57\u00b72^{\u2212(2\u221an\u22122)}, length \u221an/2 \u27f9 exponentially tiny\n  (same shape as I_I/4).\n- Total per side: |H_low| \u2264 VLeft + R(1.5) + VRight \u2248 1.07\u221an + 5.94 + \u03b5\n  by the EXACT deformation identity (Cauchy on the zero-free dog-leg\n  rectangle; orientations audited). Lower side by conjugation.\n- The mid-segment [\u22125/2, 3] at T_cut is UNTOUCHED (honest, E-032).\n\n**Key properties:** N\u2081 stays (T\u2080\u22121)\u00b2 (only T_cut enters the bridge);\nBn's dog-leg charge decomposes into C\u00b7\u221an + const + IIMaj-shaped \u03b5 \u2014\nthe SAME block shapes as the existing margin machinery (convexity\nre-proofs with coefficient edits only; the parked c = 1.5 k-shift\nbranch wip/c-1.5-margin-redo (642d47a) is NOT needed for this route\nand stays parked as the fallback). Estimated Bn impact \u2248 +2.2\u00b7\u221an\n(~700 at n = 10\u2075 vs margin ~9\u00d710\u2074; margin(N\u2081) marginally smaller but\nthe range is the full 9\u00d710\u00b2\u2074).\n\n## 1. Progress log (append one entry per sub-stage; crash-safe record)\n\n- 2026-08-25 (session 040): c = 1.5 main-line redo PAUSED by user\n  directive (goal = original N\u2081 = 9\u00d710\u00b2\u2074); WIP preserved on branch\n  wip/c-1.5-margin-redo (642d47a; resume map in its commit message).\n  PROJECT_DIRECTIVE_D-074.txt received; user protocol directives\n  (standard-protocol integration, crash-safe stop-and-go,\n  return-to-original-plan map) recorded; this anchor created;\n  NGUYEN.md \u00a75 entry ii\u2032-6-DL installed; index/db registered.\n  NEXT: DL-0 (\u00a72 coordinate audit \u2192 \u00a73 exact derivation \u2192 \u00a74 candidate\n  rational constants \u2192 \u00a75 E-034 \u2192 \u00a76 temporary fold vs N\u2081 \u2192 \u00a77 A\u2013L\n  report), per the directive \u00a719. NO Lean changes in DL-0.\n- 2026-08-25 (session 040, USER GATE APPROVED \u2192 DL-1): **DL-1\n  COMPLETE** \u2014 LiDogLeg.lean (new, ~110 lines, root-imported; full\n  build GREEN 8773 jobs; audit-session040-axioms.txt: 7 decls,\n  [propext, Classical.choice, Quot.sound] ONLY, 0 sorryAx):\n  `Jlag_differentiableAt_dogleg` (Jlag differentiable at 3 \u2264 re,\n  0 < im \u2014 \u03b6 zero-free via Mathlib riemannZeta_ne_zero_of_one_lt_re,\n  NO perimeter), `holomorphicOn_Jlag_dogleg`,\n  `rectangleIntegral_Jlag_dogleg_eq_zero` (Cauchy via\n  HolomorphicOn.vanishesOnRectangle) + the (2\u03c0i)\u207b\u00b9 form,\n  **`upper_right_horizontal_eq_dogleg`** \u2014 H(3\u2192X_R, T) =\n  H(3\u2192X_R, U) \u2212 V(X_R, T\u2192U) + V(3, T\u2192U) PROVED (the D-074 \u00a73.2 (\u2605)\n  capstone; orientations per the audit), `kFun_conj`, `Jlag_conj`\n  (conjugation machinery for the lower side). Banked: map_div needs a\n  GROUP domain (\u2102\u00d7 is not one \u2014 use map_div\u2080 for starRingEnd); rw\n  [iteratedDeriv_one] once (it rewrites both occurrences).\n- 2026-08-25 (session 040): **DL-6 COMPLETE** \u2014 the direct Dirichlet\n  bound at re = 2\u221an + the IIMaj/4 V_right re-charge (LiDogLeg.lean\n  +~350 lines, restructured with DL-6 before DL-5; full build GREEN\n  8773 jobs; audit: 36 decls, 3 standard axioms only, 0 sorryAx):\n  dirichletCX + split + tail (3^{\u2212(2\u221an\u22122)}\u00b7dirichletC2 with\n  dirichletC2 \u2264 1), `norm_logDeriv_zeta_le_dirichletCX`,\n  `norm_term_vonMangoldt_X_le_three_pow`, `dirichletCX_le`,\n  `log_nine_quarters_ge` (log(9/4) \u2265 0.8109 via the e/e^{0.1891}\n  tight route \u2014 the (1\u2212x/16)\u207b\u00b9\u2076 trick is too fat at x ~ 0.8),\n  `four_ninths_rpow_sqrt_le` ((4/9)^{\u221an} \u2264 0.164 certified),\n  `three_pow_neg_two_sqrt_sub_two_eq`, the capstone\n  **`norm_logDeriv_zeta_le_iimZeta`: \u2016\u03b6\u2032/\u03b6(2\u221an+it)\u2016 \u2264\n  0.57\u00b72^{\u2212(2\u221an\u22122)} for n \u2265 5** \u2014 the IIMaj zeta form WITHOUT\n  certifying dirichletC2 \u2264 0.57 (which needs a ~100-prime\n  partial-sum build \u2014 the antitone-integral tail is too fat at\n  K \u2264 1000) \u2014 and `vIntegral_Jlag_right_norm_le_quarter` +\n  `vIntegral_Jlag_right_le_IIMaj_quarter` (**V_right \u2264 IIMaj/4\n  EXACTLY**). **DL-5 upgraded to the quarter charge**: dogLegUpper =\n  ((\u221an+1)/2)(e^{5/2}+1)/2 + 8.38 + IIMaj(n)/4 per side (the full\n  dog-leg now totals I_I + 2\u00b7(IIMaj/4) = 1.5\u00b7IIMaj in Bn \u2014 the\n  convexity-safe coefficient: 1.5\u00b7(4/3-bracket)/(4n) = 1/(2n)\n  strictly). **E-034 re-validated at VRightBound = IIMaj/4: ALL\n  CHECKS PASS** (margins 13 160/88 911/2.458e26 \u2014 IIMaj ~ 10\u207b\u00b9\u2070\u2075\n  invisible). The D-074 analytic core is COMPLETE with NO\n  dirichletC2 \u2264 0.57 anywhere needed. Next: ii\u2032-6-a2 (the Bn\n  dog-leg redefinition + the bracket < 4/3 cherry-pick for the\n  1.5\u00b7IIMaj convexity).\n- 2026-08-25 (session 040): **DL-5 COMPLETE** \u2014 the total\n  right-horizontal bound in LiDogLeg.lean (+~210 lines; full build\n  GREEN 8773 jobs; audit: 26 decls, 3 standard axioms only, 0\n  sorryAx): **`hIntegral_Jlag_low_le_dogLegUpper`** (for n \u2265 16,\n  T \u2208 [\u221an, \u221an+1], U = (3/2)T: \u2016HIntegral (Jlag n) 3 (2\u221an) T\u2016 \u2264\n  ((\u221an+1)/2)(e^{5/2}+1)/2 + 8.38 + IIMaj/2 \u2014 the exact identity +\n  the three piece bounds, U\u2212T = T/2 accounting),\n  **`hIntegral_Jlag_low_neg_norm_le_dogLegUpper`** (the lower side by\n  conjugation: Jlag_conj + `intervalIntegral.intervalIntegral_conj` \u2014\n  the interval conj lemma is namespaced intervalIntegral.*), and\n  `dogLegUpper_two_sides`. The full dog-leg is now PROVED in Lean\n  with NO perimeter and NO assumption above T_cut. Banked: the\n  `\u2191(\u2212T)\u00b7I` vs `\u2212(\u2191T)\u00b7I` cast-form discipline (rw needs the EXACT\n  cast form `((-T : \u211d) : \u2102)`); intervalIntegral.intervalIntegral_conj\n  for the interval-level conj map (the plain integral_conj pattern\n  does not see through the interval wrapper); integral_congr goals\n  are beta-redexes (dsimp/show first). Next: ii\u2032-6-a2 (the Bn\n  dog-leg redefinition at the E-034-validated constants:\n  DogLegRight(n) = ((\u221an+1)/2)(e^{5/2}+1)/2 + 8.38 + IIMaj(n)/2 per\n  side, \u00d72 sides \u2014 margins 13 160/88 911/2.458e26 at 8e4/10\u2075/N\u2081).\n- 2026-08-25 (session 040): **DL-4 COMPLETE** \u2014 the far-right\n  vertical drop in LiDogLeg.lean (+~160 lines; full build GREEN 8773\n  jobs; audit: 23 decls, 3 standard axioms only, 0 sorryAx):\n  `kFun_right_vertical_norm_le_exp_sqrt_half_add_one` (the w = 2\u221an\n  variant of the ii\u2032-4 kernel bound: \u2016kFun n (2\u221an+it)\u2016 \u2264 e^{\u221an/2}+1\n  for n \u2265 16, t\u00b2 \u2265 n \u2014 the 4\u221an\u22121 \u2264 t\u00b2 computation) and\n  **`vIntegral_Jlag_right_norm_le`: \u2016VIntegral (Jlag n) (2\u221an) T U\u2016 \u2264\n  (U\u2212T)\u00b7(e^{\u221an/2}+1)\u00b72^{\u2212(2\u221an\u22122)}\u00b7dirichletC2** \u2014 exponentially tiny,\n  NO perimeter. **VRightBound charge decision (recorded)**: with\n  (U\u2212T) \u2264 (\u221an+1)/2 and dirichletC2 \u2264 1 the provable charge is\n  IIMaj/2 (the tight IIMaj/4 needs dirichletC2 \u2264 0.57 \u2014 same\n  documented tightening path; the fold is indifferent: IIMaj ~\n  10\u207b\u00b9\u2070\u2075). E-034 re-validated at VRightBound = IIMaj/2: ALL CHECKS\n  PASS. Banked: Real.sqrt_le_sqrt + Real.sqrt_eq_iff_eq_sq for\n  \u221a16 = 4; rw [hwid] ALONE at unfolded kFun (hwid's LHS keeps the\n  w\u22121 denominator \u2014 do NOT pre-rw hw1); the (\u00b7C2)-first/last atom\n  discipline for integral_const_mul's first-unifier. Next: DL-5 (the\n  total right-horizontal bound: upper_right_horizontal_eq_dogleg +\n  the three piece bounds + the lower side by Jlag_conj).\n- 2026-08-25 (session 040): **DL-3 COMPLETE** \u2014 the H_high stepping\n  bound in LiDogLeg.lean (+~430 lines; full build GREEN 8773 jobs;\n  audit: 21 decls, 3 standard axioms only, 0 sorryAx):\n  `norm_term_vonMangoldt_le_two_pow` + `norm_logDeriv_zeta_le_two_pow`\n  (the (6.10) halving in LSeries form: \u2016\u03b6\u2032/\u03b6(\u03c3+it)\u2016 \u2264\n  2^{\u2212(\u03c3\u22122)}\u00b7dirichletC2), `one_add_div_pow_norm_le_exp_four_ninths`\n  (the kernel envelope \u2016(1+1/((\u03c3\u22121)+iU))\u207f\u2016 \u2264 e^{(4/9)\u03c3} for \u03c3 \u2265 3,\n  n \u2264 (4/9)U\u00b2 \u2014 the (6.11) core, single-exponential form replacing\n  the unit-step geometric series), `Jlag_dogleg_norm_le_envelope`\n  (\u2016Jlag\u2016 \u2264 dirichletC2\u00b7(4e^{\u2212c\u03c3} + 4\u00b72^{\u2212\u03c3}), c = log2 \u2212 4/9 \u2014 the\n  product collapses to ONE exponential), `integral_exp_neg_le` (the\n  FTC machine \u222b\u2083^XR e^{\u2212c\u03c3}d\u03c3 \u2264 e^{\u22123c}/c), `cdog_gt` (c \u2265 0.2487,\n  d9 log 2), `exp_four_thirds_le` (e^{4/3} \u2264 3.8073, the\n  (1\u2212x/16)\u207b\u00b9\u2076 route), and the CAPSTONE\n  **`hIntegral_Jlag_dogleg_norm_le`: \u2016HIntegral (Jlag n) 3 XR U\u2016 \u2264\n  8.38** for 0 < U, n \u2264 (4/9)U\u00b2 (i.e. U \u2265 (3/2)\u221an), 3 \u2264 XR \u2014\n  NO perimeter. Charged 8.38 = 3.8073/(2\u00b70.2487) + 0.7214 with\n  dirichletC2 \u2264 1 (the tight R(1.5) = 5.94 needs a dirichletC2 \u2264 0.57\n  build \u2014 documented tightening path; the fold is indifferent: \u0394 \u2248\n  +2.4/side \u2248 +5 at the base points). **E-034 re-validated at the\n  Lean-charged constants (C_zeta3 = 0.5, HHigh = 8.38): ALL CHECKS\n  PASS** (margins 13 160/88 911/2.458e26 at 8e4/10\u2075/N\u2081 = 9\u00d710\u00b2\u2074;\n  fold fit 0.3986). Banked (see the full list below): the \u222b+\u222b\n  notation absorbs the second integral into the first integrand\n  (parens around EACH \u222b); field_simp's `.ne'` projection goes INSIDE\n  the bracket; Real.rpow_two; div_le_div\u2080; Real.exp_half for\n  \u221a(exp x); intervalIntegral.integral_nonneg/integral_const_mul/\n  norm_integral_le_of_norm_le(_const); rpow vs npow in LSeries terms.\n  Next: DL-4 (V_right \u2264 IIMaj/4 \u2014 the far-right vertical drop).\n- 2026-08-25 (session 040): **DL-2 COMPLETE** \u2014 the V_left bound in\n  LiDogLeg.lean (+~250 lines; full build GREEN 8773 jobs; audit\n  extended: 13 decls, 3 standard axioms only, 0 sorryAx):\n  `kFun_three_add_it_norm_le_exp_five_halves_add_one` (kernel\n  \u2016kFun n (3+it)\u2016 \u2264 e^{5/2}+1 for n \u2264 t\u00b2 \u2014 the 1+5/(4+t\u00b2)\n  computation), `dirichletC3` + `norm_term_vonMangoldt_three_le_half`\n  (termwise \u039b/n\u00b3 \u2264 (1/2)\u039b/n\u00b2) + `dirichletC3_le_half` (\u2264 1/2 via\n  dirichletC2 \u2264 1) + `norm_logDeriv_zeta_le_dirichletC3` +\n  `norm_logDeriv_zeta_le_half` (\u2016\u03b6\u2032/\u03b6 s\u2016 \u2264 1/2 for re s \u2265 3) and the\n  capstone **`vIntegral_Jlag_three_norm_le`**: \u2016VIntegral (Jlag n) 3 T\n  U\u2016 \u2264 (U\u2212T)\u00b7(e^{5/2}+1)/2 for 0 < T \u2264 U, n \u2264 T\u00b2. **CONSTANT DECISION\n  (recorded)**: C_zeta3 charged at the certified 0.5 (the termwise\n  comparison route, ~30 lines) rather than the tight 0.165/0.17\n  (~250-line prime-log certification) \u2014 the fold is indifferent\n  (margins 13 165/88 916 at the base points vs 14 419/90 317 at\n  0.165, both hugely positive; margin(N\u2081) unchanged 2.458e26); the\n  tightening path is documented in \u00a74. **E-034 re-validated at\n  C = 0.5: ALL CHECKS PASS** (slack 25\u201340\u00d7; fold fit 0.3986; margins\n  13 165/88 916/7.7e8/1.24e13/2.458e26). Banked: rpow vs npow in\n  LSeries.norm_term_eq (real exponents \u2014 Real.rpow_add/rpow_one);\n  one_div_le_one_div_of_le takes the SMALL side's positivity first;\n  Real.sqrt_pow/Real.sqrt_exp do NOT exist (use Real.sq_sqrt +\n  Real.exp_half); map_div\u2080 for starRingEnd (\u2102\u00d7 not a group). Next:\n  DL-3 (H_high stepping: the q = e^{4/9}/2 geometric decay +\n  geometric-series integral bound \u2014 D-073 Lemma 4.1/Cor 4.2 in Lean).\n- 2026-08-25 (session 040): **DL-0 COMPLETE.** \u00a72 audit (13-row\n  table; the Lean contour MATCHES the assumed geometry \u2014 Jlag n s =\n  (s/(s\u22121))\u207f\u22121\u00b7(\u2212\u03b6\u2032/\u03b6 s) confirmed, orientations CCW pinned, T_cut/\n  X_R/bridge/3.3-entry located; no STOP condition). \u00a73 exact\n  derivation (analyticity at Re \u2265 3 unconditional; the identity\n  H_low = H_high \u2212 V_right + V_left with audited orientations; the\n  three piece bounds; the \u00a710 dependency statement \u2014 nothing above\n  T_cut). \u00a74 constants (C_zeta3 = 0.165 \u2014 the hand-estimate 0.150 was\n  caught WRONG by the smoke test and corrected; e^{5/2}+1 \u2264 13.19;\n  q = 0.7798 \u2264 0.78; HHigh = 5.94; VRight = IIMaj/4). **E-034 ALL\n  CHECKS PASS** (identity exact to 2\u20135e-5; piece slack 4\u201313\u00d7;\n  fold: margins 14 419 / 90 317 / 2.458e26 at 8\u00d710\u2074 / 10\u2075 / N\u2081 =\n  9\u00d710\u00b2\u2074 \u2014 the ORIGINAL endpoint RESTORED; fold fit \u2264 0.399).\n  \u00a77 A\u2013L report written. **AWAITING USER GATE before DL-1 (Lean).**\n\n## 2. Coordinate/convention audit (directive \u00a72)\n\nAll items verified live in the Lean sources (session 040). The Lean\ncontour MATCHES the assumed geometry \u2014 no STOP condition triggered.\nThe one convention note: the Lean integrand is Jlag n s =\n(s/(s\u22121))\u207f\u22121 \u00b7 (\u2212\u03b6\u2032/\u03b6(s)) \u2014 i.e. k_n(s\u22121) with k_n(x) = (1+1/x)\u207f\u22121,\n\u03b6 evaluated at s (= Lagarias's s+1). The dog-leg region Re s \u2265 3 is\nLagarias's Re(s+1) \u2265 4. Same region, shifted names.\n\n| mathematical object | current Lean name (file:line) | shift | domain | orientation | existing lemma(s) |\n|---|---|---|---|---|---|\n| integrand | `Jlag n s = kFun n s * (-(deriv \u03b6 s / \u03b6 s))` (LiSides.lean:58) | s = w (Lagarias's s+1) | \u2102 \u2216 ({1} \u222a {\u03b6-zeros}) | \u2014 | `Jlag_differentiableAt` (needs s \u2260 1, \u03b6 s \u2260 0), LiSides:82 |\n| kernel | `kFun n s = (s/(s\u22121))\u207f \u2212 1` (LiSides.lean:55) | = k_n(s\u22121), k_n(x) = (1+1/x)\u207f\u22121 | pole order n at s = 1 | \u2014 | `kFun_differentiableAt` (s \u2260 1), LiSides:63 |\n| main rectangle corners | `rectZ T = \u22125/2 \u2212 iT`, `rectW n T = 2\u221an + iT` (LiAssembly.lean:64\u201365) | variant B | \u2014 | \u2014 | \u2014 |\n| orientation convention | `RectangleIntegral f z w = H f z.re w.re z.im \u2212 H f z.re w.re w.im + V f w.re z.im w.im \u2212 V f z.re z.im w.im`; `RectangleIntegral' = (1/(2\u03c0i))\u2022RectangleIntegral` (Zeta23 FromPNTPlus.ResidueCalcOnRectangles:52\u201359); H f x\u2081x\u2082y = \u222b_{x\u2081}^{x\u2082} f(x+yi)dx, V f x y\u2081y\u2082 = i\u222b_{y\u2081}^{y\u2082} f(x+yi)dy | \u2014 | \u2014 | CCW: bottom L\u2192R, right \u2191, top R\u2192L, left \u2193 | \u2014 |\n| upper horizontal (II) | top side: `\u2212H f z.re w.re (w.im)` | \u2014 | im = +T_cut | **R\u2192L** (x : 2\u221an \u2192 \u22125/2) | \u2014 |\n| lower horizontal (IV) | bottom side: `+H f z.re w.re (z.im)` | \u2014 | im = \u2212T_cut | **L\u2192R** (x : \u22125/2 \u2192 2\u221an) | \u2014 |\n| right vertical (I) | `+V f w.re z.im w.im` | \u2014 | re = 2\u221an | \u2191 (y : \u2212T \u2192 +T) | \u2014 |\n| left vertical (III) | `\u2212V f z.re z.im w.im` | \u2014 | re = \u22125/2 | \u2193 (y : +T \u2192 \u2212T) | \u2014 |\n| right edge X_R | `2 * Real.sqrt n` (= rectW's re) | \u2014 | 2\u221an \u2265 632 (n \u2265 10\u2075) | \u2014 | \u2014 |\n| T_cut (zero-avoiding) | the wide-pigeonhole T | \u2014 | T \u2208 [\u221an, \u221an+1] | \u2014 | `exists_zero_avoiding_T_wide` (LiContour:404): \u2203 T \u2208 [a,a+1], clearance 1/(9\u00b7\u0108\u2080(a+2)) vs zeros with im \u2208 (a\u22121, a+2), a \u2265 3 |\n| sides identity | `sf_abs_le_rectInt_add_zeroSum` (LiAssembly.lean:76) | T-window as HYPOTHESES (\u221an \u2264 T \u2264 \u221an+1 + clearance) | Sz = {nontrivial, \\|\u03b3\\| \u2264 T} \u222a {\u22122} | \u2014 | \\|Sf n\\| \u2264 \u2016RectInt\u2016 + \u2016\u03a3\u2016 |\n| bridge | `zeroSum_norm_le_four_FAlt_add_one` (LiAssembly.lean:443) | hTle : T \u2264 3\u00d710\u00b9\u00b2\u22121 hypothesis | \u2014 | \u2014 | \u2016\u03a3\u2016 \u2264 4\u00b7FAlt T + 1 (hRH) |\n| kernel, left vertical | `kFun_norm_le_two` (LiContour:449) | s.re \u2264 1/2 | \u2014 | \u2014 | \u2016kFun n s\u2016 \u2264 2 |\n| kernel, mid charge | `kFun_shift_norm_le_exp_four_add_one` (LiContour:503) | kFun n (s+1), s.re \u2264 3, n \u2264 (im s)\u00b2 | \u2014 | \u2014 | \u2264 e\u2074+1 |\n| kernel, I_I / V_right | `kFun_shift_norm_le_exp_sqrt_half_add_one` (LiContour:553) | kFun n (s+1), 2\u221an \u2264 s.re | \u2014 | \u2014 | \u2264 e^{\u221an/2}+1 |\n| right-half-plane \u03b6 bound | `norm_logDeriv_zeta_le_dirichlet` (LiCircleBound) | re s \u2265 2 | \u2014 | \u2014 | \u2016\u03b6\u2032/\u03b6 s\u2016 \u2264 `dirichletC2` := \u2211'\u2016LSeries.term \u039b 2 n\u2016 (\u2248 0.57) |\n| I_I majorant | `IIMaj n` (LiSkeleton:754) | \u2014 | \u2014 | \u2014 | Bn's I_I piece; `IIMaj_le_two_mul`, `IIMaj_nonneg` |\n| \"3.3\" entry point (BROKEN, D-072) | `Bn`/`marginTilde` horizontal share: `2 * (Real.exp 4 + 1) * (7 * Hhat T + 3.3)`, T = \u221an+1 (LiSkeleton Bn:2431, marginTilde:766, mK:1832) | \u2014 | \u2014 | \u2014 | the F-D inheritance \u2014 DL replaces ONLY this |\n| conj machinery | `riemannZeta_conj`, `isNontrivialZero_conj`, `zeroMult_conj` (LiTightR, session 036) | \u2014 | \u2014 | \u2014 | NO `Jlag_conj` lemma yet \u2014 DL-1 builds it (Jlag n (conj s) = conj (Jlag n s), short) |\n| perimeter | `ZeroCountProp`, `ZeroCountProp2`, `NoLowZeros`, `ZeroCountGlobalProp`, `MZeroProp` | \u2014 | \u2014 | \u2014 | declared (D-062 \u00a74 + session-038 additions) |\n| 2\u03c0 slack | RectangleIntegral' is (2\u03c0i)\u207b\u00b9-normalized; Bn charges the RAW side bounds (the paper's convention; the 1/(2\u03c0) is spare slack) | \u2014 | \u2014 | \u2014 | D-071 \u00a74.5 |\n\n**Dog-leg-specific consequences of the audit:**\n1. The dog-leg region [3, X_R]\u00d7[T_cut, U] has Re s \u2265 3 > 1: \u03b6\n   nonvanishing UNCONDITIONALLY (Mathlib nonvanishing for re > 1) and\n   s \u2260 1 (im \u2265 T_cut \u2265 315) \u2014 Jlag analytic on a neighborhood. No new\n   perimeter; NO pigeonhole/zero-avoidance needed at U (that is the\n   point of the design).\n2. The upper right tail [3, X_R] is traversed R\u2192L in the main contour;\n   the dog-leg pieces inherit compatible orientations (\u00a73).\n3. H_high needs kernel-ratio \u2264 e^{n/U\u00b2} \u2264 e^{4/9}: U \u2265 (3/2)\u221an \u27f9\n   U\u00b2 \u2265 (9/4)n \u2713 \u2014 the T_cut pigeonhole's +1 slack is harmless\n   (U := (3/2)\u00b7T_cut with T_cut \u2208 [\u221an, \u221an+1] \u27f9 U \u2265 1.5\u221an \u2713).\n4. The bridge/sides-identity lemmas take T_cut as a parameter with\n   explicit window hypotheses \u2014 the dog-leg does NOT touch them; Sz\n   stays {|\u03b3| \u2264 T_cut} \u222a {\u22122}.\n5. The broken \"3.3\" sits ONLY in the horizontal share of Bn/\n   marginTilde/mK \u2014 DL-0's fold replaces exactly that slot.\n\n## 3. Exact dog-leg derivation (directive \u00a7\u00a73\u20135, 9, 10)\n\n### 3.1 Analyticity (directive \u00a74) \u2014 no new perimeter\n\nOn the open neighborhood \u03a9 := {s : 2 < Re s, T_cut \u2212 1 < Im s < U + 1}\nof the closed dog-leg rectangle [3, X_R]\u00d7[T_cut, U]: (i) s \u2260 1\n(Im \u2265 T_cut \u2212 1 \u2265 314); (ii) \u03b6(s) \u2260 0 \u2014 Mathlib's nonvanishing for\n1 < Re s (the Euler-product region; UNCONDITIONAL, no perimeter);\n(iii) kFun analytic off s = 1 (`kFun_differentiableAt`); (iv)\n\u2212\u03b6\u2032/\u03b6 analytic (`analyticAt_riemannZeta` + (ii)); hence Jlag is\nanalytic on \u03a9 \u2283 [3, X_R]\u00d7[T_cut, U]. [PROVED-modulo-Lean-build \u2014\nDL-1 formalizes; analyticity content: standard + Mathlib]\n\n### 3.2 The exact deformation identity (directive \u00a75)\n\nCauchy's theorem on the dog-leg rectangle (analytic on a neighborhood,\n\u00a73.1 \u2014 zero residues, the residue-sum side is EMPTY; no perimeter):\n\n  RectangleIntegral (Jlag n) (3+iT) (X_R+iU) = 0\n\nwhich expands (the Zeta23 H/V convention, CCW) to\n\n  H(3\u2192X_R, T) \u2212 H(3\u2192X_R, U) + V(X_R, T\u2192U) \u2212 V(3, T\u2192U) = 0,\n\nwhere H(a\u2192b, y) = \u222b_a^b Jlag(\u03c3+iy) d\u03c3 and V(x, a\u2192b) = i\u222b_a^b\nJlag(x+it) dt. The main contour's upper right tail is the REVERSED\nlow segment (the top side runs R\u2192L), i.e. \u2212H(3\u2192X_R, T). Solving:\n\n  **upper right tail** = \u2212H(3\u2192X_R, T)\n    = \u2212H(3\u2192X_R, U) + V(X_R, T\u2192U) \u2212 V(3, T\u2192U)\n    = [H_high, traversed X_R\u21923 at U] + [V_right, traversed T\u2192U at X_R]\n      + [V_left, traversed U\u2192T at 3].\n\nEquivalently, in the same-direction (L\u2192R / upward) forms for bounding:\n  H(3\u2192X_R, T) = H(3\u2192X_R, U) \u2212 V(X_R, T\u2192U) + V(3, T\u2192U).   (\u2605)\n\n**INTERPRETATION (directive \u00a79, prominent):** we bound |\u222b Jlag| AFTER\nanalytic deformation \u2014 |H(3\u2192X_R, T)| \u2264 |H(3\u2192X_R, U)| + |V(X_R)| +\n|V(3)| \u2014 NOT \u222b|Jlag| along the dangerous low path (the e^{0.066\u221an}\nenvelope of F-D never enters). Finding F-D cannot be reintroduced:\nthe low-path envelope is simply abandoned, not bounded.\n\n### 3.3 The three piece bounds (directive \u00a7\u00a76\u20138)\n\n**V_left (lift at Re = 3).** For t \u2208 [T_cut, U], t\u00b2 \u2265 T_cut\u00b2 \u2265 n:\n|kFun n (3+it)| = |(3+it)/(2+it)|\u207f \u2212 1's magnitude \u2264\n((9+t\u00b2)/(4+t\u00b2))^{n/2} + 1 = (1+5/(4+t\u00b2))^{n/2} + 1 \u2264\nexp(5n/(2(4+t\u00b2))) + 1 \u2264 e^{5/2} + 1 (log(1+x) \u2264 x, 5n/(2(4+t\u00b2)) \u2264\n5/2). And |\u03b6\u2032/\u03b6(3+it)| \u2264 \u03a3_{m\u22652} \u039b(m)/m\u00b3 = \u2212\u03b6\u2032(3)/\u03b6(3) \u2264 C_zeta3\n(absolute convergence, Re = 3 > 1; termwise \u2264 the s = 3 sum \u2014 the\ndirichletC2 argument at 3). Hence\n\n  |V_left| \u2264 (U \u2212 T_cut)\u00b7(e^{5/2}+1)\u00b7C_zeta3\n            \u2264 ((\u221an+1)/2)\u00b7(e^{5/2}+1)\u00b7C_zeta3 =: VLeftBound(n),\n\nsince U \u2212 T_cut = (1/2)T_cut \u2264 (\u221an+1)/2. (True value \u2212\u03b6\u2032(3)/\u03b6(3) =\n0.16482; VLeftBound \u2248 1.09\u00b7(\u221an+1) \u2248 1.07\u00b7\u221an.)\n\n**H_high (traverse at U = (3/2)T_cut \u2265 (3/2)\u221an).** D-073 Cor 4.2\nAPPLIES VERBATIM with U in place of T: (i) kernel ratio per unit step\n\u2264 (1+1/U\u00b2)\u207f \u2264 e^{n/U\u00b2} \u2264 e^{4/9} (U\u00b2 \u2265 (9/4)n); (ii) the (6.10)\nhalving (\u03c3 \u2265 3 > 2, unconditional Dirichlet); (iii) the initial\nkernel charge e^{4n/(9+U\u00b2)} \u2264 e^{16/9} at Re(w\u22121) \u2208 [2,3]. With\nq := e^{4/9}/2 < 1 (certified, \u00a74):\n\n  |H_high| \u2264 \u222b\u2083^{X_R} |Jlag(\u03c3+iU)| d\u03c3\n            \u2264 Z\u2080\u00b7[ e^{16/9}/(4(1\u2212q)\u00b7log 2) + 1/(2\u00b7log 2) ] = R(1.5)\n            \u2264 5.94 =: HHighBound(n),\n\nZ\u2080 = |\u03b6\u2032/\u03b6(2)| charged at its certified upper edge 0.5703661 (E-033\nV1). HHighBound is n-INDEPENDENT. [D-073 Lemma 4.1 + Cor 4.2,\nPROVED elementary; constants E-033-validated]\n\n**V_right (drop at X_R = 2\u221an).** Kernel (ii\u2032-4\n`kFun_shift_norm_le_exp_sqrt_half_add_one`, t-independent):\n|kFun n (X_R+it)| \u2264 e^{\u221an/2}+1. Zeta: |\u03b6\u2032/\u03b6(X_R+it)| \u2264\n2^{\u2212(X_R\u22122)}\u00b7Z\u2080 \u2264 0.57\u00b72^{\u2212(2\u221an\u22122)} ((6.10), X_R > 2). Hence\n\n  |V_right| \u2264 ((\u221an+1)/2)\u00b7(e^{\u221an/2}+1)\u00b70.57\u00b72^{\u2212(2\u221an\u22122)}\n            =: VRightBound(n)  (= (1/4)\u00b7IIMaj(n) exactly \u2014\n            IIMaj(n) = 2(\u221an+1)(e^{\u221an/2}+1)\u00b70.57\u00b72^{\u2212(2\u221an\u22122)}).\n\n### 3.4 The total right-horizontal bound (directive \u00a79)\n\nPer side (upper; lower by conjugation \u2014 the Jlag conj identity\nJlag n (conj s) = conj (Jlag n s) from \u03b6's conj-symmetry and kFun's\nreal-coefficient form, DL-1):\n\n  |H_low| \u2264 VLeftBound(n) + HHighBound(n) + VRightBound(n)\n          =: DogLegRight(n).\n\nThe full horizontal charge in Bn becomes (both sides):\nmid [unchanged: (e\u2074+1)\u00b7(NI + 5.5\u00b7(10.5\u00b7log(T+2)+48)) per side] +\nDogLegRight(n) per side, \u00d72.\n\n### 3.5 The \u00a710 dependency statement (why N\u2081 = (T\u2080\u22121)\u00b2 survives)\n\n- Residues enclosed: determined by the OUTER rectangle at \u00b1T_cut \u2014\n  Sz = {nontrivial zeros, |\u03b3| \u2264 T_cut} \u222a {\u22122}\n  (`sf_abs_le_rectInt_add_zeroSum`, unchanged; the dog-leg is a local\n  deformation of a sub-path of the boundary and does not move the\n  outer rectangle or the residue sum).\n- \u03bb_n(T_cut): unchanged (the bridge `zeroSum_norm_le_four_FAlt_add_one`\n  with hTle : T_cut \u2264 3\u00d710\u00b9\u00b2\u22121; RHUpTo invoked ONLY through\n  T_cut \u2264 T\u2080).\n- The dog-leg pieces live at Re s \u2265 3: \u03b6 UNCONDITIONALLY zero-free\n  there (\u00a73.1) \u2014 no ZeroCountProp, no RHUpTo, no pigeonhole at U.\n- U = (3/2)T_cut may exceed T\u2080: IRRELEVANT \u2014 U enters only the\n  zero-free deformation, never the residue count or the bridge.\n- Endpoint: n \u2264 (T\u2080\u22121)\u00b2 \u27f9 T_cut \u2264 \u221an+1 \u2264 T\u2080 \u2713 \u2014 the session-038\n  bridge condition verbatim. **No assumption requires information\n  above T_cut.** The design preserves the endpoint: N\u2081 = (T\u2080\u22121)\u00b2 \u2248\n  9\u00d710\u00b2\u2074.\n\n## 4. Candidate rational constants (directive \u00a7\u00a76\u20138)\n\nAll certifiable by the LiBasePoints machinery (rational interval\nbounds; NO floats into Lean):\n\n| constant | value | certification route |\n|---|---|---|\n| C_zeta3 | \u2265 \u2212\u03b6\u2032(3)/\u03b6(3) = 0.16482268\u2026 \u2192 charge **0.165** (first hand-estimate 0.150 was WRONG \u2014 series truncated early; caught by the E-034 smoke test) | Dirichlet partial sum \u03a3_{m\u2264K} \u039b(m)/m\u00b3 + certified tail (2\u00b7log(K\u22121)+1)/(4(K\u22121)\u00b2) (E-034 V1: partial 0.1648226814 + tail 8.5e-9) |\n| e^{5/2}+1 | \u2264 **13.19** | e\u00b2\u00b7e^{1/2} \u2264 7.3891\u00b71.6488 = 12.185 \u2192 12.19 (+1); d9-rational route |\n| e^{4/9} | \u2264 **1.56** (< 2 \u2014 the q-condition) | e^{4/9} = e/e^{5/9}: e \u2264 2.7183, e^{5/9} \u2265 \u03a3\u2080\u2077(0.5556\u2071/i!) \u2265 1.7430 \u27f9 \u2264 1.5596 \u2192 1.56 |\n| q = e^{4/9}/2 | \u2264 **0.78** (< 1) | from the e^{4/9} bound |\n| Z\u2080 = \\|\u03b6\u2032/\u03b6(2)\\| | \u2264 **0.5703661** | E-033 V1's certified upper edge (already charged) |\n| VLeftBound(n) | ((\u221an+1)/2)\u00b713.19\u00b70.165 \u2248 1.088\u00b7(\u221an+1) | the assembled explicit form |\n| HHighBound(n) | **5.94** | D-073 R(1.5) charged (E-033: 5.93924) |\n| VRightBound(n) | (1/4)\u00b7IIMaj(n) | exact identity with IIMaj/4 |\n| DogLegRight(n) | VLeftBound + 5.94 + IIMaj/4 \u2248 1.088\u00b7(\u221an+1) + 5.94 + \u03b5 | per side |\n\nThe Bn horizontal share (both sides) becomes:\n  2\u00b7(e\u2074+1)\u00b7[NI + 5.5\u00b7(10.5\u00b7log(T+2)+48)] + 2\u00b7DogLegRight(n)\nreplacing the broken 2\u00b7(e\u2074+1)\u00b7[NI + 5.5\u00b7(10.5\u00b7log(T+2)+48) + 3.3].\n\u0394Bn vs session-038 honest Bn \u2248 2\u00b7(1.088\u00b7(\u221an+1) + 5.94) \u2212 2(e\u2074+1)\u00b73.3\n\u2248 +2.2\u00b7\u221an \u2212 355 at 10\u2075 (i.e. \u2248 +350 at 10\u2075 against margin ~9\u00d710\u2074;\nthe fold analysis is E-034's \u00a76 job).\n\n## 3. Exact dog-leg derivation (directive \u00a7\u00a73\u20135, 9)\n\n(to be written \u2014 the deformation identity with audited orientations;\nthe analyticity statement (no new perimeter); the prominent\n\"bound |\u222b| after deformation, NOT \u222b|\u00b7| along the low path\" note;\nV_left/H_high/V_right bounds with the exact constants; the conjugation\ntransfer; the \u00a710 dependency statement (residues/\u03bb_n(T_cut)/RHUpTo\nonly via T_cut \u2264 T\u2080).)\n\n## 4. Candidate rational constants (directive \u00a7\u00a76\u20138)\n\n(to be written \u2014 C_zeta3 (rational \u2265 \u2212\u03b6\u2032(3)/\u03b6(3)); e^{5/2}+1 certified;\ne^{4/9} < 2 certified; q = e^{4/9}/2 < 1 certified; VLeftBound(n),\nHHighBound(n), VRightBound(n) explicit forms; no floats into Lean.)\n\n## 5. E-034 numerical validation (directive \u00a711)\n\nE-034 (research/numerics/scripts/E-034-dogleg-validation.py + CSV/JSON\nsidecars, db-registered, dps 50): **ALL CHECKS PASS** (V1\u2013V6 + VA;\nsession 040). Architecture: certified-tail Dirichlet series primary\n(\u03c3 \u2265 5), mpmath (\u03c3 \u2208 [3,5) + verticals) validated against it\n(discrepancy \u2264 5.0\u00d710\u207b\u00b9\u2070); two trapezoid grids per piece\n(h-delta \u2264 5\u00d710\u207b\u2075).\n\n**V1 (C_zeta3 certified)**: \u2212\u03b6\u2032(3)/\u03b6(3) \u2208 [0.1648226814,\n0.1648226899] (partial K = 25 000 + certified tail 8.5\u00d710\u207b\u2079); charged\n0.165. [The first hand-estimate 0.150 was WRONG \u2014 caught by the smoke\ntest; recorded for honesty.]\n**V2 (kernel charge)**: e^{5/2}+1 = 13.182494 \u2264 13.19.\n**V3 (q certified)**: q = e^{4/9}/2 = 0.77981175 \u2264 0.78 < 1\n(e^{4/9} = 1.55962 < 2).\n\n**V4 (the identity is EXACT)** \u2014 |H_low \u2212 (H_high \u2212 V_right + V_left)|:\n\n| n | T_cut | U | residual | quadrature tol |\n|---|---|---|---|---|\n| 10\u00b3 | 31.6728 | 47.5092 | 5.0\u00d710\u207b\u2075 | 3.9\u00d710\u207b\u2074 |\n| 10\u2074 | 100.05 | 150.075 | 4.5\u00d710\u207b\u2075 | 3.5\u00d710\u207b\u2074 |\n| 10\u2075 | 316.6278 | 474.9417 | 2.1\u00d710\u207b\u2075 | 2.2\u00d710\u207b\u2074 |\n\n(residuals at the quadrature-convergence level \u2014 the identity holds to\nthe measured precision; H_low cross-validates E-032's independent\nvalues 7.18463/16.7016/26.2292 EXACTLY.)\n\n**V5 (piece slack)** \u2014 measured vs majorant:\n\n| n | \\|V_left\\| / VLeftBound | \\|H_high\\| / 5.94 | \\|V_right\\| / VRightBound | \\|H_low\\| / DogLegRight |\n|---|---|---|---|---|\n| 10\u00b3 | 8.01 / 35.5 (0.23) | 1.11 / 5.94 (0.19) | 2.3e-14 / 2.5e-11 | 7.19 / 41.44 (0.17) |\n| 10\u2074 | 16.98 / 109.9 (0.155) | 1.09 / 5.94 (0.18) | 1.3e-43 / 3.7e-37 | 16.7 / 115.8 (0.144) |\n| 10\u2075 | 26.0 / 345.2 (0.075) | 1.01 / 5.94 (0.17) | 2.9e-136 / 6.9e-120 | 26.23 / 351.1 (0.075) |\n\nAll ratios \u2264 1 with slack 4\u201313\u00d7 (V_right: 120+ orders). Note\n|V_left| \u2248 |H_low| itself \u2014 the lift carries the dominant share of\nthe dog-leg charge, as designed.\n\n## 6. Temporary fold vs N\u2081 (directive \u00a711 gate)\n\nThe temporary dog-leg Bn (session-038 honest Bn with the broken\n2(e\u2074+1)\u00b73.3 replaced by 2\u00b7DogLegRight(n), DogLegRight = VLeftBound +\n5.94 + IIMaj/4, NOT multiplied by the mid kernel charge):\n\n| n | Bn_DL(n) | margin_DL(n) = S_\u221e \u2212 Bn_DL + 1 |\n|---|---|---|\n| 8\u00d710\u2074 | 323 654 | **14 419** (session-038 broken charge: 14 682 \u2014 cost 263) |\n| 10\u2075 | 343 432 | **90 317** (broken: 90 653 \u2014 cost 336) |\n| 10\u2078 | 6.44\u00d710\u2076 | 7.73\u00d710\u2078 |\n| 10\u00b9\u00b2 | 8.19\u00d710\u2078 | 1.24\u00d710\u00b9\u00b3 |\n| **N\u2081 = 9\u00d710\u00b2\u2074** | 4.44\u00d710\u00b9\u2075 | **2.458\u00d710\u00b2\u2076** (the ORIGINAL endpoint) |\n\nFull fold: honest_DL(n) \u2264 Bn_DL(n) on the dense grid [8\u00d710\u2074, N\u2081] (the\nmid-segment fit NI + 5.5(10.5 log+48) \u2264 7H\u0302 is the unchanged E-030\nfit, max ratio 0.3986); margin > 0 everywhere (min on grid 14 419 at\n8\u00d710\u2074). **GATE (directive \u00a711): PASS.**\n\n## 7. DL-0 report (directive \u00a719, answers A\u2013L)\n\n**A. Is the dog-leg contour identity exact?** YES \u2014 Cauchy\ndeformation in the zero-free region; verified numerically to\n2\u20135\u00d710\u207b\u2075 (the quadrature-convergence level) at n = 10\u00b3/10\u2074/10\u2075,\ncross-validating E-032 exactly.\n**B. Is the entire deformation zero-free/unconditional?** YES \u2014\nRe s \u2265 3 > 1 (Euler-product nonvanishing, Mathlib), Im \u2265 314 (no\npole, no trivial zeros), kernel analytic off s = 1. NO perimeter, NO\npigeonhole at U.\n**C. Certified left-lift constant?** C_zeta3 = 0.165 (certified\nbracket [0.1648226814, 0.1648226899]); kernel \u2264 e^{5/2}+1 \u2264 13.19;\nVLeftBound(n) = ((\u221an+1)/2)\u00b713.19\u00b70.165 \u2248 1.088\u00b7(\u221an+1).\n**D. q at \u03b1 = 3/2?** q = e^{4/9}/2 = 0.77981175 \u2264 0.78 < 1\n(certified e^{4/9} < 2).\n**E. Certified high-horizontal bound?** HHighBound = 5.94 (D-073's\nR(1.5), E-033-charged, n-independent; measured |H_high| \u2264 1.11).\n**F. Certified far-right vertical bound?** VRightBound = IIMaj/4\n(measured 2.9\u00d710\u207b\u00b9\u00b3\u2076 at 10\u2075 \u2014 negligible at every scale).\n**G. Total horizontal charge replacing the broken 3.3?**\nDogLegRight(n) = VLeftBound + 5.94 + IIMaj/4 per side (\u2248 1.088\u00b7(\u221an+1)\n+ 5.94 + \u03b5), NOT multiplied by (e\u2074+1); the mid share\n(e\u2074+1)(NI + 5.5(10.5 log+48)) \u2264 (e\u2074+1)\u00b77H\u0302 is unchanged.\n**H. honest/Bn at n = 10\u2075, 10\u2078, 10\u00b9\u00b2, N\u2081?** margins 90 317 /\n7.73\u00d710\u2078 / 1.24\u00d710\u00b9\u00b3 / 2.458\u00d710\u00b2\u2076 \u2014 all positive; honest \u2264 Bn\neverywhere (fold fit \u2264 0.399).\n**I. New certified base-point margins?** margin(8\u00d710\u2074) = 14 419,\nmargin(10\u2075) = 90 317 (both > 0, increasing; cost vs the broken\ncharge only ~263\u2013336).\n**J. margin(N\u2081) > 0?** YES \u2014 2.458\u00d710\u00b2\u2076 at the ORIGINAL\nN\u2081 = (3\u00d710\u00b9\u00b2\u22121)\u00b2 \u2248 9\u00d710\u00b2\u2074.\n**K. Does any assumption require information above T_cut?** NO \u2014\nthe dog-leg lives entirely at Re \u2265 3 (unconditionally zero-free);\nRHUpTo only via T_cut \u2264 T\u2080; no zero-count input at U; residues and\n\u03bb_n(T_cut) unchanged.\n**L. Can the endpoint remain (T\u2080\u22121)\u00b2?** YES \u2014 restored: N\u2081 =\n(3\u00d710\u00b9\u00b2\u22121)\u00b2 \u2248 9\u00d710\u00b2\u2074 (margin 2.458\u00d710\u00b2\u2076).\n\n**DL-0 VERDICT: the design is validated on every directive gate.**\nAwaiting the USER GATE before DL-1 (Lean: dog-leg analyticity + the\nexact deformation identity).\n\n## 8. RETURN TO THE ORIGINAL PLAN (after D-074 completes)\n\nThis thread REPLACES the horizontal right-tail piece of ii\u2032-6-c; it\ndoes not fork the main line. On completion (DL-5 + ii\u2032-6-a2 done):\n1. **ii\u2032-6-a2** (Bn dog-leg redefinition, the freeze-exception\n   protocol: honest Bn with horizontalRightDoglegBound(n) explicit;\n   D-074/E-034 documentation; marginTilde_convex re-proof\n   (coefficient-level \u2014 same block shapes); base-point\n   re-certification; endpoint margins at N\u2081 = (T\u2080\u22121)\u00b2; git history\n   preserved; paper-correction queue; full axiom audit).\n2. **ii\u2032-6-c** (the four side bounds): horizontals =\n   mid-segment-integral machine (unchanged, session-038 design) +\n   the DL-5 dog-leg bound; other three sides unchanged (ii\u2032-4 kernel\n   bounds, 5f tight R-bound, M\u2080, I_I).\n3. **ii\u2032-6-d** (the fold \u27f9 `sfBoundProp : SfBoundProp`).\n4. **ii\u2032-7** (closure): `lambda_pos_finite_height_closed` at the\n   ORIGINAL N\u2081 = (3\u00d710\u00b9\u00b2\u22121)\u00b2 \u2248 9\u00d710\u00b2\u2074 (3 perimeter hypotheses only);\n   full axiom audit; Paper A correction note (F-A both-signs factor +\n   F-B two-unit count + the F-D dog-leg repair; the N\u2081 headline is\n   UNCHANGED from the pre-F-D paper); archive closure + errata\n   pointers. Success criterion #3 restored at the original range.\nFallbacks if D-074 fails its gates: (a) the c = 1.5 global repair\n(branch wip/c-1.5-margin-redo, N\u2081 = 4\u00d710\u00b2\u2074); (b) c = 2 (N\u2081 =\n2.25\u00d710\u00b2\u2074); (c) the T = \u221an hidden-cancellation open question\n(D-073 \u00a78 D4, research-level).\n",
  "structuredPatch": [
    {
      "oldStart": 96,
      "oldLines": 6,
      "newStart": 96,
      "newLines": 34,
      "lines": [
        "   (conjugation machinery for the lower side). Banked: map_div needs a",
        "   GROUP domain (\u2102\u00d7 is not one \u2014 use map_div\u2080 for starRingEnd); rw",
        "   [iteratedDeriv_one] once (it rewrites both occurrences).",
        "+- 2026-08-25 (session 040): **ii\u2032-6-a2 COMPLETE** \u2014 the Bn dog-leg",
        "+  redefinition (the freeze-exception protocol): DogLegRight(n) def",
        "+  (DL-5 quarter-charge form: ((\u221an+1)/2)(e^{5/2}+1)/2 + 8.38 +",
        "+  IIMaj(n)/4 per side) + Bn redefined (the horizontal share",
        "+  2(e\u2074+1)(7H\u0302+3.3) \u2192 2(e\u2074+1)(7H\u0302) + 2\u00b7DogLegRight(n); T = \u221an+1",
        "+  UNCHANGED \u2014 the endpoint N\u2081 = (T\u2080\u22121)\u00b2 \u2248 9\u00d710\u00b2\u2074 PRESERVED);",
        "+  marginTilde/marginExpanded/mK lockstep (the dog-leg charge",
        "+  decomposes into EXISTING block shapes: \u221an-linear into mIdb's",
        "+  coefficient +(e^{5/2}+1)/2, I_I/dog-leg IIMaj total \u00d71.5, mK",
        "+  loses the broken 3.3, gains 16.76 \u2014 NO new chain-rule machinery);",
        "+  the cherry-picked 4/3-bracket strengthening landed on master",
        "+  (iimaj_bracket_bound < 4/3 + IIMaj_deriv2_lt_three, from the paused",
        "+  wip branch, k-shift EXCLUDED); **marginTilde_convex RE-PROVED**",
        "+  (1.5\u00b7IIMaj\u2033 < 1.5\u00b7(4/3)/(4n) = 1/(2n) strictly, with the",
        "+  reciprocal bridge 1.5\u00b7(1/(3n)) = 1/(2n)); **base points",
        "+  re-certified** (exp_five_halves_le e^{5/2} \u2264 12.183 via the tight",
        "+  e\u00b3/e^{0.5} route; Bn(8e4) \u2208 [273 000, 332 000], Bn(10\u2075) \u2264 352 000",
        "+  \u27f9 margin(8e4) \u2265 4 001 > 0, margin(8e4) \u2264 66 001 < margin(10\u2075) \u2265",
        "+  80 501 \u2014 hbase + hbase2 hold; the doc comments carry the updated",
        "+  certified/true values); endpoint margins E-034-validated at the",
        "+  dog-leg constants (margin(N\u2081) = 2.458\u00d710\u00b2\u2076 at the ORIGINAL N\u2081).",
        "+  SfBoundProp/lambda endpoints UNCHANGED. Full build GREEN (8773",
        "+  jobs); audit: 41 decls, [propext, Classical.choice, Quot.sound]",
        "+  only, 0 sorryAx. **THE ORIGINAL PLAN NOW RESUMES**: ii\u2032-6-c (the",
        "+  four side bounds; horizontals = the session-038 mid-segment",
        "+  machine + DL-5's dogLegUpper_two_sides) \u2192 ii\u2032-6-d (fold \u27f9",
        "+  sfBoundProp) \u2192 ii\u2032-7 (closure at the ORIGINAL N\u2081 = 9\u00d710\u00b2\u2074 with the",
        "+  paper correction note covering F-A + F-B + the F-D dog-leg repair).",
        " - 2026-08-25 (session 040): **DL-6 COMPLETE** \u2014 the direct Dirichlet",
        "   bound at re = 2\u221an + the IIMaj/4 V_right re-charge (LiDogLeg.lean",
        "   +~350 lines, restructured with DL-6 before DL-5; full build GREEN"
      ]
    }
  ],
  "userModified": false,
  "replaceAll": false
}

{
  "file_path": "D:\\Python\\Quantum\\NGUYEN.md",
  "old_string": "      \u2192 ii\u2032-6-a2 (Bn dog-leg redefinition \u2014 freeze-exception protocol:\n        honest redefinition with horizontalRightDoglegBound(n)\n        explicit; convexity re-proof; base-point re-certification;\n        endpoint margins at N\u2081 = (T\u2080\u22121)\u00b2; git history; paper-correction\n        queue; full axiom audit).",
  "new_string": "      \u2192 ii\u2032-6-a2 COMPLETE (session 040): DogLegRight def + Bn\n        redefined (horizontal share 2(e\u2074+1)(7H\u0302) + 2\u00b7DogLegRight,\n        T = \u221an+1 UNCHANGED \u2014 N\u2081 = (T\u2080\u22121)\u00b2 \u2248 9\u00d710\u00b2\u2074 PRESERVED);\n        margin lockstep at coefficient level; 4/3-bracket strengthening\n        cherry-picked onto master (e11ad95); marginTilde_convex\n        re-proved (1.5\u00b7IIMaj, strict); base points re-certified\n        (Bn(8e4) \u2208 [273k, 332k], Bn(10\u2075) \u2264 352k \u27f9 margin(8e4) \u2265\n        4 001, hbase2 66 001 < 80 501); endpoints UNCHANGED; build\n        GREEN (8773 jobs); audit: 41 decls, 3 standard axioms, 0 sorryAx.\n      THEN THE ORIGINAL PLAN RESUMES (D-074 \u00a78 return map): ii\u2032-6-c\n      (four side bounds with the repaired horizontal) \u2192 ii\u2032-6-d\n      (fold \u27f9 sfBoundProp) \u2192 ii\u2032-7 (closure at the ORIGINAL N\u2081)."
}

{
  "filePath": "D:\\Python\\Quantum\\NGUYEN.md",
  "oldString": "      \u2192 ii\u2032-6-a2 (Bn dog-leg redefinition \u2014 freeze-exception protocol:\n        honest redefinition with horizontalRightDoglegBound(n)\n        explicit; convexity re-proof; base-point re-certification;\n        endpoint margins at N\u2081 = (T\u2080\u22121)\u00b2; git history; paper-correction\n        queue; full axiom audit).",
  "newString": "      \u2192 ii\u2032-6-a2 COMPLETE (session 040): DogLegRight def + Bn\n        redefined (horizontal share 2(e\u2074+1)(7H\u0302) + 2\u00b7DogLegRight,\n        T = \u221an+1 UNCHANGED \u2014 N\u2081 = (T\u2080\u22121)\u00b2 \u2248 9\u00d710\u00b2\u2074 PRESERVED);\n        margin lockstep at coefficient level; 4/3-bracket strengthening\n        cherry-picked onto master (e11ad95); marginTilde_convex\n        re-proved (1.5\u00b7IIMaj, strict); base points re-certified\n        (Bn(8e4) \u2208 [273k, 332k], Bn(10\u2075) \u2264 352k \u27f9 margin(8e4) \u2265\n        4 001, hbase2 66 001 < 80 501); endpoints UNCHANGED; build\n        GREEN (8773 jobs); audit: 41 decls, 3 standard axioms, 0 sorryAx.\n      THEN THE ORIGINAL PLAN RESUMES (D-074 \u00a78 return map): ii\u2032-6-c\n      (four side bounds with the repaired horizontal) \u2192 ii\u2032-6-d\n      (fold \u27f9 sfBoundProp) \u2192 ii\u2032-7 (closure at the ORIGINAL N\u2081).",
  "originalFile": "# NGUYEN.md\n# ============================================================\n# PROJECT NGUYEN-RH-1 \u2014 The Riemann Hypothesis Challenge\n# Autonomous Agent Research Blueprint\n# Created: [auto-date] | Status: ACTIVE | Version: 1.0\n# ============================================================\n\n## 1. MISSION STATEMENT\nProve (or make maximal rigorous progress toward) the Riemann\nHypothesis: all nontrivial zeros of \u03b6(s) satisfy Re(s) = 1/2.\nPrimary launchpad: the Anthropic paper proving \u2265 2/3 of zeros are\nsimple and on the critical line, unconditionally.\n\n## 2. RESOURCE MANIFEST\n| ID | Resource | Contents | Use |\n|----|----------|----------|-----|\n| R1 | notes.txt | RH Wikipedia link; Physics Hypertextbook (https://physics.info/ \u2014 all physics equations); full quantum-mechanics equation list (Schr\u00f6dinger eqs, commutators, uncertainty, angular momentum, Pauli matrices, hydrogen atom, harmonic oscillator, Heisenberg picture, Ehrenfest) | Track B spectral/Hilbert\u2013P\u00f3lya modeling |\n| R2 | Anthropic Riemann Hypothesis Paper.pdf | Theorems A & B (2/3 simple+on-line, 5/6 distinct); Weil-form compression G\u0303 = P + Q; rank\u2013trace inequality; Montgomery unconditional second moment; window theory R(\u03c8); sharpness analysis \u00a77.2; Lean 4 verification | Foundation for Track A; formal infra for Track D |\n| R3 | zeta-23-lean repo (tag v1.0) | Lean 4 formalization, counting functions vs Mathlib riemannZeta | Track D |\n| R4 | Cited literature ([Mon73]\u2026[GS26]) | Full method genealogy | All tracks |\n| R5 | Python stack (mpmath, sympy, numpy, scipy) | zetazero, numerical Weil forms, SDP | Numerics |\n| R6 | Compute resources | Local: Ryzen 9 7945HX 16c/32t, 64GB, RTX 4090 Laptop 16GB (CUDA 8.9). On request (ask user first, user provisions): Lambda AI multi-GPU cloud (SSH); IBM Quantum (no identified need as of 2026-08-17 \u2014 RH compute is classical) | Scaling numerics |\n| R7 | research/resources/ atlas (43 notes) | User-provided RH-equivalence atlas, step-by-step derivations of ~60 equations: all major RH criteria (Li, Lagarias, Robin, Nyman\u2013Beurling, Redheffer, Mertens, Riesz&H\u2013L, Salem, Volchkov, Franel\u2013Landau, Speiser, de Bruijn\u2013Newman, von Koch\u2013Schoenfeld, Hilbert\u2013P\u00f3lya), zero-counting/explicit formulas, RMT statistics, foundations. Index: research/resources/index.md | All tracks; cross-pollination reservoir (\u00a74A); D-037 direct inputs |\n\n## 3. KEY KNOWNS (inherited state of the art)\n- \u2265 2/3 zeros simple & on line; \u2265 5/6 distinct [R2, unconditional].\n- Montgomery\u2013Taylor window: 0.6725 / 0.83625; window-class optimum.\n- Bandwidth-one certificate ceiling \u2248 0.682 [R2 \u00a77.2].\n- Weil positivity on all of C\u00b2_c(\u211d) \u27fa RH [Weil, Bombieri].\n- Negative index of truncated Weil form counts off-line pairs [Bom00].\n- Obstruction map: X \u226b T needs prime-pair info; higher moments need\n  Rudnick\u2013Sarnak X^k \u2264 T^{2\u2212\u03b5}; HL*(\u221e) \u27f9 100% but not RH itself.\n- Any proof must FAIL for Davenport\u2013Heilbronn / Epstein zeta\n  (sanity gate \u2014 these violate RH-analogues).\n\n## 4. ATTACK TRACKS\n- **A. Certificate extension** (moments, windows, SDP, prime pairs)\n- **B. Spectral / Hilbert\u2013P\u00f3lya** (quantum formalism from R1; Gabor\n  frame \u2194 self-adjoint operator; Berry\u2013Keating; de Branges)\n- **C. Positivity criteria** (Weil growing support, Li coefficients,\n  de Bruijn\u2013Newman \u039b = 0)\n- **D. Formal verification** (Lean 4 skeletons for every lemma)\n\n## 4A. KNOWLEDGE INTEGRATION & EXTERNAL RESEARCH (STANDING ORDER)\nGoal reminder: solve RH by COMBINING all knowledge at our disposal.\n1. **Use the full equation inventory.** Every attack must actively consider\n   the complete toolset \u2014 quantum formalism (R1), analytic number theory\n   (R2, R4), spectral theory, random matrix theory, physics equations\n   (physics.info) \u2014 and seek cross-domain combinations, never stay inside\n   a single track by default.\n2. **Cross-pollination check.** Before abandoning any approach, ask: which\n   OTHER track's machinery could close this gap? Log cross-track ideas in\n   the session journal even when not pursued.\n3. **Web research before obstruction.** When knowledge is missing, research\n   the web (arXiv, surveys, MathOverflow, LMFDB, OEIS) BEFORE declaring a\n   dead end. Record every external source used \u2014 URL, what was taken, date \u2014\n   in the derivation/result file; paper-worthy sources go to references.bib.\n4. **Master tool index.** research/derivations/D-001 (built in Phase 0.1)\n   is the living index of all usable equations/tools; every newly\n   discovered tool is added there so no later session rediscovers it.\n5. **NO-BOUNDARIES RULE (user directive, 2026-08-17).** Do not merely\n   follow what has been done. The metric is success on the ultimate goal,\n   not fidelity to any tradition. Actively import ANY domain of human\n   knowledge that could crack a wall in the obstruction map (D-006 \u00a76) \u2014\n   no field is off-limits. Candidate reservoirs to sweep systematically:\n   random matrix theory & free probability; operator theory (de Branges,\n   Krein, canonical systems); harmonic analysis (uncertainty principles,\n   restriction theory, Beurling\u2013Malliavin); mathematical physics\n   (integrable systems, quantum chaos, scattering); probability (Gaussian\n   processes, determinantal point processes); algebraic geometry & finite\n   fields (Weil's proof for curves \u2014 the ONE case RH is proven); p-adic\n   and adelic methods; ergodic theory; information theory; optimization\n   (SDP/SOS hierarchies); machine-assisted discovery. At each phase\n   boundary, run a DOMAIN SWEEP: list the current walls, ask which\n   untouched field has machinery shaped like each wall, web-research the\n   top candidates (per \u00a74A.3), and log findings in D-001 Part III \u2014\n   including negative ones (a field that provably does not apply is\n   documented progress).\n\n## 5. PROJECT PLAN & CHECKLIST\n\n\u26a0 THE PLAN IS NOT CONCRETE. This is research: the plan and checklist may be\nupdated, extended, reordered, or pruned at ANY time as results demand.\nNever follow the checklist at the expense of the ultimate goal \u2014 solving\nthe Riemann Hypothesis. If a promising direction appears that is not in the\nplan, the plan changes, not the direction. All plan changes are committed\nto git with a one-line rationale.\n\n### \u2705 PHASE 0 \u2014 Initialization & Ingestion (COMPLETE 2026-08-17)\n- [x] 0.1 Parse notes.txt; index all quantum equations for Track B.\n      \u2192 research/derivations/D-001 (living master tool index, Part I done)\n- [x] 0.2 Deep-read Anthropic paper; reproduce chain (1.2) line by line.\n      \u2192 D-002 (statements/notation), D-003 (zero side), D-004 (prime side),\n      D-005 (linear algebra + chain), D-006 (sharpness/ceiling + Lean)\n- [x] 0.3 Reproduce Lemma 3.2 (rank\u2013trace) proof independently.\n      \u2192 research/derivations/D-005 (all four loss-points mapped; equality case confirmed)\n- [x] 0.4 Verify R(\u03c8\u2080) = 4/3 and R(\u03c8_MT) = \u00bd + (1/\u221a2)cot(1/\u221a2) symbolically.\n      \u2192 E-001 (sympy + mpmath, 60-digit): both PASS. Caught a hand-arithmetic\n      slip in D-004 (correct: R(\u03c8_MT) = 1.32749930, 2\u2212R = 0.67250070).\n- [x] 0.5 Clone/inspect zeta-23-lean structure; confirm axiom audit.\n      \u2192 D-007 (cloned at v1.0=3635e74; static audit consistent with\n      AUDIT.md: 0 real axioms, sorries only in trusted challenge stubs;\n      full lake rebuild deferred to Track D)\n- [x] 0.6 Numerical sandbox: compute first 10\u2074 zeros; build finite G\u0303;\n        confirm tr, \u2016\u00b7\u2016\u00b2_HS, inertia predictions empirically.\n      \u2192 E-002 (10\u2074 zeros @ dps 25, all checks pass), E-003 (finite G\u0303 at\n      T=1000/2000/4000, both windows: tr\u2248N to 0.1%, HS\u00b2/N tracks R(\u03c8)\n      with O(1/L) decay as Thm 5.7 predicts, PSD confirmed). Summary: D-008.\n\n### \u2705 PHASE 1 \u2014 Master the Ceiling (Track A groundwork) (COMPLETE 2026-08-20 \u2014 decision gate 1.5/D-013: NO within current data class, Track A \u2192 monitoring mode; 1.2 closed as deferred)\n- [x] 1.1 Re-derive the bandwidth-one ceiling \u2248 0.682; identify every\n        inequality that is not tight.\n      \u2192 D-009 (ceiling re-derived from kernel-checked Lean; inventory:\n      4 chain losses, 4 ceiling losses, 3 structural gaps; zero-density\n      route RULED OUT with reason; new candidate: multiple-zero bounds\n      as extra chain constraint \u2014 not ceiling-constrained)\n- [x] 1.2 Test window families beyond C\u00b2[\u2212\u00bd,\u00bd]; SDP over certificates\n        (CGdL20 style) numerically. \u2192 CLOSED-DEFERRED by decision\n        (calibration value only; E-005 testbed already provides CMS\n        machinery; D-013 rationale)\n- [x] 1.3 Investigate third moment tr G\u0303\u00b3 paths: what fragment of\n        [Hej94, RS96] survives unconditionally?\n      \u2192 ANSWER: none usefully. D-011 (wall: availability \u03bb\u22642/k vs cap \u03bb)\n      + E-005 (model-decisive) \u2192 G-002. Moment ladder CLOSED both sides.\n- [x] 1.4 Attempt any unconditional support-(1+\u03b4) form-factor result.\n      \u2192 D-012: none exists; missing input located EXACTLY (prime pairs\n      at lag h \u2272 X/T). Literature logged (D-001 Part III).\n- [x] 1.5 DECISION GATE: is > 2/3 achievable in this framework? Document.\n      \u2192 D-013: NO within current data class; 6-wall map (W1\u2013W6);\n      necessary conditions for any fix; routes ranked. Track A \u2192\n      monitoring mode; proceed to Tracks B/C.\n- [x] 1.6 \u03be\u2032-world bandwidth-one ceiling (LawN256 analogue) (NEW,\n        2026-08-18 regroup).\n      \u2192 ANSWER: saturated. E-020b/D-030: window-class optimum for kernel\n      D\u2081 = 0.86864 to 1e-6 \u2014 the paper's quartic window IS optimal\n      (control recovers MT 1.32749930 to 1.7e-7). The perfect-square\n      node buys ~0 headroom beyond the paper's window; nothing transfers\n      to \u03be. Adversary-side LP (E-020) documented as machinery\n      limitation (finite pool can't realize the extremal adversary).\n- [x] 1.7 T4b scoping (NEW, 2026-08-18 regroup).\n      \u2192 CLOSED with rationale (D-031): the mechanism iterates formally\n      (prime polynomial degree k \u2192 k nodes; \u03be\u2033 leading-order \u2248 0.94),\n      but (i) certificates certify \u03be\u207d\u1d4f\u207e zeros only, (ii) the G-001\n      substitution symmetry caps every \u03be\u207d\u1d4f\u207e data class below 100%, so\n      the Speiser/Levinson\u2013Montgomery route to RH is closed at every\n      derivative order, (iii) cost per derivative is high. Revival\n      condition noted (\u03be-side input route or Suzuki-line need).\n\n### \ud83d\udd36 PHASE 2 \u2014 Spectral Program (Track B) (MAPPED TO EXHAUSTION at current technology, 2026-08-19 \u2014 parked: 2.2/2.3/2.5 unprioritized; live remainder: 2.9 (L1, L3/L4 skeleton) \u2192 Paper B / post-publication)\nNOTE (2026-08-18 regroup): the Suzuki finite-interval operator program\n(spawned by 3.4c) IS the live realization of this phase \u2014 Suzuki's T_a is\na canonical-system / de Branges-type construction (2.4), its Galerkin\nrealization is a validated \u27e8\u03c8|\u0124|\u03c8\u27e9 model (2.1), and Suzuki Cor 1.6 gives\nan explicit RH-equivalent convergence target (success criterion #3).\nItems 2.6\u20132.8 are the active queue; 2.2/2.3 remain open, unprioritized.\n- [~] 2.1 Map Weil form W to candidate quadratic forms \u27e8\u03c8|\u0124|\u03c8\u27e9 using\n        R1 operator formalism (self-adjointness \u27fa real spectrum \u27fa RH).\n      \u2192 PARTIAL: Suzuki A_a Galerkin = validated Weil-form operator\n      (ledger #1; E-009a/b, D-019). General \u0124 construction: open.\n- [ ] 2.2 Analyze Berry\u2013Keating \u0124 = \u00bd(x\u0302p\u0302+p\u0302x\u0302) with boundary\n        regularizations; compare counting function to N(T). (untouched)\n- [ ] 2.3 Exploit paper's Lemma 2.1 (Poisson\u2013Gabor, critical density\n        h = 2\u03c0/L, no aliasing) as a frame for an operator model. (untouched)\n- [~] 2.4 Examine de Branges space / canonical system reformulation.\n      \u2192 ACTIVE via Suzuki line: Q-S2 (\u210b(T_a) as de Branges-type space,\n      D-019); W(a,\u03b8;z) all-real zeros (Thm 1.5) + exact interlacing\n      measured (E-014 H1, E-016 F1).\n- [ ] 2.5 DECISION GATE: any genuine self-adjoint realization? Document.\n- [x] 2.6 (Q-S3c remainder) Root-cause E-016 V3 Herglotz reconstruction\n        mismatch.\n      \u2192 RESOLVED (E-016b/E-016c, D-025): TWO recon-side defects, analytic\n      side exact (V6: direct float64 vs dps-50 \u2264 4.4e-15 to y=40).\n      (i) Galerkin W has a double zero at z\u22480 (pair \u00b1i\u03b5, \u03b5~2\u20136e-9 \u2014\n      Galerkin artifact vs Thm 1.5; found by NEW winding-excess\n      diagnostic; explains D-024 F3 \"defect at the origin\"); (ii) EM\n      tail had a spurious factor y (predicts the y=20 deficit EXACTLY at\n      both a=4 and a=10). Candidates (a)/(c) refuted. V3 REPAIRED:\n      V3R 1.99e-5 (a=4), 1.46e-5 (a=10) vs 0.02 threshold. E-016 F1\u2013F4\n      stand. Remaining: small-y-weighted \u03b8-metric (folds into 2.8).\n- [x] 2.7 (Q-S3a, analytic) Prove/disprove v\u00b1(a,\u00b7) \u2192 A_\u221e^{\u22121}e^{\u00b1\u00b7} in a\n        norm that controls W on compacts.\n      \u2192 ANSWERED STRUCTURALLY (D-026, R-003, E-017/D-027): the question\n      is REPLACED by an EXACT factorization W = F\u00b7(R\u2080 + R_\u03c4),\n      F = z\u00b2\u03be/\u03be\u2032, with R\u2080 = 2e^{a+i\u03b8/2}sin(az\u2212\u03b8/2) + o(e\u1d43) closed form.\n      Cor 1.6 \u27fa (\u2605): tail R_\u03c4 cancels the sine skeleton up to a\n      zero-free remainder \u2014 a finite-interval Wiener\u2013Hopf remainder\n      estimate on the symbol \u011d = z\u207b\u00b2\u03be\u2032/\u03be (RH-gated factorization).\n      Explains ALL measured phenomenology incl. the origin double zero.\n      E-017: (\u2605) already ~99.8% complete OFF the real axis at a=4; \u03b8=\u03c0\n      preferred quantitatively (4.7% vs 6.8%); transition = cancellation\n      descending to \u211d. Open content isolated: (\u2605) on \u211d.\n- [x] 2.8 (Q-S3b, numerics) Prime-sum backend redesign \u2192 a ~ 12\u201314;\n        track \u03b8=\u03c0 zero flow; test z\u2081\u00b7a \u2248 4.5 stiff law vs limit.\n      \u2192 COMPLETE at a=12 (E-018/E-019, D-028/D-029): backend v2\n      (blockwise \u039b, e\u00b2\u2074, validated 2.2e-7) built; descent profile shows\n      (\u2605) strip-uniform (~5\u20137e-3); a=12 zero-flow: maximal lattice\n      (1145/1146), stiff law z\u2081\u00b7a = 4.495, lattice STIFFENS (gap CV \u2193),\n      origin pair persists (+2.0000 winding excess), no non-real zeros,\n      envelope stationary. NO transition at\n      a \u2264 12 \u2014 question answered; a=13+ deprioritized by evidence\n      (revivable in ~30 min via backend cache). Key structural gain\n      (D-028): the open content of Cor 1.6 is the zero set of M, not\n      its envelope. [ERRATUM 2026-08-19, D-043 \u00a7C: the \"\u03b3-proximity\n      chance-level\" claim is RETRACTED \u2014 wrong-direction metric;\n      correct metric shows quadratic positional locking ~0.65/a\u00b2.]\n- [~] 2.9 (\u2605) analytic attack (NEW, 2026-08-18; design D-034/D-035\n        complete). Resolvent-convergence route: prove v\u00b1(a)\u2192v\u00b1(\u221e) in\n        the Krein-space \u210b(T)-norm \u27f9 D_{a,\u03b8(a)} \u2192 D strong resolvent\n        (Krein formalism) \u27f9 \"Cor 1.6 \u27fa D has real spectrum\" (deliverable\n        D1, criterion-3-shaped). Wall mapped: W-1 index unknown, W-2\n        real-spectrum persistence = RH, W-3 factorization circular for\n        proofs. Sub-tasks 2.10/2.11 support.\n      \u2192 D1 COMPLETE (session 008, D-041): Theorem D1 (deficiency\n      convergence \u27fa strong resolvent convergence) stated with proof\n      skeleton; reduction \"(1.12) \u27fa spec(D) \u2282 \u211d\" assembled (\u21d2 Suzuki\n      Cor 1.6; \u21d0 via L3/L4 WH literature assembly); lemma map\n      L0\u2013L4/W1\u2013W3; limit extension identified as the \u03c0/2 one (Suzuki\n      \u00a77.2\u20137.5); D-040 \u0394-constraint formalized as necessary conditions\n      N1\u2013N3 \u2014 the \u03b8(a) flow is obligatory, target the \u03c0/2-extension.\n      Remaining: L1 (unconditional embedding), L3/L4 (WH class\n      assembly), \u03b8(a) theory (\u2192 2.12).\n- [x] 2.10 (E-022/E-022b, D-040) Spectral-measure convergence numerics\n        (D-035 D2). COMPLETE (session 008): Clark/de Branges spectral\n        measures \u03bc_a = \u03a3 (1/K_a(z_k,z_k))\u03b4_{z_k} computed for a \u2264 12\n        (V0\u2013V3 pass). Findings: mass conservation (\u2248184, a-independent);\n        coarse weak metric FLAT; **K_a(z,z) has deep valleys exactly at\n        the true \u03b3's** (\u0394(a) = 2.16\u21922.94, corr(d,log K) \u2248 +0.4) \u2014 the\n        \u03b3-information flows through the WEIGHTS, not the positions\n        (within-z-bin + shifted-null controlled); mass within \u00b10.1 of\n        \u03b3's 63%\u219272.5%; **\u0394(a) \u2248 3.33 \u2212 4.76/a SATURATES at fixed \u03b8=\u03c0**\n        \u2014 fixed-\u03b8 ceiling; consolidation (\u0394\u2192\u221e) requires the \u03b8(a) flow\n        (new constraint on 2.9-D1). \u0394(a) is now the sharp, cheap\n        convergence probe for any candidate \u03b8(a).\n- [x] 2.11 (D-038) Transition-scale lower bound from skeleton + E-019\n        data: quantify the a-scale at which (\u2605)-consistent consolidation\n        must begin (D-035 D3). [NEW 2026-08-18]\n      \u2192 COMPLETE (session 008, D-038): consolidation functional\n      R(a) = (aZ/\u03c0)e^{\u2212\u0394(a)} (validated 15% vs measured residual);\n      onset criterion \u0394\u2032(a) > 1/a; margin C(a) = \u0394 \u2212 log a decreasing\n      0.77 \u2192 0.46 (a = 4\u219212); **a* > 12**; fixed-\u03b8 consolidation\n      asymptotically IMPOSSIBLE (saturation ceiling vs log a growth).\n- [x] 2.12 (E-024, D-042) \u03b8-flow numerics. COMPLETE (session 008):\n      **\u03b8-INDEPENDENCE proved numerically** (residual spread \u2264 2.2%,\n      valley masses \u2248 1.00 for all \u03b8; only lattice phase responds) \u2014\n      the \u03b8(a) flow CANNOT drive consolidation (de Branges prediction\n      confirmed); channel closed by evidence. **Linear-K law found**:\n      K_plateau \u2248 1.9a (\u2248 (6/\u03c0)a, 5 points to 0.3%), valley floor \u2248 1\n      (mass gauge m_\u03b3 = 1) \u27f9 residual \u2192 Z/6 \u2260 0 \u2014 the family\n      equilibrates EXACTLY at the consolidation boundary (margin\n      C(a) \u2192 0.4 const). Consolidation channel relocated to Suzuki's\n      own lever: \u03bb \u2192 \u03bb_a\u207b (ground-state regime, sister conjecture\n      (1.2)) \u2192 task 2.13. [ERRATUM 2026-08-19 (D-060): the 1.9a fit /\n      Z/6 residual are superseded by D-045 \u2014 plateau K/(2a) \u2192 1\n      (measured 0.973\u20130.997), residual \u2192 Z/(2\u03c0); the equilibrium\n      conclusion is unchanged.]\n- [x] 2.13 (E-025, D-043) \u03bb-flow numerics. COMPLETE (session 008):\n      (A) **discretization floor found**: pencil bottom crosses 0 at\n      a \u2248 5.2 (h=0.01), O(h) artifact \u2192 0; true \u03bb_a unresolvable for\n      a \u2273 3 \u2014 the \u03bb\u2192\u03bb_a\u207b experiment is machinery-limited (D-019 F1's\n      cliff tail = floor, upper bounds stand). (B) \u03bb-flow RESPONSE\n      confirmed qualitatively: near-singular T \u27f9 \u0394 deepens (2.2\u21927.0 at\n      a=4), residual drops 48\u219211 \u2014 but the approached mode at a \u2265 6 is\n      the artifact mode (sister corr \u2248 0). (C) **MAJOR CORRECTION**:\n      E-019's \"\u03b3-proximity chance-level\" was a wrong-direction metric;\n      correct direction shows **quadratic positional locking\n      ~0.65/a\u00b2**, improving through a=12 (D-029 erratum). Revised\n      picture: positions lock + weights concentrate; obstruction =\n      excess-zero outflow + residual \u2192 Z/6 (linear-K equilibrium).\n      [ERRATUM 2026-08-19 (D-060): residual \u2192 Z/(2\u03c0) per D-045; the\n      obstruction conclusion is unchanged.]\n\n### \u2705 PHASE 3 \u2014 Positivity Criteria (Track C) (COMPLETE 2026-08-19 \u2014 3.1\u20133.8 all answered/closed, R-004 full tag; 3.1/3.2 closed by evidence, 3.5 fulfilled via 3.6\u20133.8)\n- [x] 3.1 Weil positivity on supports [\u2212a,a], push a beyond Yoshida.\n      \u2192 ANSWERED/CLOSED by evidence: landscape mapped (D-014);\n      E-006/D-015: positivity horizon resolution-limited at 1e-10;\n      E-007/E-007b + D-017: floor decays ~e^{\u22121.65a}; pushing further\n      needs new conditioning machinery.\n- [x] 3.2 Li coefficients \u03bb_n: numerics to n ~ 10\u2075; asymptotic attack.\n      \u2192 E-008: zero-side table certifies \u03bb_n > 0 for n \u2264 116 (explicit\n      tail bound). E-011/R-001: arithmetic side (BL Thm 2, zero-free,\n      flint Stieltjes + Arb \u03b6, dps 1000) \u03bb_n > 0 \u2200 n \u2264 2000,\n      cross-validated vs E-008; refined asymptotic ratio 1.00216 at\n      n = 2000. E-015 (session 005, detached): extended to n \u2264 3000,\n      ALL CHECKS PASS (dps 1450; \u03bb_3000 = 8617.2192; ratio 0.999845).\n      Next: asymptotic attack \u2192 task 3.5; further pushes (cost ~n\u2074:\n      n=4000 \u2248 9 h) only in support of 3.5 (e.g. ratio trend data).\n      CLOSED 2026-08-20: the n ~ 10\u2075 own-table target is superseded \u2014\n      R-004's finite verification uses our table to 3000 + external\n      Misguich\u2013Voros to 5\u00d710\u2075 (10\u00d7 overlap), and 3.5's deliverable was\n      achieved via 3.6\u20133.8 (R-004).\n- [x] 3.3 de Bruijn\u2013Newman: study heat-flow dynamics of zeros; can the\n        paper's 2/3 density constrain \u039b?\n      \u2192 ANSWER: NO \u2014 one-sided information (D-021): theorem lower-bounds\n      on-line fraction, \u039b needs an upper bound on the complex fraction;\n      plus extremal-vs-averaged (E-012: collision times span 4.5 orders,\n      two-body accurate to 4.8% vs full ODE) and asymptotic-vs-explicit.\n      Route \u2192 G-003 (do not retry with stronger density results).\n- [x] 3.4 Cross-pollinate: does 2/3-simplicity feed any criterion?\n      \u2192 ANSWER: YES \u2014 it fed the Suzuki operator line, now the live\n      spectral program. 3.4a CLOSED (D-016, scale mismatch); 3.4b floor\n      decay (D-017); 3.4c COMPLETE (Suzuki operators: D-018, E-009a/b,\n      D-019 \u2014 \u03bb_a cliff; Galerkin Weil form validated 4.5e-6; E-010/\n      D-020 lattice law). Continuation moved to Phase 2 (2.6\u20132.8) as of\n      the 2026-08-18 regroup.\n- [x] 3.5 Li-coefficient asymptotic attack (NEW, 2026-08-18 regroup).\n      \u2192 DESIGN COMPLETE (D-032/D-033, session 006 cont.7). Voros:\n      \"\u03bb_n > 0 \u2200 n \u2265 N\u2080\" \u27fa RH at ANY N\u2080 \u2014 no partial version exists.\n      ACHIEVABLE DELIVERABLE identified: EXPLICIT finite-height theorem\n      (\u03bb_n > 0 \u2200 n \u2264 N\u2081 from Lagarias Thm 6.1's bridge + Platt's\n      T\u2080 \u2248 3e12 + traced constants + finite verification) \u2014 nobody has\n      assembled this chain. Wall mapped: arithmetic-side triangle\n      bounds explode ((15/14)\u207f); the three-way cancellation IS RH.\n      Remaining work \u2192 tasks 3.6\u20133.8. COMPLETE 2026-08-19: 3.6\u20133.8 all\n      done \u2192 R-004 (finite-height theorem, ledger #6, full tag).\n- [x] 3.6 (D-036) Explicit |\u03be\u2032/\u03be| / |L\u2032/L| contour bounds for \u03b6 with\n        constants (Lagarias Lemma 6.1; Davenport Ch. 15) + explicit\n        N(T) bound (Backlund\u2013Rosser/Trudgian). [NEW 2026-08-18]\n      \u2192 COMPLETE (session 006 cont.9; D-036). I_III dominant\n      ~4.7\u221an log n first estimate; constants A = 0.9, B\u2080 = 1.0\n      MEASURED by E-021 (D-036 \u00a76 updated).\n- [x] 3.7 (E-021) Exact S_\u221e(n) computation n \u2264 10\u2074 (Lagarias\n        T-function closed forms) \u2192 explicit O(1) constant; measure true\n        |S_f(n)| curve vs the traced bound. [NEW 2026-08-18]\n      \u2192 COMPLETE (session 007, after 6-bug root-cause saga \u2014 mpmath\n      zeta ~58-digit ceiling, GAMMA_E float literal, 3\u00d7 parse-before-\n      dps, \u03c3-omission boundary (15/14)\u207f, float64 zeros; journal-007).\n      ALL CHECKS PASS: V1 \u03bb_n vs E-015 4.8e-25 (n \u2264 3000); V2\n      A = 0.9, B\u2080 = 1.0; V3 c\u2080 = \u22121/4 with exact correction 1/(24n).\n      |S_f(n)| max 13.52 at n = 3298 vs traced bound ~2280 (slack\n      ~170\u00d7). n = 10\u2074 rerun available via cache.\n- [x] 3.8 (D-037 + R-004) Assemble the finite-height theorem: N\u2081\n        explicit; finite verification table; adversarial review; tag\n        [PROVED-CONDITIONAL(computational RH-to-height-T\u2080)]. [NEW]\n      \u2192 COMPLETE (session 008; D-037, R-004, E-023 ALL CHECKS PASS).\n      **\u03bb_n > 0 for all n \u2264 N\u2081 = (T\u2080\u22121)\u00b2 \u2248 9.0\u00d710\u00b2\u2074** (T\u2080 = 3\u00d710\u00b9\u00b2\n      Platt\u2013Trudgian; conservative window N\u2081* = 2.73\u00d710\u00b2\u00b9). N\u2080 = 5\u00d710\u2074\n      (margin 67 705, convex chain); finite verification ours to 3000 +\n      Misguich\u2013Voros to 5\u00d710\u2075 (10\u00d7 overlap). D-036 |t|<10 gap found and\n      closed (M\u2080 = 1.3352). Follow-ups: D-039 (digamma sub-bound proof),\n      E-023b (acb box cover).\n\n### \u2705 PHASE 4 \u2014 Synthesis Assault (COMPLETE 2026-08-19, session 009)\n- [x] 4.1 Combine strongest partial results from Phases 1\u20133.\n      \u2192 D-052 (session 008): result inventory; T-1/T-2/T-3 final forms.\n- [x] 4.2 State best new theorem(s); classify [PROVED]/[CONDITIONAL].\n      \u2192 D-052; classifications corrected by D-054 (session 009).\n- [x] 4.3 Adversarial gauntlet: Davenport\u2013Heilbronn/Epstein sanity gate;\n        independent-instance review; error-hunting pass.\n      \u2192 4.3a D-053 (session 008): GATE PASSES structurally for T-1/T-2/T-3.\n      \u2192 4.3b D-054 (session 009): four independent review instances;\n      ALL THREE TAGS downgraded after hand-verification \u2014 D-039 proof\n      broken (bound true), D-036 \u00a71 far-sum O(|t| log t) hole\n      (reference-point trick missing), D-049 B1/B3 lower bounds broken\n      (Lemma-D 1/g\u00b2 term dropped; sinc\u00b2 factor 2), \u03b4_crit one-direction,\n      T-2 \u21d0 skeleton, D-052 accounting fixes (C1\u2013C5). Theorem\n      STATEMENTS survive (margins dwarf the gaps). Repair map opened:\n- [x] 4.5a D-056 (session 009): reference-point R-bound PROVED\n      (A = 10.5, B\u2080 = 48, honest C\u2080 incl. log log term \u2014 D-036 \u00a70\n      erratum) + digamma remainder |r| \u2264 1.2/|w|\u00b2 PROVED + I_I\n      housekeeping. E-028 ALL CHECKS PASS (26\u00d7 slack); N\u2080 = 80 000,\n      overlap 6.25\u00d7, margin(N\u2081) = 2.458e26. R-004 tag RESTORED.\n- [x] 4.5b D-057 (session 009): margin convexity PROVED (chain-rule\n      reduction \u03c6(T(n))\u2033 = \u03c8[\u03c6](T)/4n + 11-block table with elementary\n      sign arguments + I_I direct bound). E-029 ALL CHECKS PASS.\n- [x] 4.5c D-058 (session 009): valley lower bounds repaired \u2014\n      B1\u2032(i) isolated zeros clean rate PROVED; B1\u2032(ii) general via\n      node-killing projection (Gram constant + annulus count E(\u03b3,a));\n      B3\u2032 sinc\u00b2((z\u2212\u03b3)a) fix; m_\u03b3 fix (K \u2264 1/m_\u03b3); detector\n      restatement three-level (bare/pencil/carrier).\n- [x] 4.5d D-059 (session 009): bookkeeping write-ups \u2014 (1.12)\n      punctured-compact reading; R_\u03c4 := W/F \u2212 R\u2080 + distributional\n      representation; Lemma FD (form-domain identification, flat\n      bumps admissible); L1 write-up (PWS step named).\n- [x] 4.4 Numerical stress test vs known zero data.\n      \u2192 E-027 + D-055 (session 009, ALL CHECKS PASS): synthetic\n      off-line pair stress test of the T-3 detector \u2014 bare-form\n      negativity IMMEDIATE for any \u03b4 > 0 (no threshold; strict\n      Schwarz); tuned-carrier threshold \u03c0/(2a) EXACT (\u22640.9% at\n      a = 4, 8); T_a-pencil onset magnitude-limited (\u03b4 \u2248 0.11 at\n      a = 4, 0.038 at a = 8); negative directions localized at the\n      pair. D-050 erratum sharpened.\n\n### \u2b1c PHASE 5 \u2014 Verification & Write-up (Track D)\n- [~] 5.1 Lean 4 formalization of all new lemmas (build on zeta-23-lean).\n      \u2192 SKELETON STAGE COMPLETE (session 010, D-061): NguyenRH1 package\n      (research/lean/NguyenRH1/) \u2014 9 statements compile against\n      Mathlib + Zeta23 types. **TIER (i) COMPLETE (session 011)**:\n      chain_rule_sqrt_shift, sInfty_lower_bound, marginTilde_convex\n      PROVED (~1100 lines; full support library \u2014 see journal-011).\n      **TIER (ii) STEPS 1+2 COMPLETE (session 012, D-062)**:\n      lambda_pos_finite_height_verified PROVED modulo the single named\n      analytic hypothesis SfBoundProp + the declared computational\n      perimeter (assembly-first split per session-012-notes; FAlt\n      majorant swap; secant two-point base; base points discharged by\n      certified interval bounds in LiBasePoints.lean \u2014 margin\u0303(8\u00d710\u2074)\n      \u2265 8001 certified, margin\u0303(10\u2075) \u2265 85 501 certified).\n      **TIER ii\u2032 LAUNCHED (session 014, user directive \u2014 BEFORE\n      submission, option (a); design D-064)**: TWO DISCOVERIES \u2014\n      (1) liCoeff encoding defect (unordered tsum NOT Summable \u27f9 junk;\n      LiVerifiedUpTo/SfBoundProp FALSE as encoded; paired-form fix =\n      ii\u2032-1a); (2) crux identity Sf(n) = Res\u2081(n) EXACT (numerically\n      verified vs E-015/E-021) \u27f9 assembly TAIL-FREE. Routes R1\u2013R5;\n      sub-stage map ii\u2032-1a..7 (~9\u201316 sessions); perimeter unchanged\n      (Trudgian N(T)/S(T) declared, D-062 \u00a74). Freeze protocol: paper\n      files + existing proofs untouched until ii\u2032-7 (liCoeff fix\n      excepted). Remaining after ii\u2032: (iii) valley, (iv) Suzuki.\n- [~] 5.2 `#print axioms` audit \u2014 only propext, Classical.choice,\n        Quot.sound permitted.\n      \u2192 Inherited library VERIFIED LIVE (session 010, D-061 \u00a73): full\n      build (9010 jobs) + all comparator PrintAxioms scripts match\n      AUDIT.md verbatim. NguyenRH1: all proved declarations (tier (i),\n      session 011; tier (ii) steps 1+2 incl.\n      lambda_pos_finite_height_verified, session 012) show the 3\n      standard axioms ONLY; sorryAx remains only on the 5 skeleton\n      statements (1 Suzuki + 4 valley) by design. No new axioms\n      anywhere.\n- [x] 5.3 Full paper draft with proofs, numerics appendix, Lean appendix.\n      \u2192 COMPLETE (session 010): all stubs written (Introduction,\n      Background, Formal verification), abstract refreshed with tags,\n      references resolve, MiKTeX compile clean (12 pp).\n- [x] 5.4 Final honesty audit: every claim tagged and justified.\n      \u2192 COMPLETE (session 010, D-060): ~55 claims, 4 independent\n      audit instances; 0 unsupported; 10 draft corrections (critical:\n      (1.12)\u27fa split \u2014 converse is skeleton L3/L4); 7 archive errata\n      filed (D-036 sign, D-056 title, D-055/D-058 0.9% overclaim,\n      D-042/D-043 Z/6 supersession by D-045, R-004 post-repair).\n\n### \ud83d\udd36 PHASE 5B \u2014 TIER ii\u2032: close SfBoundProp in Lean (ACTIVE 2026-08-21 \u2014 user directive: BEFORE submission; design D-064; ~9\u201316 sessions)\nFREEZE PROTOCOL: paper files (paperA/paperB/draft/references.bib) and\nexisting Lean proofs are untouched until ii\u2032-7 \u2014 the ONLY exception is\nthe liCoeff correctness fix (ii\u2032-1a). Paper A stays submission-ready at\nevery sub-stage boundary (D-064 \u00a78). Perimeter (D-062 \u00a74 + the\nsession-035 additions, user-approved 2026-08-23): Platt\u2013Trudgian\nRHUpTo, LiVerifiedUpTo, Trudgian N(T)/S(T) [ZeroCountProp \u2014\nstrengthened to the mult-weighted form session 035, matching the\ndeclared source; PLUS ZeroCountProp2 (the two-unit specialization) and\nNoLowZeros (|\u03b3| \u2265 14, the Platt-class zero-location certificate),\nboth for 5f], M\u2080.\n- [x] ii\u2032-0 Design + capability inventory + identity chain.\n      \u2192 COMPLETE (session 014, D-064). TWO DISCOVERIES: (1) liCoeff\n      encoding defect \u2014 unordered tsum NOT Summable \u27f9 junk 0;\n      LiVerifiedUpTo/SfBoundProp FALSE as encoded (theorems vacuous);\n      paired-form fix designed. (2) Crux identity Sf(n) = Res\u2081(n)\n      EXACT (Lagarias (4.10) summed binomially; verified numerically:\n      j=0 exact 15 digits, \u03bb\u2082 matches E-015 certified value, residue\n      theorem sides = \u03bb_n(T)+triv+Res\u2081 to 2e-21) \u27f9 assembly TAIL-FREE:\n      |Sf| \u2264 |\u03bb_n(T)| + |sides| + |triv| = B(n). All 8 planned Zeta23\n      dependencies axiom-checked live (3 standard axioms only).\n- [x] ii\u2032-1a liCoeff pairing fix + summability (D-064 \u00a71).\n      \u2192 COMPLETE (session 015). liSummand = \u00bd\u00b7mult\u00b7(f \u03c1 + f \u03c1\u0304)\n      (manifestly real, liSummand_eq) replaces the junk tsum;\n      `liSummable` PROVED (re_li_summand_le |Re f(\u03c1)| \u2264 2n\u00b2/\u2016\u03c1\u2016\u00b2 tail\n      + normSq_gammaOf_le_mul_norm_sq (9/4) + liSummand_norm_le\n      (9/2)n\u00b2\u00b7mult/(1+\u2016\u03b3\u2016\u00b2) + Zeta23 zero_sum_inv_sq comparison +\n      finite ball via IsCompact.inter_riemannZetaZeros_finite).\n      Full rebuild GREEN (8741 jobs, zero downstream changes); axiom\n      audit: 3 standard axioms only on all new + main declarations.\n      LiVerifiedUpTo/SfBoundProp now TRUE statements (defect repaired).\n- [x] ii\u2032-1b R1 residue machinery: general finite-order residue\n      (MeromorphicNF), rectangle residue theorem extension beyond\n      HasSimplePolesOn, w=1 residue by Leibniz ((w\u22121)^{n+1}J =\n      [w\u207f\u2212(w\u22121)\u207f]h(w), h = (w\u22121)(\u2212\u03b6\u2032/\u03b6)), zero residues via vendored\n      logDerivResidue.\n      \u2192 COMPLETE (sessions 016\u2013017): LiResidue.lean (zetaA/hLi\n      analytic at 1; lcoeff; A_iter; **ResW1_eq_sum** \u2014 the w=1 residue\n      = \u03a3_j C(n,j)\u00b7lcoeff(j\u22121) by iteratedDeriv_mul) + LiPrincipal.lean\n      (rectInt_deriv_eq_zero per-side FTC; **rectInt'_ppart** \u2014 principal\n      part integrates to ResW1 n on any rectangle with 1 interior) +\n      LiSides.lean (session 017: **rectInt'_Jlag** \u2014 RectangleIntegral'\n      (Jlag n) z w = ResW1 n + \u03a3_{\u03c1\u2208Sz} (zeroMult \u03c1)\u00b7(1\u2212(\u03c1/(\u03c1\u22121))\u207f) on\n      rectangles with 1 interior, \u03b6 \u2260 0 on border; removable singularity\n      at 1 via Ffun\u2212TaylP order \u2265 n+1; logDeriv NF residues at zeros,\n      multiple zeros OK; vendored residueTheorem_finset; full build\n      GREEN 8745 jobs \u2014 root now imports all three files; 19 new decls,\n      3 standard axioms only). NOTE: zeroMult(\u22122) = 1 (trivial-zero\n      simplicity) deferred \u2014 zeroMult stays symbolic in the sum; the\n      Sz = {nontrivial} \u222a {\u22122} split is ii\u2032-4 territory.\n- [x] ii\u2032-2 R2(i)/(ii) elementary swaps: \u03bb_n = \u03a3_j(\u22121)^{j+1}C(n,j)\u03c3_j\n      (binomial + paired swap); S_\u221e = \u03a3_j C(n,j)\u03c4_{j\u22121} (odd-m tsum \u2194\n      binomial form, D-037 \u00a73 swap).\n      \u2192 COMPLETE (session 018): LiSwaps.lean \u2014 **liCoeff_eq_sum_sigma**\n      (paired power sums \u03c3_j := sigmaP; per-slice summability cloned\n      from the ii\u2032-1a skeleton: j=1 via Re(1/\u03c1) = Re(\u03c1)/|\u03c1|\u00b2 exactness,\n      j\u22652 by |\u03c1|^{\u2212j} \u2264 |\u03c1|^{\u22122}, radius-2 finite ball; swap via\n      Summable.tsum_finsetSum + CommRing-polymorphic one_sub_one_sub_pow)\n      + **sInfty_eq_sum** (SInfty n = \u03a3_{j=1}^n (\u22121)^jC(n,j)\u00b7lagariasA j,\n      n \u2265 1; lagariasA encoded 1 + odd\u22653 tsum; oddSlice_summable by\n      p-series domination; \u03a3_{j=2}^n(\u22121)^jC(n,j) = n\u22121). Full build\n      GREEN (8746 jobs); 12 new decls, 3 standard axioms only.\n- [x] ii\u2032-3 R2(iii) Lagarias (4.10): \u03c4_j = c_j + (\u22121)\u02b2\u03c3_{j+1} \u2212 (\u22121)\u02b2\n      \u2014 LONG POLE. Sanity gate: j=0 is \u03a31/\u03c1 = 1 + \u03b3/2 \u2212 \u00bdlog 4\u03c0.\n      \u2192 DESIGN COMPLETE (session 019, D-066): route **\u03b24** ADOPTED\n      (contour moments + coefficient split) \u2014 \u03b21 (Hadamard) ruled out\n      (Mathlib has no Weierstrass product/order theory;\n      extract_zeros_poles is finite-only), \u03b22 (EF reuse) ruled out\n      (moments not entire \u2014 outside the EF test class). Factorization:\n      (4.10-a) \u27fa (M) moments \u03c3_k = \u2212g^{(k\u22121)}(0)/(k\u22121)! [contour] +\n      (A) \u03c4_j = (\u22121)^{j+1}a_{j+1} [digamma] + (B) \u03b6-piece [done];\n      R-bound SHARED with ii\u2032-5 \u27f9 resequenced pipeline:\n      ii\u2032-3a (A+B) \u2192 ii\u2032-4 \u2192 ii\u2032-5 \u2192 ii\u2032-3b (moments) \u2192 ii\u2032-3c\n      (assembly \u2192 crux). Piece (B) PROVED (session 019,\n      LiZetaCoeff.lean: iteratedDeriv_hLiExt \u2014 Taylor coefficients of\n      1/s + \u03b6\u2032/\u03b6(1+s) at 0 are \u2212j!\u00b7lcoeff j; 6 decls axiom-clean;\n      build 8747 jobs green). Piece (A) next: \u03c4\u2080 via Mathlib\n      digamma_one_half; j \u2265 1 via digamma series from logGammaSeq.\n      **ii\u2032-3a COMPLETE (session 020)**: piece (A) PROVED \u2014\n      LiArchimedean.lean + LiDigamma.lean (~1200 lines): the capstone\n      `iteratedDeriv_logDeriv_Gamma\u211d` \u2014 the archimedean Taylor\n      coefficients of logDeriv Gamma\u211d(1+s) at 0 are\n      (\u22121)^{j+1}\u00b7j!\u00b7lagariasA(j+1) for ALL j \u2265 0. Via: the Gamma\u211d\n      logDeriv split + \u03c4\u2080 (Mathlib digamma_one_half) + the digamma\n      partial-fraction series BUILT FROM SCRATCH (logGammaSeq \u2192 real\n      identity by deriv-limit interchange \u2192 complex series by\n      Weierstrass + identity principle \u2192 polygamma values at 1/2 by\n      iteratedDerivWithin_tsum \u2192 odd-m reindexing \u2192 2^{j+1} scaling).\n      Build GREEN (8749 jobs); 18 key decls audited: 3 standard axioms.\n      **ii\u2032-3c COMPLETE (session 038)**: LiCrux.lean (~430 lines,\n      root-imported, full build GREEN 8771 jobs): the FE derivative\n      relation (gFun_one_sub_fun + iteratedDeriv_gFun_zero via the\n      UNCONDITIONAL iteratedDeriv_comp_const_sub), the shift expansion\n      (gFun_one_add_punctured/gFun_one_add_eventuallyEq), the\n      coefficient extraction (iteratedDeriv_gFun_one) \u27f9\n      **`lagarias_4_10_a (hZC)` PROVED** (lcoeff (k\u22121) =\n      (\u22121)^k\u00b7(lagariasA k + sigmaP k) + (\u22121)^{k\u22121}, all k \u2265 1) \u27f9\n      **THE CRUX `sf_eq_resW1 (hZC)` PROVED**: (ResW1 n).re = Sf n for\n      n \u2265 1 (ResW1_eq_sum + (4.10-a) + both ii\u2032-2 swaps + the binomial\n      sum \u03a3(\u22121)^{j\u22121}C(n,j) = 1). Audit session038b: 8 decls, 3\n      standard axioms only. **ii\u2032-3 (ALL of Lagarias (4.10)) COMPLETE \u2014\n      Sf(n) = Res\u2081(n) is Lean-proved modulo the declared perimeter.**\n      **ii\u2032-3b COMPLETE (sessions 037\u2013038) \u2014 ROUTE REVISION (D-070)**:\n      the moments (M) came from 5e's partialFraction_identity by PURE\n      ALGEBRA + series calculus (no contours \u2014 the contour work was\n      5e's): gFun := logDeriv xiL = B + seriesFun at good points (xiL\n      entire via the \u039b\u2080 closed form; perimeter ZeroCountProp ONLY \u2014\n      5f's hZC2/hNLZ not needed). LiMoments.lean (~1020 lines,\n      root-imported, full build GREEN 8770 jobs): xiL + the\n      conj/reflect subtype equivs, (G) gFun_eq_momentB, evaluations\n      gFun_zero/gFun_one/gFun_one_eq_neg (FE sign), the summability\n      budget (master \u03a3 mult/\u2016\u03c1\u2016\u00b2 + AM-GM mixed bound), the reindex\n      machinery (sigmaP_eq_unpaired k \u2265 2, vTerm_tsum_eq_zero), k = 1\n      (sigmaP_one_eq_neg_gFun_zero), \u00a75 the termwise iterated\n      derivation at 0 (iteratedDeriv_zpow_neg_one,\n      iteratedDeriv_seriesTerm, the M-test\n      seriesTerm_deriv_summableLocallyUniformlyOn,\n      iteratedDeriv_seriesFun_zero \u2014 the LiDigamma:749\u2013785\n      iteratedDerivWithin_tsum pattern), \u00a76 gFun_eventuallyEq_zero +\n      **THE CAPSTONE `sigmaP_eq_neg_iteratedDeriv_gFun_div (hZC :\n      ZeroCountProp)`: sigmaP k = \u2212gFun^{(k\u22121)}(0)/(k\u22121)! PROVED for\n      ALL k \u2265 1** (session 038, first-pass green). Audit session038:\n      23 decls, 3 standard axioms only. Remaining: ii\u2032-3c (the\n      (4.10-a) assembly; needs the FE derivative relation\n      gFun^{(k\u22121)}(0) = (\u22121)^k\u00b7gFun^{(k\u22121)}(1), small from\n      xiL_one_sub).\n- [x] ii\u2032-4 L3 zero-avoiding T (pigeonhole on perimeter C\u2080/FAlt) +\n      L1 kernel bounds (|k_n| \u2264 2, e\u2074+1, e^{\u221an/2}+1; trivial residue).\n      \u2192 COMPLETE (session 021, LiContour.lean, ~400 lines): L3\n      `exists_zero_avoiding_T` \u2014 clearance 1/(3\u00b7C0hat(a+1)) in any unit\n      window [a, a+1], a \u2265 2, from the perimeter `ZeroCountProp`\n      (Trudgian N(T)/S(T) in \u0108\u2080 form) via the midpoint pigeonhole\n      `exists_avoiding_midpoint` (k+1 midpoints, injective-badness);\n      finiteness via Zeta23 zerosIn_finite. L1: `kFun_norm_le_two`\n      (re s \u2264 1/2), `kFun_shift_norm_le_exp_four_add_one` (horizontals,\n      re s \u2264 3, n \u2264 im\u00b2), `kFun_shift_norm_le_exp_sqrt_half_add_one`\n      (right vertical, 2\u221an \u2264 re s), `kFun_neg_two` + norm \u2264 1.\n      PLUS the deferred trivial-zero simplicity `zeroMult_neg_two`\n      (zeroMult(\u22122) = 1): local factorization \u03b6 = (s+2)\u00b7\u039b/Hfun with\n      Hfun = 4\u03c0^{\u2212s/2}\u0393(s/2+2)/s analytic, Hfun(\u22122) = \u22122\u03c0 \u2260 0,\n      \u039b(\u22122) = \u039b(3) = \u0393R(3)\u03b6(3) \u2260 0. Build GREEN (8751 jobs); 17 decls\n      audited: 3 standard axioms only.\n- [~] ii\u2032-5 R3 R-bound (D-056, A = 10.5, B\u2080 = 48) via LOCAL route:\n      Borel\u2013Carath\u00e9odory (Mathlib) + Jensen (Mathlib) + Blaschke\n      (StrongPNTPrefix); FE polynomial strip bound via\n      riemannZeta_one_sub + Stirling; digamma Lemma D.\n      \u2192 DESIGN COMPLETE (session 022, D-067): route b\u2033 \u2014 Davenport disc\n      at 2+it (R = 5/2) + FE-reflection with EXACT zero-sum\n      cancellation; Stirling-free (Zeta23 digamma_stirling subsumes\n      Lemma D), Hadamard-free; geometry obstruction (every covering\n      disc dips left of \u03c3 = 0) resolved via one extra EM level.\n      **ii\u2032-5b COMPLETE (session 022)**: LiRBound.lean \u2014 the level-2\n      Euler\u2013Maclaurin representation \u03b6(s) = 1/2 + 1/(s\u22121) \u2212\n      s(s+1)\u222b\u2081^\u221e B\u0303\u2082(x)x^{\u2212s\u22122}dx (re s > \u22121; b2Fun machinery, IBP\n      identity, parameter-integral analyticity, W\u00b1 convex-region\n      identity principle) + `norm_riemannZeta_le_disc`: \u2016\u03b6\u2016 \u2264 (3/4)|t|\u00b2\n      on B(2+it, 5/2), |t| \u2265 10. Build GREEN (8752 jobs); 27 decls\n      audited clean. **ROUTE REVISION (session 023, D-067 \u00a76)**: the\n      disc-only constants provably CANNOT reach the baked 10.5/48 (BC\n      derivative factor \u2265 16\u00d7 the M-coefficient; honest assembly ~270)\n      \u27f9 two-stage plan: loose disc bound as the GROWTH INPUT for the\n      partial-fraction identity (5e), tight constants from D-056's\n      analysis of the identity (5f). **ii\u2032-5c COMPLETE (sessions\n      023\u2013024)**: LiDisc.lean \u2014 zeroDiscFinset + zeroDisc_isNontrivial;\n      scaledZeta (unit-disc scaling) + F(0) = 1 via Zeta23\n      zeta_lower_bound_two (\u2016\u03b6(2+it)\u2016 \u2265 1/3, no \u03bc-series build); the\n      multiplicity-invariance chain (analyticOrderNatAt_riemannZeta_\n      affine/const_mul/scaledZeta); scaledZeta_jensen_count (ZerosBound,\n      \u2264 log((9/4)|t|\u00b2)/log(33/32)); **session 024 back half**: R-gap via\n      the \u00d710-rescaled midpoint pigeonhole (R_c \u2208 [2.3, 2.4], clearance\n      gapD = 1/(50(k+1))); g = Cf r_c F analytic + nonvanishing on\n      closedBall(0, r_c) (Zeta23 Cf/ZeroFactorization); |g| \u2264\n      (9/4)|t|\u00b2\u00b7gapD^{\u2212M_c} on the ball (max-modulus over the zero-free\n      sphere); LogOfAnalyticFunction + BorelCaratheodoryDeriv (450\u00b7M\n      factor); logDeriv chain + affine push-forward + near/extras split.\n      **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-5d COMPLETE (session 025)**: LiReflect.lean (~640 lines, 26\n      decls audited clean) \u2014 `logDeriv_zeta_fe` (pointwise logDeriv FE:\n      logDeriv \u03b6 s = \u2212logDeriv \u03b6(1\u2212s) \u2212 [logDeriv \u0393R s +\n      logDeriv \u0393R(1\u2212s)]); `sum_nearZeros_neg_reflect` (the EXACT\n      zero-sum cancellation under \u03c1 \u21a6 1\u2212\u03c1: nearZeros(\u2212t) = image,\n      zeroMult invariant via analyticOrderAt_zeta_one_sub);\n      `logDeriv_Gamma\u211d_shift` (the +4 \u0393R shift putting both digamma\n      arguments in re > 0) + digamma_stirling \u27f9 \u0393R-bracket \u2264\n      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- [x] ii\u2032-5e R3 partial-fraction identity (D-068 design; two-stage\n      plan's second stage). **COMPLETE session 034 \u2014 capstone\n      `partialFraction_identity` PROVED (perimeter ZeroCountProp only).**\n      \u2192 DESIGN COMPLETE (session 026, D-068) with TWO CORRECTIONS to\n      D-067 \u00a76: (C1) the circle series bound is O((log R)\u00b3) via the\n      RADIAL split (\u03b3-gap only in the critical annulus [R\u00b12]; the\n      naive split gives O(R log R) \u2014 fatal, recorded with fix); (C2)\n      the near-axis left-plane digamma bound is a separate build.\n      **5e-0 COMPLETE (session 026)**: LiTrivialZeros.lean \u2014\n      `gamma_mul_prod` (product-form \u0393 recurrence) + the `HfunT n`\n      cofactor + **zeroMult_neg_two_mul**: zeroMult(\u22122n) = 1 for ALL\n      n \u2265 1 (8 decls audited clean; build 8762 jobs, root-imported).\n      **5e-i COMPLETE (session 027)**: LiGapCircles.lean \u2014\n      `exists_gapCircle_radius` (R \u2208 [4k+5/2, 4k+3], dist(R/2,\u2124) \u2265 1/4,\n      ordinate clearance 1/(16\u00b7C0hat(4k+9/2)); \u00d72-rescaled pigeonhole).\n      **5e-ii COMPLETE (session 027)**: LiDigammaLeft.lean \u2014\n      `norm_digamma_le_of_two_le_re` (B: \u2016\u03c8\u2016 \u2264 20 log(2+\u2016w\u2016), re \u2265 2),\n      `digamma_recip_sum_le` (C: \u03a3\u2016(w+j)\u207b\u00b9\u2016 \u2264 2/c+2+2 log m),\n      `norm_digamma_le_of_dist_nat` (A: near-axis bound, re \u2264 2),\n      `logDeriv_Gamma\u211d_eq` (G: the general identity for im \u2260 0);\n      15 decls audited clean; build 8764 jobs.\n      **5e-iii COMPLETE (session 028)**: LiSeries.lean \u2014 the zero-side\n      partial-fraction series `seriesFun s := \u2211' \u03c1, mult\u00b7(1/(s\u2212\u03c1)+1/\u03c1)`:\n      `seriesSummable` (unconditional, the ii\u2032-1a D-trick with the\n      (17/12)\u2016\u03c1\u2016\u00b2 comparison), `seriesFun_analyticOnNhd` off the\n      nontrivial zeros (three-case avoiding balls + the Weierstrass\n      M-test pattern), `nontrivialZero_isolated` (min-distance),\n      `seriesFunSub_analyticAt` + `seriesFun_sub_polar_analyticAt`\n      (series \u2212 mult/(s\u2212\u03c1\u2080) analytic AT \u03c1\u2080 \u2014 the 5e-iv residue\n      cancellation input); 22 decls audited clean; build 8765 jobs.\n      **5e-iv COMPLETE (session 029)**: LiFEntire.lean \u2014 F ENTIRE via\n      the punctured-limit extension `Gentire s := limUnder (\ud835\udcdd[\u2260] s)\n      Fexpr` (no removable-singularity theorem in Mathlib; junk values\n      at the excluded points sidestepped by limUnder uniqueness):\n      principal-part-split witnesses at nontrivial zeros (NF +\n      seriesFun_sub_polar_analyticAt), at 1 (logDeriv zetaA), at 0 and\n      \u22122n (the digamma-series splits: digammaSeriesPart on ball(0,1/2),\n      digammaSeriesPartSub on ball(\u2212n,1/2), both M-test); supporting\n      `zeta_zero_classification` (zeros = nontrivial \u222a {0} \u222a {\u22122n}) +\n      `analyticAt_digamma` (off {0}\u222a\u2212\u2115). Capstone\n      `gentire_analyticAt_and_eq`: (\u2200 s, AnalyticAt \u2102 Gentire s) \u2227\n      (\u2200 s good, Gentire s = Fexpr s); 30 decls audited clean; build\n      8766 jobs. **5e-v-b + 5e-v-c COMPLETE (sessions 030\u2013033)**:\n      LiCircleBound.lean (~3928 lines) \u2014 count bridges (A0count from\n      Zeta23's RvM local count, mult-weighted, all t, unconditional),\n      the Dirichlet bound \u2016\u03b6\u2032/\u03b6\u2016 \u2264 dirichletC2 (re \u2265 2),\n      tsum_split_finset, lowZeroConst, the far-tail bound\n      zero_tail_inv_sq_le (\u03a3_{|\u03b3|>X} m/(1+\u03b3\u00b2) \u2264 16\u00b7A\u2080\u00b7log X/X,\n      X \u2265 200 \u2014 the dyadic fiber machine + ENNReal.tsum_fiberwise),\n      **the series circle bound seriesFun_norm_le_gapCircle**\n      (\u2016seriesFun s\u2016 \u2264 2\u00b7lowZeroConst + 2900\u00b7A\u2080\u00b7\u0108\u2080(4k+9/2)\u00b7(log R)\u00b2\n      on the \u03b3-gap circle, k \u2265 4000), and **the Fexpr circle bound\n      Fexpr_circle_le** (\u2016Fexpr s\u2016 \u2264 2\u00b7lowZeroConst + dirichletC2 +\n      400000\u00b7A\u2080\u00b7\u0108\u2080(R+2)\u00b7(log R)\u00b2): three-region logDeriv assembly\n      (Dirichlet / 5c+5d capstones + the near sum via gapCircle_sep /\n      FE + \u0393R bracket), digamma_circle_le (uniform \u03c8 bound, left\n      near-axis via the \u2124-clearance), and\n      **logDeriv_Gamma\u211d_eq_of_not_neg_nat** (the (G) formula at any\n      non-pole point incl. s = \u2212R \u2014 direct logDeriv_mul, no\n      continuity). **5e-v-d COMPLETE (session 034) \u2014 ii\u2032-5e DONE**:\n      LiSqueeze.lean (~330 lines, 5 decls audited clean; LiCircleBound\n      + LiSqueeze root-imported; full build GREEN) \u2014 the Schwarz\n      squeeze (`gentire_const`: max-modulus + ball-form Schwarz on the\n      \u03b3-gap circles, growth (log R)\u00b3/R \u2192 0 via Q := R^{1/4} \u27f9\n      Gentire \u2261 Gentire 0 =: B) and **THE CAPSTONE\n      `partialFraction_identity` (hZC : ZeroCountProp)**: \u2203 B : \u2102,\n      \u03b6\u2032/\u03b6(s) = B + seriesFun s \u2212 1/s \u2212 1/(s\u22121) + \u00bdlog \u03c0 \u2212 \u00bd\u03c8(s/2)\n      off the excluded set \u2014 the partial-fraction identity Lean-proved\n      modulo ONLY the declared perimeter. Remaining: 5f (tight\n      constants 10.5/48 from D-056's two-point analysis).\n- [x] ii\u2032-5f R3 tight constants (D-056's Theorem R: |R(s)| \u2264 10.5\u00b7log\n      (|t|+2) + 48). \u2192 COMPLETE (sessions 035\u2013036, LiTightR.lean ~4300\n      lines). **Perimeter repair** (user-approved): ZeroCountProp\n      strengthened to the mult-weighted form (the second ii\u2032-1a-class\n      encoding defect \u2014 the unweighted set-card under-captured the\n      declared Trudgian N(T) source; `one_le_zeroMult` bridge;\n      consumers adapted; full build green, audit clean). **P1/P2\n      perimeter additions** (user-approved, D-069): ZeroCountProp2\n      (two-unit count 0.6\u00b7L + 0.886\u00b7LL + 2.7) + NoLowZeros (|\u03b3| \u2265 14).\n      **D-069 Finding 1**: D-056's piece 2 charges the near sum one\n      C\u2080(t) for a TWO-unit window \u2014 the honest two-unit Trudgian form\n      makes the assembly fit 10.5/48 (pinch margin \u2248 1.9). **Finding\n      2** (ii\u2032-6 repair map): H(T)'s near sum has a clearance-coverage\n      gap (honest \u2248 7\u00b7\u0108\u2080\u00b2 vs baked 3\u00b7\u0108\u2080\u00b2; margin survives, crossover\n      moves). 5f-i COMPLETE (Rexpr_decomp + pieces 1 dirichletC2_le_one,\n      2 near_sum_refPoint_le, 4/5 one_div_diff_le); 5f-ii piece 6\n      COMPLETE (digamma_diff_le \u2264 6/t) + **piece 3 COMPLETE (session\n      036)**: the far interval machine \u2014 certified numerics, farW +\n      S\u2083 \u2264 1.3476, six tail bricks (RW\u2080/1/2 = 0.1/0.3303/0.1216,\n      LA\u2080/1/2 = 1/23/0.1687/0.0621), C0hat bridges (2k+1/j+1/2t+1),\n      zeroMult_conj machinery, farG + norm reduction, main bucket\n      machine (unit_family_le + main_bucket_count + farG_main_le), two\n      tail machines (farGLeft_le \u2264 1.1729, farGRight_le \u2264 2.7343),\n      far_series_le \u2264 12.1284\u00b7C\u2080 + 7.2425. **5f-iii COMPLETE (session\n      036)**: pinch lemma pinch_tight_R (11.6318\u00b7LL \u2212 4.6484\u00b7L \u2264\n      0.397094 for L \u2265 log 12, concave tangent at the certified\n      critical point 2.5024, f(2.5024) \u2264 \u22120.96231) + the C0hat L/LL\n      conversion + **THE CAPSTONE\n      `logDeriv_riemannZeta_sub_nearZeros_le_tight (hZC) (hZC2)\n      (hNLZ)`: \u2016logDeriv \u03b6 s \u2212 \u03a3_{near} m/(s\u2212\u03c1)\u2016 \u2264 10.5\u00b7log(t+2) +\n      48 PROVED** (six-piece assembly; fold 5.8516L + 11.6318LL +\n      47.6029 \u2264 10.5L + 48 via the pinch). Audits session036/036b:\n      33 decls, 3 standard axioms only; full build GREEN (8762 jobs).\n- [~] ii\u2032-6 L0 assembly: sides identity + bridge |\u03bb_n(T)| \u2264 4\u00b7FAlt(T)\n      (hRH, BOTH-signs correction F-A) + |Sf n| \u2264 Bn FAlt n on [10\u2075, N\u2081].\n      \u26a0 **FINDING F-D (session 038, D-072)**: the (6.12) stepping in\n      Lagarias's Thm 6.1 is broken at T = \u221an (right-tail ~e^{0.066\u221an},\n      ~5.9\u00d710\u00b9\u2070 envelope at n = 10\u2075 measured by E-031); D-036/D-037/\n      R-004's B(n) inherits it (charge \"3.3\" off by ~10\u2077\u00d7; margin\n      collapses for n \u2273 3\u00d710\u2074). Theorem statement survives (verified\n      to 5\u00d710\u2075; sides cancel by conjugation + phase winding); all\n      Lean work to date survives. **REPAIR ROUTE CHOSEN (2026-08-25,\n      user directive): the D-074 zero-free dog-leg (entry below) \u2014\n      keeps T_cut = \u221an and the ORIGINAL N\u2081 = (T\u2080\u22121)\u00b2 \u2248 9\u00d710\u00b2\u2074; the\n      horizontal right-tail piece of ii\u2032-6-c now comes from ii\u2032-6-DL.**\n      The T = c\u221an global repair (D-073: N\u2081 \u2192 (T\u2080/c)\u00b2) is the PAUSED\n      fallback (c = 1.5 WIP on branch wip/c-1.5-margin-redo, 642d47a).\n      \u2192 ii\u2032-6-0 DESIGN COMPLETE (session 038, D-071 + E-030 ALL CHECKS\n      PASS): THREE findings \u2014 F-A bridge factor-2 (both-signs sum with\n      one-sign N(T) in D-036/D-037/E-023; R-004 unaffected, paper\n      erratum at ii\u2032-7), F-B I_III two-unit count ((2/3)Z2 honest),\n      F-C baked Bn unprovable beyond ~5\u00d710\u2077. USER-APPROVED (8-step\n      protocol): redefine Bn honestly (2F \u2192 4F, (2/3)\u0108\u2080 \u2192 (2/3)Z2hat);\n      fold validated (E-030 V2/V3/V4). Perimeter additions approved:\n      ZeroCountGlobalProp (global Trudgian N(T) \u2264 FAlt) + MZeroProp\n      (M\u2080 \u2264 1.3352). Sub-stages: 6-a (Bn redefinition + convexity\n      re-proof + base-point re-certification) \u2192 6-b (perimeter Props +\n      extended pigeonhole + sides identity + bridge) \u2192 6-c (four side\n      bounds; horizontals = segment-integral machine) \u2192 6-d (fold \u27f9\n      sfBoundProp).\n- [x] ii\u2032-6-R F-D REPAIR SIDE THREAD (COMPLETE, 2026-08-25, session\n      039): focused re-proof of ONLY the right part of the horizontal\n      segments in Lagarias Thm 6.1 (the broken (6.12) stepping).\n      \u2192 6-R-0 (E-032 diagnostic, ALL CHECKS PASS): TRUE complex\n        I_right at T = \u221an by direct quadrature (Dirichlet series\n        certified-tail primary, mpmath validated 6e-10, dps 50) \u2014\n        verdict **HIDDEN CANCELLATION, decisive**: |I_right| =\n        7.2/16.7/26.2 vs envelope 5.1e1/1.0e4/4.7e10 (n = 10\u00b3/10\u2074/10\u2075),\n        ratio collapsing to 5.6e-10; the per-side claim |I_II| = O(\u221an)\n        is empirically TRUE (|I_II|/\u221an decreasing 0.235 \u2192 0.098) but\n        envelope-unprovable at T = \u221an; mid-segment honest (ratio\n        0.7\u20130.95); repair heights honest (ratio \u2248 1, envelope\n        collapses). STOP-rule reported; user direction: repair only,\n        salvage parked (open question, D-073 \u00a78 D4).\n      \u2192 6-R-1 (D-073 \u00a7\u00a73\u20137, repaired proof): dependency audit (only\n        the stepping is proof-breaking; the (1+4/(16+n))\u207f intermediate\n        is a harmless looseness, e\u2074+1 valid); **Lemma 4.1 corrected\n        stepping + Cor 4.2 explicit R(c) = |\u03b6\u2032/\u03b6(2)|\u00b7[e^{4/c\u00b2}/\n        (4(1\u2212q)log 2) + 1/(2 log 2)], q = e^{1/c\u00b2}/2 [PROVED,\n        elementary]**; AUDIT CORRECTION \u2014 recommend **c = 1.5**\n        (reverses D-072's \"2 margin/1.5 range\": the fold is\n        I_III-length-dominated, c = 1.5 wins BOTH base margins\n        (181 256 vs 109 370 at 10\u2075) AND range (N\u2081 = 4\u00d710\u00b2\u2074); c = 2 the\n        ultra-conservative option, R = 1.97 < broken 3.3); consequence\n        audit (Thm 6.1 statement unchanged, O-constant c-dependent;\n        Thm 1.1 height ((T\u2080\u22121)/c)\u00b2; no new perimeter); E-033 ALL\n        CHECKS PASS (Z\u2080 certified [0.5699210, 0.5703661], R covers\n        E-032 measured 3.2\u20136.3\u00d7, kernel charge, fold fit \u2264 0.40,\n        margins > 0 to N\u2081, full fold).\n      \u2192 6-R-2 (D-073 \u00a78, drafts only, correspondence untouched):\n        D3 letter repair paragraph + D4 T = \u221an per-side verdict\n        paragraph (open question: the hidden-cancellation mechanism).\n      THEN: main line executes repair (R) \u2014 8-step protocol re-run at\n      **c = 1.5** (ii\u2032-6-a redo: Bn_c(n) := 4F + 4T[(2/3)Z2 + 10.5 log\n      + 48] + 40\u00b71.3352 + 2(e^{16/9}+1)(7H\u0302 + 5.94) + IIMaj_c + 1,\n      T = 1.5\u221an+1; convexity re-proof + base-point re-certification,\n      values IMPROVE) \u2192 ii\u2032-6-c with the fixed stepping.\n      [SUPERSEDED as the main route 2026-08-25 by ii\u2032-6-DL (user\n      directive: the goal is the ORIGINAL N\u2081 = 9\u00d710\u00b2\u2074); preserved as\n      the PAUSED FALLBACK \u2014 WIP on branch wip/c-1.5-margin-redo\n      (642d47a, resume map in its commit message).]\n- [~] ii\u2032-6-DL F-D DOG-LEG REPAIR (ACTIVE, 2026-08-25, user directive;\n      directive file **PROJECT_DIRECTIVE_D-074.txt**; design/progress\n      anchor **D-074**; route to the ORIGINAL N\u2081 = (T\u2080\u22121)\u00b2 \u2248 9\u00d710\u00b2\u2074).\n      Design: keep T_cut = \u221an (residues/bridge/\u03bb_n(T_cut) UNCHANGED);\n      replace ONLY the broken right horizontal tail [3, 2\u221an] by a\n      zero-free dog-leg: lift \u03c3 = 3 from T_cut to U = (3/2)\u221an\n      (V_left \u2264 (\u221an/2)(e^{5/2}+1)\u00b7C_zeta3 \u2248 1.07\u221an explicit), traverse\n      at U (H_high = D-073's R(1.5) = 5.94, q = e^{4/9}/2 < 1\n      certified), drop at X_R = 2\u221an (V_right exponentially tiny);\n      the dog-leg rectangle is entirely in Re w \u2265 3 \u2014 \u03b6 zero-free +\n      no pole UNCONDITIONALLY (no new perimeter, no RH above T_cut).\n      Mid-segment [\u22125/2, 3] at T_cut untouched (honest, E-032).\n      Bn impact \u2248 +2.2\u221an; the dog-leg charge decomposes into existing\n      margin-block shapes (convexity re-proves at coefficient level).\n      Sub-stages (crash-safe, commit per sub-stage; D-074 \u00a71 log):\n      \u2192 DL-0 COMPLETE (session 040): \u00a72 audit (Lean contour matches;\n        Jlag n s = (s/(s\u22121))\u207f\u22121\u00b7(\u2212\u03b6\u2032/\u03b6 s), CCW orientations pinned);\n        \u00a73 derivation (identity H_low = H_high \u2212 V_right + V_left;\n        analyticity unconditional at Re \u2265 3); \u00a74 constants (C_zeta3 =\n        0.165 certified \u2014 hand-estimate 0.150 caught wrong by smoke\n        test; e^{5/2}+1 \u2264 13.19; q = 0.7798; HHigh = 5.94; VRight =\n        IIMaj/4); **E-034 ALL CHECKS PASS** (identity exact to 2\u20135e-5;\n        piece slack 4\u201313\u00d7; margins 14 419 / 90 317 / 2.458e26 at\n        8\u00d710\u2074 / 10\u2075 / N\u2081 = (3\u00d710\u00b9\u00b2\u22121)\u00b2 \u2014 ORIGINAL endpoint restored;\n        fold fit \u2264 0.399); \u00a77 A\u2013L report \u2014 **AWAITING USER GATE\n        before DL-1 (Lean)**.\n      \u2192 DL-1 COMPLETE (session 040, LiDogLeg.lean, build 8773 jobs,\n        audit clean): Jlag_differentiableAt_dogleg +\n        holomorphicOn_Jlag_dogleg (Re \u2265 3 zero-free via Mathlib, NO\n        perimeter), rectangleIntegral(_')_Jlag_dogleg_eq_zero (Cauchy),\n        **upper_right_horizontal_eq_dogleg** (the exact identity (\u2605)\n        PROVED), kFun_conj/Jlag_conj (lower-side machinery).\n      \u2192 DL-2 COMPLETE (session 040, LiDogLeg.lean +~250 lines, build\n        8773, audit clean): kFun_three_add_it_norm_le_exp_five_halves_add_one\n        (kernel \u2264 e^{5/2}+1), dirichletC3 \u2264 1/2 (termwise 3-vs-2\n        comparison + dirichletC2 \u2264 1 \u2014 C_zeta3 charged 0.5, fold-\n        indifferent; 0.165/0.17 tightening path documented),\n        norm_logDeriv_zeta_le_half (\u2016\u03b6\u2032/\u03b6\u2016 \u2264 1/2, re \u2265 3),\n        **vIntegral_Jlag_three_norm_le**: \u2016V_left\u2016 \u2264\n        (U\u2212T)(e^{5/2}+1)/2. E-034 re-validated at C = 0.5: ALL CHECKS\n        PASS (margins 13 165/88 916/2.458e26).\n      \u2192 DL-3 COMPLETE (session 040, LiDogLeg.lean +~430 lines, build\n        8773, audit clean): norm_term/norm_logDeriv_zeta_le_two_pow\n        (zeta halving 2^{\u2212(\u03c3\u22122)}\u00b7dirichletC2),\n        one_add_div_pow_norm_le_exp_four_ninths (kernel envelope\n        e^{(4/9)\u03c3} \u2014 single-exponential, no geometric series),\n        Jlag_dogleg_norm_le_envelope (dirichletC2\u00b7(4e^{\u2212c\u03c3}+4\u00b72^{\u2212\u03c3})),\n        integral_exp_neg_le (FTC machine), cdog_gt (c \u2265 0.2487),\n        exp_four_thirds_le (e^{4/3} \u2264 3.8073),\n        **hIntegral_Jlag_dogleg_norm_le \u2264 8.38** (charged with\n        dirichletC2 \u2264 1; tight R(1.5) = 5.94 = documented tightening\n        path). E-034 re-validated at Lean constants: ALL CHECKS PASS\n        (margins 13 160/88 911/2.458e26).\n      \u2192 DL-4 COMPLETE (session 040, LiDogLeg.lean +~160 lines, build\n        8773, audit clean): kFun_right_vertical_norm_le_exp_sqrt_half_add_one\n        (w = 2\u221an kernel variant, e^{\u221an/2}+1),\n        **vIntegral_Jlag_right_norm_le** \u2264 (U\u2212T)(e^{\u221an/2}+1)\n        2^{\u2212(2\u221an\u22122)}\u00b7dirichletC2 \u2014 exponentially tiny; VRightBound\n        charged IIMaj/2 (provable with dirichletC2 \u2264 1; IIMaj/4 =\n        tightening path).\n      \u2192 DL-5 COMPLETE (session 040, LiDogLeg.lean +~210 lines, build\n        8773, audit clean): **hIntegral_Jlag_low_le_dogLegUpper** +\n        **hIntegral_Jlag_low_neg_norm_le_dogLegUpper** (both \u2264\n        ((\u221an+1)/2)(e^{5/2}+1)/2 + 8.38 + IIMaj/2 for T \u2208 [\u221an, \u221an+1],\n        U = (3/2)T) + dogLegUpper_two_sides \u2014 the full dog-leg PROVED\n        in Lean, no perimeter, nothing above T_cut.\n      \u2192 DL-6 COMPLETE (session 040, LiDogLeg.lean +~350 lines, build\n        8773, audit clean): the direct Dirichlet bound at re = 2\u221an \u2014\n        **norm_logDeriv_zeta_le_iimZeta \u2264 0.57\u00b72^{\u2212(2\u221an\u22122)} (n \u2265 5),\n        NO dirichletC2 \u2264 0.57 needed** (log2-leading + 3^{\u2212(2\u221an\u22122)}\n        tail with dirichletC2 \u2264 1); **V_right \u2264 IIMaj/4 EXACTLY**;\n        DL-5 upgraded to the quarter charge (dogLegUpper = VLeft +\n        8.38 + IIMaj/4 per side \u27f9 1.5\u00b7IIMaj total in Bn, the\n        convexity-safe coefficient). E-034 re-validated at IIMaj/4:\n        ALL CHECKS PASS.\n      \u2192 ii\u2032-6-a2 (Bn dog-leg redefinition \u2014 freeze-exception protocol:\n        honest redefinition with horizontalRightDoglegBound(n)\n        explicit; convexity re-proof; base-point re-certification;\n        endpoint margins at N\u2081 = (T\u2080\u22121)\u00b2; git history; paper-correction\n        queue; full axiom audit).\n      THEN THE ORIGINAL PLAN RESUMES (D-074 \u00a78 return map): ii\u2032-6-c\n      (four side bounds with the repaired horizontal) \u2192 ii\u2032-6-d (fold\n      \u27f9 sfBoundProp) \u2192 ii\u2032-7 (closure at the ORIGINAL N\u2081 \u2248 9\u00d710\u00b2\u2074).\n      Fallbacks: (a) c = 1.5 paused branch (N\u2081 = 4\u00d710\u00b2\u2074); (b) c = 2\n      (N\u2081 = 2.25\u00d710\u00b2\u2074); (c) T = \u221an hidden-cancellation open question\n      (D-073 \u00a78 D4).\n- [ ] ii\u2032-7 Closure: theorem sfBoundProp : SfBoundProp; final\n      lambda_pos_finite_height_closed (3 perimeter hypotheses only);\n      full axiom audit; paper Appendix B + tag upgrade (D-062 \u00a74\n      endpoint); archive closure + D-037 line-63 erratum pointer.\n\n## 6. GRAVEYARD (documented dead ends \u2014 REQUIRED logging)\n| # | Attempt | Track | Obstruction found | Date |\n|---|---------|-------|-------------------|------|\n| G-001 | Multiple-zero bounds as chain constraint (Idea C) | A | s\u2082/p substitution symmetry (depth\u21920 pairs = doubles in all 2-moment data) | 2026-08-17 |\n| (A) | Zero-density input into chain (D-009 Idea A) | A | depth\u21920 off-line pairs invisible to N(\u03c3,T) bounds | 2026-08-17 |\n| G-002 | Moment-ladder certificates (tr G\u0303\u1d4f, k\u22653; oversampled grids) | A | RS availability \u03bb\u22642/k bites before usefulness; caps 0.607N (k=3, \u03bb=2/3) and 0.502N (k=4, \u03bb=1/2) both < 2/3; n\u208a q-invariant (E-005) | 2026-08-17 |\n| G-003 | Density certificates \u2192 de Bruijn\u2013Newman \u039b (task 3.3) | C | one-sided information: density theorems lower-bound the on-line fraction, \u039b needs an upper bound on the complex fraction; extremal vs averaged (E-012); asymptotic vs explicit | 2026-08-17 |\n| G-004 | \u03bb \u2192 \u03bb_a\u207b ground-state channel (task 2.13 follow-up) | B | disjoint feasibility windows: ground-state resolution needs a \u2272 1.3 (\u03bb_a superexponential), zero resolution needs a \u2273 4\u20136; discretization floor out-ranks \u03bb_a; D-046 sizing | 2026-08-19 |\n\n## 7. RESULT LEDGER\n| # | Claim | Status tag | Location |\n|---|-------|-----------|----------|\n| 0 | \u22652/3 simple on-line (inherited) | [PROVED] (R2) | Paper Thm A |\n| 1 | Galerkin realization of Suzuki's Weil-form operator A_a validated to 4.5e-6 against the zero-side explicit formula; Weil formula conventions machine-verified (Gaussian test, 9e-16) | [NUMERICAL-VALIDATED] | E-009a/b, D-019 \u00a71 |\n| 2 | \u03bb_a (bottom of Weil-form spectrum) positive at a = 0.25..5 with steep cliff (0.414 \u2192 \u22641.7e-12), consistent with Yoshida \u03bb_a>0 \u2200a \u27fa RH; independently matches Kim et al. superexponential decay report | [NUMERICAL] (upper bounds; conforming Galerkin) | E-009b, D-019 F1 |\n| 3 | Li coefficients \u03bb_n > 0 for all n \u2264 3000 computed from the arithmetic side (BL Thm 2, zero-free; flint Stieltjes + Arb \u03b6, dps 1000\u20131450), cross-validated vs E-008 zero side; \u03bb_1 to 102 digits; refined asymptotic ratio 1.00216 at n=2000, 0.999845 at n=3000 | [NUMERICAL-VALIDATED] | E-011, E-015, R-001 |\n| 4 | \u03be\u2032-certificate strength mechanism: perfect-square node in the diagonal law D\u2081 \u2248 s(1\u22122s)\u00b2 (prime-scale cancellation p ~ \u221a(T/2\u03c0)); Remark 7.1 constants reproduced to 5e-6; s\u2082/p symmetry does NOT break; gain not portable to \u03be | [NUMERICAL-VALIDATED] | E-013, R-002, D-022 |\n| 5 | Exact factorization W(a,\u03b8;z) = F\u00b7(R\u2080+R_\u03c4), F = z\u00b2\u03be/\u03be\u2032, with R\u2080 = 2e^{a+i\u03b8/2}sin(az\u2212\u03b8/2)+o(e\u1d43) closed form; Suzuki Cor 1.6 \u27fa (\u2605) tail-cancellation (Wiener\u2013Hopf remainder, RH-gated); W(a,\u03b8;0) = 0 double \u2200a,\u03b8; explains full E-010\u2013E-016 phenomenology | [PROVED (modulo std tempered-FT bookkeeping)] + [NUMERICAL-VALIDATED] (E-017: skeleton 3.7%\u21920.009%, off-axis cancellation 99.8%, \u03b8=\u03c0 preferred) | R-003, D-026, D-027, E-017 |\n| 6 | Explicit finite-height Li theorem: \u03bb_n > 0 for all n \u2264 N\u2081 = (T\u2080\u22121)\u00b2 \u2248 9.0\u00d710\u00b2\u2074 (T\u2080 = 3\u00d710\u00b9\u00b2 Platt\u2013Trudgian); conservative window N\u2081* = 2.73\u00d710\u00b2\u00b9; first assembled explicit chain (S_\u221e elementary lower bound + traced contour constants + margin convexity + finite verification) | [PROVED-CONDITIONAL(computational RH-to-T\u2080; finite verification)] \u2014 R-bound fully traced D-056 (A = 10.5, B\u2080 = 48, honest C\u2080; E-028 verified, 26\u00d7 slack); N\u2080 = 80 000; margin convexity PROVED D-057 (E-029) | R-004, D-037, D-056, D-057, E-023, E-028 |\n\n## 8. SESSION PROTOCOL & RESEARCH ARCHIVE (MANDATORY)\n\nMulti-stage project: computer is shut down between stages. NOTHING may live\nonly in conversation. The archive below is the single source of truth.\n\n### 8.1 Archive map\n```\nSTATE.md                    \u2b50 resume point \u2014 READ FIRST every session\nresearch/\n\u251c\u2500\u2500 journal/session-NNN.md  per-session narrative log\n\u251c\u2500\u2500 results/R-NNN-*.md      one file per result (+ index.md ledger)\n\u251c\u2500\u2500 graveyard/G-NNN-*.md    one file per dead end (+ index.md)\n\u251c\u2500\u2500 derivations/D-NNN-*.md  worked derivations (+ index.md)\n\u251c\u2500\u2500 numerics/scripts/       deterministic experiment scripts\n\u251c\u2500\u2500 numerics/data/          E-NNN-*.csv + E-NNN-*.json metadata sidecars\n\u251c\u2500\u2500 research.db             SQLite catalog (sessions, results, graveyard,\n\u2502                           derivations, experiments) \u2014 schema in\n\u2502                           numerics/scripts/schema.sql, CLI: db.py\n\u2514\u2500\u2500 paper/                  paperA.tex (Paper A, split 2026-08-20),\n                            paperB.tex (research-note skeleton),\n                            draft.tex (FROZEN pre-split combined copy),\n                            references.bib\n```\n\n### 8.2 Storage conventions\n- Results/derivations/graveyard: plain Markdown, honesty tag on every claim.\n- Numerics: DUAL storage \u2014 CSV+JSON sidecar (human/paper-readable) AND\n  SQLite registration (queryable), written together via db.py.\n- Data is cached; scripts never recompute unless --force.\n- Paper assembled only from tagged files in results/.\n\n### 8.3 Session START protocol\n1. Read STATE.md \u2192 resume point, next action, open threads, blockers.\n2. Skim latest journal entry + results/index.md.\n\n### 8.4 Session END protocol (before any shutdown \u2014 no exceptions)\n1. Write journal/session-NNN.md (work, decisions, outcomes).\n2. File every result/dead end/derivation in its own file; update index.md\n   files; register in research.db.\n3. Update NGUYEN.md checklist (\u00a75), Graveyard (\u00a76), Result Ledger (\u00a77).\n4. Update STATE.md LAST with an explicit \"NEXT ACTION:\" line.\n5. git add + commit with session number in the message.\nNOTE: save artifacts IMMEDIATELY when produced (crash-safe), not batched.\n\n### 8.4a FORK RULE (user directive, 2026-08-17)\nWhen the path FORKS (multiple candidate directions), do ALL of them \u2014\none by one \u2014 then pause to gather thoughts and evaluate the next step\ntogether. No path is dropped at a fork by choice alone; paths are only\nclosed by documented obstruction (Graveyard) or deprioritized by\nevidence after all forks are explored.\n\n### 8.5 PACING & SUB-STAGES (user directive, 2026-08-17)\n- NO RUSH. This is long-term research; correctness and rigor outrank speed.\n  Take whatever time a stage needs to be done right.\n- SUB-STAGE RULE: if a stage will take a few hours, break it into smaller\n  sub-stages, each ending in a clean, committed, resumable state (per \u00a78.4).\n  Record sub-stage breakdowns in STATE.md.\n- BREAK PROMPT: if work is running long \u2014 ESPECIALLY approaching 5:00 PM\n  local time \u2014 pause and ASK the user whether to continue, take a break,\n  or log off (run \u00a78.4 end protocol before stopping).\n\n### 8.6 SESSION LOG (summary; details in research/journal/)\n- Session 001 (2026-08-17): Blueprint + mission prompt ingested; research\n  archive installed (git + SQLite + LaTeX skeleton). \u2192 Begin Phase 0.\n- Session 002 (2026-08-17): Phase 0 + Phase 1 complete (Track A \u2192\n  monitoring mode, D-013); Track C begun (3.1 D-014, E-006\u2013E-008, 3.4a/b,\n  D-018 Suzuki scoping).\n- Session 003 (2026-08-17): Q-3.4c complete \u2014 E-009a (Suzuki g validated),\n  E-009b (Galerkin A_a, validated vs zero side 4.5e-6; \u03bb_a cliff),\n  D-019 (analysis; Q-S1 verdict; E-010 proposed). Weil explicit-formula\n  conventions machine-verified (D-001 NT-1).\n- Session 004 (2026-08-17): recovered killed session (E-011 orphaned\n  mid-edit); paper archive reorg; E-010 extended (a\u22648, \u03bb=\u22121); ALL 4 FORKS\n  COMPLETE \u2014 E-010 (fork 1, session 003); E-011/R-001 (fork 2: Li \u03bb_n > 0,\n  n \u2264 2000, arithmetic side); 3.3 answered NO (fork 3: D-021 \u2192 G-003,\n  E-012); T4 CLOSED (fork 4: D-022/R-002 \u2014 \u03be\u2032 strength = perfect-square\n  node in D\u2081, not portable to \u03be; T4b opened). Q-S3 attacked (D-023,\n  E-014): Cor 1.6 density wall mapped to a=10 (maximal lattice,\n  interlacing exact, no thinning \u2014 scale limitation, not a wall);\n  \u03b8=\u03c0 candidate found; Q-S3a/b/c queued. Detached-run machinery\n  established.\n- Session 005 (2026-08-18): user approved do-all-one-by-one plan\n  (A3\u2192A1\u2192A2\u2192C\u2192B, D in background). D launched: E-015 Li n\u22643000\n  detached (in progress at stop; sandbox blocks multiprocessing spawn \u2014\n  detached launches need sandbox disabled). A3 done: E-016 + D-024 \u2014\n  Herglotz \u03c1_W at \u03b8=\u03c0 vs \u03c1_F; V1/V2/V4 pass, V3 (zero-Poisson\n  reconstruction) fails rel ~0.3, root cause open; findings: \u03b8=\u03c0 zeros\n  real, z\u2081(\u03c0)\u00b7a\u22484.5 stiff law, no \u03b8=\u03c0 zero in (0,\u03c0/a), raw-L2 \u03b8=\u03c0\u2248\u03b8=0\n  (plateau-dominated metric). Stopped mid-V3-root-cause (user break;\n  3 network dropouts, no state loss).\n- Session 006 (2026-08-18): REGROUP (user-requested). Full archive audit:\n  all 16 experiments have CSV+JSON sidecars and db registrations; fixed\n  db hygiene (sessions 3\u20135 registered; row_counts corrected for E-010\u2013\n  E-016). Checklist revised: Phase 2 restructured \u2014 Suzuki/Cor 1.6 line\n  recognized as the live spectral program (2.1 partial, 2.4 active; new\n  tasks 2.6 V3-root-cause, 2.7 Q-S3a analytic, 2.8 Q-S3b backend);\n  3.4 checked off (answered YES); NEW tasks 3.5 (Li asymptotic attack \u2014\n  most direct criterion-#1 path), 1.6 (\u03be\u2032-world ceiling), 1.7 (T4b\n  scoping). Active order confirmed: 2.6 \u2192 2.7 \u2192 2.8 \u2192 1.6 \u2192 1.7, with\n  3.5 as standing high-value background thread.\n- Session 006 cont. (2026-08-18): task 2.6 COMPLETE \u2014 E-016 V3\n  root-caused (E-016b: winding-excess diagnostic finds double zero at\n  origin, \u00b1i\u03b5 pair; EM-tail factor-y bug found + confirmed quantitatively)\n  and REPAIRED (E-016c: V5 1.75e-16, V6 \u22644.4e-15, V3R 1.5\u20132.0e-5, ALL\n  CHECKS PASS); D-025 filed; E-016 F1\u2013F4 stand.\n- Session 006 cont.2 (2026-08-18): task 2.7 COMPLETE \u2014 **breakthrough\n  reduction**: W(a,\u03b8;z) = F\u00b7(R\u2080+R_\u03c4) EXACT (F = z\u00b2\u03be/\u03be\u2032, R\u2080 closed-form\n  sine skeleton); Cor 1.6 \u27fa (\u2605) tail-cancellation (Wiener\u2013Hopf remainder,\n  RH-gated). R-003 promoted to ledger (#5). E-017: off-axis cancellation\n  already 99.8% at a=4; \u03b8=\u03c0 preferred; open content isolated to \u211d.\n- Session 006 cont.3 (2026-08-18): task 2.8(i) complete \u2014 E-018 descent\n  profile: (\u2605) cancellation strip-uniform (median |M|/|R\u2080| ~5\u20137e-3,\n  y\u2080\u2208[0.1,1]); open content = zero set of M only; \u03b8-preference found\n  metric-dependent. D-028.\n- Session 006 cont.4 (2026-08-18): task 2.8(ii) complete \u2014 backend v2\n  (blockwise \u039b to e\u00b2\u2074, validated 2.2e-7/4.4e-8) + E-019 at a=12: NO\n  transition (maximal lattice, z\u2081\u00b7a=4.495, gap CV \u2193, origin pair +2.0000\n  winding excess, \u03b3-proximity chance-level, envelope stationary). 2.8\n  CLOSED; a=13+ deprioritized by evidence (D-029). \u2192 Next: 1.6\n  (\u03be\u2032-world ceiling).\n- Session 006 cont.5 (2026-08-18): task 1.6 COMPLETE \u2014 E-020b window\n  optimum for kernel D\u2081 = 0.86864 to 1e-6 (quartic window IS the\n  optimum; control recovers MT); \u03be\u2032-world saturated, nothing transfers\n  to \u03be; E-020 adversary-pool limitation documented (D-030). User\n  decision: do 1.6 then 1.7 as queued (option #1). \u2192 Next: 1.7 (T4b\n  scoping).\n- Session 006 cont.6 (2026-08-18): task 1.7 COMPLETE \u2014 T4b CLOSED\n  (D-031): node mechanism iterates formally (\u03be\u2033 \u2248 0.94 leading-order)\n  but G-001 symmetry caps every \u03be\u207d\u1d4f\u207e data class below 100%; Speiser/\n  Levinson\u2013Montgomery route to RH closed at every order; revival\n  condition noted. Session-005 queue (A3\u2192A1\u2192A2\u2192C\u2192B) NOW FULLY DONE.\n  \u2192 Next: 3.5 (Li asymptotic attack) or (\u2605) analytic attack.\n- Session 006 cont.7 (2026-08-18): task 3.5 DESIGN COMPLETE (user\n  directive: do 3.5 then (\u2605), then analyze for next stage). D-032\n  literature map: Voros \u2014 \"\u03bb_n>0 \u2200n\u2265N\u2080\" \u27fa RH at ANY N\u2080; Lagarias\n  Thm 6.1 finite-height bridge is the exploitable skeleton. D-033:\n  achievable deliverable = EXPLICIT finite-height theorem (\u03bb_n>0 \u2200n\u2264N\u2081\n  \u2248 10\u00b2\u2070\u201310\u00b2\u2074 from Platt T\u2080 + traced constants + finite verification);\n  wall = three-way arithmetic cancellation (triangle bounds explode).\n  New tasks 3.6/3.7/3.8 (D-036 constants, E-021 S_\u221e, D-037 assembly).\n- Session 006 cont.8 (2026-08-18): task (\u2605) DESIGN COMPLETE. D-034:\n  WH factorization + RH is unexplored territory (26 arXiv hits all\n  Riemann\u2013Hilbert); Krein/Gohberg\u2013Feldman/de Branges\u2013Krein machinery\n  exists. D-035: resolvent-convergence route \u2014 D_{a,\u03b8(a)}\u2192D in Krein\n  space; Cor 1.6 \u27fa D has real spectrum (deliverable D1); three-layer\n  wall (index/persistence=RH/circularity); off-axis 99.8% cancellation\n  is TAUTOLOGICAL (entirety of W forces it), the \u211d-envelope is the\n  whole problem. New tasks 2.9/2.10/2.11.\n- Session 007 (2026-08-18/19): task 3.6 marked done; task 3.7 (E-021)\n  COMPLETE after 6-bug root-cause saga (mpmath zeta ~58-digit ceiling,\n  GAMMA_E float literal, 3\u00d7 parse-before-dps, \u03c3-omission boundary\n  (15/14)\u207f, float64 zeros). E-021 ALL CHECKS PASS: V1 4.8e-25 vs\n  E-015; A = 0.9, B\u2080 = 1.0 measured; c\u2080 = \u22121/4 (+1/(24n) correction);\n  |S_f| max 13.52 at n = 3298 vs traced bound ~2280 (~170\u00d7 slack).\n  Resources folder (29 RH-equivalence notes) read in full. Next: 3.8\n  (D-037 \u2192 R-004 finite-height theorem assembly).\n- Session 008 (2026-08-19): REGROUP + R7 registration (resources atlas\n  indexed: resources/index.md, manifest R7, D-001 Part III pointer).\n  Task 3.8 COMPLETE \u2014 **R-004 finite-height Li theorem**: \u03bb_n > 0 for\n  all n \u2264 N\u2081 = (T\u2080\u22121)\u00b2 \u2248 9.0\u00d710\u00b2\u2074 (T\u2080 = 3\u00d710\u00b9\u00b2 Platt\u2013Trudgian);\n  conservative window N\u2081* = 2.73\u00d710\u00b2\u00b9. E-023 support computation ALL\n  CHECKS PASS: D-036 |t|<10 gap found + closed (M\u2080 = 1.3352), S_\u221e\n  elementary lower bound validated vs exact (min slack 9.52), N\u2080 =\n  5\u00d710\u2074 adopted (crossover 32 871 traced / 30 217 measured), margin\n  convex, margin(N\u2081) = 2.46\u00d710\u00b2\u2076. Ledger #6. Criterion-3 deliverable \u2014\n  the maximal content of the Li route short of RH. Task 2.10 COMPLETE\n  same session: E-022/E-022b + D-040 \u2014 spectral measures \u03bc_a (Clark\n  weights 1/K_a(z_k,z_k)) for a \u2264 12; **valley observable**: K_a(z,z)\n  dips exactly at the true \u03b3's, \u0394(a) \u2248 3.33 \u2212 4.76/a saturating at\n  fixed \u03b8=\u03c0; \u03b3-information flows through weights, not positions; mass\n  within \u00b10.1 of \u03b3's 63\u219272.5%; new constraint on 2.9-D1 (\u03b8(a) must\n  drive \u0394 \u2192 \u221e). Next: 2.9-D1, 2.11 (D-038); optional D-039 digamma\n  upgrade.\n- Session 009 (2026-08-19): **PHASE 4 COMPLETE.** Session-008 leftovers\n  (D-052 4.1/4.2, D-053 4.3a gate PASS) committed. 4.3b (D-054): four\n  independent-instance reviews + hand-verification \u2014 ALL THREE TAGS\n  downgraded (D-039 proof broken/bound true; D-036 \u00a71 far-sum\n  O(|t| log t) hole \u2014 reference-point trick missing; D-049 B1/B3 lower\n  bounds broken; \u03b4_crit one-direction; T-2 \u21d0 skeleton; D-052 accounting\n  fixes). Theorem statements survive (margins robust); repair map\n  4.5a\u20134.5d opened. 4.4 (E-027 + D-055, ALL CHECKS PASS): detector\n  stress test \u2014 bare-form negativity immediate for any \u03b4 > 0 (no\n  threshold); tuned-carrier threshold \u03c0/(2a) exact (\u22640.9%); pencil\n  onset magnitude-limited (0.11@a=4, 0.038@a=8); directions localized\n  at the pair. **Repairs 4.5a\u20134.5d COMPLETE same day**: D-056 (R-bound\n  reference-point proof, A = 10.5/B\u2080 = 48, honest C\u2080) + E-028 (N\u2080 =\n  80 000, 26\u00d7 slack); D-057 (convexity proved) + E-029; D-058 (valley\n  lower bounds via node-killing; B3/m_\u03b3/detector fixes); D-059\n  (bookkeeping: punctured compacts, R_\u03c4, Lemma FD, L1). R-004 tag\n  fully restored with the analytic chain proved end-to-end. Paper\n  updated (R-004 constants, valley theorem corrected form, E-027\n  appendix item). Next: Phase 5 / paper finalization.\n- Session 010 (2026-08-19): **PHASE 5: 5.3 + 5.4 COMPLETE; 5.1/5.2 at\n  skeleton stage.** 5.3: paper draft fully written (Introduction,\n  Background, Formal verification; abstract retagged; clean 12 pp\n  MiKTeX compile). 5.4 (D-060): full honesty audit \u2014 4 independent\n  instances, ~55 claims, 0 unsupported; 10 draft corrections\n  (critical: (1.12)\u27faspec(D)\u2282\u211d split \u2014 converse is SKELETON L3/L4;\n  flat-window fix; B(n) explicit remainders); 7 archive errata filed\n  (D-036 \u22121/(24n) sign, D-056 title constants, D-055/D-058 \"0.9%\" \u2192\n  0.02\u20132.3%, D-042/D-043 Z/6 \u2192 Z/(2\u03c0) supersession by D-045, R-004\n  post-repair update). 5.1/5.2 (D-061): elan + v4.33.0-rc2 installed;\n  zeta-23-lean FULL BUILD green (9010 jobs \u2014 D-007 rebuild done);\n  5.2 verified LIVE (all comparator PrintAxioms = 3 standard axioms,\n  verbatim AUDIT.md match); NguyenRH1 skeleton package created\n  (research/lean/NguyenRH1/, 9 statements compile, path-requires to\n  the vendored repo, no new axioms, sorryAx-marked). Next: prove the\n  elementary Lean tier (sInfty_lower_bound, marginTilde_convex) or\n  optional numerics (E-023b, E-021 n=10\u2074).\n- Session 011 (2026-08-19): **Lean tier (i) COMPLETE** (journal-011;\n  ~1100 lines, 10 commits; user machine crashed mid-session, zero work\n  lost). chain_rule_sqrt_shift, sInfty_lower_bound (Bernoulli truncation\n  + \u03b3-shifted harmonic bounds, parity algebra, tsum summability\n  discharged), marginTilde_convex (8-block \u03c8-table + analytic IIMaj\u2033\n  bound \u2264 1.316 < 2 via factor monotonicity; convexOn_of_deriv2_nonneg)\n  all PROVED, PrintAxioms = 3 standard axioms only. End-of-session user\n  directive: read session-012-notes.txt before Session 012.\n- Session 012 (2026-08-20): **Lean tier (ii) STEP 1 COMPLETE** (option\n  (a) per session-012-notes.txt, assembly-first split).\n  lambda_pos_finite_height PROVED modulo the single named analytic\n  hypothesis SfBoundProp (\u2200 n \u2208 [10\u2075, N\u2081], |Sf n| \u2264 Bn FAlt n) +\n  perimeter (RHUpTo, LiVerifiedUpTo) + 2 elementary margin evaluations\n  (hbase/hbase2). No sorryAx in LiSkeleton.lean. Design: FAlt majorant\n  swap (true F+S_b has \u03c8 > 0 on [5.47,~16] \u2014 caught pre-instantiation;\n  negative-weight term dropped, cost 0.9\u221an); secant two-point base\n  (pos_of_convex_of_two_points); margin regularity \u2192 ContDiffOn (Ioi 1).\n  D-062: SfBoundProp triage (layers L0\u2013L7) + PERIMETER DECISION \u2014\n  Trudgian 2014 N(T)/S(T) inside the trusted perimeter, declared in the\n  paper appendix (compile clean, 12 pp). D-062 \u00a75: base-point discharge\n  plan validated at dps 40 (plan bounds margin(8\u00d710\u2074) > 9 960;\n  margin(10\u2075) > margin(8\u00d710\u2074) by \u2265 2.2\u00d710\u2074 slack). CONTINUATION same\n  day (session-012-end-notes.txt, mathematician review actioned):\n  **tier (ii) STEP 2 COMPLETE** \u2014 LiBasePoints.lean (~560 lines)\n  discharges both margin evaluations by certified rational interval\n  bounds (exp \u2264 (1\u2212x/16)\u207b\u00b9\u2076 trick, partial sums, d9/d20 rationals);\n  **lambda_pos_finite_height_verified** = R-004 modulo SfBoundProp +\n  perimeter ONLY (3 hypotheses), PrintAxioms clean. Paper reconciled:\n  margin trail footnote (16 020 \u2192 15 764 \u2192 \u2265 8 001 certified),\n  formal-status paragraph at 3 hypotheses; compile clean 12 pp.\n  Review guidance adopted: tier ii\u2032 (contour interior) is\n  post-publication; Paper A ready to split/finish.\n- Session 013 (2026-08-20): **PAPER SPLIT EXECUTED** (user \"go go\"\n  after the minor-items assessment). paperA.tex (8 pp, clean): the\n  self-contained finite-height Li artifact \u2014 retargeted abstract/intro\n  with the three-named-hypotheses Lean headline, \u00a73 R-004 with the\n  reconciled margin-trail footnote, obstruction context, Li numerics\n  appendix, formal-verification appendix. paperB.tex (6 pp skeleton):\n  spectral-line note opening with the \u00a70 standing-items box (trace-or-\n  demote R-003's FT bookkeeping/o(e\u1d43); L3/L4; authorship policy).\n  draft.tex FROZEN (pre-split combined archive copy). Minor item 1\n  (number-trail note) filed at 10fdda6 before the split. Author block\n  carried verbatim except one typo fix (\"fromAnthropic\" \u2192 \"from\n  Anthropic\"); authorship itself untouched (user's call). Also\n  repaired: the \u00a79 header accidentally eaten by the session-011/012\n  log edit. CONTINUED same day: authorship set to sole author Dan T\n  Nguyen, Research Ai (user directive; both papers + frozen draft);\n  AI Contribution Statement + title footnote + one-line\n  Acknowledgments added to both papers (user directive, review\n  template); voros2017li reference corrected (real: Exp. Math. 29(4)\n  2020); submission documents written (cover-letter.md targeting\n  Experimental Mathematics + referee-list.md); **pre-submission audit\n  of NguyenRH1 ALL CHECKS PASS (D-063)**: clean-room rebuild green,\n  exhaustive axiom sweep of all 139 declarations (134 standard-only +\n  5 intended skeletons), statement-to-paper correspondence exact,\n  inherited comparators verbatim. Paper A is submission-ready pending\n  the user's read-through. Paper B assessment: more experiments NOT\n  needed (evidence ceiling documented); queued Task 1 = R-003\n  tempered-FT bookkeeping trace (\u2192 D-064) as next research action.\n- Session 014 (2026-08-21): **TIER ii\u2032 LAUNCHED** (user decision:\n  option (a) \u2014 close SfBoundProp in Lean BEFORE submission; Paper A\n  frozen/submittable throughout). Sub-stage ii\u2032-0 COMPLETE (D-064\n  design doc). TWO DISCOVERIES: (1) **liCoeff encoding defect** \u2014\n  unordered tsum NOT Summable (junk 0) \u27f9 LiVerifiedUpTo/SfBoundProp\n  FALSE as encoded, session-012 theorems vacuous; paired-form fix\n  designed (ii\u2032-1a, next). (2) **Crux identity Sf(n) = Res\u2081(n) EXACT**\n  (Sf := S_\u221e+1\u2212\u03bb_n = the w=1 residue \u03a3_j C(n,j)c_{j\u22121}) \u2014 numerically\n  verified: (4.10) j=0 exact 15 digits; \u03bb\u2082 prediction matches E-015\n  certified value; residue theorem sides = \u03bb_n(T)+triv+Res\u2081 verified\n  2e-21. Assembly TAIL-FREE: |Sf| \u2264 |\u03bb_n(T)|+|sides|+|triv| = B(n).\n  Routes R1\u2013R5 decided (R2(iii) (4.10) = long pole: EF-reuse first,\n  Hadamard fallback); sub-stage map ii\u2032-1a..7 (~9\u201316 sessions); all 8\n  planned Zeta23 dependencies axiom-checked live (clean). NOTE: the\n  R-003 bookkeeping doc is renumbered D-065 (D-064 taken by this\n  design doc). Freeze protocol in force.\n- Session 015 (2026-08-21): **ii\u2032-1a COMPLETE** \u2014 liCoeff encoding\n  defect repaired: paired symmetric liSummand (\u00bd\u00b7mult\u00b7(f \u03c1 + f \u03c1\u0304),\n  manifestly real) replaces the junk tsum; `liSummable` PROVED\n  (~340 lines LiSkeleton \u00a71: geometric-sum tail bound |Re f| \u2264 2n\u00b2/\u2016\u03c1\u2016\u00b2,\n  (9/4)\u2016\u03c1\u2016\u00b2 comparison, (9/2)n\u00b2\u00b7mult/(1+\u2016\u03b3\u2016\u00b2) dominator, Zeta23\n  zero_sum_inv_sq + finite ball); full rebuild GREEN (8741 jobs, zero\n  downstream changes); axiom audit 3 standard axioms only.\n  LiVerifiedUpTo/SfBoundProp are now TRUE statements. Phase 5B\n  checklist installed (commit 7a395b2). Next: ii\u2032-1b residue machinery.\n- Session 016 (2026-08-21): **ii\u2032-1b(i)+(ii) COMPLETE** \u2014 LiResidue.lean\n  (zetaA = (w\u22121)\u03b6 analytic at 1 via removable singularity; hLi analytic,\n  value 1, punctured agreement; lcoeff; A_iter; **ResW1_eq_sum**: the\n  w=1 residue = \u03a3_{j=1}^n C(n,j)\u00b7lcoeff(j\u22121) by iteratedDeriv_mul\n  Leibniz) + LiPrincipal.lean (rectInt_deriv_eq_zero per-side FTC;\n  Acoeff/ppart/Gprim; **rectInt'_ppart**: principal part integrates to\n  ResW1 n on any rectangle with 1 interior). 3 standard axioms only.\n- Session 017 (2026-08-21): **ii\u2032-1b(iii) COMPLETE \u2014 ii\u2032-1b FULLY\n  DONE** \u2014 LiSides.lean (~460 lines): **rectInt'_Jlag**, the rectangle\n  residue theorem for the Lagarias-kernel integrand:\n  RectangleIntegral' (Jlag n) z w = ResW1 n + \u03a3_{\u03c1\u2208Sz} (zeroMult\n  \u03c1)\u00b7(1\u2212(\u03c1/(\u03c1\u22121))\u207f) (1 interior, \u03b6 \u2260 0 on border, Sz = zeros inside,\n  supplied form). Removable singularity at 1 via Taylor-remainder order\n  \u2265 n+1 (Ffun\u2212TaylP); logDeriv-NF residues at zeros (multiple zeros\n  OK); zeta_order_ne_top_of_ne via the entire zetaA (identity\n  principle on univ, no punctured-plane connectedness needed; zetaA 1\n  = 1 makes \u03b6(1)'s junk value irrelevant). Root NguyenRH1.lean now\n  imports LiResidue/LiPrincipal/LiSides; full build GREEN (8745 jobs);\n  19 new decls, 3 standard axioms only. Deferred: zeroMult(\u22122) = 1\n  (trivial-zero simplicity) \u2014 ii\u2032-4. Next: ii\u2032-2 elementary swaps.\n- Session 018 (2026-08-21): **ii\u2032-2 COMPLETE** \u2014 LiSwaps.lean: the two\n  elementary swaps. R2(i) `liCoeff_eq_sum_sigma`: \u03bb_n = \u03a3_{j=1}^n\n  (\u22121)^{j+1}C(n,j)\u03c3_j with paired power sums (per-slice summability via\n  the ii\u2032-1a skeleton; j=1 paired exactness Re(1/\u03c1) = Re(\u03c1)/|\u03c1|\u00b2).\n  R2(ii) `sInfty_eq_sum`: S_\u221e(n) = \u03a3_{j=1}^n (\u22121)^jC(n,j)a_j (n \u2265 1;\n  oddSlice p-series domination; the j=1 \u2212n/m + n/m exact cancellation;\n  \u03a3_{j=2}^n(\u22121)^jC(n,j) = n\u22121). 12 new decls, 3 standard axioms only;\n  full build GREEN (8746 jobs). Next: ii\u2032-3 (4.10), the long pole.\n- Session 019 (2026-08-21): **ii\u2032-3 DESIGN (D-066) + piece (B)\n  PROVED**. Route investigation: \u03b21 (Hadamard) OUT \u2014 Mathlib lacks\n  Weierstrass/order machinery (extract_zeros_poles is finite-only);\n  \u03b22 (EF reuse) OUT \u2014 moment kernels not entire. **Route \u03b24 ADOPTED**:\n  contour moments (ii\u2032-1b machinery) + coefficient split; R-bound\n  identified as shared with ii\u2032-5 \u27f9 resequenced pipeline ii\u2032-3a \u2192\n  ii\u2032-4 \u2192 ii\u2032-5 \u2192 ii\u2032-3b \u2192 ii\u2032-3c. Mathlib inventory verified live\n  (digamma_one_half \u2713, Weierstrass-convergence \u2713, LSeries vonMangoldt\n  \u2713, logGammaSeq \u2713; completedRiemannZeta\u2080 noted as the wrong \u03be).\n  Piece (B): LiZetaCoeff.lean \u2014 iteratedDeriv_hLiExt (coefficients of\n  1/s + \u03b6\u2032/\u03b6(1+s) at 0 are \u2212j!\u00b7lcoeff j); 6 decls, 3 standard axioms;\n  build 8747 green. Next: piece (A) archimedean \u03c4-evaluation.\n- Session 020 (2026-08-21/22): **ii\u2032-3a COMPLETE** \u2014 piece (A) PROVED:\n  `iteratedDeriv_logDeriv_Gamma\u211d` (the archimedean Taylor coefficients\n  are (\u22121)^{j+1}\u00b7j!\u00b7a_{j+1}, all j \u2265 0). The digamma partial-fraction\n  series built from scratch (logGammaSeq \u2192 deriv-limit interchange \u2192\n  Weierstrass + identity principle \u2192 iteratedDerivWithin_tsum termwise\n  values \u2192 odd-m reindexing \u2192 2^{j+1} scaling); LiDigamma.lean +\n  LiArchimedean.lean. Build GREEN (8749 jobs); 18 decls audited clean.\n  Two elaboration gotchas banked (bare \u03c0 auto-binds; bare \u2191 drops coe).\n  Next: ii\u2032-4 (L3 zero-avoiding T + L1 kernel bounds).\n- Session 021 (2026-08-22): **ii\u2032-4 COMPLETE** (LiContour.lean, ~400\n  lines, three sub-stage commits). L3 `exists_zero_avoiding_T` (midpoint\n  pigeonhole on the perimeter `ZeroCountProp`; clearance\n  1/(3\u00b7C0hat(a+1))). L1 kernel bounds (`kFun_norm_le_two`,\n  `kFun_shift_norm_le_exp_four_add_one`,\n  `kFun_shift_norm_le_exp_sqrt_half_add_one`, `kFun_neg_two` \u2264 1) via the\n  normSq core `norm_one_add_one_div_le`. Trivial-zero simplicity\n  `zeroMult_neg_two` (zeroMult(\u22122) = 1) via \u03b6 = (s+2)\u00b7\u039b/Hfun near \u22122,\n  Hfun = 4\u03c0^{\u2212s/2}\u0393(s/2+2)/s, Hfun(\u22122) = \u22122\u03c0 \u2260 0, \u039b(\u22122) = \u039b(3) \u2260 0.\n  Build GREEN (8751 jobs); 17 decls audited: 3 standard axioms only.\n  Also (website, non-research): fixed /dashboard/ 500 (git_log cp1252\n  decode) + Roadmap Phase 2/5B list rendering (python-markdown list\n  interruption) \u2014 web/ only, logged in RH-WEBSITE.md \u00a77. Next: ii\u2032-5\n  (R-bound, the long pole).\n- Session 022 (2026-08-22): **ii\u2032-5a DESIGN (D-067) + ii\u2032-5b COMPLETE**.\n  D-067: route b\u2033 for the R-bound \u2014 Davenport disc at 2+it (R = 5/2)\n  + FE-reflection with exact zero-sum cancellation; Stirling-free\n  (digamma_stirling subsumes Lemma D), Hadamard-free; the \"every disc\n  dips left of \u03c3 = 0\" obstruction resolved by one extra EM level.\n  ii\u2032-5b (LiRBound.lean, ~640 lines): b2Fun machinery (comp_fract''\n  continuity trick), the level-2 IBP identity integral_b1_cpow_eq,\n  parameter-integral analyticity (re > \u22121), the level-2 \u03b6\n  representation via the convex W\u00b1 regions (sidesteps the\n  punctured-halfplane connectedness grind), and norm_riemannZeta_le_disc\n  (\u2016\u03b6\u2016 \u2264 (3/4)|t|\u00b2 on B(2+it, 5/2), |t| \u2265 10). Build GREEN (8752\n  jobs); 27 decls axiom-clean. Next: ii\u2032-5c (Davenport disc argument).\n- Session 023 (2026-08-22, HALT BY USER at a clean boundary): **ROUTE\n  REVISION (D-067 \u00a76)** \u2014 the disc-only BC constants provably cannot\n  reach the baked 10.5/48 (factor \u2265 16\u00d7 the M-coefficient) \u27f9 two-stage\n  plan: loose disc bound = growth input for the partial-fraction\n  identity (5e), then D-056's tight analysis of the identity (5f).\n  **ii\u2032-5c HALF** (LiDisc.lean, green): zeroDiscFinset +\n  zeroDisc_isNontrivial (re \u2265 1 via Mathlib's one_le_re nonvanishing;\n  re \u2264 0 via \u0393R-pole/FE); scaledZeta + F(0) = 1 (Zeta23\n  zeta_lower_bound_two, no \u03bc-series build); the multiplicity-invariance\n  chain (affine/const-mul/scaled); scaledZeta_jensen_count\n  (ZerosBound). Next: 5c back half \u2014 R-gap, g analytic+nonvanishing,\n  BC assembly.\n- Session 024 (2026-08-22): **ii\u2032-5c COMPLETE** (commit c7cbae5;\n  LiDisc.lean +~1000 lines, 32 new decls, all audited: 3 standard\n  axioms only). R-gap selection by the \u00d710-RESCALE TRICK (zero new\n  pigeonhole code: exists_avoiding_midpoint at a = 23 on the \u00d710\n  zero-norm image, \u00f710 \u27f9 R_c \u2208 [2.3, 2.4], clearance gapD =\n  1/(50(k+1))); the Blaschke quotient g = Cf r_c F built entirely on\n  Zeta23's Cf API (CfAnalytic/ZeroFactorization; nonvanishing on\n  closedBall(0, r_c) \u2014 the gap makes the sphere zero-free); |g| \u2264\n  (9/4)|t|\u00b2\u00b7gapD^{\u2212M_c} by max-modulus; center log|g(0)| \u2265 0;\n  LogOfAnalyticFunction (r = 3/5, R = r_c) + BorelCaratheodoryDeriv\n  (16M\u00b7r_c\u00b2/(r_c\u22123/5)\u00b3 \u2264 450M); logDeriv chain (div/prod/pow/comp) +\n  the affine push-forward (sum_image + order invariance) + the\n  near/extras split (extras \u2264 Jensen count via |s\u2212\u03c1| \u2265 |t\u2212\u03b3| \u2265 1).\n  **Capstone `logDeriv_riemannZeta_sub_nearZeros_le`**: the LOOSE\n  R-bound \u2264 100000\u00b7(log|t|)\u00b2 on \u03c3 \u2208 [1/2, 7/2], |t| \u2265 10, \u03b6 s \u2260 0 \u2014\n  no perimeter hypothesis (Jensen count, not ZeroCountProp). Constant\n  fold: log(33/32) \u2265 1/33 (log x \u2265 1\u22121/x), log 4150 \u2264 9 (e > 2.71),\n  M_bound \u2264 420L\u00b2. Build GREEN (8753 jobs; LiDisc now root-imported).\n  Next: ii\u2032-5d (FE-reflection + left digamma bound).\n- Session 025 (2026-08-22): **ii\u2032-5d COMPLETE** (LiReflect.lean, ~640\n  lines, 26 new decls, all audited: 3 standard axioms only). The FE\n  logDeriv identity `logDeriv_zeta_fe` (via \u039b =\u1da0 \u0393R\u00b7\u03b6 near good points\n  + the \u039b(1\u2212z) = \u039b(z) chain-rule negation); the EXACT zero-sum\n  cancellation `sum_nearZeros_neg_reflect` (nearZeros(\u2212t) = image under\n  \u03c1 \u21a6 1\u2212\u03c1 by the symmetric ball estimate (1+\u03c1.re)\u00b2+(\u03c1.im\u2212t)\u00b2 \u2264 5;\n  zeroMult invariant by analyticOrderAt_zeta_one_sub); the \u0393R +4 shift\n  `logDeriv_Gamma\u211d_shift` (Gamma\u211d_def + Gamma_add_one twice + exp-form\n  cpow arithmetic) putting both digamma arguments in re > 0, then\n  StirlingVert digamma_stirling \u27f9 \u0393R-bracket \u2264 4(log|t|)\u00b2. **Capstone\n  `logDeriv_riemannZeta_sub_nearZeros_le_left`**: the loose R-bound\n  \u2264 200000\u00b7(log|t|)\u00b2 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 for\n  2 \u2264 |im w|, uniform in the shift chain (digamma_add_natCast +\n  first-order EM `sum_eq_integral_add_integral_deriv` + arctan-FTC\n  \u222bdx/((x+a)\u00b2+c\u00b2) \u2264 \u03c0/c \u2014 no full-line integral needed). Build GREEN\n  (8761 jobs; LiReflect root-imported). Banked gotchas: this Mathlib's\n  add_le_add_left/right are swapped vs classic; push_cast EM\n  conclusions before linear_combination; single-cast sum families.\n  Next: ii\u2032-5e (partial-fraction identity), first item zeroMult(\u22122n)\n  = 1 for all n (generalize ii\u2032-4c).\n- Session 026 (2026-08-22): **ii\u2032-5e PREP + DESIGN COMPLETE** (commit\n  0d9887a). LiTrivialZeros.lean (~290 lines, 8 decls audited clean):\n  `gamma_mul_prod` (product-form \u0393 recurrence by induction on\n  Gamma_add_one) + the `HfunT n` cofactor (analytic/nonzero at \u22122n)\n  + **zeroMult_neg_two_mul**: zeroMult(\u22122n) = 1 for ALL n \u2265 1 (the\n  ii\u2032-4c pattern via analyticOrderAt_eq_natCast). D-068 (5e design):\n  F entire via principal-part splits (no removable-singularity\n  theorem, no Hadamard); TWO CORRECTIONS to D-067 \u00a76 \u2014 (C1) circle\n  series bound O((log R)\u00b3) via the RADIAL split (the naive annulus\n  split gives O(R log R) \u2014 fatal); (C2) near-axis left-plane digamma\n  bound separate (recurrence + separated reciprocal sum). Sub-stage\n  map 5e-i..v. Banked: DifferentiableAt.analyticAt does NOT exist\n  (use fun_prop); Gamma\u211d_eq_zero_iff gives \u2212(2*\u2191m); lt_trichotomy\n  exists / le_or_lt does NOT. Next: ii\u2032-5e-i (\u03b3-gap circles).\n- Session 027 (2026-08-22): **ii\u2032-5e-i + 5e-ii COMPLETE** (commits\n  e28eff6, 0e9336e, ec13029; two new files, 17 decls, all audited:\n  3 standard axioms only). 5e-i (LiGapCircles.lean):\n  `exists_gapCircle_radius` \u2014 R \u2208 [4k+5/2, 4k+3] with dist(R/2,\u2124) \u2265 1/4\n  and ordinate clearance \u2265 1/(16\u00b7C0hat(4k+9/2)) (the \u00d72-rescaled\n  midpoint pigeonhole + C0hat_mono). 5e-ii (LiDigammaLeft.lean): the\n  telescope tail + **norm_digamma_le_of_two_le_re** (B: Weierstrass\n  split, harmonic head + telescoping tail, integers via\n  digamma_natCast_eq) + **digamma_recip_sum_le** (C: the V-split\n  separated reciprocal sum) + **norm_digamma_le_of_dist_nat** (A: the\n  near-axis bound via digamma_add_natCast\u2032 \u2014 pole-avoidance form,\n  covering real points) + **logDeriv_Gamma\u211d_eq** (G: logDeriv \u0393R s =\n  \u2212(log \u03c0)/2 + \u00bd\u03c8(s/2) for im \u2260 0, the m-fold shift). Build GREEN\n  (8764 jobs). Banked: ascribe cast haves (stuck typeclasses else);\n  pin \u2115-sub casts (Nat.cast_sub before push_cast; elaborator lifts\n  Real.log (m\u2212k) to real-sub); sum_add_tsum_nat_add's shifted terms\n  are beta-redexes (state goals in redex form); prod_range_succ's f\n  explicit-first. Next: ii\u2032-5e-iii (the zero series).\n- Session 028 (2026-08-23): **ii\u2032-5e-iii COMPLETE** (LiSeries.lean,\n  ~600 lines, 22 decls, all audited: 3 standard axioms only). The\n  zero-side partial-fraction series `seriesFun s := \u2211' \u03c1 : nontrivial\n  zeros, mult\u00b7(1/(s\u2212\u03c1)+1/\u03c1)`: `seriesSummable` at every s (the ii\u2032-1a\n  D-trick; tail 2\u2016s\u2016/\u2016\u03c1\u2016\u00b2 via 1/(s\u2212\u03c1)+1/\u03c1 = s/(\u03c1(s\u2212\u03c1)); the (17/12)\u2016\u03c1\u2016\u00b2\n  \u03b3-comparison; Zeta23 zero_sum_inv_sq dominator); `seriesFun_analyticAt`\n  + `seriesFun_analyticOnNhd` off the nontrivial zeros (the three-case\n  avoiding balls: \u03b6\u22600 continuity / \u03b6=0 order normal form / s\u2080=1 zetaA;\n  the Weierstrass M-test `of_norm_le_summable_eventually` + the\n  journal-020/021 TendstoLocallyUniformlyOn\u2192differentiableOn\u2192\n  analyticOnNhd pattern); `nontrivialZero_isolated` (finite unit-ball\n  min-distance); `seriesFunSub_analyticAt` (the \u03c1\u2080-term-zeroed series\n  analytic AT \u03c1\u2080); `seriesFun_sub_term` (the everywhere split\n  seriesFun = seriesFunSub + the \u03c1\u2080-term); capstone\n  `seriesFun_sub_polar_analyticAt` (series \u2212 mult/(s\u2212\u03c1\u2080) analytic at\n  \u03c1\u2080) \u2014 the 5e-iv residue-cancellation input. Build GREEN (8765 jobs,\n  LiSeries root-imported). Banked: redex-RHS show-before-rw; no rw at\n  set-var-dependent hypotheses (standalone membership iff route);\n  obtain-rfl needs a variable RHS; if_pos/if_neg under binders via\n  simp only; Finset.image lambda type-pinning; file ends `end\n  NguyenRH1` then `end`; push_neg/Set.mem_setOf_eq deprecated. Next:\n  ii\u2032-5e-iv (F entire by the principal-part splits).\n- Session 029 (2026-08-23): **ii\u2032-5e-iv COMPLETE** (commits 58e03e2 +\n  closure; LiFEntire.lean, ~1130 lines, 30 decls, all audited: 3\n  standard axioms only). F ENTIRE: the difference Fexpr = logDeriv \u03b6 \u2212\n  seriesFun + 1/s + 1/(s\u22121) \u2212 (log \u03c0)/2 + \u03c8(s/2)/2 extends via the\n  punctured limit `Gentire s := limUnder (\ud835\udcdd[\u2260] s) Fexpr` (Mathlib has\n  no general removable-singularity theorem; the junk point-values are\n  sidestepped by limUnder uniqueness + per-bad-point analytic\n  witnesses). Witnesses: nontrivial zeros (the NF logDeriv witness +\n  5e-iii polar subtraction), s = 1 (logDeriv zetaA), s = 0\n  (digamma-series split, \u03c8(s/2)/2 + 1/s = \u2212\u03b3/2 + \u00bd\u00b7series), s = \u22122n\n  (NF + zeroMult_neg_two_mul + the dropped-term series H_n). Support:\n  `zeta_zero_classification` (every zero is nontrivial/0/\u22122n \u2014 the\n  LiDisc argument globalized via completedRiemannZeta_eq_zero_iff +\n  Gamma\u211d_eq_zero_iff), `analyticAt_digamma` (off {0}\u222a\u2212\u2115). Capstone\n  `gentire_analyticAt_and_eq`: Gentire analytic everywhere AND equal\n  to Fexpr at every good point. Build GREEN (8766 jobs, LiFEntire\n  root-imported). Banked: AnalyticAt.comp HOU pin (f := ...); the\n  (\u22122\u2191n)/2 non-defeq value-normalization; cast-leaf vs single-cast\n  pinning (((x:\u2124):\u2102) forms); abs_re_le_norm as the robust\n  norm-of-cast-expr route; eventually_ne's implicit target pinned by\n  ascription; EventuallyEq wrapper vs raw \u2200\u1da0 (show-bridges); subst\n  eliminating the wrong local. Next: ii\u2032-5e-v (the circle bound\n  O((log R)\u00b3) + the max-modulus squeeze \u27f9 \u2203 B capstone).\n- Session 030 (2026-08-23): **ii\u2032-5e-v STARTED \u2014 5e-v-a + 5e-v-b\n  chunk 1 COMPLETE** (commits 5d24756, e6a654b; LiCircleBound.lean,\n  ~340 lines so far, clean elaboration, not yet root-imported). 5e-v-a:\n  `isNontrivialZero_conj`; the count bridges \u2014 `A0count` from Zeta23's\n  RvM `zeta_local_zero_count` (mult-weighted, two-sided, ALL t,\n  unconditional \u2014 the series-bound count input) + `Ncount_window_le` /\n  `Ncount_add_of_le` / `Ncount_chain_le` / `Ncount_le_of_interval` /\n  `Ncount_le_of_interval_gen`; `norm_logDeriv_zeta_le_dirichlet`\n  (\u2016\u03b6\u2032/\u03b6\u2016 \u2264 dirichletC2 for re \u2265 2, the LSeries vonMangoldt pattern\n  from ZetaBounds); 5e-v-b chunk 1: `tsum_split_finset` (tsum =\n  finset sum + if-zeroed tail via tsum_eq_sum) + `lowZeros`/\n  `lowZeroConst`. Full remaining design (tail bound via\n  ENNReal.tsum_fiberwise + the key machinery; the one-split series\n  bound; logDeriv/elem assembly; Schwarz squeeze; \u2203 B capstone) in\n  journal-030. Banked: le_or_gt (le_or_lt absent); finsum_mem_union/\n  finsum_mem_empty/tsum_eq_sum forms; Nat.cast_nonneg ascription;\n  Ncount_add_of_le endpoint pinning; nested calc-by parser fragility;\n  positivity vs Classical.choose defs; [DecidableEq \u03b9] for\n  statement-level ifs; _root_.riemannZeta_conj. Next: 5e-v-b chunk 2\n  (the tail bound + the main series circle bound).\n- Session 031 (2026-08-23): **ii\u2032-5e-v-b chunk 2 COMPLETE** (commits\n  c26241c, f984afc, closure 8f16424; LiCircleBound.lean ~830 lines,\n  clean). The far-tail bound `zero_tail_inv_sq_le`: \u03a3_{|\u03b3|>X}\n  m/(1+\u03b3\u00b2) \u2264 16\u00b7A0count\u00b7log X / X for X \u2265 200 \u2014 the dyadic fiber\n  machine: `dyadClass` (Nat.log-2 classes) + lower/upper bounds,\n  `dyadClass_fiber_finite`, `fiber_mult_count` (the two-window cover\n  via Ncount_le_of_interval_gen), `fiber_tail_le` (per-fiber bound via\n  tsum_subtype + tsum_eq_sum + filter split), `tsum_dyadic_log`\n  (closed form 10 log 2 + 2 log X via hasSum_coe_mul_geometric) and\n  the ENNReal.tsum_fiberwise + ofReal_tsum_of_nonneg assembly.\n  Banked: coercion-lambda type-pinning in Finset.image/filter/\n  sum_subtype (use Subtype.val); the unary-minus precedence\n  (-(2^(j+1) * X) parenthesization + abs_neg/neg_mul);\n  Finset.disjoint_left; tsum_subtype explicit args; indicator_of_notMem\n  camelCase; of_norm_bounded's norm-kept goal; rw-pow_succ' rfl-close\n  (no trailing ring); nlinarith can't multiply hypotheses by factors \u2014\n  rw the pow identity at goal+haves first. Next: 5e-v-b chunk 3 (the\n  main seriesFun circle bound).\n- Session 032 (2026-08-23): **ii\u2032-5e-v-b chunk 3 COMPLETE** (commits\n  787b9c0, 727f656, d2bfde6, 222d65d + capstone; LiCircleBound.lean\n  ~2867 lines, clean, zero warnings; audit-session032-axioms.txt: 19\n  decls, 3 standard axioms only). The series circle bound\n  `seriesFun_norm_le_gapCircle`: \u2016seriesFun s\u2016 \u2264 2\u00b7lowZeroConst +\n  2900\u00b7A\u2080\u00b7\u0108\u2080(4k+9/2)\u00b7(log R)\u00b2 on the \u03b3-gap circle (k \u2265 4000). Pieces:\n  3a `gapCircle_threshold` (416\u00b7\u0108\u2080 \u2264 4k+5/2, explicit exp/log\n  arithmetic) + `not_isNontrivialZero_on_gapCircle`; 3b\n  `seriesTerm_norm_eq_div`, `circleZeros R`, the count brick\n  `sum_zeroMult_le_of_im_band` (band [a,b] + sign-separation c \u27f9\n  3\u00b7A\u2080\u00b7(b\u2212a+2)\u00b7log(3\u00b7max|a||b|+5) via the (M\u22121,b] \u222a (\u2212b\u22121,\u2212M]\n  two-window cover), `series_tail_le` (91\u00b7A\u2080\u00b7log R),\n  `seriesFun_norm_le_split`; 3c `dyadic_family_le` (generic machine\n  via Finset.sum_fiberwise_of_maps_to with t := Ico 1 (J+1) \u2014 avoids\n  the Fintype-\u2115 gap), `shell_low` (2\u00b7lowZeroConst),\n  `shell_inlo`/`shell_inhi` (60\u00b7A\u2080L\u00b2), `shell_up` (45\u00b7A\u2080L\u00b2, dyadic\n  class reaches J+1), `shell_crit` (2688\u00b7\u0108\u2080A\u2080L: uniform separation\n  1/(32\u0108\u2080) \u2014 strip arcs |t\u2212\u03b3| \u2265 1/(32\u0108\u2080) via the \u03b3-gap (conj for\n  \u03b3 < 0) + the threshold; near-axis |s\u2212\u03c1| \u2265 \u221a13\u22121), and the five-way\n  partition assembly. Banked: linarith can't relate distinct\n  reciprocal atoms (bridge P = 2Q by field_simp first);\n  sum_fiberwise needs Fintype (use sum_fiberwise_of_maps_to);\n  sum_image's f is auto-bound (pin (f := ...));\n  Finset.eq_empty_iff_forall_notMem; div_le_div_of_nonneg_right\n  exists / div_le_div_right does NOT; floor-integrality must route\n  through \u2115 +1-cast before linarith; filter-conjunction nesting\n  \u27e8hF, pred\u27e9; lt_of_not_le does NOT exist (lt_of_not_ge). Next:\n  5e-v-c (logDeriv/elem assembly \u27f9 \u2016Fexpr\u2016 \u2264 C(log R)\u00b3).\n- Session 033 (2026-08-23): **ii\u2032-5e-v-c COMPLETE** (commits 1c76576,\n  5da957c + capstone; LiCircleBound.lean ~3928 lines, clean, zero\n  warnings; audit-session033-axioms.txt: 14 decls, 3 standard axioms\n  only). The Fexpr circle bound `Fexpr_circle_le`: \u2016Fexpr s\u2016 \u2264\n  2\u00b7lowZeroConst + dirichletC2 + 400000\u00b7A\u2080\u00b7\u0108\u2080(R+2)\u00b7(log R)\u00b2 on the\n  \u03b3-gap circle (k \u2265 4000). Pieces: c-i\n  `differentiableAt_Gamma\u211d_of_not_neg_nat` +\n  **`logDeriv_Gamma\u211d_eq_of_not_neg_nat`** (the (G) formula at ANY\n  non-pole point incl. s = \u2212R \u2014 direct logDeriv_mul on Gamma\u211d_def,\n  digamma := logDeriv \u0393 by def, no continuity argument) +\n  `gapCircle_sep` (standalone \u03b3-gap separation) +\n  `nearZeros_count_le` + `gapCircle_sep_of_mem_nearZeros`; c-ii\n  `digamma_right_le` (48+23\u00b7log) + `digamma_circle_le` (uniform\n  62+23\u00b7log(2+R/2): strip sub-log, right_le, left near-axis via\n  5e-ii (A) c = 1/8 from the \u2124-clearance \u2014 the R+re s = im\u00b2/(R\u2212re s)\n  identity, no square roots) + elems; c-iii `logDeriv_circle_le`\n  (three regions: Dirichlet / 5c+5d capstones + near sum \u2264\n  32\u0108\u2080\u00b7count / FE `logDeriv_zeta_fe` with all 10 hyps discharged +\n  Dirichlet at 1\u2212s + \u0393R bracket) and the six-norm-chain assembly.\n  Banked: riemannZeta_ne_zero_of_one_le_re takes ONLY re;\n  div_lt_iff\u2080 is a/c<b here (lt_div_iff\u2080 for a<b/c);\n  add_le_add_left/right SWAPPED (use per-step norm haves + linarith);\n  rw [X = 1*X] rewrites everywhere (use calc); linear_combination -h\n  for the 1\u2212s bridges; congrArg Complex.re + simp for cast-bridges;\n  left-assoc products through every calc; Real.pi_lt_d2 : \u03c0 < 3.15;\n  abs_one/abs_neg for |x\u00b11|; one_div_le_one_div_of_le takes the small\n  side's positivity first. Next: 5e-v-d (Schwarz squeeze \u27f9 \u2203 B\n  capstone partialFraction_identity).\n- Session 034 (2026-08-23): **ii\u2032-5e-v-d COMPLETE \u2014 ii\u2032-5e DONE**\n  (commit 5a262a1; new file LiSqueeze.lean, ~330 lines, clean, zero\n  warnings; LiCircleBound + LiSqueeze root-imported; full build GREEN;\n  audit-session034-axioms.txt: 5 decls, 3 standard axioms only).\n  `C0hat_add_two_le` (\u0108\u2080(R+2) \u2264 5\u00b7log R, R \u2265 16002);\n  `not_badPoint_on_gapCircle` (every gap-circle point good);\n  `gentire_circle_le` (the circle bound transfers to Gentire);\n  **`gentire_const`** (the Schwarz squeeze: max-modulus via Zeta23's\n  AnalyticOn.norm_le_of_norm_le_on_sphere + the ball-form Schwarz lemma\n  on the \u03b3-gap circle sequence; growth RB \u2264 C\u2080\u2032 + 64\u00b7C\u2081\u00b7Q\u00b3 with\n  Q := R^{1/4}, R = Q\u2074 (Real.log_le_rpow_div + pow_le_pow_left\u2080 +\n  rpow_inv_natCast_pow), radius choice Q \u2265 2 + (128\u00b7C\u2081+2\u00b7C\u2080\u2032)\u00b7\u2016z\u2080\u2016/\u03b5\n  \u27f9 dist \u2264 \u03b5 \u27f9 Gentire \u2261 Gentire 0); **THE CAPSTONE\n  `partialFraction_identity (hZC : ZeroCountProp)`**: \u2203 B : \u2102, \u2200 s\n  good, logDeriv riemannZeta s = B + seriesFun s \u2212 1/s \u2212 1/(s\u22121) +\n  (log \u03c0)/2 \u2212 \u03c8(s/2)/2 \u2014 the partial-fraction identity Lean-proved\n  modulo ONLY the declared perimeter (first perimeter use in the 5e\n  chain: the \u03b3-gap circles need ZeroCountProp). Banked: le_or_lt\n  absent (le_or_gt + the dist/2 contradiction closes the squeeze);\n  set-Q + rw [\u2190 hQ] after push_cast for the rpow_inv_natCast_pow\n  bridge; log_le_rpow_div's exponent-hypothesis form. Next: ii\u2032-5f\n  (D-056's tight constants 10.5/48 from the identity) \u2192 ii\u2032-3b \u2192\n  ii\u2032-3c \u2192 ii\u2032-6 \u2192 ii\u2032-7.\n- Session 035 (2026-08-23/24): **ii\u2032-5f STARTED \u2014 5f-0 + 5f-i + piece\n  6 COMPLETE** (commits 75172e6, f850d9a, 0cca091, d808f52, 1eeda9b,\n  c9c1362, b5e3f53). **Perimeter repair** (user-approved): ZeroCountProp\n  strengthened to the mult-weighted form (the second ii\u2032-1a-class\n  encoding defect \u2014 the unweighted set-card under-captured the declared\n  Trudgian N(T) source; `one_le_zeroMult` bridge via\n  analyticOrderAt_ne_zero + ENat.toNat_pos; exists_zero_avoiding_T +\n  exists_gapCircle_radius adapted via card \u2264 \u03a3 mult; full build GREEN;\n  audit-session035-axioms.txt: 5 decls, 3 standard axioms only).\n  **P1/P2 perimeter additions** (user-approved, D-069): ZeroCountProp2\n  (the two-unit Trudgian specialization 0.6\u00b7L + 0.886\u00b7LL + 2.7) +\n  NoLowZeros (|\u03b3| \u2265 14, Platt-class zero-location certificate).\n  **D-069 Finding 1**: D-056's piece-2 one-C\u2080 usage is for a TWO-unit\n  window \u2014 the honest two-unit form makes the assembly fit 10.5/48\n  (margin \u2248 1.9). **Finding 2** (ii\u2032-6 map): H(T) clearance coverage\n  (honest \u2248 7\u00b7\u0108\u2080\u00b2 vs baked 3\u00b7\u0108\u2080\u00b2). **5f-i** (LiTightR.lean, new file):\n  tsum_split_finset_complex, nearZerosSub, seriesDiffTerm +\n  seriesFun_sub_seriesFun, **Rexpr_decomp** (the six-piece\n  reference-point decomposition; B cancels; linear_combination\n  hsid \u2212 hs\u2080id + hdiff + hsplit + hnear), piece 1\n  `dirichletC2_le_one` (the level-2 integral machinery:\n  hasDerivAt_neg_log_add_one_div + integral_Ioi_of_hasDerivAt_of_tendsto'\n  + AntitoneOn.tsum_comp_add_le_integral + the log2/log3 numeric fold),\n  piece 2 `near_sum_refPoint_le`, pieces 4/5 `one_div_diff_le` (\u2264\n  0.045). **5f-ii piece 6**: `log_diff_le` (the segment-FTC log\n  bound \u2264 5/t) + `digamma_diff_le` (\u2016(\u03c8(s/2)\u2212\u03c8(s\u2080/2))/2\u2016 \u2264 6/t via the\n  +2 shift + StirlingVert.digamma_stirling + digamma_add_natCast). The\n  sharp Lemma-D remainder turned out UNNECESSARY (digamma_stirling's\n  3/im\u00b2 suffices; piece 3's sharper interval sum freed the budget).\n  Banked: the real-cast-first ((t/2 : \u211d) : \u2102)\u00b7I form; re/im ext-goals\n  via explicit per-component rw chains; field_simp can close the goal;\n  Summable.sum_add_tsum_nat_add method form; cpow_natCast's (2:\u2102) =\n  ((2:\u2115):\u2102) bridge. Next: piece 3 (the far-sum interval machine) \u2192\n  5f-iii (assembly + pinch + capstone) \u2192 ii\u2032-3b \u2192 ii\u2032-3c \u2192 ii\u2032-6 \u2192\n  ii\u2032-7.\n- Session 036 (2026-08-24): **ii\u2032-5f COMPLETE** (commits 79c506b,\n  0829421, 7a2af96, 642b851, 22b98c9, b347559, 52bb2cb, e6d57e1).\n  **Piece 3** (LiTightR.lean sections 9\u201319, ~2700 lines): certified\n  numerics (integral-comparison log machines + all certified log/exp/\n  sqrt bounds), the farW weight with S\u2083 \u2264 1.3476 (4 exact sqrt-rational\n  terms + telescope 1/4), the six tail bricks via the antitone-integral\n  machine (RW\u2080/1/2 = 0.1/0.3303/0.1216 with the loglog \u2264 (1/e)log\n  trick; LA\u2080/1/2 = 1/23/0.1687/0.0621 with the \u2212log x/(x+10) +\n  (1/10)log(x/(x+10)) antiderivative), the C0hat bridges (2k+1/j+1/\n  2t+1 + C0hat(2t+1) \u2264 C0hat(t+1)+0.55), the conj machinery\n  (hasDerivAt_conj_of_conj_eq \u2192 iteratedDeriv_riemannZeta_conj \u2192\n  analyticOrderAt_riemannZeta_conj \u2192 zeroMult_conj), farG + summability\n  + the per-term bound + norm reduction, the main bucket machine\n  (unit_family_le + main_bucket_count + farG_main_le), the two tail\n  machines (farGLeft_le \u2264 1.1729, farGRight_le \u2264 2.7343, ENNReal\n  fiberwise cloned from LiCircleBound), the tail split farG_tail_eq,\n  and **far_series_le \u2264 12.1284\u00b7C\u2080 + 7.2425**. **5f-iii** (sections\n  20\u201321, ~550 lines): the pinch lemma pinch_tight_R (11.6318\u00b7LL \u2212\n  4.6484\u00b7L \u2264 0.397094 for L \u2265 log 12 \u2014 concave tangent at the certified\n  critical point 2.5024, f\u2032 antitone, FTC both directions, f(2.5024) \u2264\n  \u22120.96231 certified), the supporting bounds (log 12 = 4 log 2 \u2212\n  log(4/3) \u2265 2.4848 via the 4-term neg_log machine, log 12 \u2264 2.5024,\n  log 3 \u2264 1.0987, log 2.5024 \u2264 0.9173), the C0hat L/LL conversion, and\n  **THE CAPSTONE `logDeriv_riemannZeta_sub_nearZeros_le_tight (hZC)\n  (hZC2) (hNLZ)`: \u2016logDeriv \u03b6 s \u2212 \u03a3_{near} m/(s\u2212\u03c1)\u2016 \u2264 10.5\u00b7log(t+2) +\n  48 PROVED** (six-piece assembly: dirichletC2 \u2264 1 + near two-unit\n  0.6L+0.886LL+2.7 + far 12.1284\u00b7C\u2080+7.2425 + 2\u00d70.045 + 6/t \u2264 0.6;\n  fold 5.8516L + 11.6318LL + 47.6029 \u2264 10.5L + 48 via the pinch).\n  Audits session036/036b: 33 decls, 3 standard axioms only; full build\n  GREEN (8762 jobs). Banked: `a * b / c` parses as `(a\u00b7b)/c` (write\n  `c * (b / d)` with parens or isDefEq explodes); Float-literal pinning;\n  rw first-unifier-only; x\u207b\u00b9 vs 1/x; div/mul_le_mul signatures;\n  pow_nonneg for odd powers; Summable.mul_left/add lambda forms;\n  tsum_add beta-rfl bridges; two_le_C0hat for C0hat nonnegativity;\n  pinch coefficient-exactness (mixed-sign rounding breaks large L).\n  Next: ii\u2032-3b (moments) \u2192 ii\u2032-3c \u2192 ii\u2032-6 \u2192 ii\u2032-7.\n- Session 037 (2026-08-24, HALT at a clean boundary \u2014 user log-off):\n  **capstone dependency audit** (user-requested, pre-ii\u2032-3b):\n  AuditSession037.lean + audit-session037-axioms.txt \u2014 `#print axioms\n  logDeriv_riemannZeta_sub_nearZeros_le_tight` = [propext,\n  Classical.choice, Quot.sound] ONLY; the exact perimeter recorded\n  verbatim (ZeroCountProp unit-window mult-weighted \u2264 \u0108\u2080(t+1);\n  ZeroCountProp2 two-unit 0.6L+0.886LL+2.7; NoLowZeros |\u03b3| \u2265 14;\n  nearZerosSub/Zeta23.zeroMult/zeroAbsWindow constructs).\n  **ii\u2032-3b STARTED \u2014 ROUTE REVISION (D-070)**: the moments (M) come\n  from 5e's partialFraction_identity by pure algebra + series calculus\n  (NO contours \u2014 the contour work was 5e's): gFun := logDeriv xiL =\n  B + seriesFun at good points; xiL entire via the \u039b\u2080 closed form;\n  perimeter ZeroCountProp ONLY (5f's hZC2/hNLZ not needed).\n  **LiMoments.lean \u00a71\u2013\u00a74 COMPLETE, build GREEN** (~730 lines): xiL +\n  conj/reflect subtype equivs, (G) gFun_eq_momentB, evaluations\n  gFun_zero/gFun_one/gFun_one_eq_neg (FE sign), the summability budget\n  (master \u03a3 mult/\u2016\u03c1\u2016\u00b2 + AM-GM mixed bound), the reindex machinery\n  (sigmaP_eq_unpaired k \u2265 2 via the conj reindex, vTerm_tsum_eq_zero\n  via V = W = \u2212V), **k = 1 PROVED: sigmaP_one_eq_neg_gFun_zero**\n  (2\u03c3\u2081 = seriesFun 1 = \u22122\u00b7gFun 0 by the FE sign). \u00a75/\u00a76 fully\n  designed + Mathlib-probed (iteratedDerivWithin_tsum/\n  SummableLocallyUniformlyOn_of_locally_bounded/iteratedDeriv_neg/\n  AnalyticAt.contDiffAt/Equiv.tsum_eq/Summable.tsum_add signatures all\n  confirmed); skeleton banked in journal-037. Banked: SummationFilter\n  refactor (tsum_add/tsum_sub are method-form Summable.tsum_add only;\n  tsum_neg/tsum_zero/tsum_congr/tsum_mul_left plain);\n  eq_zero_of_neg_eq needs LinearOrder (\u2102 N/A \u2192 2V = 0 route);\n  Complex.norm_conj takes starRingEnd directly; ascribe EVERY tsum\n  binder (zeroMult \u03c1 coerces \u03c1 to \u2102 otherwise); beta-redex\n  show-before-rw; deriv_comp's point arg explicit; field_simp's\n  trailing-ring errors \u00d73. Housekeeping: Scratch.lean (old session-029\n  audit script) overwritten with the lemma probe \u2014 session-029 audit\n  results preserved in audit-session029-axioms.txt. Next: LiMoments \u00a75\n  (termwise iterated derivation at 0, k \u2265 2) \u2192 \u00a76 (capstone\n  sigmaP_eq_neg_iteratedDeriv_gFun_div) \u2192 root import (with LiTightR)\n  \u2192 audit \u2192 ii\u2032-3c.\n- Session 038 (2026-08-24): **ii\u2032-3b COMPLETE** (LiMoments.lean \u00a75/\u00a76,\n  ~290 new lines, file now ~1020 lines). \u00a75: iteratedDeriv_zpow_neg_one,\n  iteratedDeriv_seriesTerm, seriesTerm_deriv_summableLocallyUniformlyOn\n  (the M-test on ball(0, \u03b4/2); dominator j!\u00b72^{j+1}\u00b7(1/\u03b4)^{j\u22121}\u00b7mult/\u2016\u03c1\u2016\u00b2;\n  the h1/h2/h3 one_div/div_pow/pow_add chain), iteratedDeriv_seriesFun_zero\n  (the LiDigamma:749\u2013785 iteratedDerivWithin_tsum pattern verbatim; local\n  pole_free via norm_sub_norm_le + norm_sub_rev). \u00a76:\n  gFun_eventuallyEq_zero (eventually_nhdsWithin_iff + point values) +\n  **THE CAPSTONE `sigmaP_eq_neg_iteratedDeriv_gFun_div (hZC :\n  ZeroCountProp)`: sigmaP k = \u2212(iteratedDeriv (k\u22121) gFun 0)/(k\u22121)!\n  PROVED for ALL k \u2265 1** (k=1: \u00a74 reindex; k\u22652: (G) + \u00a75 + per-term\n  sign algebra (\u22121)^k\u00b7(\u22121)^{k+1} = \u22121 + \u2190 sigmaP_eq_unpaired +\n  field_simp k! \u2260 0 \u2014 FIRST-PASS GREEN). Perimeter: ZeroCountProp ONLY.\n  Closure: LiTightR + LiMoments root-imported; full build GREEN (8770\n  jobs); AuditSession038.lean + audit-session038-axioms.txt \u2014 23 decls,\n  [propext, Classical.choice, Quot.sound] ONLY, 0 sorryAx. Banked:\n  factorial `!` needs `open scoped Nat` (the parse error looks like\n  spacing); Summable.mul_left dominators CONSTANT-FIRST (D \u03c1 * C\n  whnf-loops the refine); rw [seriesFun] fails UNAPPLIED (show\n  beta-expansion); norm_sub_norm_le has no abs on the LHS here;\n  simpa-only a copy of memberships before rw-ing them away;\n  (neg_neg _).symm funext direction; simp only [neg_mul, neg_neg] for\n  buried negs; iteratedDeriv_add needs the Pi.add bridge (hsplit :=\n  rfl); calc reassociation via trailing mul_assoc. CONTINUED same day:\n  **ii\u2032-3c COMPLETE** (LiCrux.lean, ~430 lines, root-imported) \u2014 the FE\n  relation (gFun_one_sub_fun + iteratedDeriv_gFun_zero via the\n  unconditional iteratedDeriv_comp_const_sub), the shift expansion\n  (gFun_one_add_punctured/eventuallyEq), iteratedDeriv_gFun_one \u27f9\n  **lagarias_4_10_a (hZC) PROVED** (all k \u2265 1) \u27f9 **THE CRUX\n  sf_eq_resW1 (hZC) PROVED: (ResW1 n).re = Sf n for n \u2265 1** \u2014 Sf(n) =\n  Res\u2081(n) in Lean, perimeter ZeroCountProp only. Full build GREEN\n  (8771 jobs); audit session038b: 8 decls, 3 standard axioms only.\n  **ii\u2032-3 (ALL of (4.10)) DONE.** Banked: ContDiffAt.congr_of_eventuallyEq\n  takes hev NOT hev.symm; Finset.sum_add RENAMED Finset.sum_add_distrib;\n  succ-normalize via Nat.succ_eq_add_one before Nat.add_sub_cancel;\n  `simp using X.deriv` silently derails (use the direct .deriv term);\n  ContinuousAt.comp numerals not kernel-defeq (add_zero-rw hg FIRST);\n  show-statements ASCII-only (U+2212 breaks the parser); \u2190 hS direction\n  after sum-splits; mul_div_cancel_left\u2080 for (s\u00b7X)/s; div_add_div +\n  div_eq_div_iff + ring as the always-works fraction pattern. CONTINUED:\n  **ii\u2032-6-0 DESIGN COMPLETE (D-071 + E-030 ALL CHECKS PASS)** \u2014 THREE\n  findings: F-A bridge factor-2 (\u03bb_n(T) both-signs \u27f9 honest 4\u00b7FAlt vs\n  baked 2\u00b7FAlt; R-004 unaffected, paper erratum at ii\u2032-7), F-B I_III\n  two-unit count ((2/3)Z2 vs (2/3)\u0108\u2080 \u2014 D-069 Finding 2 exact), F-C\n  baked Bn unprovable beyond ~5\u00d710\u2077 (killers T\u00b7log T outgrow (log T)\u00b2\n  slack: 0.656 at 10\u2075 \u2192 1.012 at 10\u00b9\u00b2). USER-APPROVED 8-step protocol:\n  redefine Bn honestly (4F, (2/3)Z2hat); convexity re-proof; base\n  points re-certification (values improve); endpoint margins re-run;\n  ii\u2032-6 against corrected Bn; paper correction note at ii\u2032-7; audit\n  history preserved (E-030). Perimeter additions approved:\n  ZeroCountGlobalProp + MZeroProp. CONTINUED: **ii\u2032-6-a COMPLETE** \u2014\n  Bn redefined honestly (4F, (2/3)Z2hat); marginTilde_convex re-proved\n  (\u03c8-row literals + norm_num; Z2hat added to the eq_expanded unfold\n  list; a hardcoded const_mul fixed); base points re-certified\n  (329,000/350,000; margins \u2265 7,001/82,501); endpoint margins re-run\n  (14,682/90,653/2.458\u00d710\u00b2\u2076); full build GREEN (8771 jobs); audit\n  session038c: 3 standard axioms only. Banked: lake env lean uses the\n  STALE olean \u2014 lake build the dependency first; re-check certified\n  constants at 1e-4 (114.0655 vs 114.06553 linarith catch).\n  CONTINUED: **ii\u2032-6-b COMPLETE** \u2014 perimeter Props ZeroCountGlobalProp\n  + MZeroProp declared; wide pigeonhole exists_zero_avoiding_T_wide;\n  LiAssembly.lean NEW (sides identity + bridge \u2016\u03a3\u2016 \u2264 4\u00b7FAlt + 1);\n  build GREEN (8772 jobs); audit session038d: 3 standard axioms only.\n  Banked: RectangleBorder-rcases trap (rw + simp only + tauto route);\n  Finset.image plain-function + Set.InjOn; set-x breaks mem_toFinset;\n  linarith proves \u2260; projections for IsNontrivialZero; sq_eq_sq\u2080;\n  pow_le_one\u2080 implicit n. CONTINUED to ii\u2032-6-c design-check \u2014\n  **FINDING F-D (D-072, session end, user paused to think)**: the\n  (6.12) stepping in Lagarias's Thm 6.1 is broken at T = \u221an (product\n  ratio e/2 > 1; right-tail ~e^{0.066\u221an}, ~5.9\u00d710\u00b9\u2070 envelope at\n  n = 10\u2075 measured by E-031); D-036/D-037/R-004's B(n) inherits it\n  (charge \"3.3\" off by ~10\u2077\u00d7; margin collapses for n \u2273 3\u00d710\u2074). The\n  theorem statement survives (verified to 5\u00d710\u2075; sides cancel by\n  conjugation + phase winding); all Lean work to date survives (the\n  bug is in the horizontal piece, not yet built). Repair path (R)\n  verified numerically: T = c\u221an with c > 1.2012 \u27f9 the stepping works\n  (monotone decrease at c = 1.5, 2); N\u2081 \u2192 (T\u2080/c)\u00b2 \u2248 2.25\u20134\u00d710\u00b2\u2074.\n  Literature: no erratum found. Session ends at a clean committed\n  boundary with the direction OPEN.\n\n## 9. SUCCESS CRITERIA (ordered)\n1. \ud83c\udfc6 Full proof of RH (formally verified).\n2. \ud83e\udd47 Unconditional improvement past 2/3 (or past 0.6725 / 5/6).\n3. \ud83e\udd48 New equivalence, reduction, or removal of a known obstruction.\n4. \ud83e\udd49 Rigorously documented obstruction map advancing the field.",
  "structuredPatch": [
    {
      "oldStart": 867,
      "oldLines": 11,
      "newStart": 867,
      "newLines": 18,
      "lines": [
        "         8.38 + IIMaj/4 per side \u27f9 1.5\u00b7IIMaj total in Bn, the",
        "         convexity-safe coefficient). E-034 re-validated at IIMaj/4:",
        "         ALL CHECKS PASS.",
        "-      \u2192 ii\u2032-6-a2 (Bn dog-leg redefinition \u2014 freeze-exception protocol:",
        "-        honest redefinition with horizontalRightDoglegBound(n)",
        "-        explicit; convexity re-proof; base-point re-certification;",
        "-        endpoint margins at N\u2081 = (T\u2080\u22121)\u00b2; git history; paper-correction",
        "-        queue; full axiom audit).",
        "+      \u2192 ii\u2032-6-a2 COMPLETE (session 040): DogLegRight def + Bn",
        "+        redefined (horizontal share 2(e\u2074+1)(7H\u0302) + 2\u00b7DogLegRight,",
        "+        T = \u221an+1 UNCHANGED \u2014 N\u2081 = (T\u2080\u22121)\u00b2 \u2248 9\u00d710\u00b2\u2074 PRESERVED);",
        "+        margin lockstep at coefficient level; 4/3-bracket strengthening",
        "+        cherry-picked onto master (e11ad95); marginTilde_convex",
        "+        re-proved (1.5\u00b7IIMaj, strict); base points re-certified",
        "+        (Bn(8e4) \u2208 [273k, 332k], Bn(10\u2075) \u2264 352k \u27f9 margin(8e4) \u2265",
        "+        4 001, hbase2 66 001 < 80 501); endpoints UNCHANGED; build",
        "+        GREEN (8773 jobs); audit: 41 decls, 3 standard axioms, 0 sorryAx.",
        "+      THEN THE ORIGINAL PLAN RESUMES (D-074 \u00a78 return map): ii\u2032-6-c",
        "+      (four side bounds with the repaired horizontal) \u2192 ii\u2032-6-d",
        "+      (fold \u27f9 sfBoundProp) \u2192 ii\u2032-7 (closure at the ORIGINAL N\u2081).",
        "       THEN THE ORIGINAL PLAN RESUMES (D-074 \u00a78 return map): ii\u2032-6-c",
        "       (four side bounds with the repaired horizontal) \u2192 ii\u2032-6-d (fold",
        "       \u27f9 sfBoundProp) \u2192 ii\u2032-7 (closure at the ORIGINAL N\u2081 \u2248 9\u00d710\u00b2\u2074)."
      ]
    }
  ],
  "userModified": false,
  "replaceAll": false
}