{
  "file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDigammaLeft.lean",
  "old_string": "      have h := hker_summ.sum_add_tsum_nat_add N\n      trace_state\n      exact h.symm",
  "new_string": "      rw [hker_summ.sum_add_tsum_nat_add N]"
}

{
  "filePath": "D:\\Python\\Quantum\\STATE.md",
  "oldString": "**Paper:** research/paper/paperA.tex \u2014 Paper A (finite-height Li +\nmachine-verified reduction), **9 pp, compiles clean, zero undefined\nrefs, CLOSED at ii\u2032-7** (eight-hypotheses headline; B(n) display\ncorrected + the F-A/F-B/F-D/F-E correction-note footnote; Appendix B:\nsecond tier COMPLETE). paperA.pdf committed. paperB.tex \u2014 spectral-\nline research note (skeleton, standing items in \u00a70), 6 pp. draft.tex \u2014\nFROZEN combined archive copy (12 pp).",
  "newString": "**Paper:** research/paper/paperA.tex \u2014 Paper A (finite-height Li +\nmachine-verified reduction), **11 pp, compiles clean, zero undefined\nrefs, REVISED at session 042** (seven-hypotheses headline; the theorem\nstatement exposes all assumptions; B(n) display corrected + the\nF-A/F-B/F-E correction-note footnote; the F-D dog-leg promoted to\n\u00a73.1; Appendix B: second tier COMPLETE + the verbatim Lean signature +\nthe instantiation list + the dependency-chain diagram; Section 2\ncompressed to one paragraph; hedged novelty with Oesterl\u00e9's\nunpublished precursor noted). paperA.pdf committed. paperB.tex \u2014\nspectral-line research note (skeleton, standing items in \u00a70), 6 pp.\ndraft.tex \u2014 FROZEN combined archive copy (12 pp).",
  "originalFile": "# STATE.md \u2014 NGUYEN-RH-1 RESUME POINT\n# \u2b50 READ THIS FIRST at the start of every session.\nLast updated: 2026-08-26 (session 042) | **ii\u2032-6 + ii\u2032-7 COMPLETE\n(session 041); SESSION-042 REVIEW REVISION COMPLETE: the user's\npaper-A review fully actioned \u2014 the finite-verification certificate\nRETRACTED (Misguich\u2013Voros = deformed sequence, private communication)\nand replaced by Johansson 2015 \u00a7 4.2 (rigorous, published, ordinary\n\u03bb_n to 10\u2075); LiVerifiedUpTo (5\u00b710\u2075) \u2192 (10\u2075) in Lean (79c96f2, audit\nclean); the hypothesis count corrected (8 \u2192 SEVEN, caught by the\nuser); the theorem statement now exposes all assumptions; F-D dog-leg\npromoted to its own \u00a73.1 with precise Lagarias wording (proof-gap\nframing, not theorem-false); Appendix B gains the verbatim Lean\nsignature + the instantiation list + the dependency-chain diagram;\nnovelty claims hedged (Oesterl\u00e9 2000's unpublished precursor n \u2264 T\u2080\u00b2\nnoted; Lagarias 2007's published weaker window); Section 2 compressed\nto one paragraph; revision date updated. Paper A compiles clean,\n11 pp, zero undefined refs. NEXT: user read-through of the REVISED\npaperA.pdf + submission decision.**\n\n## SESSION 042 HEADLINES (review revision \u2014 see journal-042)\n1. **Certificate RETRACTED + REPLACED (79c96f2)**: the user's top\n   finding \u2014 Misguich\u2013Voros (Voros 2020, Exp. Math. 29(4)) verifies a\n   DEFORMED Keiper\u2013Li sequence \u039b_n (G. Misguich, private communication\n   2017), not the ordinary \u03bb_n, so the citation could not carry the\n   finite splice. Verified against the paper's own text (arXiv\n   1703.02844). Replacement: **Johansson 2015 \u00a7 4.2** (Numer. Algor.\n   69:253\u2013270, arXiv 1309.2877) \u2014 rigorous interval-arithmetic\n   computation of the ORDINARY Keiper\u2013Li coefficients \u03bb_0\u2026\u03bb_{100000},\n   all positive (\u03bb_100000 certified to ~2900 digits). Lean perimeter\n   `LiVerifiedUpTo` reduced (5\u00b710\u2075) \u2192 (10\u2075) (the assembly's hfinite\n   branch uses exactly n < 10\u2075 \u2014 nothing else changes); rebuild GREEN\n   (8775 jobs); audit re-run clean.\n2. **Count caught by the user: EIGHT \u2192 SEVEN named hypotheses** (2\n   computational: RHUpTo, LiVerifiedUpTo; 5 analytic: ZeroCountProp,\n   ZeroCountProp2, ZeroCountGlobalProp, NoLowZeros, MZeroProp). Fixed\n   in the paper (abstract/intro/App B + the verbatim signature),\n   LiClosed docstrings, NGUYEN.md, R-004, this file.\n3. **Theorem statement \u2194 trust boundary aligned**: both Theorem\n   environments now assume (i) RH verified to T\u2080 (Platt\u2013Trudgian)\n   (ii) \u03bb_n > 0 for n \u2264 10\u2075 (Step 5); Appendix B's new instantiation\n   list maps each of the seven hypotheses to its cited\n   source/certificate.\n4. **F-D dog-leg promoted to \u00a73.1** (\"Repair of the right-horizontal\n   estimate\") with the precise Lagarias framing: \"the geometric-\n   decrease conclusion following (6.12) is not implied by the\n   displayed bounds when T \u224d \u221an, since the resulting majorant ratio is\n   e/2 > 1\" \u2014 a proof-gap statement, not a theorem-false claim; the\n   exact deformation H_low = H_high \u2212 V_right + V_left displayed; the\n   open hidden-cancellation question (E-032) recorded but not relied\n   on. The Step-2 footnote now carries only F-A/F-B/F-E.\n5. **Novelty hedged**: \"first\" \u2192 \"we have found no previous explicit\n   assembly\"; \"maximal content\" \u2192 the narrow Voros form (eventual\n   positivity of all large \u03bb_n \u27f9 RH, so no result short of RH asserts\n   an infinite positive tail); **Oesterl\u00e9 2000's unpublished precursor\n   (prop. 2: RH-to-T\u2080 \u27f9 \u03bb_n \u2265 0 for n \u2264 T\u2080\u00b2, cited in Voros 2020)\n   explicitly noted** + Lagarias 2007's published weaker window.\n6. **Appendix B**: verbatim Lean signature (tt-quote, unicode via\n   math), the instantiation list, and the dependency-chain display\n   (partial fractions \u2192 S_f = Res\u2081 \u2192 rectangle identity \u2192 four side\n   bounds \u2192 sfBoundProp \u2192 lambda_pos_finite_height_closed).\n7. **Section 2 compressed** to one paragraph (the certificate method;\n   the R(\u03c8) display and rank-trace detail deferred to the companion\n   note). **Revision date** 2026-08-20 \u2192 2026-08-26.\n8. **Side effects checked**: cover-letter.md + referee-list.md\n   Misguich mentions corrected to Johansson; draft.tex (FROZEN),\n   paperB.tex, and the user's correspondence package untouched.\n\n## SESSION 041 HEADLINES (ii\u2032-6-c..6-d + ii\u2032-7 \u2014 THE CLOSURE SESSION)\n1. **ii\u2032-6-c COMPLETE** (4 commits): 6-c-ii I_III\n   `vIntegral_Jlag_left_norm_le` (6e5a98f \u2014 tails via the 5f tight\n   R-bound + near count (2/5)Z\u2082, middle via the perimeter MZeroProp,\n   even-symmetry tail identification); 6-c-iii I_I F-E form\n   `vIntegral_Jlag_right_le_exp_third_IIMaj` (9bd8ba9 \u2014 the uniform\n   kernel lemma `kFun_right_vertical_norm_le_exp_sqrt_add_third`:\n   plain triangle + \u2016w\u22121\u2016 \u2265 re(w\u22121) = 2\u221an\u22121, worst case t = 0);\n   6-c-iv the mid-horizontal segment machine (1fed1df \u2014 the\n   arcsinh-FTC `integral_one_div_sqrt_sq_add_sq` from scratch: the\n   direct antiderivative F(\u03c3) = log((\u03c3\u2212\u03b2)+\u221a((\u03c3\u2212\u03b2)\u00b2+\u03b4\u00b2)), g\u2032 = g/\u221ah\n   exactly; endpoints F(3) \u2264 log(6+\u03b4), \u2212F(\u22125/2) \u2264 log(7+\u03b4)+2log(1/\u03b4)\n   via the rationalization \u03b4\u00b2/(u+\u221a); per-zero \u2264 2\u00b7log(16.5/\u03b4) by PURE\n   log-mono ((6+\u03b4)(7+\u03b4) \u2264 56 \u2264 272.25 = 16.5\u00b2 \u2014 NO certified log\n   numerics)); 6-c-v the horizontal assembly (5d3dc0a \u2014 split at 3 via\n   HIntegral_split, mid by 6-c-iv, tails by DL-5, both sides).\n2. **6-d THE FOLD (774fec5): `sfBoundProp : SfBoundProp` PROVED** \u2014\n   |Sf n| \u2264 Bn FAlt n on [10\u2075, N\u2081] from EXACTLY the six declared\n   perimeter hypotheses (RHUpTo, ZeroCountProp, ZeroCountProp2,\n   ZeroCountGlobalProp, NoLowZeros, MZeroProp). `pinch_horizontal`\n   (NI + 5.5R \u2264 7\u00b7H\u0302) discharged by a fully elementary chain:\n   \u0108\u2080(\u221an+2) \u2264 \u221an+2 (`C0hat_le_self`, log x \u2264 x/e with 1/e \u2264 0.36789\n   from Real.exp_one_gt_d9, loglog \u2264 log\u22121) \u27f9 148.5\u00b7\u0108\u2080(\u221an+2) \u2264\n   (\u221an+2)\u00b2 \u27f9 its log \u2264 2\u00b7log(T+2); Z\u2082 \u2264 2\u00b7\u0108\u2080; \u0108\u2080 \u2265 0.433\u00b7log and\n   8 \u2264 21\u00b70.433 = 9.093; 5.5 \u2264 7 on the R-part. The bridge cloned at\n   (hTle : T \u2264 3\u00b710\u00b9\u00b2) \u2014 the range the internal\n   `zeroSum_nontriv_norm_le` actually uses (the public T \u2264 3\u00b710\u00b9\u00b2\u22121\n   hypothesis fails at the very top: n = N\u2081 has \u221an = 3\u00b710\u00b9\u00b2\u22121 exactly\n   and the pigeonhole T can land in (3\u00b710\u00b9\u00b2\u22121, 3\u00b710\u00b9\u00b2]).\n3. **ii\u2032-7a+7b (a0943a6)**: `lambda_pos_finite_height_closed` PROVED\n   (LiClosed.lean, root-imported) \u2014 \u03bb_n > 0 for ALL 1 \u2264 n \u2264 N\u2081 from\n   the declared hypotheses (count corrected session 042: SEVEN \u2014 two\n   computational certificates:\n   RHUpTo, LiVerifiedUpTo; five analytic perimeter Props: ZeroCountProp,\n   ZeroCountProp2, ZeroCountGlobalProp, NoLowZeros, MZeroProp). Full\n   axiom audit (AuditSession041): 29 declarations \u2014 ALL [propext,\n   Classical.choice, Quot.sound] only, 0 sorryAx.\n4. **ii\u2032-7c (b64a839)**: Paper A closed (compiles clean, 9 pp, zero\n   undefined refs): abstract/intro \u2192 the seven-hypotheses headline\n   (session-042 recount);\n   \u00a73 Step 2 the B(n) display corrected (4F(T), (2/3)Z\u2082(T),\n   2(e\u2074+1)\u00b77H(T) + 2\u00b7DL(n), I_Maj) + the F-A/F-B/F-D/F-E\n   correction-note footnote; \u00a73 Step 3 the bridge 4F (both signs);\n   Appendix B rewritten (second tier COMPLETE \u2014 SfBoundProp machine-\n   proved, the six analytic inputs enumerated, the full complex-\n   analytic content list); AI Contribution Statement factual refresh\n   (sessions 001\u2013041, closure declarations).\n5. **ii\u2032-7d (this commit)**: archive closed \u2014 D-037 erratum block\n   (the four corrections with pointers), R-004 Lean-closure status\n   line, NGUYEN.md (Phase 5B \u2192 COMPLETE, ii\u2032-6/ii\u2032-7 checked, Ledger\n   #6 machine-proved note), STATE.md (this file), journal-041.\n6. **Banked gotchas (journal-041)**: \u03a3 (U+03A3) is NOT an identifier\n   character in Lean 4 (lexes as Sigma-notation; a phantom ?m.NNN\n   metavariable goal at the DECLARATION HEAD is the tell-tale of a\n   downstream parse break); `\u222b x in a..b, body` captures trailing +/\u2212\n   into the integrand (parenthesize every integral summand);\n   ContinuousAt.comp/ContinuousWithinAt.comp need (g :=) (f :=)\n   (x :=) pinned (arg-first elaboration misdecomposes the point);\n   Continuous.div/.mul/.sub produce Pi-op forms (ascribe the per-term\n   type or show-bridge to the Pi form \u2014 the const ?c otherwise leaks\n   as an unsolved ?m); linarith CANNOT multiply by atom-constants\n   ((1/(2\u03c0)), (e\u2074+1)) \u2014 every such step needs a pre-packaged\n   mul_le_mul_of_nonneg_*; in large contexts use linarith only /\n   nlinarith only (the context scan on giant types deterministically\n   times out at isDefEq); norm_le_insert' : \u2016a\u2016 \u2264 \u2016b\u2016+\u2016a\u2212b\u2016 (the\n   unprimed has the args swapped); eq_div_iff for c = a/b goals\n   (div_eq_iff is for a/b = c); Finset.sum_mul for constant-RIGHT\n   extraction (Finset.mul_sum is constant-LEFT); le_of_pow_le_pow_left\u2080\n   takes the nonneg on the RIGHT (b) side; Real.add_one_le_exp is\n   x+1 \u2264 e^x (not 1+x \u2014 bridge by linarith); neg_le_abs : \u2212a \u2264 |a|\n   (neg_abs_le is \u2212|a| \u2264 a); HasDerivAt.pow yields Pi.pow forms (simpa\n   bridges); rw [hre] closes `-5/2 \u2264 -5/2` by auto-rfl le_refl\n   (le_of_eq hre.symm is deterministic).\n\n## CURRENT POSITION\n\u2714 PHASE 0, 1, 3, 4 COMPLETE. PHASE 2 (Track B): mapped to exhaustion\nat current technology (2.6\u20132.13, parked). PHASE 5: 5.3 \u2714 5.4 \u2714 5.2 \u2714\n(live). PHASE 5B (tier ii\u2032): **COMPLETE (session 041)** \u2014 all\nsub-stages ii\u2032-0..ii\u2032-7 done (see NGUYEN.md \u00a75B for the full log).\n\n**Theorem status (session 041 \u2014 the closed forms):**\n- T-1 (R-004): [PROVED-CONDITIONAL(computational RH-to-T\u2080;\n  computational finite verification)] \u2014 **FULLY MACHINE-PROVED in\n  Lean 4**: `lambda_pos_finite_height_closed` (LiClosed.lean) \u2014\n  \u03bb_n > 0 for ALL 1 \u2264 n \u2264 N\u2081 = (3\u00d710\u00b9\u00b2\u22121)\u00b2 from EXACTLY SEVEN\n  declared hypotheses: RHUpTo (Platt\u2013Trudgian), LiVerifiedUpTo(10\u2075)\n  (finite Li verification: E-011/E-015 to 3000 + Johansson 2015 \u00a7 4.2\n  rigorous ordinary-\u03bb_n table to 10\u2075), ZeroCountProp/ZeroCountProp2/\n  ZeroCountGlobalProp (Trudgian N(T)/S(T) forms), NoLowZeros\n  (Platt-class zero-location), MZeroProp (M\u2080 interval certificate).\n  Axiom audit on the full chain: [propext, Classical.choice,\n  Quot.sound] only, 0 sorryAx (AuditSession041, 29 decls).\n  sorryAx remains ONLY on the 5 skeleton statements (1 Suzuki + 4\n  valley) by design.\n- T-2 (R-003 + D-041): factorization + (\u2605) \u27fa (1.12) [PROVED modulo\n  Phase-5 formalities]; (1.12) \u27f9 spec(D) \u2282 \u211d [PROVED via Suzuki + D1];\n  \u21d0 [SKELETON L3/L4].\n- T-3 (valley, D-049 + D-058): [PROVED-CONDITIONAL(RH)].\n\n**Paper:** research/paper/paperA.tex \u2014 Paper A (finite-height Li +\nmachine-verified reduction), **9 pp, compiles clean, zero undefined\nrefs, CLOSED at ii\u2032-7** (eight-hypotheses headline; B(n) display\ncorrected + the F-A/F-B/F-D/F-E correction-note footnote; Appendix B:\nsecond tier COMPLETE). paperA.pdf committed. paperB.tex \u2014 spectral-\nline research note (skeleton, standing items in \u00a70), 6 pp. draft.tex \u2014\nFROZEN combined archive copy (12 pp).\n\n**Lean:** research/lean/NguyenRH1/ \u2014 full build GREEN (8775 jobs);\nall 26 modules root-imported incl. LiSideBounds (ii\u2032-6-c..d) and\nLiClosed (ii\u2032-7). sorryAx remains ONLY on: R003_exact_factorization\n(tier iv) + 4 valley statements (tier iii).\n\n**Deprioritized / open threads:** a=13+ push; adversary-ceiling LP;\nT4b; \u03bb-channel (G-004); \u03b8-channel (dead, E-024); Paper B Task 1\n(R-003 tempered-FT bookkeeping trace, queued); user read-through of\npaperA.pdf (NOW THE FRONT ITEM \u2014 nothing blocks it); repo-publication\nprep; submission decision (cover-letter.md + referee-list.md exist\nfrom session 013, target Experimental Mathematics); the c = 1.5\nfallback branch wip/c-1.5-margin-redo (642d47a, preserved, unneeded);\nthe T = \u221an hidden-cancellation open question (D-073 \u00a78 D4); the\nLagarias F-D correspondence package (user's own work-in-progress in\nresearch/correspondence/lagarias-F-D-package/, uncommitted \u2014 NOT\nmine to commit).\n\n## NEXT ACTION\n**AT A CLEAN BOUNDARY (session 041 end, ii\u2032-6 + ii\u2032-7 COMPLETE). The\nuser's read-through of paperA.pdf + the submission decision is the\nfront item. If told to continue research: Paper B Task 1 (R-003\ntempered-FT bookkeeping trace) or the parked Track-B remainders per\nthe user's call.**\n\n## SUPERSEDED RETROSPECTIVES (sessions 037\u2013040)\nThe long session-037/038/039/040 headline blocks and the ii\u2032-6-a..c\nsub-stage maps that previously lived here are superseded by the\nsession-041 closure above; the full record is in git history (commits\nthrough 2979f57) and journals 037\u2013040. Key preserved facts: the c = 1.5\nfallback branch wip/c-1.5-margin-redo (642d47a, BUILD BROKEN mid-\nconvexity, resume map in its commit message); the D-073 \u00a78 D4 open\nquestion (T = \u221an per-side claim empirically true by hidden\ncancellation, E-032).\n\n## COMPLETED (Sessions 001\u2013010)\n- [x] Phase 0, Phase 1 (Track A \u2192 monitoring mode, D-013).\n- [x] 2.6 V3 root-cause + repair (E-016b/c, D-025).\n- [x] 2.7 R-003 exact factorization (D-026, E-017/D-027, ledger #5).\n- [x] 2.8 a=12 no transition (E-018/D-028, backend v2, E-019/D-029).\n- [x] 1.6 \u03be\u2032-world saturated (E-020b/D-030); 1.7 T4b closed (D-031).\n- [x] 3.3 \u2192 G-003; 3.4 (Suzuki line spawned); 3.5 design (D-032/D-033).\n- [x] (\u2605) design (D-034/D-035); new tasks 2.9/2.10/2.11.\n- [x] 3.6 D-036 explicit contour constants (session 006 cont.9).\n- [x] 3.7 E-021 (session 007): S_\u221e exact + c\u2080, |S_f| curve, A/B\u2080\n      measured; 6-bug saga documented.\n- [x] Session 008: regroup; R7 resources atlas registered; 3.8\n      COMPLETE (D-037, E-023, R-004 ledger #6); 2.10 COMPLETE\n      (E-022/E-022b + D-040, valley observable); 2.9-D1 COMPLETE\n      (D-041); 2.11 COMPLETE (D-038); 2.12 COMPLETE (E-024 + D-042,\n      \u03b8-independence); 2.13 COMPLETE (E-025 + D-043, discretization\n      floor; quadratic locking correction).\n- [x] Session 009: PHASE 4 COMPLETE (D-052/D-053/D-054, E-027 + D-055,\n      repairs 4.5a\u2013d: D-056\u2013D-059; R-004 tag restored).\n- [x] Session 010: 5.3 paper draft complete; 5.4 honesty audit (D-060);\n      5.1/5.2 skeleton stage (D-061).\n- [x] Session 011: Lean proof tier (i) COMPLETE \u2014 sInfty_lower_bound,\n      marginTilde_convex, chain_rule_sqrt_shift PROVED (journal-011;\n      10 commits; D-061 \u00a75 updated).\n\n## OPEN CONJECTURES / THREADS\n- (\u2605) (R-003): central conjectural target (task 2.9).\n- Q-S1 (D-019 \u00a73): L\u00b2\u2192uniform lifting. Q-S2: \u210b(T_a) de Branges (2.4).\n  \u03b8(a) theory: must explain both metrics (D-028 F3) + z\u2081\u00b7a\u22484.5 law.\n- Q6 (D-001); Q14 Gutzwiller (Phase 2); T2 Christoffel/CMS (D-006).\nCLOSED: T1, T3, T4, T4b (D-031), T5 (\u2192G-001), 3.4a/b/c, 3.3 (\u2192G-003),\n2.8 (D-029), 1.6 (D-030), 1.7 (D-031), 3.5-design (D-033), (\u2605)-design\n(D-035), 3.6 (D-036), 3.7 (E-021), 3.8 (D-037/R-004), 5.3, 5.4,\n5.1-tier-(i), ii\u2032-5f (D-056's tight R-bound, session 036),\nii\u2032-3b (sessions 037\u2013038, moments capstone, hZC-only).\n\n## BLOCKERS\n(none)\n\n## HANDOFF NOTES\n- db.py add-derivation/log-experiment use INSERT OR REPLACE keyed by\n  id \u2014 a mistyped re-register OVERWRITES the row.\n- db.py: init, log-experiment, add-result, add-derivation, add-graveyard,\n  list. add-derivation signature: positional id, --title --task\n  --status --file (NO --date flag). Session registration via direct\n  sqlite3 insert (journal_file column).\n- venv: ./.venv/Scripts/python.exe. git: git -c user.name=\"NGUYEN-RH-1\"\n  -c user.email=\"research@local\" commit (config NOT modified).\n- LONG RUNS: DETACHED + sandbox DISABLED + log file; poll. For lake:\n  SINGLE command per detached spawn; short PrintAxioms in foreground.\n- LEAN: elan 4.2.3 at ~/.elan/bin (export PATH per shell); toolchain\n  v4.33.0-rc2; zeta-23-lean fully built (9010 jobs) + cache ~7 GB;\n  NguyenRH1 at research/lean/NguyenRH1 with path requires. Iterate\n  single-file with `lake env lean NguyenRH1/LiMoments.lean` (or\n  LiSkeleton.lean, LiTightR.lean) from the package dir;\n  `lake build NguyenRH1.LiTightR` to produce the olean for cross-file\n  imports.\n- LEAN 4 gotchas (session 038 additions \u2014 full list in journal-038):\n  factorial `!` is scoped-notation in Nat \u2014 needs `open scoped Nat`\n  (the parse error points at `!` and looks like spacing; it is a\n  MISSING OPEN); Summable.mul_left dominators must be C * (D \u03c1)\n  CONSTANT-FIRST (D \u03c1 * C whnf-loops the anonymous-constructor refine\n  to 800k heartbeats \u2014 bisect with dominator-only/mulleft-only\n  sorries); rw [seriesFun] fails on the UNAPPLIED constant (use a\n  `show` beta-expansion); norm_sub_norm_le : \u2016a\u2016\u2212\u2016b\u2016 \u2264 \u2016a\u2212b\u2016 has NO\n  abs on the LHS here; don't rw-away a membership still needed as a\n  membership (simpa-only a copy); (neg_neg _).symm for the funext\n  direction; buried negs: simp only [neg_mul, neg_neg];\n  iteratedDeriv_add needs the Pi.add form (bridge hsplit := rfl);\n  calc reassociation closes via trailing mul_assoc in the rw chain.\n- LEAN 4 gotchas (session 037 additions \u2014 full list in journal-037):\n  SummationFilter refactor \u2014 `Summable.tsum_add`/`Summable.tsum_sub`\n  method-form ONLY (plain tsum_add UNKNOWN), tsum_neg/tsum_zero/\n  tsum_congr/tsum_mul_left plain; eq_zero_of_neg_eq needs LinearOrder\n  (\u2102 N/A \u2014 2V = 0 via linear_combination + mul_eq_zero.resolve_left);\n  Complex.norm_conj takes starRingEnd DIRECTLY (don't starRingEnd_apply\n  first); iteratedDeriv_neg EXISTS (explicit args); AnalyticAt.contDiffAt\n  exists; Equiv.tsum_eq e f : \u2211' a, f (e a) = \u2211' b, f b;\n  Equiv.summable_iff e : Summable (f\u2218e) \u2194 Summable f (f implicit);\n  ASCRIBE every tsum binder (zeroMult \u03c1 coerces \u03c1 to \u2102 \u2192 wrong domain);\n  beta-redex show-before-rw; field_simp closes goals (trailing ring\n  errors) but needs the COMPLEX nonzeros (x \u2260 0, not \u2016x\u2016 \u2260 0);\n  deriv_comp point arg EXPLICIT first; ContinuousAt.add on\n  continuousAt_const \u2192 use defeq assignment, not simpa [Pi.add_apply];\n  linear_combination works over \u2102, linarith does NOT.\n- LEAN 4 gotchas (session 011, hard-won \u2014 full list in journal-011):\n  HasDerivAt.add_const adds to VALUE (use .comp for precomposition);\n  Pi.mul_apply/Pi.add_apply/Pi.sub_apply simp after .mul/.add/.sub;\n  convert leaves instance side-goals \u2192 `first | rfl | ring`;\n  field_simp often closes goals (trailing ring errors \u2014 banked 4\u00d7\n  this session);\n  Finset.sum_image takes Set.InjOn, map = g, summand = f;\n  deriv^[2] \u2260 deriv (deriv \u00b7) syntactically (show bridges);\n  subtype coercions (m : \u211d) vs (m.1 : \u211d) can explode isDefEq \u2014 pin\n  families explicitly; -a*b vs -(a*b) breaks Real.exp_neg rewrites;\n  check norm_num digit-bounds by hand (two tight ones failed);\n  set_option maxHeartbeats goes BEFORE the doc comment;\n  iimaj_bracket_bound needs maxHeartbeats 800000.\n- flint for ALL \u03b6/Stieltjes >16 digits; mp.zetazero safe; mpmath\n  complex-\u03b6 OK to ~1e-10; mpmath zeta (integer+Hurwitz)\n  UNTRUSTWORTHY beyond ~57 digits at any dps.\n- PRECISION RULES (session 007): (1) mp.mp.dps = X BEFORE every\n  mp.mpf(string) parse; (2) long decimal constants as STRINGS;\n  (3) float64 zero ordinates insufficient for \u03c3_m; (4) Li binomial\n  truncation boundary error ~C(n,M)\u00b714^{\u2212M} peaks at M = n/15.\n- prime_backend_v2: blockwise \u039b to e\u00b2\u2074, cache E-019-backend-cache.npz;\n  monkeypatch E16.prime_sum_vec + E16._BUILD.clear().\n- Winding diagnostic: \u22654000 pts/edge near real zeros.\n- E-016/E-016b FROZEN; correct machinery: E-016c, E-017/E-018.\n- \u03b3-locking claim protocol: D-029 \u00a73.\n- Lagarias paper math/0404394 (research/paper/): \u00a75\u20136 read in full.\n- research/resources/: 43-note RH-equivalence atlas = R7.\n- E-021 caches: E-021-zeta-cache.json, E-021-zeros100-hi-cache.json,\n  E-021-zeros-cache.npy (4624 zeros float64 \u2014 P1 use ONLY).\n- E-023: E-023-assembly.csv + .json (M\u2080, N\u2080, N\u2081, margins).\n- E-027: detector stress test; zeros cache E-027-zeros-cache.npy;\n  rerun 16 s with cache (--force).\n- PAPER: build with pdflatex+bibtex in research/paper/ (MiKTeX);\n  draft.pdf is gitignored. Audit rule (D-060 \u00a75): any edit to\n  draft.tex re-opens the audit for the edited lines.\n- Housekeeping (session 037): Scratch.lean (previously the session-029\n  audit script) was overwritten with the session-037 lemma probe \u2014\n  session-029 audit RESULTS preserved in audit-session029-axioms.txt.\n",
  "structuredPatch": [
    {
      "oldStart": 165,
      "oldLines": 12,
      "newStart": 165,
      "newLines": 16,
      "lines": [
        " - T-3 (valley, D-049 + D-058): [PROVED-CONDITIONAL(RH)].",
        " ",
        " **Paper:** research/paper/paperA.tex \u2014 Paper A (finite-height Li +",
        "-machine-verified reduction), **9 pp, compiles clean, zero undefined",
        "-refs, CLOSED at ii\u2032-7** (eight-hypotheses headline; B(n) display",
        "-corrected + the F-A/F-B/F-D/F-E correction-note footnote; Appendix B:",
        "-second tier COMPLETE). paperA.pdf committed. paperB.tex \u2014 spectral-",
        "-line research note (skeleton, standing items in \u00a70), 6 pp. draft.tex \u2014",
        "-FROZEN combined archive copy (12 pp).",
        "+machine-verified reduction), **11 pp, compiles clean, zero undefined",
        "+refs, REVISED at session 042** (seven-hypotheses headline; the theorem",
        "+statement exposes all assumptions; B(n) display corrected + the",
        "+F-A/F-B/F-E correction-note footnote; the F-D dog-leg promoted to",
        "+\u00a73.1; Appendix B: second tier COMPLETE + the verbatim Lean signature +",
        "+the instantiation list + the dependency-chain diagram; Section 2",
        "+compressed to one paragraph; hedged novelty with Oesterl\u00e9's",
        "+unpublished precursor noted). paperA.pdf committed. paperB.tex \u2014",
        "+spectral-line research note (skeleton, standing items in \u00a70), 6 pp.",
        "+draft.tex \u2014 FROZEN combined archive copy (12 pp).",
        " ",
        " **Lean:** research/lean/NguyenRH1/ \u2014 full build GREEN (8775 jobs);",
        " all 26 modules root-imported incl. LiSideBounds (ii\u2032-6-c..d) and"
      ]
    }
  ],
  "userModified": false,
  "replaceAll": false
}