Session 020 — 2026-08-21 — ii′-3a COMPLETE (pieces A + B both done)

Directive

Continue tier ii′ per D-066: ii′-3a piece (A) — the archimedean τ-evaluation (STATE.md NEXT ACTION).

Work done

ii′-3a piece (A) COMPLETE — the full archimedean coefficient evaluation, capstone iteratedDeriv_logDeriv_Gammaℝ (commits 0b4133e, c4cff18, c15ab75, d119b70, 8e04c98, 8bd8c9b, e480e77, b7ff872):

for all j ≥ 0: iteratedDeriv j (fun s => logDeriv Gammaℝ (1+s)) 0 = (−1)^{j+1}·j!·↑lagariasA(j+1).

The chain, all in two new files:

• LiArchimedean.lean (part 1): logDeriv_Gammaℝ_one_add (the split logDeriv Gammaℝ (1+s) = −(log π)/2 + (1/2)·digamma((1+s)/2) via Gammaℝ_def + logDeriv_mul + the cpow-as-exp bridge) and logDeriv_Gammaℝ_one (τ₀ = −a₁ via Mathlib's Complex.digamma_one_half).
• LiDigamma.lean (~960 lines): the digamma partial-fraction series — NOT in Mathlib — built from BohrMollerup's logGammaSeq:
• real side: psiReal_eq_DinfR — Γ'(x)/Γ(x) = −γ − 1/x + Σ_{m≥1} (1/m − 1/(x+m)) for x > 0, via hasDerivAt_of_tendstoLocallyUniformlyOn with the M-test on compacts (tendstoUniformlyOn_tsum_nat) and Real.tendsto_harmonic_sub_log;
• complex side: DinfC summable + analytic on the ball dpsiDomain (Weierstrass TendstoLocallyUniformlyOn.differentiableOn);
• identity principle digamma_eq_DinfC_on (eqOn_of_preconnected_of_frequently_eq through the real segment);
• the polygamma values iteratedDeriv_digamma_half via iteratedDerivWithin_tsum (termwise iterated derivation — this lemma carried most of the weight) + the bespoke inverse-power iterated derivative iteratedDeriv_neg_zpow_neg_one_add;
• the odd-m reindexing tsum_two_mul_add_one_inv_pow (bespoke equiv oddGeThreeEquiv : ℕ ≃ {m // Odd m ∧ 3 ≤ m} + Equiv.tsum_eq) and the 2^{j+1} scaling tsum_half_add_nat_zpow;
• the affine comp iteratedDeriv_one_add_div_two (induction with generalized point + AnalyticAt.iteratedDeriv-aux).

TWO elaboration gotchas (important for future sessions)

1. Bare π is NOT valid with the LiDigamma/LiArchimedean opens — it auto-binds as a spurious implicit variable (silent!). Always Real.pi.
2. Bare ↑(...) with no expected ℂ type gets its coercion DROPPED (the elaborator defaults the coe target to the source type when unconstrained) — e.g. fun y : ℝ => ↑(g y) elaborates to ℝ → ℝ! Always ascribe (↑(...) : ℂ) when the context doesn't force ℂ. Also: AnalyticAt.comp/ContinuousAt.comp mis-decompose a beta-reduced point (1+0)/2 as HDiv.hDiv (1+0) applied to 2 — use the _of_eq variants (AnalyticAt.comp_of_eq, ContinuousAt.comp_of_eq) with the point equality as a separate hypothesis.

Build + audit

Full lake build GREEN (8749 jobs — the whole package incl. LiDigamma, LiArchimedean now in the root closure). Axiom audit of 18 key declarations: 3 standard axioms only.

State at stop

ii′-3a (pieces A + B) FULLY COMPLETE. The (4.10)-a-form factorization now has: (A) archimedean coefficients ✓ (this session), (B) ζ-piece ✓ (session 019, LiZetaCoeff), and (M) the moment identities remain — queued after ii′-4 (L3+L1) and ii′-5 (R-bound), per the D-066 resequencing. Next: ii′-4 — L3 zero-avoiding T (pigeonhole on the perimeter C₀/FAlt) + L1 kernel bounds (|k_n| ≤ 2, e⁴+1, e^{√n/2}+1; the trivial residue value) — elementary, ~1 session.