{
  "replace_all": false,
  "file_path": "D:\\Python\\Quantum\\STATE.md",
  "old_string": "# STATE.md \u2014 NGUYEN-RH-1 RESUME POINT\n# \u2b50 READ THIS FIRST at the start of every session.\nLast updated: 2026-08-25 | **c = 1.5 MAIN-LINE REDO PAUSED (user\ndirective, session 040): the goal is the ORIGINAL N\u2081 = 9\u00d710\u00b2\u2074. The\nc = 1.5 WIP is preserved on branch `wip/c-1.5-margin-redo` (642d47a,\nBUILD BROKEN mid-convexity \u2014 resume map in the commit message);\nmaster is green (36b9e79) with the session-038 honest Bn (4F, (2/3)Z2)\nwhose right-tail charge \"3.3\" is the F-D-broken one (D-072). NEW LIVE\nDIRECTIVE: PROJECT_DIRECTIVE_D-074.txt \u2014 the ZERO-FREE DOG-LEG\nREPAIR: keep T_cut = \u221an (\u27f9 bridge/residues/N\u2081 = (T\u2080\u22121)\u00b2 unchanged),\ndeform ONLY the right horizontal tail [3, X_R] up to U = (3/2)\u221an\n(where D-073's repaired stepping applies, q = e^{4/9}/2 < 1) through\nthe UNCONDITIONALLY zero-free region Re w \u2265 3 > 1. Immediate task per\n\u00a719: execute \u00a72\u2013\u00a711 (coordinate audit \u2192 exact derivation \u2192 E-034 \u2192\ntemporary fold), then STOP and report answers A\u2013L.**\nSession 039 COMPLETE \u2014 **ii\u2032-6-R side thread COMPLETE (D-073): E-032\nverdict HIDDEN CANCELLATION (per-side claim empirically TRUE at\nT = \u221an, |I|/env down to 5.6e-10, but envelope-unprovable there);\nrepaired proof Lemma 4.1 + R(c) explicit (R(1.5) = 5.94 \u2014 reused by\nthe D-074 dog-leg's H_high verbatim); c = 1.5 global repair validated\nbut superseded by D-074; drafts D3/D4 in D-073 \u00a78.**",
  "new_string": "# STATE.md \u2014 NGUYEN-RH-1 RESUME POINT\n# \u2b50 READ THIS FIRST at the start of every session.\nLast updated: 2026-08-26 | **ii\u2032-6 + ii\u2032-7 COMPLETE (session 041):\n`sfBoundProp : SfBoundProp` and `lambda_pos_finite_height_closed`\nPROVED in Lean from EXACTLY the eight declared hypotheses; full axiom\naudit clean; Paper A closed (B(n) correction note F-A/F-B/F-D/F-E,\nAppendix B rewritten, compiles clean 9 pp); archive closed (D-037\nerratum block, R-004 Lean-closure status, NGUYEN.md, this file,\njournal-041). The finite-height Li theorem \u03bb_n > 0 for ALL\n1 \u2264 n \u2264 N\u2081 = (3\u00d710\u00b9\u00b2\u22121)\u00b2 \u2248 9\u00d710\u00b2\u2074 is now FULLY MACHINE-PROVED with\nthe ORIGINAL N\u2081 PRESERVED (D-074 dog-leg endpoint). Master @ b64a839+\n(archive commits after). NEXT: user read-through of paperA.pdf +\nsubmission decision; deprioritized threads below.**\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   EXACTLY EIGHT declared hypotheses (two computational certificates:\n   RHUpTo, LiVerifiedUpTo; six 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 eight-hypotheses headline;\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 EIGHT\n  declared hypotheses: RHUpTo (Platt\u2013Trudgian), LiVerifiedUpTo\n  (finite Li verification), 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.**"
}

{
  "filePath": "D:\\Python\\Quantum\\STATE.md",
  "oldString": "# STATE.md \u2014 NGUYEN-RH-1 RESUME POINT\n# \u2b50 READ THIS FIRST at the start of every session.\nLast updated: 2026-08-25 | **c = 1.5 MAIN-LINE REDO PAUSED (user\ndirective, session 040): the goal is the ORIGINAL N\u2081 = 9\u00d710\u00b2\u2074. The\nc = 1.5 WIP is preserved on branch `wip/c-1.5-margin-redo` (642d47a,\nBUILD BROKEN mid-convexity \u2014 resume map in the commit message);\nmaster is green (36b9e79) with the session-038 honest Bn (4F, (2/3)Z2)\nwhose right-tail charge \"3.3\" is the F-D-broken one (D-072). NEW LIVE\nDIRECTIVE: PROJECT_DIRECTIVE_D-074.txt \u2014 the ZERO-FREE DOG-LEG\nREPAIR: keep T_cut = \u221an (\u27f9 bridge/residues/N\u2081 = (T\u2080\u22121)\u00b2 unchanged),\ndeform ONLY the right horizontal tail [3, X_R] up to U = (3/2)\u221an\n(where D-073's repaired stepping applies, q = e^{4/9}/2 < 1) through\nthe UNCONDITIONALLY zero-free region Re w \u2265 3 > 1. Immediate task per\n\u00a719: execute \u00a72\u2013\u00a711 (coordinate audit \u2192 exact derivation \u2192 E-034 \u2192\ntemporary fold), then STOP and report answers A\u2013L.**\nSession 039 COMPLETE \u2014 **ii\u2032-6-R side thread COMPLETE (D-073): E-032\nverdict HIDDEN CANCELLATION (per-side claim empirically TRUE at\nT = \u221an, |I|/env down to 5.6e-10, but envelope-unprovable there);\nrepaired proof Lemma 4.1 + R(c) explicit (R(1.5) = 5.94 \u2014 reused by\nthe D-074 dog-leg's H_high verbatim); c = 1.5 global repair validated\nbut superseded by D-074; drafts D3/D4 in D-073 \u00a78.**",
  "newString": "# STATE.md \u2014 NGUYEN-RH-1 RESUME POINT\n# \u2b50 READ THIS FIRST at the start of every session.\nLast updated: 2026-08-26 | **ii\u2032-6 + ii\u2032-7 COMPLETE (session 041):\n`sfBoundProp : SfBoundProp` and `lambda_pos_finite_height_closed`\nPROVED in Lean from EXACTLY the eight declared hypotheses; full axiom\naudit clean; Paper A closed (B(n) correction note F-A/F-B/F-D/F-E,\nAppendix B rewritten, compiles clean 9 pp); archive closed (D-037\nerratum block, R-004 Lean-closure status, NGUYEN.md, this file,\njournal-041). The finite-height Li theorem \u03bb_n > 0 for ALL\n1 \u2264 n \u2264 N\u2081 = (3\u00d710\u00b9\u00b2\u22121)\u00b2 \u2248 9\u00d710\u00b2\u2074 is now FULLY MACHINE-PROVED with\nthe ORIGINAL N\u2081 PRESERVED (D-074 dog-leg endpoint). Master @ b64a839+\n(archive commits after). NEXT: user read-through of paperA.pdf +\nsubmission decision; deprioritized threads below.**\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   EXACTLY EIGHT declared hypotheses (two computational certificates:\n   RHUpTo, LiVerifiedUpTo; six 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 eight-hypotheses headline;\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 EIGHT\n  declared hypotheses: RHUpTo (Platt\u2013Trudgian), LiVerifiedUpTo\n  (finite Li verification), 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.**",
  "originalFile": "# STATE.md \u2014 NGUYEN-RH-1 RESUME POINT\n# \u2b50 READ THIS FIRST at the start of every session.\nLast updated: 2026-08-25 | **c = 1.5 MAIN-LINE REDO PAUSED (user\ndirective, session 040): the goal is the ORIGINAL N\u2081 = 9\u00d710\u00b2\u2074. The\nc = 1.5 WIP is preserved on branch `wip/c-1.5-margin-redo` (642d47a,\nBUILD BROKEN mid-convexity \u2014 resume map in the commit message);\nmaster is green (36b9e79) with the session-038 honest Bn (4F, (2/3)Z2)\nwhose right-tail charge \"3.3\" is the F-D-broken one (D-072). NEW LIVE\nDIRECTIVE: PROJECT_DIRECTIVE_D-074.txt \u2014 the ZERO-FREE DOG-LEG\nREPAIR: keep T_cut = \u221an (\u27f9 bridge/residues/N\u2081 = (T\u2080\u22121)\u00b2 unchanged),\ndeform ONLY the right horizontal tail [3, X_R] up to U = (3/2)\u221an\n(where D-073's repaired stepping applies, q = e^{4/9}/2 < 1) through\nthe UNCONDITIONALLY zero-free region Re w \u2265 3 > 1. Immediate task per\n\u00a719: execute \u00a72\u2013\u00a711 (coordinate audit \u2192 exact derivation \u2192 E-034 \u2192\ntemporary fold), then STOP and report answers A\u2013L.**\nSession 039 COMPLETE \u2014 **ii\u2032-6-R side thread COMPLETE (D-073): E-032\nverdict HIDDEN CANCELLATION (per-side claim empirically TRUE at\nT = \u221an, |I|/env down to 5.6e-10, but envelope-unprovable there);\nrepaired proof Lemma 4.1 + R(c) explicit (R(1.5) = 5.94 \u2014 reused by\nthe D-074 dog-leg's H_high verbatim); c = 1.5 global repair validated\nbut superseded by D-074; drafts D3/D4 in D-073 \u00a78.**\nSession 038 COMPLETE \u2014 **ii\u2032-3b + ii\u2032-3c +\nii\u2032-6-0 + ii\u2032-6-a + ii\u2032-6-b DONE; FINDING F-D DOCUMENTED (D-072,\nuser paused to think): the (6.12) stepping in Lagarias's Thm 6.1 is\nbroken at T = \u221an (product ratio e/2 > 1; 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/R-004's\nB(n) inherits it (the right-tail charge \"3.3\" is off by ~10\u2077\u00d7; margin\ncollapses for n \u2273 3\u00d710\u2074). The theorem statement survives (verified to\n5\u00d710\u2075; sides cancel by conjugation + phase winding); ALL Lean work to\ndate survives (the bug is in the horizontal piece ii\u2032-6-c, not yet\nbuilt). Repair path (R) verified: T = c\u221an, c > 1.2012 (kernel ratio\n< 2 \u27f9 stepping works; monotone decrease confirmed at c = 1.5, 2);\nN\u2081 \u2192 (T\u2080/c)\u00b2 \u2248 2.25\u20134\u00d710\u00b2\u2074.**\n\n## SESSION 039 HEADLINES (ii\u2032-6-R side thread \u2014 COMPLETE)\n1. **6-R-0 (E-032, ALL CHECKS PASS, commit ded9603)**: the TRUE\n   complex right-tail integral at T = \u221an (zero-avoiding) by direct\n   quadrature \u2014 Dirichlet series with certified tail (\u03c3 \u2265 5) +\n   mpmath (validated 6\u00d710\u207b\u00b9\u2070), dps 50, trapezoid h-delta \u2264 5e-5.\n   **VERDICT: HIDDEN CANCELLATION, decisive** \u2014 |I_right| =\n   7.18/16.70/26.23 vs envelope 50.8/1.03e4/4.71e10 (n = 10\u00b3/10\u2074/10\u2075),\n   ratio 0.141 \u2192 1.6e-3 \u2192 **5.57e-10**; full side |I_II| =\n   7.44/19.21/30.89 (|I_II|/\u221an DECREASING 0.235 \u2192 0.098): the per-side\n   claim is empirically TRUE but envelope-unprovable at T = \u221an.\n   Mid-segment [\u22125/2, 3] almost no cancellation (0.7\u20130.95) \u2014 its bound\n   honest. Repair heights: envelope collapses (\u22481.0 at c = 1.5,\n   \u22480.35 at c = 2), ratio \u2248 1 \u2014 the repair needs no cancellation.\n   STOP-rule reported; user direction: **repair proof only**, the\n   T = \u221an salvage parked as an open question (D-073 \u00a78 D4).\n2. **6-R-1 (D-073 \u00a7\u00a73\u20137)**: dependency audit (13 ingredients; ONLY\n   the (6.12) stepping is proof-breaking; the (1+4/(16+n))\u207f\n   intermediate is a harmless looseness \u2014 e\u2074+1 valid); **Lemma 4.1\n   (corrected stepping, P(\u03c3+1)/P(\u03c3) \u2264 q = e^{1/c\u00b2}/2) + Cor 4.2\n   (explicit R(c)) [PROVED, elementary, self-contained]**; c-choice\n   with AUDIT CORRECTION (recommend **c = 1.5**, reversing D-072's\n   \"2 margin/1.5 range\" \u2014 the fold is I_III-length-dominated:\n   margin(10\u2075) 181 256 vs 109 370, N\u2081 4\u00d710\u00b2\u2074 vs 2.25\u00d710\u00b2\u2074; c = 2\n   documented as the conservative option); consequence audit (Thm 6.1\n   statement unchanged, O-constant c-dependent; Thm 1.1 height\n   ((T\u2080\u22121)/c)\u00b2; NO new perimeter); **E-033 ALL CHECKS PASS** (Z\u2080\n   certified [0.5699210, 0.5703661]; q-table incl. q(1) = 1.359 = the\n   bug; R covers the E-032 measured truth with 3.2\u20136.3\u00d7 slack; kernel\n   charges 5.65 \u2264 6.92 / 2.06 \u2264 3.72; fold fit \u2264 0.3925/0.3883;\n   margins > 0 on [8\u00d710\u2074, N\u2081(c)] both c; full fold). V1 first-run\n   failure was a script-tolerance error (certified bracket correct),\n   fixed, audit trail in git.\n3. **6-R-2 (D-073 \u00a78)**: D3 letter repair paragraph + D4 T = \u221an\n   per-side verdict paragraph \u2014 DRAFTS ONLY; correspondence files\n   untouched (freeze protocol in force).\n4. **THREAD COMPLETE** \u2014 all three success criteria met. Main line\n   resumes with repair (R): see NEXT ACTION.\n\n## SESSION 038 HEADLINES (ii\u2032-6-0 \u2014 THIS SESSION'S ENDPOINT)\n0. **ii\u2032-6-0 DESIGN (D-071) + E-030 (ALL CHECKS PASS) + two user\n   approvals**: THREE findings \u2014 F-A bridge factor-2 (\u03bb_n(T) is\n   both-signs; honest 4\u00b7FAlt vs baked 2\u00b7FAlt; R-004 unaffected, paper\n   erratum at ii\u2032-7); F-B I_III two-unit count ((2/3)Z2 honest vs\n   (2/3)\u0108\u2080 baked \u2014 D-069 Finding 2 made exact); F-C baked Bn unprovable\n   beyond ~5\u00d710\u2077 (killers grow T\u00b7log T > (log T)\u00b2 slack).\n   RESOLUTION (user-approved 8-step protocol): redefine Bn honestly\n   (4F, (2/3)Z2) \u2014 fold works everywhere (V4), margin positive + larger\n   near 10\u2075 (V2), horizontal segment-integral \u2264 0.40 of share (V3).\n   Perimeter additions approved: ZeroCountGlobalProp (global Trudgian\n   N(T) \u2264 FAlt) + MZeroProp (M\u2080 \u2264 1.3352). Sub-stage map ii\u2032-6-a..d \u2192\n   ii\u2032-7.\n0c. **FINDING F-D (D-072, user paused to think)**: the (6.12)\n   stepping in Lagarias's Thm 6.1 is broken at T = \u221an \u2014 the per-step\n   product ratio is e/2 > 1 (zeta halves, kernel ratio \u2264 e), so the\n   horizontal right-tail GROWS from \u03c3 = 3 to \u03c3 \u2248 0.36\u221an, peaking at\n   ~e^{0.066\u221an}. E-031 (ALL CHECKS PASS): right-tail envelope\n   ~5.9\u00d710\u00b9\u2070 at n = 10\u2075 (peak 1.6\u00d710\u2079 at \u03c3 = 111); direct factor\n   evaluation |k_n(100+317i)| = 4.4\u00d710\u00b3\u2079, |\u03b6\u2032/\u03b6(101+317i)| \u2248\n   1.8\u00d710\u207b\u00b3\u00b9. D-036/D-037/R-004 inherit it verbatim (charge \"3.3\" off\n   by ~10\u2077\u00d7; margin collapses for n \u2273 3\u00d710\u2074). The theorem statement\n   survives (verified to 5\u00d710\u2075; sides cancel by conjugation + phase\n   winding); all Lean work to date survives (the bug is in the\n   horizontal piece, not yet built). Repair path (R) verified:\n   T = c\u221an with c > 1.2012 \u27f9 stepping works (monotone decrease at\n   c = 1.5, 2); N\u2081 \u2192 (T\u2080/c)\u00b2 \u2248 2.25\u20134\u00d710\u00b2\u2074. No erratum found in the\n   literature (arXiv v4, web search).\n0b. **ii\u2032-6-b COMPLETE**: perimeter Props ZeroCountGlobalProp +\n   MZeroProp declared (LiContour); the wide pigeonhole\n   exists_zero_avoiding_T_wide (3-unit Finding-2 repair, clearance\n   1/(9\u00b7C0hat(a+2))); LiAssembly.lean NEW (~460 lines, root-imported):\n   the sides identity sf_abs_le_rectInt_add_zeroSum (rectInt'_Jlag on\n   the variant-B rectangle; border zero-free via the zero\n   classification + wide pigeonhole; |Sf n| \u2264 \u2016RectInt\u2016 + \u2016\u03a3\u2016) + the\n   bridge zeroSum_norm_le_four_FAlt_add_one (\u2016\u03a3\u2016 \u2264 4\u00b7FAlt + 1 via\n   RHUpTo + conj-image reindex + NoLowZeros + trivTerm \u2264 1). Full\n   build GREEN (8772 jobs); audit session038d: 12 decls, 3 standard\n   axioms only. Banked (journal-038): the RectangleBorder-rcases trap\n   (rw + simp only [mem_union, mem_reProdIm, mem_singleton_iff] +\n   tauto route); Finset.image plain-function + Set.InjOn form; set-x\n   breaks mem_toFinset patterns; linarith proves \u2260 directly;\n   projections for IsNontrivialZero (structure opacity); sq_eq_sq\u2080;\n   pow_le_one\u2080's implicit n.\n0a. **ii\u2032-6-a COMPLETE** (user protocol steps 1\u20135): Bn redefined\n   honestly (4F, (2/3)Z2hat \u2014 new def with the D-071 comment);\n   marginTilde/mFblock/mTL1b/mIdb lockstep; marginTilde_convex\n   RE-PROVED (\u03c8-row literal updates + norm_num; the eq_expanded needed\n   Z2hat in the unfold list; a hardcoded const_mul (\u22122) in\n   continuousOn_marginExpanded); base points RE-CERTIFIED\n   (Bn_FAlt_80000_le 328,000 \u2192 329,000, Bn_FAlt_100000_le 347,000 \u2192\n   350,000 \u2014 the old bounds FAIL for the corrected Bn; margins\n   \u2265 7,001 / 82,501, doc comments updated); endpoint margins re-run\n   (margin\u0303(8\u00d710\u2074) = 14,682, margin\u0303(10\u2075) = 90,653, margin(N\u2081) =\n   2.458\u00d710\u00b2\u2076 unchanged); full build GREEN (8771 jobs); audit\n   session038c: endpoint + convexity + base points all 3 standard\n   axioms only. Banked: lake env lean uses the STALE olean \u2014 lake\n   build the dependency first; re-check certified constants at 1e-4.\n## SESSION 038 HEADLINES (ii\u2032-3c)\n1. **ii\u2032-3c COMPLETE** (LiCrux.lean NEW, ~430 lines, root-imported):\n   `gFun_one_sub_fun` (FE as a function identity, xiL_one_sub +\n   chain rule), `iteratedDeriv_gFun_zero` (g^{(m)}(0) =\n   (\u22121)^{m+1}g^{(m)}(1) via the UNCONDITIONAL\n   iteratedDeriv_comp_const_sub), `gFun_one_add_punctured`/\n   `gFun_one_add_eventuallyEq` (the shift expansion gFun(1+s) =\n   1/(1+s) + hLiExt s + \u0393R\u2032/\u0393R(1+s)), `iteratedDeriv_gFun_one`\n   (coefficient extraction (\u22121)^m\u00b7m! \u2212 m!\u00b7c_m + (\u22121)^{m+1}\u00b7m!\u00b7a_{m+1}),\n   **`lagarias_4_10_a (hZC)` PROVED** (lcoeff (k\u22121) = (\u22121)^k(a_k +\n   sigmaP k) + (\u22121)^{k\u22121}, all k \u2265 1 \u2014 the multiplied-out\n   linear_combination + mul_left_cancel\u2080 (m! \u2260 0)), and **THE CRUX\n   `sf_eq_resW1 (hZC)` PROVED**: (ResW1 n).re = Sf n for n \u2265 1\n   (ResW1_eq_sum + (4.10-a) + both ii\u2032-2 swaps + the binomial sum\n   \u03a3(\u22121)^{j\u22121}C(n,j) = 1). Audit session038b: 8 decls, 3 standard\n   axioms only. **ii\u2032-3 (ALL of Lagarias (4.10)) \u2192 COMPLETE.**\n2. **ii\u2032-3b COMPLETE** (LiMoments.lean \u00a75/\u00a76, ~290 new lines, file now\n   ~1020 lines): \u00a75 the termwise iterated derivation at 0 \u2014\n   `iteratedDeriv_zpow_neg_one`, `iteratedDeriv_seriesTerm`,\n   `seriesTerm_deriv_summableLocallyUniformlyOn` (the M-test on\n   ball(0, \u03b4/2), dominator j!\u00b72^{j+1}\u00b7(1/\u03b4)^{j\u22121}\u00b7mult/\u2016\u03c1\u2016\u00b2),\n   `iteratedDeriv_seriesFun_zero` (the LiDigamma:749\u2013785\n   iteratedDerivWithin_tsum pattern verbatim). \u00a76:\n   `gFun_eventuallyEq_zero` (\ud835\udcdd[\u2260] \u2192 \ud835\udcdd via eventually_nhdsWithin_iff) +\n   **THE CAPSTONE `sigmaP_eq_neg_iteratedDeriv_gFun_div`**: sigmaP k =\n   \u2212(iteratedDeriv (k\u22121) gFun 0)/(k\u22121)! for ALL k \u2265 1 (k=1 via \u00a74's\n   reindex; k\u22652 via (G) + \u00a75 + the per-term sign algebra\n   (\u22121)^k\u00b7(\u22121)^{k+1} = \u22121 + \u2190 sigmaP_eq_unpaired + field_simp k! \u2260 0;\n   FIRST-PASS GREEN). Perimeter: **ZeroCountProp ONLY**.\n3. **Closure (3b)**: LiTightR + LiMoments root-imported; AuditSession038.lean +\n   audit-session038-axioms.txt \u2014 23 declarations, [propext,\n   Classical.choice, Quot.sound] ONLY, 0 sorryAx.\n4. Banked gotchas (journal-038): factorial `!` needs `open scoped Nat`;\n   Summable.mul_left dominators must be C * (D \u03c1) (constant FIRST \u2014\n   D \u03c1 * C whnf-loops the refine); rw [seriesFun] fails on the UNAPPLIED\n   constant (use `show` beta-expansion); norm_sub_norm_le has NO abs on\n   the LHS in this Mathlib; don't rw-away memberships still needed as\n   memberships (simpa-only a copy).\n\n## SESSION 037 HEADLINES (superseded \u2014 ii\u2032-3b now DONE)\n1. **Capstone dependency audit** (user-requested, pre-ii\u2032-3b):\n   `AuditSession037.lean` + `audit-session037-axioms.txt` \u2014\n   `#print axioms logDeriv_riemannZeta_sub_nearZeros_le_tight` =\n   **[propext, Classical.choice, Quot.sound] ONLY**; the exact perimeter\n   recorded verbatim from the elaborator: `ZeroCountProp` (unit window,\n   mult-weighted, \u2264 C0hat(t+1), t \u2265 2; C0hat t = 0.433\u00b7log(t+2) +\n   0.886\u00b7log log(t+2) + 2.9), `ZeroCountProp2` (two-unit, \u2264 0.6\u00b7L +\n   0.886\u00b7LL + 2.7, t \u2265 10), `NoLowZeros` (\u2200 \u03c1 nontrivial, 14 \u2264 |Im \u03c1|);\n   constructs nearZerosSub / Zeta23.zeroMult / zeroAbsWindow also printed.\n2. **ii\u2032-3b ROUTE REVISION (D-070)**: the moments (M)\n   sigmaP k = \u2212gFun^{(k\u22121)}(0)/(k\u22121)! come from 5e's\n   `partialFraction_identity (hZC : ZeroCountProp)` by PURE ALGEBRA +\n   series calculus \u2014 NO contours (D-066 \u00a73's rectangle plan superseded;\n   the contour work was 5e's). The identity (G): gFun := logDeriv xiL =\n   B + seriesFun at every good point; xiL := (s(s\u22121)/2)\u00b7\u039b entire via the\n   \u039b\u2080 closed form xiL s := (s(s\u22121)/2)\u00b7\u039b\u2080(s) \u2212 (s\u22121)/2 + s/2 (Mathlib\n   `completedRiemannZeta_eq`). Perimeter: ZeroCountProp ONLY (5f's\n   hZC2/hNLZ NOT needed for the moments).\n3. **LiMoments.lean \u00a71\u2013\u00a74 COMPLETE, build GREEN** (~730 lines; new file,\n   NOT yet root-imported; imports NguyenRH1.LiTightR + LiSwaps + LiResidue\n   + LiDigamma + LiReflect):\n   \u00a71 xiL (differentiable/analytic everywhere, xiL_eq_mul off {0,1},\n   xiL_zero/xiL_one = 1/2, xiL_one_sub FE, xiL_ne_zero) + the subtype\n   involutions conjZeroEquiv/oneSubZeroEquiv + isNontrivialZero_one_sub;\n   \u00a72 `gFun_eq_momentB` \u2014 (G) at good points (logDeriv_mul chains +\n   logDeriv_Gamma\u211d_eq_of_not_neg_nat + momentB_spec);\n   \u00a73 `eq_of_eventuallyEq_nhd_ne`, good-eventually sets at 0 (\u03b6(0) = \u22121/2)\n   and 1 (zetaA), `seriesFun_zero` (= 0), `seriesFun_one` (= \u03a3\n   mult/(\u03c1(1\u2212\u03c1))), `gFun_zero` (gFun 0 = B), `gFun_one` (gFun 1 = B +\n   seriesFun 1), `gFun_one_eq_neg` (FE sign, deriv_comp chain rule);\n   \u00a74 summability budget (master `summable_mult_div_norm_sq`,\n   `exists_norm_lower_bound` \u03b4-ball, `summable_mult_inv_pow` k \u2265 2, AM-GM\n   `mult_div_norm_mul_norm_le`) + reindex machinery\n   (`tsum_mult_inv_pow_conj`, `sigmaP_eq_unpaired` k \u2265 2,\n   `summable_mult_div_norm_sq_one_sub`, `vTerm_tsum_eq_zero` via V = W =\n   \u2212V) and **the k = 1 capstone `sigmaP_one_eq_neg_gFun_zero` PROVED**\n   (2\u03c3\u2081 = seriesFun 1 = gFun 1 \u2212 B = \u22122\u00b7gFun 0 by the FE sign).\n\n## CURRENT POSITION\n\u2714 PHASE 0, 1, 4 COMPLETE. PHASE 3 (Track C): 3.1\u20133.8 CLOSED (R-004,\nfull tag). PHASE 2 (Track B): mapped to exhaustion at current\ntechnology (2.6\u20132.13). PHASE 5: 5.3 \u2714, 5.4 \u2714, 5.2 \u2714 (live);\n5.1 skeleton \u2714 + tier (i) \u2714 (session 011) + tier (ii) STEP 1 \u2714\n(session 012). PHASE 5B (tier ii\u2032, user decision: option (a) \u2014 close\nSfBoundProp in Lean BEFORE submission; Paper A frozen/submittable\nthroughout): DONE: ii\u2032-0 (D-064 design + liCoeff defect + crux Sf =\nRes\u2081 found), ii\u2032-1a (liCoeff defect REPAIRED), ii\u2032-1b (R1 residue\nmachinery: rectInt'_Jlag), ii\u2032-2 (elementary swaps), ii\u2032-3-DESIGN\n(D-066, \u03b24), ii\u2032-3a (pieces A+B: LiZetaCoeff, LiArchimedean, LiDigamma),\nii\u2032-4 (LiContour.lean: L3 exists_zero_avoiding_T + L1 kernel bounds +\nzeroMult_neg_two), ii\u2032-5a (D-067 design), ii\u2032-5b (LiRBound.lean:\nlevel-2 \u03b6 representation + norm_riemannZeta_le_disc \u2016\u03b6\u2016 \u2264 (3/4)|t|\u00b2),\nii\u2032-5c (LiDisc.lean: the loose disc R-bound \u2264 100000\u00b7(log|t|)\u00b2 on\n\u03c3 \u2208 [1/2, 7/2] via R-gap + Blaschke + BC, Jensen count, NO perimeter),\nii\u2032-5d (LiReflect.lean: FE-reflection + left loose bound \u2264\n200000\u00b7(log|t|)\u00b2 on \u03c3 \u2208 [\u22125/2, 1/2] + the 5e digamma input), ii\u2032-5e\n(LiTrivialZeros, LiGapCircles, LiDigammaLeft, LiSeries, LiFEntire,\nLiCircleBound (~3928 lines), LiSqueeze \u2014 **the partial-fraction identity\n`partialFraction_identity (hZC : ZeroCountProp)` PROVED**), ii\u2032-5f\n(LiTightR.lean ~4300 lines \u2014 **the tight R-bound\n`logDeriv_riemannZeta_sub_nearZeros_le_tight (hZC) (hZC2) (hNLZ)` \u2264\n10.5\u00b7log(|t|+2) + 48 PROVED**; capstone dependency-audited session 037:\n3 standard axioms only, perimeter verbatim). **ii\u2032-3b COMPLETE (sessions\n037\u2013038, LiMoments.lean ~1020 lines): the moments capstone\n`sigmaP_eq_neg_iteratedDeriv_gFun_div (hZC)` PROVED for all k \u2265 1 \u2014\nD-070 route, perimeter ZeroCountProp ONLY. **ii\u2032-3c COMPLETE (session\n038, LiCrux.lean ~430 lines): `lagarias_4_10_a (hZC)` + THE CRUX\n`sf_eq_resW1 (hZC)` PROVED \u2014 Sf(n) = Res\u2081(n) in Lean. ii\u2032-3 (ALL of\n(4.10)) DONE.**\n\n**Theorem status (session 012 Lean upgrade + session 036):**\n- T-1 (R-004): [PROVED-CONDITIONAL(computational RH-to-T\u2080;\n  computational finite verification)] \u2014 **Lean-verified modulo\n  SfBoundProp + the declared computational perimeter only**:\n  `lambda_pos_finite_height_verified` (LiBasePoints.lean) PROVED from\n  (hRH : RHUpTo 3\u00d710\u00b9\u00b2) (hfinite : LiVerifiedUpTo 5\u00d710\u2075)\n  (hSf : SfBoundProp). PrintAxioms = 3 standard axioms, no sorryAx.\n  The two margin evaluations are discharged by certified interval\n  bounds (margin\u0303(8\u00d710\u2074) \u2265 8001 certified / 15 764 true; margin\u0303(10\u2075)\n  \u2265 85 501 certified). LiSkeleton + LiBasePoints both sorry-free.\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 assembly), 8 pp, compiles clean, zero undefined refs.\npaperB.tex \u2014 spectral-line research note (skeleton, standing items in\n\u00a70), 6 pp. draft.tex \u2014 FROZEN combined archive copy (12 pp). No\nfigures yet.\n\n**Lean:** research/lean/NguyenRH1/ \u2014 full build GREEN (8771 jobs);\nLiTightR + LiMoments + LiCrux root-imported (session 038). sorryAx\nremains ONLY on: R003_exact_factorization (tier iv) + 4 valley\nstatements (tier iii).\n\n## ACTIVE PLAN (tier ii\u2032, per D-064 \u00a76)\nFreeze protocol in force (user directive 2026-08-21): no edits to\npaperA.tex/paperB.tex/draft.tex/references.bib until ii\u2032-7; no edits\nto existing Lean proofs except the liCoeff correctness fix (ii\u2032-1a);\ncommit at every sub-stage. Fallback integrity: D-064 \u00a78.\nRemaining sub-stages: **ii\u2032-6** (L0\nassembly: sides identity + bridge |\u03bb_n(T)| \u2264 2\u00b7FAlt(T) (hRH) +\n|Sf n| \u2264 Bn FAlt n on [10\u2075, N\u2081]; D-069 Finding 2's H(T) near-sum\nrepair map (honest \u2248 7\u00b7\u0108\u2080\u00b2 vs baked 3\u00b7\u0108\u2080\u00b2, margin survives via E-028's\n26\u00d7 slack) lives here) \u2192 **ii\u2032-7** (closure: theorem sfBoundProp :\nSfBoundProp; final lambda_pos_finite_height_closed with the 3 perimeter\nhypotheses only; full axiom audit; paper Appendix B + tag upgrade\n(D-062 \u00a74 endpoint); archive closure + D-037 line-63 erratum pointer).\nDeprioritized: a=13+ push; adversary-ceiling LP; T4b; \u03bb-channel\n(G-004); \u03b8-channel (dead, E-024); Paper B Task 1 (R-003 bookkeeping)\nholds as queued after ii\u2032; user read-through of paperA.pdf still open\n(nothing blocks it); repo-publication prep still open.\n\n## NEXT ACTION\n**STOPPED AT A CLEAN BOUNDARY (session 040 block B, user log-off):\nii\u2032-6-c-i COMPLETE + COMMITTED (master @ a8c5b1e); 6-c-ii DESIGNED\nbut NO Lean written yet. Resume at 6-c-ii below.**\nCompleted this block: ii\u2032-6-a2 committed (0dfbd6e); FINDING F-E +\nrepair decision logged (D-074 \u00a79, 8068ea6); 6-c-i scaffolding\n(a8c5b1e, LiSideBounds.lean \u2014 build GREEN; provides Z2hat_mono,\nnearZerosSub_mult_sum_le, continuousAt/On_logDeriv_zeta,\nJlag_norm_eq, zeta_ne_zero_left_vertical, zeta_ne_zero_horizontal,\nrectangleIntegral_Jlag_eq, VIntegral_norm, HIntegral_split,\njlag_left_vertical_norm_even). Journal: session-040.md CONTINUATION\nsection. NGUYEN.md checklist updated. Git identity: pass per-command\n(-c user.name=\"NGUYEN-RH-1\" -c user.email=\"research@local\") \u2014 never\nconfig.\n**ii\u2032-6-c sub-stage map (file research/lean/NguyenRH1/NguyenRH1/\nLiSideBounds.lean, n \u2265 10\u2075 throughout so T \u2265 316):**\n6-c-i \u2713 \u2192 **6-c-ii I_III (NEXT)** \u2192 6-c-iii I_I (F-E form) \u2192 6-c-iv\nmid-horizontal machine \u2192 6-c-v horizontal assembly \u2192 6-d fold \u2192 ii\u2032-7.\n**6-c-ii RECIPE (I_III, left vertical \u03c3 = \u22125/2; target statement):**\n`vIntegral_Jlag_left_norm_le (hZC) (hZC2) (hNLZ) (hMZ : MZeroProp)\n{n} (hn : 100000 \u2264 n) {T} (hTn : \u221an \u2264 T) (hTn1 : T \u2264 \u221an+1) :\n\u2016VIntegral (Jlag n) (-5/2) (-T) T\u2016 \u2264 4*T*((2/3)*Z2hat T +\n10.5*log(T+2) + 48) + 40*1.3352`.\n1. VIntegral_norm + norm_integral_le_integral_norm (\u2212T \u2264 T):\n   \u2016\u00b7\u2016 \u2264 \u222b_{\u2212T}^{T} g, g t := \u2016Jlag n (\u2191(-5/2:\u211d)+\u2191t\u00b7I)\u2016.\n   Integrability of g: Jlag continuous on the path\n   (kFun_differentiableAt (s\u22601 via re=\u22125/2) .continuousAt + my\n   continuousAt_logDeriv_zeta (zeta_ne_zero_left_vertical) \u2192 .mul/.neg)\n   composed with the path map u \u21a6 \u2191x+\u2191u\u00b7I (fun_prop) \u2192 .norm \u2192\n   ContinuousOn.intervalIntegrable.\n2. Split \u222b_{\u2212T}^{T} = \u222b_{\u2212T}^{\u221210} + \u222b_{\u221210}^{10} + \u222b_{10}^{T}\n   (integral_add_adjacent_intervals \u00d72). The left piece:\n   \u222b_{\u2212T}^{\u221210} g = \u222b_{10}^{T} g \u2014 g is EVEN\n   (jlag_left_vertical_norm_even) + integral_comp_neg\n   (\u222b_a^b f(\u2212x) = \u222b_{\u2212b}^{\u2212a} f).\n3. Middle: per t \u2208 Icc(\u221210,10): g t \u2264 2\u00b71.3352 (Jlag_norm_eq +\n   kFun_norm_le_two (re \u2264 1/2) + hMZ t (|t| \u2264 10); CAST BRIDGE:\n   MZeroProp's point is (-5/2:\u2102)+\u2191t\u00b7I, mine is \u2191(-5/2:\u211d)+\u2191t\u00b7I \u2014\n   `(-5/2:\u2102) = \u2191(-5/2:\u211d)` by push_cast; ring). Then integral_mono_on\n   + integral_const: \u2264 20\u00b7(2\u00b71.3352) = 40\u00b71.3352.\n4. Tails: per t \u2208 Icc(10,T): g t \u2264 K := 2*((2/3)*Z2hat T +\n   10.5*log(T+2) + 48). Via Jlag_norm_eq + kFun_norm_le_two +\n   \u2016logDeriv\u2016 \u2264 \u2016logDeriv \u2212 \u03a3near\u2016 + \u2016\u03a3near\u2016:\n   - capstone logDeriv_riemannZeta_sub_nearZeros_le_tight hZC hZC2\n     hNLZ (ht : 10 \u2264 t) (h\u03c3lo/h\u03c3hi : re = \u22125/2, by simp)\n     (him : s.im = t, by simp) (h\u03b6 : zeta_ne_zero_left_vertical t)\n     \u27f9 \u2016\u00b7\u2212\u03a3\u2016 \u2264 10.5\u00b7log(|t|+2)+48 = 10.5\u00b7log(t+2)+48 (abs_of_nonneg)\n     \u2264 10.5\u00b7log(T+2)+48 (Real.log_le_log, t \u2264 T).\n   - \u2016\u03a3near\u2016 \u2264 \u03a3 \u2016mult/(s\u2212\u03c1)\u2016 \u2264 (2/5)\u00b7\u03a3 mult \u2264 (2/5)\u00b7Z2hat t \u2264\n     (2/3)\u00b7Z2hat T: per \u03c1: \u2016s\u2212\u03c1\u2016 \u2265 |re(s\u2212\u03c1)| = 5/2+\u03c1.re \u2265 5/2\n     (abs_re_le_norm; re(s\u2212\u03c1) = \u22125/2\u2212\u03c1.re, abs_of_neg) \u27f9 1/\u2016s\u2212\u03c1\u2016 \u2264\n     2/5; \u03a3 mult \u2264 Z2hat t (nearZerosSub_mult_sum_le hZC2);\n     Z2hat_mono (1 \u2264 t \u2264 T) + 2/5 \u2264 2/3 + Z2hat T \u2265 0.\n   Then integral_mono_on + integral_const: \u222b_{10}^{T} g \u2264 (T\u221210)\u00b7K.\n5. Assemble: \u222b \u2264 2\u00b7(T\u221210)\u00b7K + 40\u00b71.3352 \u2264 2T\u00b7K + 40\u00b71.3352 =\n   4T\u00b7((2/3)Z2hat T + 10.5 log(T+2) + 48) + 40\u00b71.3352 (K \u2265 0 since\n   Z2hat T \u2265 0 for T \u2265 1: log(T+2) \u2265 1, loglog \u2265 0).\n**6-c-iii RECIPE (I_I, F-E form):** NEW kernel lemma\n`kFun_right_vertical_norm_le_exp_sqrt_add_third` {n} (hn : 4 \u2264 n) (t):\n\u2016kFun n (\u2191(2\u221an)+\u2191t\u00b7I)\u2016 \u2264 exp(\u221an/2+1/3)+1 \u2014 |w/(w\u22121)| \u2264 1+1/(2\u221an\u22121)\n(norm_one_add_one_div_le + normSq monotone in t\u00b2, worst t=0:\n(2\u00b7re(w\u22121)+1)/normSq(w\u22121) = (4\u221an\u22121)/((2\u221an\u22121)\u00b2+t\u00b2) \u2264 (4\u221an\u22121)/(2\u221an\u22121)\u00b2\n\u27f9 |1+1/(w\u22121)| \u2264 1+1/(2\u221an\u22121) \u2014 sqrt of both sides, sq_le_sq\u2080), then\n(1+1/(2\u221an\u22121))\u207f \u2264 exp(n/(2\u221an\u22121)) (add_one_le_exp^\u207f) and\nn/(2\u221an\u22121) \u2264 \u221an/2+1/3 \u27fa n \u2265 4 (cross-multiply, pure nlinarith) \u27f9\nexp mono. Then I_I \u2264 2T\u00b7(e^{\u221an/2+1/3}+1)\u00b70.57\u00b72^{\u2212(2\u221an\u22122)} \u2264\ne^{1/3}\u00b7IIMaj n (norm_logDeriv_zeta_le_iimZeta (n\u22655); e^{\u221an/2+1/3}+1\n\u2264 e^{1/3}(e^{\u221an/2}+1); T \u2264 \u221an+1; unfold IIMaj + ring).\n**6-c-iv RECIPE (mid-horizontal [\u22125/2,3] at height \u00b1T):** per-zero\nintegral \u222b_{\u22125/2}^{3} d\u03c3/\u221a((\u03c3\u2212\u03b2)\u00b2+\u03b4\u00b2) \u2014 FTC with the DIRECT\nantiderivative F(\u03c3) := Real.log((\u03c3\u2212\u03b2) + Real.sqrt((\u03c3\u2212\u03b2)\u00b2+\u03b4\u00b2))\n(Real.arcsinh does NOT exist here; F\u2032 = integrand exactly:\ng := (\u03c3\u2212\u03b2)+\u221a(h(\u03c3)) > 0 since \u221ah > |\u03c3\u2212\u03b2|; HasDerivAt via\nhasDerivAt_id.sub/Real.hasDerivAt_sqrt/Real.hasDerivAt_log + the\nidentity g\u2032 = g/\u221ah; integral_eq_sub_of_hasDerivAt). Bound:\nF(3)\u2212F(\u22125/2) = log(num/den) with num \u2264 2(3\u2212\u03b2)+\u03b4 \u2264 6+\u03b4, den =\n(\u2212u+\u221a(u\u00b2+\u03b4\u00b2)) = \u03b4\u00b2/(u+\u221a(u\u00b2+\u03b4\u00b2)) \u2265 \u03b4\u00b2/(7+\u03b4) (u := \u03b2+5/2 \u2264 7/2) \u27f9\n\u222b \u2264 log(6+\u03b4)+log(7+\u03b4)+2\u00b7log(1/\u03b4) \u2264 2\u00b7log(16.5/\u03b4) (\u03b4 \u2264 1 from\nmem_nearZerosSub; log 7 \u2264 1.946, log 8 \u2264 2.08, 2\u00b7log 16.5 \u2265 5.606).\nPer-zero \u2264 2\u00b7log(16.5/c_clear) with c_clear = 1/(9\u00b7C0hat(\u221an+2)) (the\nwide pigeonhole: nearZerosSub T's zeros have \u03b3 \u2208 (T\u22121,T+1) \u2286\n(\u221an\u22121,\u221an+2) \u2713). Swap \u222b\u03a3 = \u03a3\u222b (integral_finsetSum \u2014 the deprecated\nintegral_finset_sum's new name; per-term integrability by continuity,\ndenominator > 0). \u03a3 mult \u2264 Z2hat T (nearZerosSub_mult_sum_le hZC2,\nT \u2265 10) \u27f9 near-integral \u2264 2\u00b7Z2hat(T)\u00b7log(148.5\u00b7C0hat(\u221an+2)) =: NI.\nR-part: capstone per \u03c3 (him : s.im = T by simp; h\u03b6 :\nzeta_ne_zero_horizontal hTwide) \u27f9 \u222b \u2016R\u2016 \u2264 5.5\u00b7(10.5\u00b7log(T+2)+48).\nKernel e\u2074+1 (kFun_shift_norm_le_exp_four_add_one at s := w\u22121:\nre s = \u03c3\u22121 \u2264 3 \u27fa \u03c3 \u2264 4 \u2713 covers [\u22125/2,3]; n \u2264 T\u00b2 from \u221an \u2264 T).\nAssembly per side: \u2016H(\u22125/2\u21923, \u00b1T)\u2016 \u2264 (e\u2074+1)\u00b7(NI + 5.5(10.5 log+48));\nthe bottom (\u2212T) by the conj trick (intervalIntegral_conj + Jlag_conj,\nDL-5 pattern).\n**6-c-v RECIPE:** HIntegral_split at 3 (integrability via\nzeta_ne_zero_horizontal for the mid, re \u2265 3 zero-free for the tail) \u27f9\n\u2016H(\u22125/2\u21922\u221an, \u00b1T)\u2016 \u2264 mid + DogLegRight (dogLegUpper_two_sides,\nhIntegral_Jlag_low(_neg)_norm_le_dogLegUpper \u2713 PROVED); both sides:\n\u2264 2(e\u2074+1)(NI + 5.5(...)) + 2\u00b7DogLegRight.\n**6-d RECIPE (the fold):** sides identity\nsf_abs_le_rectInt_add_zeroSum hZC (T from exists_zero_avoiding_T_wide\nhZC at a := \u221an, \u221an \u2265 316 \u2265 3) + bridge\nzeroSum_norm_le_four_FAlt_add_one hRH hZCG hNLZ (T \u2264 3\u00d710\u00b9\u00b2\u22121 from\nn \u2264 N\u2081; 2 \u2264 T) + \u2016RectInt'\u2016 = (1/(2\u03c0))\u00b7\u2016RectInt\u2016 \u2264 (1/2\u03c0)\u00b7(sides)\n(RectangleIntegral' def, norm_smul, \u20161/(2\u03c0i)\u2016 = 1/(2\u03c0)) \u27f9\n|Sf n| \u2264 (1/2\u03c0)(I_III + Horiz + e^{1/3}IIMaj) + (4F+1) \u2264\n(1/2\u03c0)(I_III-charge + Horiz-charge) + IIMaj + 4F + 1 (e^{1/3} \u2264 1.4 \u2264\n2\u03c0 \u2014 the F-E absorption, one linarith; e^{1/3} \u2264 1.4 via\n(exp(1/3))\u00b3 = e \u2264 2.7183 \u2264 2.744 = 1.4\u00b3 + le_of_pow_le_pow_left\u2080) \u2264\nBn FAlt n \u2014 with the HORIZONTAL PINCH as the only real-analytic\ncomparison: NI + 5.5(10.5 log+48) \u2264 7\u00b7Hhat T (pinch-lemma pattern\nfrom 5f-iii: certified endpoint at n = 10\u2075 + growth direction; E-030\nV3 witness ratio \u2264 0.40; suffices 2\u00b7Z2hat(T)\u00b7log(148.5\u00b7C0hat(\u221an+2)) \u2264\n21\u00b7C0hat(T)\u00b2 since 5.5 \u2264 7 on the (10.5 log+48) part \u2014 elementary\nL/LL comparisons with log x \u2264 x/e (Real.log_le_sub_one_of_pos at\nx/e), certified numerics for the endpoint constants).\n- **I_III (left vertical, \u03c3 = \u22125/2)**: kernel \u2264 2 (kFun_norm_le_two \u2713\n  ii\u2032-4); |t| \u2265 10: tight R-bound (5f capstone \u2713) + near sum \u2264\n  (2/3)\u00b7Z2(T); |t| \u2264 10: MZeroProp \u2713; length 2T \u2014 see recipe above.\n- **I_II/I_IV (horizontals)**: mid [\u22125/2, 3] kernel \u2264 e\u2074+1 +\n  segment-integral machine (NI); right tail [3, 2\u221an] \u2014\n  dogLegUpper_two_sides \u2713 PROVED (LiDogLeg, NO perimeter).\n- **I_I (right vertical, \u03c3\u2081 = 2\u221an)**: \u26a0 **FINDING F-E (session 040,\n  D-074 \u00a79)**: the charged kernel e^{\u221an/2}+1 is off by one (the ii\u2032-4\n  lemma needs re w \u2265 2\u221an+1; DL-4's variant needs t\u00b2 \u2265 n; at t = 0 the\n  true kernel is (2\u221an/(2\u221an\u22121))\u207f = e^{\u221an/2+1/8}). REPAIR (adopted):\n  charge I_I honestly as **e^{1/3}\u00b7IIMaj(n)** \u2014 uniform-in-t kernel\n  \u2264 e^{\u221an/2+1/3}+1 (n \u2265 4: |w/(w\u22121)| \u2264 1+1/(2\u221an\u22121), add_one_le_exp,\n  n/(2\u221an\u22121) \u2264 \u221an/2+1/3) + norm_logDeriv_zeta_le_iimZeta (DL-6 \u2713) +\n  length 2T \u2264 2(\u221an+1). The overrun is absorbed by the fold's FREE\n  dropped 2\u03c0 normalization (e^{1/3} \u2264 1.4 \u2264 2\u03c0 \u2014 one linarith step in\n  ii\u2032-6-d). NO change to Bn/IIMaj/DogLegRight/convexity/pinch/base\n  points. (Fattening IIMaj's constant REJECTED: iimaj_bracket_bound\n  is an absolute \u03c8\u0303-bracket with 4.56 linear \u2014 \u00d71.404 breaks 4/3.)\n- **triv(\u22122)**: \u2264 1 (zeroMult_neg_two \u2713 ii\u2032-4).\nFold \u27f9 |Sf n| \u2264 Bn FAlt n (the ii\u2032-6-b sides identity\nsf_abs_le_rectInt_add_zeroSum + bridge zeroSum_norm_le_four_FAlt_add_one,\nboth PROVED session 038; the per-piece fits are E-030/E-034-validated:\nNI + 5.5(10.5 log+48) \u2264 7H\u0302 (ratio \u2264 0.40), DogLegRight matches Bn's\n2\u00b7DogLegRight slot, I_I \u2264 e^{1/3}\u00b7IIMaj \u2264 2\u03c0\u00b7IIMaj (F-E), bridge \u2264\n4F, triv \u2264 1).\n**ii\u2032-6-c sub-stage map (session 040, new file LiSideBounds.lean):**\n6-c-i scaffolding (rectangle side decomposition, HIntegral split,\npath integrability, Jlag-norm factorization, even-symmetry helper,\nZ2hat_mono, nearZerosSub mult-count bridge \u2264 Z2hat t) \u2192 6-c-ii I_III\n\u2192 6-c-iii I_I (F-E form) \u2192 6-c-iv mid-horizontal segment machine\n(per-zero arcsinh FTC integral \u2264 2\u00b7log(16.5/\u03b4), near-sum swap,\nR-part 5.5\u00b7(10.5 log+48); bottom by conj) \u2192 6-c-v horizontal\nassembly (mid + DL-5 tails both sides). THEN 6-d: the pinch\nNI + 5.5(...) \u2264 7H\u0302 + the 2\u03c0 fold \u27f9 `sfBoundProp : SfBoundProp` \u2192\nii\u2032-7 (closure at the ORIGINAL N\u2081 = (3\u00d710\u00b9\u00b2\u22121)\u00b2 with the paper\ncorrection note: F-A both-signs + F-B two-unit + F-D dog-leg +\nF-E I_I kernel footnote).\nRead first: D-071 \u00a74.4 (the four-side component designs with the\ndog-leg swap) + LiAssembly.lean (the sides identity) + LiDogLeg.lean\n(the horizontal deliverables).\n**Crash-safe protocol (user directive 2026-08-25):** artifacts saved\nIMMEDIATELY when produced; commit per sub-stage; D-074 \u00a71 progress\nlog is the in-thread record; STATE.md updated LAST.\n**Fallbacks:** (a) c = 1.5 paused branch wip/c-1.5-margin-redo\n(642d47a, N\u2081 = 4\u00d710\u00b2\u2074); (b) c = 2 (N\u2081 = 2.25\u00d710\u00b2\u2074); (c) T = \u221an\nhidden-cancellation open question (D-073 \u00a78 D4).\n\n### Superseded: the c = 1.5 main-line redo (record, session 040 start \u2014\n### PAUSED by user directive; the 8-step re-run plan is preserved in\n### git history (commit range ded9603..e81c35a) and on the fallback\n### branch wip/c-1.5-margin-redo)\n\n### Superseded option menu (record, session 038 end \u2014 resolved by the\n### ii\u2032-6-R thread, session 039)\nSession 039 was to return to Finding F-D. Resolved: repair (R)\nadopted and PROVED in D-073 with c = 1.5 recommended (option (i),\nwith the c-choice corrected by E-033 data); the T = \u221an salvage\n(option (ii)) is settled numerically \u2014 the per-side claim is\nempirically TRUE via hidden cancellation (E-032) \u2014 and parked as an\nopen question (D-073 \u00a78 D4); the literature check (option (iii))\nfound nothing (D-072 \u00a77); submission strategy (option (iv)) unchanged\n\u2014 Paper A frozen/submittable at its 3-hypothesis form, with the\ncorrection note queued at ii\u2032-7.\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": 1,
      "oldLines": 24,
      "newStart": 1,
      "newLines": 144,
      "lines": [
        " # STATE.md \u2014 NGUYEN-RH-1 RESUME POINT",
        " # \u2b50 READ THIS FIRST at the start of every session.",
        "-Last updated: 2026-08-25 | **c = 1.5 MAIN-LINE REDO PAUSED (user",
        "-directive, session 040): the goal is the ORIGINAL N\u2081 = 9\u00d710\u00b2\u2074. The",
        "-c = 1.5 WIP is preserved on branch `wip/c-1.5-margin-redo` (642d47a,",
        "-BUILD BROKEN mid-convexity \u2014 resume map in the commit message);",
        "-master is green (36b9e79) with the session-038 honest Bn (4F, (2/3)Z2)",
        "-whose right-tail charge \"3.3\" is the F-D-broken one (D-072). NEW LIVE",
        "-DIRECTIVE: PROJECT_DIRECTIVE_D-074.txt \u2014 the ZERO-FREE DOG-LEG",
        "-REPAIR: keep T_cut = \u221an (\u27f9 bridge/residues/N\u2081 = (T\u2080\u22121)\u00b2 unchanged),",
        "-deform ONLY the right horizontal tail [3, X_R] up to U = (3/2)\u221an",
        "-(where D-073's repaired stepping applies, q = e^{4/9}/2 < 1) through",
        "-the UNCONDITIONALLY zero-free region Re w \u2265 3 > 1. Immediate task per",
        "-\u00a719: execute \u00a72\u2013\u00a711 (coordinate audit \u2192 exact derivation \u2192 E-034 \u2192",
        "-temporary fold), then STOP and report answers A\u2013L.**",
        "-Session 039 COMPLETE \u2014 **ii\u2032-6-R side thread COMPLETE (D-073): E-032",
        "-verdict HIDDEN CANCELLATION (per-side claim empirically TRUE at",
        "-T = \u221an, |I|/env down to 5.6e-10, but envelope-unprovable there);",
        "-repaired proof Lemma 4.1 + R(c) explicit (R(1.5) = 5.94 \u2014 reused by",
        "-the D-074 dog-leg's H_high verbatim); c = 1.5 global repair validated",
        "-but superseded by D-074; drafts D3/D4 in D-073 \u00a78.**",
        "+Last updated: 2026-08-26 | **ii\u2032-6 + ii\u2032-7 COMPLETE (session 041):",
        "+`sfBoundProp : SfBoundProp` and `lambda_pos_finite_height_closed`",
        "+PROVED in Lean from EXACTLY the eight declared hypotheses; full axiom",
        "+audit clean; Paper A closed (B(n) correction note F-A/F-B/F-D/F-E,",
        "+Appendix B rewritten, compiles clean 9 pp); archive closed (D-037",
        "+erratum block, R-004 Lean-closure status, NGUYEN.md, this file,",
        "+journal-041). The finite-height Li theorem \u03bb_n > 0 for ALL",
        "+1 \u2264 n \u2264 N\u2081 = (3\u00d710\u00b9\u00b2\u22121)\u00b2 \u2248 9\u00d710\u00b2\u2074 is now FULLY MACHINE-PROVED with",
        "+the ORIGINAL N\u2081 PRESERVED (D-074 dog-leg endpoint). Master @ b64a839+",
        "+(archive commits after). NEXT: user read-through of paperA.pdf +",
        "+submission decision; deprioritized threads below.**",
        "+",
        "+## SESSION 041 HEADLINES (ii\u2032-6-c..6-d + ii\u2032-7 \u2014 THE CLOSURE SESSION)",
        "+1. **ii\u2032-6-c COMPLETE** (4 commits): 6-c-ii I_III",
        "+   `vIntegral_Jlag_left_norm_le` (6e5a98f \u2014 tails via the 5f tight",
        "+   R-bound + near count (2/5)Z\u2082, middle via the perimeter MZeroProp,",
        "+   even-symmetry tail identification); 6-c-iii I_I F-E form",
        "+   `vIntegral_Jlag_right_le_exp_third_IIMaj` (9bd8ba9 \u2014 the uniform",
        "+   kernel lemma `kFun_right_vertical_norm_le_exp_sqrt_add_third`:",
        "+   plain triangle + \u2016w\u22121\u2016 \u2265 re(w\u22121) = 2\u221an\u22121, worst case t = 0);",
        "+   6-c-iv the mid-horizontal segment machine (1fed1df \u2014 the",
        "+   arcsinh-FTC `integral_one_div_sqrt_sq_add_sq` from scratch: the",
        "+   direct antiderivative F(\u03c3) = log((\u03c3\u2212\u03b2)+\u221a((\u03c3\u2212\u03b2)\u00b2+\u03b4\u00b2)), g\u2032 = g/\u221ah",
        "+   exactly; endpoints F(3) \u2264 log(6+\u03b4), \u2212F(\u22125/2) \u2264 log(7+\u03b4)+2log(1/\u03b4)",
        "+   via the rationalization \u03b4\u00b2/(u+\u221a); per-zero \u2264 2\u00b7log(16.5/\u03b4) by PURE",
        "+   log-mono ((6+\u03b4)(7+\u03b4) \u2264 56 \u2264 272.25 = 16.5\u00b2 \u2014 NO certified log",
        "+   numerics)); 6-c-v the horizontal assembly (5d3dc0a \u2014 split at 3 via",
        "+   HIntegral_split, mid by 6-c-iv, tails by DL-5, both sides).",
        "+2. **6-d THE FOLD (774fec5): `sfBoundProp : SfBoundProp` PROVED** \u2014",
        "+   |Sf n| \u2264 Bn FAlt n on [10\u2075, N\u2081] from EXACTLY the six declared",
        "+   perimeter hypotheses (RHUpTo, ZeroCountProp, ZeroCountProp2,",
        "+   ZeroCountGlobalProp, NoLowZeros, MZeroProp). `pinch_horizontal`",
        "+   (NI + 5.5R \u2264 7\u00b7H\u0302) discharged by a fully elementary chain:",
        "+   \u0108\u2080(\u221an+2) \u2264 \u221an+2 (`C0hat_le_self`, log x \u2264 x/e with 1/e \u2264 0.36789",
        "+   from Real.exp_one_gt_d9, loglog \u2264 log\u22121) \u27f9 148.5\u00b7\u0108\u2080(\u221an+2) \u2264",
        "+   (\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",
        "+   8 \u2264 21\u00b70.433 = 9.093; 5.5 \u2264 7 on the R-part. The bridge cloned at",
        "+   (hTle : T \u2264 3\u00b710\u00b9\u00b2) \u2014 the range the internal",
        "+   `zeroSum_nontriv_norm_le` actually uses (the public T \u2264 3\u00b710\u00b9\u00b2\u22121",
        "+   hypothesis fails at the very top: n = N\u2081 has \u221an = 3\u00b710\u00b9\u00b2\u22121 exactly",
        "+   and the pigeonhole T can land in (3\u00b710\u00b9\u00b2\u22121, 3\u00b710\u00b9\u00b2]).",
        "+3. **ii\u2032-7a+7b (a0943a6)**: `lambda_pos_finite_height_closed` PROVED",
        "+   (LiClosed.lean, root-imported) \u2014 \u03bb_n > 0 for ALL 1 \u2264 n \u2264 N\u2081 from",
        "+   EXACTLY EIGHT declared hypotheses (two computational certificates:",
        "+   RHUpTo, LiVerifiedUpTo; six analytic perimeter Props: ZeroCountProp,",
        "+   ZeroCountProp2, ZeroCountGlobalProp, NoLowZeros, MZeroProp). Full",
        "+   axiom audit (AuditSession041): 29 declarations \u2014 ALL [propext,",
        "+   Classical.choice, Quot.sound] only, 0 sorryAx.",
        "+4. **ii\u2032-7c (b64a839)**: Paper A closed (compiles clean, 9 pp, zero",
        "+   undefined refs): abstract/intro \u2192 the eight-hypotheses headline;",
        "+   \u00a73 Step 2 the B(n) display corrected (4F(T), (2/3)Z\u2082(T),",
        "+   2(e\u2074+1)\u00b77H(T) + 2\u00b7DL(n), I_Maj) + the F-A/F-B/F-D/F-E",
        "+   correction-note footnote; \u00a73 Step 3 the bridge 4F (both signs);",
        "+   Appendix B rewritten (second tier COMPLETE \u2014 SfBoundProp machine-",
        "+   proved, the six analytic inputs enumerated, the full complex-",
        "+   analytic content list); AI Contribution Statement factual refresh",
        "+   (sessions 001\u2013041, closure declarations).",
        "+5. **ii\u2032-7d (this commit)**: archive closed \u2014 D-037 erratum block",
        "+   (the four corrections with pointers), R-004 Lean-closure status",
        "+   line, NGUYEN.md (Phase 5B \u2192 COMPLETE, ii\u2032-6/ii\u2032-7 checked, Ledger",
        "+   #6 machine-proved note), STATE.md (this file), journal-041.",
        "+6. **Banked gotchas (journal-041)**: \u03a3 (U+03A3) is NOT an identifier",
        "+   character in Lean 4 (lexes as Sigma-notation; a phantom ?m.NNN",
        "+   metavariable goal at the DECLARATION HEAD is the tell-tale of a",
        "+   downstream parse break); `\u222b x in a..b, body` captures trailing +/\u2212",
        "+   into the integrand (parenthesize every integral summand);",
        "+   ContinuousAt.comp/ContinuousWithinAt.comp need (g :=) (f :=)",
        "+   (x :=) pinned (arg-first elaboration misdecomposes the point);",
        "+   Continuous.div/.mul/.sub produce Pi-op forms (ascribe the per-term",
        "+   type or show-bridge to the Pi form \u2014 the const ?c otherwise leaks",
        "+   as an unsolved ?m); linarith CANNOT multiply by atom-constants",
        "+   ((1/(2\u03c0)), (e\u2074+1)) \u2014 every such step needs a pre-packaged",
        "+   mul_le_mul_of_nonneg_*; in large contexts use linarith only /",
        "+   nlinarith only (the context scan on giant types deterministically",
        "+   times out at isDefEq); norm_le_insert' : \u2016a\u2016 \u2264 \u2016b\u2016+\u2016a\u2212b\u2016 (the",
        "+   unprimed has the args swapped); eq_div_iff for c = a/b goals",
        "+   (div_eq_iff is for a/b = c); Finset.sum_mul for constant-RIGHT",
        "+   extraction (Finset.mul_sum is constant-LEFT); le_of_pow_le_pow_left\u2080",
        "+   takes the nonneg on the RIGHT (b) side; Real.add_one_le_exp is",
        "+   x+1 \u2264 e^x (not 1+x \u2014 bridge by linarith); neg_le_abs : \u2212a \u2264 |a|",
        "+   (neg_abs_le is \u2212|a| \u2264 a); HasDerivAt.pow yields Pi.pow forms (simpa",
        "+   bridges); rw [hre] closes `-5/2 \u2264 -5/2` by auto-rfl le_refl",
        "+   (le_of_eq hre.symm is deterministic).",
        "+",
        "+## CURRENT POSITION",
        "+\u2714 PHASE 0, 1, 3, 4 COMPLETE. PHASE 2 (Track B): mapped to exhaustion",
        "+at current technology (2.6\u20132.13, parked). PHASE 5: 5.3 \u2714 5.4 \u2714 5.2 \u2714",
        "+(live). PHASE 5B (tier ii\u2032): **COMPLETE (session 041)** \u2014 all",
        "+sub-stages ii\u2032-0..ii\u2032-7 done (see NGUYEN.md \u00a75B for the full log).",
        "+",
        "+**Theorem status (session 041 \u2014 the closed forms):**",
        "+- T-1 (R-004): [PROVED-CONDITIONAL(computational RH-to-T\u2080;",
        "+  computational finite verification)] \u2014 **FULLY MACHINE-PROVED in",
        "+  Lean 4**: `lambda_pos_finite_height_closed` (LiClosed.lean) \u2014",
        "+  \u03bb_n > 0 for ALL 1 \u2264 n \u2264 N\u2081 = (3\u00d710\u00b9\u00b2\u22121)\u00b2 from EXACTLY EIGHT",
        "+  declared hypotheses: RHUpTo (Platt\u2013Trudgian), LiVerifiedUpTo",
        "+  (finite Li verification), ZeroCountProp/ZeroCountProp2/",
        "+  ZeroCountGlobalProp (Trudgian N(T)/S(T) forms), NoLowZeros",
        "+  (Platt-class zero-location), MZeroProp (M\u2080 interval certificate).",
        "+  Axiom audit on the full chain: [propext, Classical.choice,",
        "+  Quot.sound] only, 0 sorryAx (AuditSession041, 29 decls).",
        "+  sorryAx remains ONLY on the 5 skeleton statements (1 Suzuki + 4",
        "+  valley) by design.",
        "+- T-2 (R-003 + D-041): factorization + (\u2605) \u27fa (1.12) [PROVED modulo",
        "+  Phase-5 formalities]; (1.12) \u27f9 spec(D) \u2282 \u211d [PROVED via Suzuki + D1];",
        "+  \u21d0 [SKELETON L3/L4].",
        "+- 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).",
        "+",
        "+**Lean:** research/lean/NguyenRH1/ \u2014 full build GREEN (8775 jobs);",
        "+all 26 modules root-imported incl. LiSideBounds (ii\u2032-6-c..d) and",
        "+LiClosed (ii\u2032-7). sorryAx remains ONLY on: R003_exact_factorization",
        "+(tier iv) + 4 valley statements (tier iii).",
        "+",
        "+**Deprioritized / open threads:** a=13+ push; adversary-ceiling LP;",
        "+T4b; \u03bb-channel (G-004); \u03b8-channel (dead, E-024); Paper B Task 1",
        "+(R-003 tempered-FT bookkeeping trace, queued); user read-through of",
        "+paperA.pdf (NOW THE FRONT ITEM \u2014 nothing blocks it); repo-publication",
        "+prep; submission decision (cover-letter.md + referee-list.md exist",
        "+from session 013, target Experimental Mathematics); the c = 1.5",
        "+fallback branch wip/c-1.5-margin-redo (642d47a, preserved, unneeded);",
        "+the T = \u221an hidden-cancellation open question (D-073 \u00a78 D4); the",
        "+Lagarias F-D correspondence package (user's own work-in-progress in",
        "+research/correspondence/lagarias-F-D-package/, uncommitted \u2014 NOT",
        "+mine to commit).",
        "+",
        "+## NEXT ACTION",
        "+**AT A CLEAN BOUNDARY (session 041 end, ii\u2032-6 + ii\u2032-7 COMPLETE). The",
        "+user's read-through of paperA.pdf + the submission decision is the",
        "+front item. If told to continue research: Paper B Task 1 (R-003",
        "+tempered-FT bookkeeping trace) or the parked Track-B remainders per",
        "+the user's call.**",
        " Session 038 COMPLETE \u2014 **ii\u2032-3b + ii\u2032-3c +",
        " ii\u2032-6-0 + ii\u2032-6-a + ii\u2032-6-b DONE; FINDING F-D DOCUMENTED (D-072,",
        " user paused to think): the (6.12) stepping in Lagarias's Thm 6.1 is"
      ]
    }
  ],
  "userModified": false,
  "replaceAll": false
}