Session 013 — 2026-08-20 — Paper A split + finalize

Directive

User ("go go") after reviewing the assessment of the mathematician's minor suggestions: execute the split recommendation — Paper A as a self-contained artifact, Paper B as a research-note skeleton carrying the standing items.

Pre-split minor item (session-012-end-notes item 1) — DONE (10fdda6)

Number-trail note filed: D-062 §5 + LiBasePoints.lean header now carry the one-line explanation that the dps-40 plan bound (> 9 960) and the Lean-certified bound (≥ 8 001) differ by deliberate outward rounding (norm_num comfort); both suffice. NGUYEN.md session-log word collision ("certified > 9 960" for plan numbers) fixed to "plan bounds > 9 960".

The split (this session)

• paperA.tex (NEW, 8 pp, compiles clean, zero undefined refs): "An explicit finite-height Li-positivity theorem with a machine-verified assembly." Contents: retargeted abstract/intro (single contribution + companion-note pointer + the three-named- hypotheses Lean headline), Background (forward refs to the spectral sections replaced by companion-note pointers; sanity gate retained), §3 = the R-004 theorem with the full five-step proof sketch (reconciled margin trail footnote included), §4 obstruction analysis (Track A ceiling, G-001, G-003, ξ⁽ᵏ⁾ routes; the G-004 ground-state bullet moved to Paper B), Appendix A = Li-coefficient machinery (E-011/E-015/E-021/E-023/E-028), Appendix B = Formal verification (three-hypothesis final form; remaining tier ii′ declared post-publication).
• paperB.tex (NEW, 6 pp, compiles clean): "The Suzuki operator line: exact factorization, spectral-measure equilibrium, and the valley theorem (research note, in preparation)." Opens with §0 STANDING ITEMS box (per the review): (1) Theorem R-003's tempered-FT bookkeeping + o(eᵃ) — trace or demote to Proposition; (2) L3/L4 open (converse = proof skeleton); (3) authorship policy. Then §3.2/§3.3 content, the G-004 obstruction note, Appendix A = spectral-measure numerics (E-016–E-027).
• draft.tex: FROZEN with a superseded header comment (compiles clean, 12 pp pre-split state retained as the combined archive copy).

Editorial decisions (flagged for the user)

• Author block carried over verbatim to both papers EXCEPT one typo fix: "harness fromAnthropic" → "harness from Anthropic" (thanks footnote). Authorship itself untouched — journal-policy question is the user's call at submission (standing item 3).
• Paper A date bumped to 2026-08-20.
• Paper A obstruction lead-in made precise ("graveyard G-001--G-003; derivations D-009--D-031" — the bullets cite D-022/D-030/D-031, outside the old D-009--D-013 range; the imprecision predates the split and is fixed in Paper A only).

Audit-routine note

Paper A's moved content is verbatim from the audited combined draft; the NEW/CHANGED lines (abstract, intro, background paragraph, section lead-ins, Appendix B retargeting, date) were re-read in final form against the archive state (three hypotheses, axiom profile, no-sorry in the Li chain, margin trail numbers 16 020 / 15 764 / ≥ 8 001, overlap factor 5 at the 10⁵ split). All consistent.

Files

• research/paper/paperA.tex, paperB.tex (NEW); draft.tex (frozen header)
• research/journal/session-013.md (this file); STATE.md; NGUYEN.md (archive map + session log); research.db (session 13)

State at stop

Paper A is a complete, self-contained, compile-clean artifact. Remaining optional polish (user's call): figures from numerics CSVs; E-023b acb M₀ certificate; a full read-through by the user before any circulation. Paper B checklist lives in its §0. Tier ii′ (contour formalization) remains post-publication.

AUTHORSHIP CHANGE (2026-08-20, user directive)

User: "remove Kimi K3 and Claude Code as an author. Keep only Dan T Nguyen, Research Ai." Applied to paperA.tex, paperB.tex, AND the frozen draft.tex (so no stale-authored PDF can circulate from any file; the freeze covers content, not metadata). New block: \author{Dan T Nguyen\thanks{Research Ai}}. Paper B §0 standing item 3 annotated with the decision. All three PDFs rebuilt clean (8/6/12 pp). This partially resolves the mathematician's authorship-policy standing item; venue/disclosure wording remains the user's call at submission.

AI CONTRIBUTION STATEMENT + ACKNOWLEDGMENTS (2026-08-20, user directive)

Per the user's concrete implementation request (the mathematician's template): both live papers now carry (b) a title footnote ("This work was produced with substantial machine assistance; see the AI Contribution Statement"), (c) an AI Contribution Statement as back matter before the bibliography — Paper A's version cites sessions 001–013, D-036/D-037/D-056/D-057, the NguyenRH1 Li chain, E-001–E-029, D-060; Paper B's version adapted to its actual content (D-018–D-051, E-009–E-027, D-048–D-050/D-058, the statement-level skeletons, D-054/D-060) and notes the companion paper's Li chain is machine-verified — and (d) a one-sentence Acknowledgments thanking Moonshot AI and Anthropic, with the substantive record kept in the contribution statement. Human-author guarantor clause included verbatim. Frozen draft.tex untouched. Paper A now 9 pp, Paper B 6 pp, both compile clean, zero undefined refs.

PRE-SUBMISSION AUDIT OF NguyenRH1 (2026-08-20, user directive) — ALL CHECKS PASS

Full re-audit of the Lean package before circulation (D-063):

• A. Source sweep: exactly 5 sorry tactics (1 Suzuki + 4 valley skeletons, all intended); zero forbidden constructs (no admit/axiom declarations/native_decide/unsafe/implemented_by); one set_option (maxHeartbeats — elaborator budget only).
• B. Clean-room rebuild: .lake/build wiped, lake build green (8707 jobs).
• C. Exhaustive axiom audit: mechanically generated #print axioms for EVERY public declaration (139). 134 = the 3 standard axioms only; 5 = the intended skeletons (+sorryAx); nothing else anywhere. Output archived: research/lean/NguyenRH1/audit-session013-axioms.txt (+ PrintAxiomsAll.lean generator).
• D. Statement-to-paper correspondence: lambda_pos_finite_height_verified is verbatim the paper's Theorem R-004 with exactly the three declared named hypotheses (table in D-063 §D).
• E. Inherited zeta-23-lean comparators re-verified LIVE: 27 main + 16 amendment statements, verbatim match with AUDIT.md. Verdict: submission-ready. Registered as D-063.

ALSO THIS SESSION (submission support + Paper B assessment)

• Fixed the voros2017li reference (was a fabricated title with empty journal; correct: Voros, "Discretized Keiper/Li approach to the Riemann hypothesis", Exp. Math. 29(4) (2020) 452–469 — verified via the arXiv record). bibtex warning cleared (cfc7ff1).
• Submission documents: research/paper/cover-letter.md (target venue Experimental Mathematics) + research/paper/referee-list.md (6 names with fit rationale: Platt, Trudgian, Voros, Lagarias, Booker, Kontorovich) (0d5ee7c).
• Noted: empty placeholder research/paper/submit/instructions.txt exists (user-created 13:57; left untouched).
• Paper B assessment (user question: "do we need more experiments?"): answer NO — Phase 2 was mapped to exhaustion at current technology (a=13+ deprioritized D-029; θ-channel dead E-024; λ-channel G-004; (★) is an analytic gap, not an evidence gap). Paper B's gaps are proof gaps: Task 1 = trace R-003's tempered-FT bookkeeping (bounded work: D-026/D-027 derivation exists, D-059 R_τ representation, D-001 NT-1 machine-verified conventions; make o(eᵃ) quantitative; → D-064, 1–2 sessions) — the review's "take the medicine" option; Task 2 = leave L3/L4 as the honestly-tagged skeleton (open mathematics, correct state). User will continue later; Task 1 is queued as the recommended next research action.

STATE AT STOP (session 013 end)

Paper A: split, sole-authored, AI-contribution-stated, reference-fixed, audit-clean — submission-ready pending the user's read-through. Session protocol complete; everything committed.