Session 018 — 2026-08-21 — Tier ii′ sub-stage ii′-2 COMPLETE (elementary swaps)

Directive

Continue tier ii′ per D-064: sub-stage ii′-2 — R2(i)/(ii) elementary swaps (STATE.md NEXT ACTION).

Work done

ii′-2 COMPLETE (commit 291e30e) — LiSwaps.lean (~340 lines, 12 new declarations; single-file check clean; full lake build GREEN 8746 jobs; axiom audit: 3 standard axioms only on all 12):

• §0 shared helpers: sum_Icc_one_eq_sum_range, sum_Icc_two_eq_sum_range (bespoke Icc→range conversions via Finset.sum_bij, same pattern as ResW1_eq_sum's reindexing), sum_Icc_one_eq_add_sum_Icc_two (peel j=1), and one_sub_one_sub_pow — the CommRing-polymorphic binomial expansion 1 − (1−x)ⁿ = Σ_{j=1}^n (−1)^{j+1}C(n,j)x^j (add_pow + sum_range_succ' + neg_pow; used at both ℂ (i) and ℝ (ii)).
• R2(i) liCoeff_eq_sum_sigma: liCoeff n = Σ_{j=1}^n (−1)^{j+1}C(n,j)·σ_j with σ_j := ∑' ρ, (mult/2)((1/ρ)^j + (1/ρ̄)^j) (sigmaP, paired).
• sigmaSlice_summable (j ≥ 1): clones the ii′-1a skeleton (radius-2 ball + WeilEF.zero_sum_inv_sq + finite-ball compactness) with bound sigmaSlice_norm_le: j = 1 by the paired exactness (mult/2)(1/ρ + 1/ρ̄) = mult·Re(1/ρ) = mult·Re(ρ)/|ρ|² (add_conj + Complex.inv_re) with 0 < Re ρ < 1; j ≥ 2 by |ρ|^{−j} ≤ |ρ|^{−2} (‖ρ‖ ≥ 2); then mult/‖ρ‖² ≤ (9/4)mult/(1+‖γ‖²) (normSq_gammaOf_le_mul_norm_sq at n = 1).
• The swap: liSummand_eq_sum_slices (per-ρ binomial expansion, the two conjugate terms share coefficients) + Summable.tsum_finsetSum + tsum_mul_left.
• R2(ii) sInfty_eq_sum (n ≥ 1): SInfty n = Σ_{j=1}^n (−1)^j C(n,j)·a_j with lagariasA j := lagariasA1 (j = 1) | 1 + odd≥3 tsum (j ≥ 2) — the m = 1 term peeled by DEFINITION (no tsum-omit lemma needed).
• sInfty_summand_eq: h⁺(m) = (1−1/m)ⁿ − 1 + n/m = Σ_{j=2}^n (−1)^jC(n,j)(1/m)^j — the j = 1 term cancels +n/m EXACTLY (D-037 §3).
• oddSlice_summable (j ≥ 2): Real.summable_one_div_nat_pow restricted to the odd≥3 subtype (Summable.subtype) + one_div comparison.
• sum_Icc_two_neg_one_choose: Σ_{j=2}^n (−1)^jC(n,j) = n − 1 (n ≥ 1) via (1+(−1))ⁿ = 0 and two peels.
• Assembly: tsum_finsetSum swap + the two algebra identities close by ring.

Both identities check out against the session-014 numeric verification (D-064 §3: the crux bookkeeping S_∞ + 1 − λ_n = Res₁ was verified to 2e-21 at n = 2, 3).

Lean notes (hard-won this session, additions to the handoff list)

• Summable.tsum_finsetSum (hf : ∀ i ∈ s, Summable (f i)) — the finite-sum/tsum commute (NOT "tsum_sum" — that name does not exist).
• Summable.subtype (hf) (p : β → Prop) — restriction to {x // p x}.
• Summable.of_nonneg_of_le — args (0 ≤ g) (g ≤ f) (Summable f) : Summable g (lives in .../InfiniteSum/ENNReal.lean despite being about ℝ).
• Real.summable_one_div_nat_pow : Summable (fun n => 1/(n:ℝ)^p) ↔ 1 < p (Real-namespaced).
• Complex.norm_real : ‖(r : ℂ)‖ = ‖r‖ (ℝ-norm RHS; follow with Real.norm_eq_abs). RCLike.norm_ofReal does NOT match the ↑-cast here.
• starRingEnd_apply : starRingEnd ℂ z = star z (NOT conj z) — for Complex.add_conj (pattern z + conj z) bridge via a have ascription (z + starRingEnd ℂ z defeq z + conj z).
• div_le_div_iff_of_pos_right (hc : 0 < c) : a/c ≤ b/c ↔ a ≤ b (GroupWithZero/Basic); div_le_div_right does NOT exist.
• abs_div then abs_of_nonneg for denominators known ≥ 0.
• k+1+1 = k+2 holds by rfl in ℕ (literal recursion); use it to normalize sum_range_succ' double-peels.
• field_simp sometimes closes the cleared goal (trailing ring then errors "no goals" — remove on recompile).

State at stop

ii′-2 COMPLETE. Next: ii′-3 — R2(iii) Lagarias (4.10), the LONG POLE: in a-form, c_{k−1} = (−1)^k(a_k + σ_k) + (−1)^{k−1} for k ≥ 1 (derived in journal handoff from D-064's τ_j = c_j + (−1)^jσ_{j+1} − (−1)^j with τ_{j−1} = (−1)^j a_j). Route β2 first: reuse Zeta23's proved explicit formula (EF_lit_zeta, axiom-clean) — σ_j as moments of the zero measure; (4.10) is a moment identity. Fallback β1: Hadamard product of ξ. Sanity gate: k = 1 gives σ₁ = 1 + γ/2 − ½log 4π (Davenport value, verified 15 digits session 014). Investigation of EF_lit_zeta's exact statement is the first task.