{
  "file_path": "D:\\Python\\Quantum\\STATE.md",
  "content": "# STATE.md \u2014 NGUYEN-RH-1 RESUME POINT\n# \u2b50 READ THIS FIRST at the start of every session.\nLast updated: 2026-08-24 | Session 037 COMPLETE at a clean boundary (user\nlog-off) \u2014 **ii\u2032-3b STARTED: \u00a71\u2013\u00a74 DONE, k=1 moment PROVED; \u00a75/\u00a76 remain.**\n\n## SESSION 037 HEADLINES\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 STARTED (session\n037 \u2014 this state file's header): \u00a71\u2013\u00a74 done, k = 1 PROVED.**\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 (8762 jobs);\nLiSqueeze + LiCircleBound root-imported (session 034); LiTightR.lean\n(~4300 lines, NOT yet root-imported \u2014 import it from the root together\nwith LiMoments at the end of ii\u2032-3b); **LiMoments.lean NEW (~730 lines,\n\u00a71\u2013\u00a74, single-file green, NOT yet root-imported)**. sorryAx remains\nONLY on: R003_exact_factorization (tier iv) + 4 valley statements\n(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-3b \u00a75/\u00a76** (the k \u2265 2 moments by termwise\niterated derivation at 0 + the unified capstone\nsigmaP_eq_neg_iteratedDeriv_gFun_div; full skeleton banked in\njournal-037, all Mathlib signatures probed) \u2192 root-import LiTightR +\nLiMoments \u2192 audit \u2192 **ii\u2032-3c** (assembly of Lagarias (4.10):\n\u03c4_j = c_j + (\u22121)\u02b2\u03c3_{j+1} \u2212 (\u22121)\u02b2 \u2014 the crux identity Sf(n) = Res\u2081(n);\nneeds also the FE derivative relation gFun^{(k\u22121)}(0) =\n(\u22121)^k\u00b7gFun^{(k\u22121)}(1), small from xiL_one_sub) \u2192 **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\nSession 038: **LiMoments \u00a75 then \u00a76** (ii\u2032-3b back half). Read first:\njournal-037's \"REMAINING for ii\u2032-3b (\u00a75/\u00a76) \u2014 full skeleton\" (every\nlemma + proof step + probed Mathlib signature) and the banked-gotchas\nlist (SummationFilter refactor: `Summable.tsum_add`/`Summable.tsum_sub`\nmethod-form ONLY, tsum_neg/tsum_zero/tsum_congr/tsum_mul_left plain;\neq_zero_of_neg_eq needs LinearOrder (\u2102 N/A \u2014 use 2V = 0);\nComplex.norm_conj takes starRingEnd directly; iteratedDeriv_neg EXISTS\n(explicit args); AnalyticAt.contDiffAt exists; Equiv.tsum_eq/\nEquiv.summable_iff signatures; ascribe EVERY tsum binder; beta-redex\nshow-before-rw; field_simp's trailing-ring errors; deriv_comp's point\narg explicit). \u00a75 targets: iteratedDeriv_zpow_neg_one \u2192\niteratedDeriv_seriesTerm \u2192 seriesTerm_deriv_summableLocallyUniformlyOn\n(M-test on ball(0, \u03b4/2), dominator C_j\u00b7mult/\u2016\u03c1\u2016\u00b2) \u2192\niteratedDeriv_seriesFun_zero (iteratedDerivWithin_tsum, the\nLiDigamma:749\u2013785 call pattern verbatim). \u00a76 targets:\ngFun_eventuallyEq_zero (eventually_nhdsWithin_iff upgrade) \u2192 the\ncapstone sigmaP_eq_neg_iteratedDeriv_gFun_div (k=1 defeq branch +\nk\u22652: iteratedDeriv_congr_of_eventuallyEq \u2192 add/const split \u2192\niteratedDeriv_seriesFun_zero \u2192 per-term sign algebra \u2192\nsigmaP_eq_unpaired \u2192 field_simp (k\u22121)! \u2260 0). Then: root-import\nNguyenRH1.LiTightR + NguyenRH1.LiMoments, full build, axiom audit\n(expect 3 standard; hZC-only), journal/db/STATE/NGUYEN updates, commit.\nii\u2032-3b THEN DONE \u2192 ii\u2032-3c (the (4.10-a) assembly; also needs the FE\nderivative relation gFun^{(k\u22121)}(0) = (\u22121)^k\u00b7gFun^{(k\u22121)}(1)).\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 \u00a71\u2013\u00a74 + k=1 (session 037).\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 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"
}