← Session 22 — ii′-1: liCoeff pairing fix + residue machinery
thinking (345 chars)
Session 018 complete. Summarize for the user. Two sub-stages done today (ii′-1b(iii) in session 017, ii′-2 in session 018). Next is ii′-3, the long pole. Per the pacing rules I should note the natural pause point. I don't know the current time — the break prompt rule says especially approaching 5 PM. Let me just report and let the user decide.
**Session 018 complete — ii′-2 DONE** (the two elementary swaps).
## What was proved (LiSwaps.lean, ~340 lines, 12 declarations)
**R2(i) `liCoeff_eq_sum_sigma`** — the zero-side swap:
```
liCoeff n = Σ_{j=1}^n (−1)^{j+1} C(n,j)·σ_j
```
- `sigmaP j` = paired power sums over the zeros, each slice summable (`sigmaSlice_summable`, cloning the ii′-1a skeleton): j = 1 via the paired exactness Re(1/ρ) = Re(ρ)/|ρ|² with 0 < Re ρ < 1; j ≥ 2 by |ρ|^{−j} ≤ |ρ|^{−2} for ‖ρ‖ ≥ 2; radius-2 ball finite by compactness
- Swap via `Summable.tsum_finsetSum` + the CommRing-polymorphic binomial expansion `one_sub_one_sub_pow`
**R2(ii) `sInfty_eq_sum`** — the archimedean swap (n ≥ 1):
```
SInfty n = Σ_{j=1}^n (−1)^j C(n,j)·lagariasA j
```
- `lagariasA j` = a₁ for j = 1, else 1 + odd≥3 tsum (the m = 1 term peeled by definition — no tsum-omit lemma needed)
- `sInfty_summand_eq`: the j = 1 term cancels +n/m exactly (D-037 §3); `oddSlice_summable` by p-series domination; the alternating identity Σ_{j=2}^n (−1)^jC(n,j) = n−1
## Verification
- Full `lake build` GREEN (8746 jobs); axiom audit: **3 standard axioms only** on all 12 declarations
- Commits 291e30e (work) + 29c7dfd (closure): journal-018, STATE, NGUYEN checklist, db
## Phase 5B map
ii′-0 ✅ → 1a ✅ → 1b ✅ → 2 ✅ → **3 (next — the long pole, 2–4 sessions)** → 4 → 5 → 6 → 7
Next session: **ii′-3** — Lagarias (4.10), the analytic heart of the crux. First task is a design note (D-066): read Zeta23's proved explicit formula `EF_lit_zeta` and the WeilEF/Contour machinery to decide route β2 (EF-reuse) vs β1 (Hadamard). Sanity gate: k = 1 must give σ₁ = 1 + γ/2 − ½log 4π.
This is a clean sub-stage boundary — good place to pause if you'd like, or say the word and I'll start the ii′-3 design investigation.
raw content_json (database row)
[{"type":"thinking","thinking":"Session 018 complete. Summarize for the user. Two sub-stages done today (ii′-1b(iii) in session 017, ii′-2 in session 018). Next is ii′-3, the long pole. Per the pacing rules I should note the natural pause point. I don't know the current time — the break prompt rule says especially approaching 5 PM. Let me just report and let the user decide.","signature":""},{"type":"text","text":"**Session 018 complete — ii′-2 DONE** (the two elementary swaps).\n\n## What was proved (LiSwaps.lean, ~340 lines, 12 declarations)\n\n**R2(i) `liCoeff_eq_sum_sigma`** — the zero-side swap:\n```\nliCoeff n = Σ_{j=1}^n (−1)^{j+1} C(n,j)·σ_j\n```\n- `sigmaP j` = paired power sums over the zeros, each slice summable (`sigmaSlice_summable`, cloning the ii′-1a skeleton): j = 1 via the paired exactness Re(1/ρ) = Re(ρ)/|ρ|² with 0 < Re ρ < 1; j ≥ 2 by |ρ|^{−j} ≤ |ρ|^{−2} for ‖ρ‖ ≥ 2; radius-2 ball finite by compactness\n- Swap via `Summable.tsum_finsetSum` + the CommRing-polymorphic binomial expansion `one_sub_one_sub_pow`\n\n**R2(ii) `sInfty_eq_sum`** — the archimedean swap (n ≥ 1):\n```\nSInfty n = Σ_{j=1}^n (−1)^j C(n,j)·lagariasA j\n```\n- `lagariasA j` = a₁ for j = 1, else 1 + odd≥3 tsum (the m = 1 term peeled by definition — no tsum-omit lemma needed)\n- `sInfty_summand_eq`: the j = 1 term cancels +n/m exactly (D-037 §3); `oddSlice_summable` by p-series domination; the alternating identity Σ_{j=2}^n (−1)^jC(n,j) = n−1\n\n## Verification\n- Full `lake build` GREEN (8746 jobs); axiom audit: **3 standard axioms only** on all 12 declarations\n- Commits 291e30e (work) + 29c7dfd (closure): journal-018, STATE, NGUYEN checklist, db\n\n## Phase 5B map\nii′-0 ✅ → 1a ✅ → 1b ✅ → 2 ✅ → **3 (next — the long pole, 2–4 sessions)** → 4 → 5 → 6 → 7\n\nNext session: **ii′-3** — Lagarias (4.10), the analytic heart of the crux. First task is a design note (D-066): read Zeta23's proved explicit formula `EF_lit_zeta` and the WeilEF/Contour machinery to decide route β2 (EF-reuse) vs β1 (Hadamard). Sanity gate: k = 1 must give σ₁ = 1 + γ/2 − ½log 4π.\n\nThis is a clean sub-stage boundary — good place to pause if you'd like, or say the word and I'll start the ii′-3 design investigation."}]