← Session 18 — Lean tier (ii): finite-height proof + certified base points
Here is the complete submission map for Paper A.
---
## 0. First, a fix I just made
The `voros2017li` reference had a **fabricated title and no journal** (bibtex was warning about it). Corrected to the real publication: Voros, *Discretized Keiper/Li approach to the Riemann Hypothesis*, **Exp. Math. 29(4) (2020), 452–469**. Bonus: your key predecessor citation was published in *Experimental Mathematics* — which is also my top venue suggestion below.
## 1. What you're submitting
`research/paper/paperA.pdf` (9 pp): a conditional theorem (λ_n > 0 to ≈9×10²⁴, assuming Platt–Trudgian's computation + finite Li verification) with every constant traced, plus a Lean-4 verification story (3 named hypotheses, clean axiom audit). Category: **computational/analytic number theory + formal verification**.
## 2. Pre-submission checklist (what still needs doing)
| # | Item | Who | Effort |
|---|---|---|---|
| 1 | **Full read-through of paperA.pdf** — non-negotiable; you're the guarantor | you | an evening |
| 2 | **Make the project archive public** — the paper's honesty claims ("deterministic, archived scripts", "session logs preserved") need a public URL. GitHub repo + a tagged release; optionally Zenodo for a DOI | me (prep), you (account/publish click) | ~1 hr |
| 3 | Lean reproducibility note (toolchain v4.33.0-rc2, vendored zeta-23-lean v1.0, `lake build`, `lake env lean PrintAxioms.lean`) — goes in the repo README | me | 20 min |
| 4 | Optional: one figure (margin curve from E-023/E-028 CSVs) — nice, not required | me | 30 min |
| 5 | Optional: E-023b (acb certificate for M₀) — removes the last "grid-verified" asterisk | me | ~1 hr compute |
| 6 | **ORCID** registration (free, 5 min) — required by most journal submission systems | you | 5 min |
## 3. Route A — arXiv first (strongly recommended, do this first)
Free, fast, establishes priority, and is how the field will find it.
**What arXiv needs:**
- **LaTeX source**, not just PDF: `paperA.tex` + `paperA.bbl` (rename to `paperA.bbl`→ included; arXiv runs its own compile) + `references.bib` optional once the .bbl is baked in. It compiles with standard packages only (amsmath/amssymb/amsthm/mathtools/microtype/hyperref — all fine).
- An **arXiv account** and — the one real hurdle — **endorsement**: first-time submitters in math.NT need an endorser (an active arXiv author in the area). If you don't know one, arXiv's endorsement-request process handles it, but it can take days. **Start this now.**
- Metadata: title, abstract, MSC classes (primary **11M26**, secondary 11Y35, 11M06, 03B35/68V15 for the formal-verification angle), license choice (CC-BY or arXiv's minimal license).
- **AI policy**: arXiv prohibits AI *authorship* (you're compliant — sole human author) and expects disclosure of substantial AI-generated content (your AI Contribution Statement is exactly that). You're ahead of the policy curve here.
Timeline: submission → announcement typically 1–3 business days (longer if moderation flags the AI-disclosure novelty — unlikely).
## 4. Route B — journal submission (after arXiv posts)
**Venue shortlist, ranked by fit:**
1. **Experimental Mathematics** (Taylor & Francis) — the best fit on record: computational results with conditional/experimental components are its remit, *and it published Voros–Misguich* (your λ-verification predecessor). Subscription route: no APC; optional OA with APC (waivers available).
2. **Mathematics of Computation** (AMS) — rigorous-constants computation; high bar on novelty but your "first assembled explicit chain + machine-verified assembly" is pitched correctly. No APC on the standard route.
3. **Research in Number Theory** (Springer, fully OA) — solid fit, fast, but APC ~US$2k (waivers for independent/unfunded authors — ask).
4. **Journal of Formalized Reasoning** — only if you want to lean into the Lean side as the headline (I'd keep it as the verification appendix instead).
**What a journal submission needs:**
- The PDF + source files.
- **Cover letter** (I can draft: one page — what's new, why it fits the venue, the conditional-on-computation honesty, the machine-verified assembly, the AI disclosure already in the paper).
- 3–5 **suggested referees** (I can propose criteria/names to research — people in explicit-computation NT: e.g. the Platt/Trudgian circle, Voros, formalization-adjacent number theorists).
- Statements: funding (none/self-funded), conflicts of interest (none), **data/code availability** (your public repo URL — item 2 above), ORCID.
- The AI Contribution Statement is already in the paper — most publishers (T&F, AMS, Springer) now require exactly this and prohibit AI authorship; you're compliant by construction.
**What a referee will push on** (be ready): precise Platt–Trudgian dependency (cited correctly now); the Misguich–Voros overlap (now correctly cited to Exp. Math.); M₀'s grid-verified status (E-023b removes this if you want); the novelty claim "first assembled explicit chain"; and the SfBoundProp perimeter — which the paper already declares as its honest formal target.
## 5. Recommended order of operations
1. **You**: read-through of paperA.pdf; register ORCID; start the **arXiv endorsement request** (longest lead time).
2. **Me** (say the word): repo publication prep (README, Lean build instructions, license file), optional figure + E-023b, cover-letter draft, referee-suggestion list.
3. **You**: flip the repo public, submit to arXiv.
4. After arXiv posts: journal submission to *Experimental Mathematics* (first choice).
## 6. What only you can do
Account creation, endorsement requests, ORCID, the actual submission clicks, signing the cover letter, and any author warranties (originality, etc.). Everything else — repo prep, cover letter draft, referee list, figure, E-023b, final formatting to a journal's house style — I can do here.
Want me to start on the repo-publication prep + cover letter + referee list now?
raw content_json (database row)
[{"type":"text","text":"Here is the complete submission map for Paper A.\n\n---\n\n## 0. First, a fix I just made\n\nThe `voros2017li` reference had a **fabricated title and no journal** (bibtex was warning about it). Corrected to the real publication: Voros, *Discretized Keiper/Li approach to the Riemann Hypothesis*, **Exp. Math. 29(4) (2020), 452–469**. Bonus: your key predecessor citation was published in *Experimental Mathematics* — which is also my top venue suggestion below.\n\n## 1. What you're submitting\n\n`research/paper/paperA.pdf` (9 pp): a conditional theorem (λ_n > 0 to ≈9×10²⁴, assuming Platt–Trudgian's computation + finite Li verification) with every constant traced, plus a Lean-4 verification story (3 named hypotheses, clean axiom audit). Category: **computational/analytic number theory + formal verification**.\n\n## 2. Pre-submission checklist (what still needs doing)\n\n| # | Item | Who | Effort |\n|---|---|---|---|\n| 1 | **Full read-through of paperA.pdf** — non-negotiable; you're the guarantor | you | an evening |\n| 2 | **Make the project archive public** — the paper's honesty claims (\"deterministic, archived scripts\", \"session logs preserved\") need a public URL. GitHub repo + a tagged release; optionally Zenodo for a DOI | me (prep), you (account/publish click) | ~1 hr |\n| 3 | Lean reproducibility note (toolchain v4.33.0-rc2, vendored zeta-23-lean v1.0, `lake build`, `lake env lean PrintAxioms.lean`) — goes in the repo README | me | 20 min |\n| 4 | Optional: one figure (margin curve from E-023/E-028 CSVs) — nice, not required | me | 30 min |\n| 5 | Optional: E-023b (acb certificate for M₀) — removes the last \"grid-verified\" asterisk | me | ~1 hr compute |\n| 6 | **ORCID** registration (free, 5 min) — required by most journal submission systems | you | 5 min |\n\n## 3. Route A — arXiv first (strongly recommended, do this first)\n\nFree, fast, establishes priority, and is how the field will find it.\n\n**What arXiv needs:**\n- **LaTeX source**, not just PDF: `paperA.tex` + `paperA.bbl` (rename to `paperA.bbl`→ included; arXiv runs its own compile) + `references.bib` optional once the .bbl is baked in. It compiles with standard packages only (amsmath/amssymb/amsthm/mathtools/microtype/hyperref — all fine).\n- An **arXiv account** and — the one real hurdle — **endorsement**: first-time submitters in math.NT need an endorser (an active arXiv author in the area). If you don't know one, arXiv's endorsement-request process handles it, but it can take days. **Start this now.**\n- Metadata: title, abstract, MSC classes (primary **11M26**, secondary 11Y35, 11M06, 03B35/68V15 for the formal-verification angle), license choice (CC-BY or arXiv's minimal license).\n- **AI policy**: arXiv prohibits AI *authorship* (you're compliant — sole human author) and expects disclosure of substantial AI-generated content (your AI Contribution Statement is exactly that). You're ahead of the policy curve here.\n\nTimeline: submission → announcement typically 1–3 business days (longer if moderation flags the AI-disclosure novelty — unlikely).\n\n## 4. Route B — journal submission (after arXiv posts)\n\n**Venue shortlist, ranked by fit:**\n\n1. **Experimental Mathematics** (Taylor & Francis) — the best fit on record: computational results with conditional/experimental components are its remit, *and it published Voros–Misguich* (your λ-verification predecessor). Subscription route: no APC; optional OA with APC (waivers available).\n2. **Mathematics of Computation** (AMS) — rigorous-constants computation; high bar on novelty but your \"first assembled explicit chain + machine-verified assembly\" is pitched correctly. No APC on the standard route.\n3. **Research in Number Theory** (Springer, fully OA) — solid fit, fast, but APC ~US$2k (waivers for independent/unfunded authors — ask).\n4. **Journal of Formalized Reasoning** — only if you want to lean into the Lean side as the headline (I'd keep it as the verification appendix instead).\n\n**What a journal submission needs:**\n- The PDF + source files.\n- **Cover letter** (I can draft: one page — what's new, why it fits the venue, the conditional-on-computation honesty, the machine-verified assembly, the AI disclosure already in the paper).\n- 3–5 **suggested referees** (I can propose criteria/names to research — people in explicit-computation NT: e.g. the Platt/Trudgian circle, Voros, formalization-adjacent number theorists).\n- Statements: funding (none/self-funded), conflicts of interest (none), **data/code availability** (your public repo URL — item 2 above), ORCID.\n- The AI Contribution Statement is already in the paper — most publishers (T&F, AMS, Springer) now require exactly this and prohibit AI authorship; you're compliant by construction.\n\n**What a referee will push on** (be ready): precise Platt–Trudgian dependency (cited correctly now); the Misguich–Voros overlap (now correctly cited to Exp. Math.); M₀'s grid-verified status (E-023b removes this if you want); the novelty claim \"first assembled explicit chain\"; and the SfBoundProp perimeter — which the paper already declares as its honest formal target.\n\n## 5. Recommended order of operations\n\n1. **You**: read-through of paperA.pdf; register ORCID; start the **arXiv endorsement request** (longest lead time).\n2. **Me** (say the word): repo publication prep (README, Lean build instructions, license file), optional figure + E-023b, cover-letter draft, referee-suggestion list.\n3. **You**: flip the repo public, submit to arXiv.\n4. After arXiv posts: journal submission to *Experimental Mathematics* (first choice).\n\n## 6. What only you can do\n\nAccount creation, endorsement requests, ORCID, the actual submission clicks, signing the cover letter, and any author warranties (originality, etc.). Everything else — repo prep, cover letter draft, referee list, figure, E-023b, final formatting to a journal's house style — I can do here.\n\nWant me to start on the repo-publication prep + cover letter + referee list now?"}]