← Session 36 — ii′-6-DL dog-leg + side bounds; Paper A review
**ii′-6 + ii′-7 COMPLETE.** Session closed at a clean boundary, everything committed (master @ `77ff068`).
## The final state
**The finite-height Li theorem is fully machine-proved.** `lambda_pos_finite_height_closed` (LiClosed.lean): λ_n > 0 for all 1 ≤ n ≤ N₁ = (3×10¹²−1)² ≈ 9×10²⁴, from exactly **eight** declared hypotheses — the two computational certificates (RHUpTo, LiVerifiedUpTo) plus six analytic perimeter Props (Trudgian N(T)/S(T) ×3, NoLowZeros, MZeroProp). The original N₁ is preserved via the D-074 dog-leg. Axiom audit on the full chain: 3 standard axioms only, 0 sorryAx (29 decls).
**This session's eight commits:**
1. `6e5a98f` — 6-c-ii (I_III left vertical)
2. `9bd8ba9` — 6-c-iii (I_I right vertical, F-E kernel)
3. `1fed1df` — 6-c-iv (mid-horizontal arcsinh-FTC machine, from scratch)
4. `5d3dc0a` — 6-c-v (horizontal assembly)
5. `774fec5` — **6-d: `sfBoundProp : SfBoundProp` PROVED** (six perimeter hyps)
6. `a0943a6` — ii′-7a+7b (closed theorem + full axiom audit)
7. `b64a839` — ii′-7c (Paper A closed, 9 pp clean: eight-hypotheses headline, corrected B(n) + the F-A/F-B/F-D/F-E correction-note footnote, Appendix B rewritten)
8. `77ff068` — ii′-7d (archive: D-037 erratum block, R-004 status, NGUYEN.md Phase 5B ✅, STATE.md rewritten, journal-041, db registration)
**Notes:**
- The bridge needed a variant at T ≤ 3·10¹² — the public T ≤ 3·10¹²−1 hypothesis provably fails at the top of the range (n = N₁ has √n = 3·10¹²−1 exactly). Caught and handled honestly.
- The pinch (NI + 5.5R ≤ 7·Ĥ) discharged by a fully elementary log-mono chain — no certified log numerics.
- Your Lagarias F-D correspondence files remain uncommitted (your work-in-progress).
- paperA.pdf is now versioned (submission-ready artifact, 9 pp).
**Next per STATE.md:** your read-through of paperA.pdf + the submission decision (cover letter + referee list from session 013, target *Experimental Mathematics*). Research-wise the open threads are Paper B Task 1 (R-003 bookkeeping) and the parked Track-B remainders — your call.
raw content_json (database row)
[{"type":"text","text":"**ii′-6 + ii′-7 COMPLETE.** Session closed at a clean boundary, everything committed (master @ `77ff068`).\n\n## The final state\n\n**The finite-height Li theorem is fully machine-proved.** `lambda_pos_finite_height_closed` (LiClosed.lean): λ_n > 0 for all 1 ≤ n ≤ N₁ = (3×10¹²−1)² ≈ 9×10²⁴, from exactly **eight** declared hypotheses — the two computational certificates (RHUpTo, LiVerifiedUpTo) plus six analytic perimeter Props (Trudgian N(T)/S(T) ×3, NoLowZeros, MZeroProp). The original N₁ is preserved via the D-074 dog-leg. Axiom audit on the full chain: 3 standard axioms only, 0 sorryAx (29 decls).\n\n**This session's eight commits:**\n1. `6e5a98f` — 6-c-ii (I_III left vertical)\n2. `9bd8ba9` — 6-c-iii (I_I right vertical, F-E kernel)\n3. `1fed1df` — 6-c-iv (mid-horizontal arcsinh-FTC machine, from scratch)\n4. `5d3dc0a` — 6-c-v (horizontal assembly)\n5. `774fec5` — **6-d: `sfBoundProp : SfBoundProp` PROVED** (six perimeter hyps)\n6. `a0943a6` — ii′-7a+7b (closed theorem + full axiom audit)\n7. `b64a839` — ii′-7c (Paper A closed, 9 pp clean: eight-hypotheses headline, corrected B(n) + the F-A/F-B/F-D/F-E correction-note footnote, Appendix B rewritten)\n8. `77ff068` — ii′-7d (archive: D-037 erratum block, R-004 status, NGUYEN.md Phase 5B ✅, STATE.md rewritten, journal-041, db registration)\n\n**Notes:**\n- The bridge needed a variant at T ≤ 3·10¹² — the public T ≤ 3·10¹²−1 hypothesis provably fails at the top of the range (n = N₁ has √n = 3·10¹²−1 exactly). Caught and handled honestly.\n- The pinch (NI + 5.5R ≤ 7·Ĥ) discharged by a fully elementary log-mono chain — no certified log numerics.\n- Your Lagarias F-D correspondence files remain uncommitted (your work-in-progress).\n- paperA.pdf is now versioned (submission-ready artifact, 9 pp).\n\n**Next per STATE.md:** your read-through of paperA.pdf + the submission decision (cover letter + referee list from session 013, target *Experimental Mathematics*). Research-wise the open threads are Paper B Task 1 (R-003 bookkeeping) and the parked Track-B remainders — your call."}]