← Session 33 — ii′-3b/3c crux + F-D finding; Lagarias letter package
thinking (79 chars)
User just wants a status summary. Give concise summary of where the project is.
# Project NGUYEN-RH-1 — Status (Session 037 complete, 2026-08-24)
## The big picture
The project's flagship result is **R-004: the explicit finite-height Li theorem** — λ_n > 0 for all n ≤ N₁ ≈ 9×10²⁴ (T₀ = 3×10¹² Platt–Trudgian), the maximal content of the Li-coefficient route short of RH itself. Phases 0, 1, 3, 4 are complete; Phase 2 (spectral/Track B) is mapped to exhaustion at current technology.
## Where we are right now: Phase 5B (tier ii′)
**Goal:** close the last named analytic hypothesis (`SfBoundProp`) in Lean 4 **before** submitting Paper A, so `lambda_pos_finite_height_verified` rests only on the declared computational perimeter (Platt–Trudgian RHUpTo, LiVerifiedUpTo, Trudgian N(T)/S(T), NoLowZeros, M₀). Paper A stays frozen/submittable throughout.
**Done (sessions 014–037):**
- ii′-0: design (D-064) — found + fixed the liCoeff encoding defect; found the crux identity Sf(n) = Res₁(n) ⟹ assembly is tail-free
- ii′-1a/1b/2: paired liCoeff + summability, rectangle residue machinery (`rectInt'_Jlag`), elementary swaps
- ii′-3a: archimedean + ζ Taylor coefficients (digamma series built from scratch)
- ii′-4: zero-avoiding T + kernel bounds + trivial-zero simplicity
- ii′-5a–5f (the long pole, ~11k lines across 7 files): **partial-fraction identity proved** (modulo ZeroCountProp only) and the **tight R-bound `‖ζ′/ζ(s) − Σ_near m/(s−ρ)‖ ≤ 10.5·log(t+2) + 48` proved** (LiTightR.lean, session 036)
- Session 037: capstone dependency audit (3 standard axioms only, perimeter verbatim); **ii′-3b started** — LiMoments.lean §1–§4 done (~730 lines, build green), the k=1 moment `sigmaP_one_eq_neg_gFun_zero` PROVED
## Next action (Session 038)
**LiMoments §5 then §6** (ii′-3b back half): termwise iterated derivation of the zero series at 0 for k ≥ 2, then the capstone `sigmaP_eq_neg_iteratedDeriv_gFun_div`. Full skeleton + probed Mathlib signatures are banked in journal-037. Then root-import LiTightR + LiMoments, build, audit.
Remaining after that: **ii′-3c** (assemble Lagarias (4.10) ⟹ crux Sf = Res₁) → **ii′-6** (L0 assembly, incl. D-069 Finding 2's H(T) near-sum repair) → **ii′-7** (closure: `sfBoundProp` proved, paper Appendix B, tag upgrade).
**Blockers:** none. Full build green (8762 jobs); sorryAx remains only on the 5 intended skeleton statements (1 Suzuki + 4 valley).
raw content_json (database row)
[{"type":"thinking","thinking":"User just wants a status summary. Give concise summary of where the project is.","signature":""},{"type":"text","text":"# Project NGUYEN-RH-1 — Status (Session 037 complete, 2026-08-24)\n\n## The big picture\nThe project's flagship result is **R-004: the explicit finite-height Li theorem** — λ_n > 0 for all n ≤ N₁ ≈ 9×10²⁴ (T₀ = 3×10¹² Platt–Trudgian), the maximal content of the Li-coefficient route short of RH itself. Phases 0, 1, 3, 4 are complete; Phase 2 (spectral/Track B) is mapped to exhaustion at current technology.\n\n## Where we are right now: Phase 5B (tier ii′)\n**Goal:** close the last named analytic hypothesis (`SfBoundProp`) in Lean 4 **before** submitting Paper A, so `lambda_pos_finite_height_verified` rests only on the declared computational perimeter (Platt–Trudgian RHUpTo, LiVerifiedUpTo, Trudgian N(T)/S(T), NoLowZeros, M₀). Paper A stays frozen/submittable throughout.\n\n**Done (sessions 014–037):**\n- ii′-0: design (D-064) — found + fixed the liCoeff encoding defect; found the crux identity Sf(n) = Res₁(n) ⟹ assembly is tail-free\n- ii′-1a/1b/2: paired liCoeff + summability, rectangle residue machinery (`rectInt'_Jlag`), elementary swaps\n- ii′-3a: archimedean + ζ Taylor coefficients (digamma series built from scratch)\n- ii′-4: zero-avoiding T + kernel bounds + trivial-zero simplicity\n- ii′-5a–5f (the long pole, ~11k lines across 7 files): **partial-fraction identity proved** (modulo ZeroCountProp only) and the **tight R-bound `‖ζ′/ζ(s) − Σ_near m/(s−ρ)‖ ≤ 10.5·log(t+2) + 48` proved** (LiTightR.lean, session 036)\n- Session 037: capstone dependency audit (3 standard axioms only, perimeter verbatim); **ii′-3b started** — LiMoments.lean §1–§4 done (~730 lines, build green), the k=1 moment `sigmaP_one_eq_neg_gFun_zero` PROVED\n\n## Next action (Session 038)\n**LiMoments §5 then §6** (ii′-3b back half): termwise iterated derivation of the zero series at 0 for k ≥ 2, then the capstone `sigmaP_eq_neg_iteratedDeriv_gFun_div`. Full skeleton + probed Mathlib signatures are banked in journal-037. Then root-import LiTightR + LiMoments, build, audit.\n\nRemaining after that: **ii′-3c** (assemble Lagarias (4.10) ⟹ crux Sf = Res₁) → **ii′-6** (L0 assembly, incl. D-069 Finding 2's H(T) near-sum repair) → **ii′-7** (closure: `sfBoundProp` proved, paper Appendix B, tag upgrade).\n\n**Blockers:** none. Full build green (8762 jobs); sorryAx remains only on the 5 intended skeleton statements (1 Suzuki + 4 valley)."}]