Before we finish Paper A, let's look at these minor suggestions. Let me know if this is doable. 1. One small internal note worth a line somewhere The pre-verified discharge plan (D-062 §5, dps 40) promised >9,960; the Lean-certified bound is ≥8,001. Both are comfortably positive and the gap is exactly what you'd expect — Lean's rational interval arithmetic rounds more coarsely than mpmath at dps 40 — but since the archive contains both numbers, a one-line note ("certified bound coarser than the dps-40 plan; both suffice") preempts the same class of question the margin trail just answered. Minor, but this project's brand is that no two numbers ever disagree without a filed explanation. 2. What remains unchanged — my standing items - Theorem 3 still carries "modulo standard tempered-FT bookkeeping" and the o(eᵃ) inside its statement. Part 1 fixed this exact disease twice (B(n)'s o(1), the margin trail); Part 2 should take the same medicine or demote to Proposition. - L3/L4 remain open — but the split is now stated with real precision in §3.2 ("this direction is proved... the converse... is tagged a proof skeleton"). Honest as-is. - The papers are still combined. My split recommendation stands: §3.1 + Appendices A.1/B is now a complete, self-contained, genuinely novel artifact — the first explicit finite-height Li theorem with a machine-verified assembly — and it should not share referee fate with a section whose headline theorem contains an untraced qualifier. - Authorship will still hit journal policy walls regardless of the mathematics.