Session 026 — 2026-08-22 — ii′-5e prep (zeroMult(−2n) = 1, ALL n) + D-068 (5e design)

Directive

Continue tier ii′-5 per STATE.md: session 026 first item — generalize ii′-4c's zeroMult_neg_two to all trivial zeros — then the ii′-5e design. User: "yes" (to the queued plan).

Outcome 1: zeroMult(−2n) = 1 for ALL n ≥ 1 — COMPLETE (commit 0d9887a)

New file NguyenRH1/LiTrivialZeros.lean (~290 lines, 8 decls, all axiom-audited: 3 standard axioms only, zero sorryAx), root-imported; full build GREEN (8762 jobs).

Build path:

1. gamma_mul_prod: the product-form Γ recurrence Γ(z)·∏_{j<n}(z+j) = Γ(z+n) for z avoiding {0,…,−(n−1)} — clean induction on Complex.Gamma_add_one (empty-product base, no side conditions at n = 0; the multiplied form avoids division side-conditions entirely).
2. The cofactor HfunT n s = 2·π^{−s/2}·Γ(s/2+n+1)/trivQ n s with trivQ n s = ∏_{j<n}(s/2+j): analytic at −2n (Γ(s/2+n+1) analytic via re(s/2+n+1) ∈ (1/2, 3/2) on the unit ball — away from the Gamma poles; trivQ a polynomial with trivQ(−2n) = ∏(−n+j) ≠ 0) and HfunT(−2n) = 2πⁿ·Γ(1)/trivQ(−2n) ≠ 0.
3. The punctured identity HfunT_eq: (s+2n)·ΓR(s) = HfunT n s on ball(−2n, 1) ∖ {−2n} — the recurrence side conditions (∀ k ≤ n, s/2 ≠ −k) from the ball geometry (s/2 = −k ⟹ s = −2k at distance 2|n−k| ≥ 2 from −2n unless k = n = the puncture).
4. zeroMult_neg_two_mul: ζ = (s+2n)·(Λ/HfunT n) near −2n with Λ(−2n) = Λ(1+2n) = ΓR(1+2n)·ζ(1+2n) ≠ 0 (FE + ΓR-ne-zero-of-re_pos + riemannZeta_ne_zero_of_one_lt_re) ⟹ analyticOrderAt = 1 via analyticOrderAt_eq_natCast (the ii′-4c pattern verbatim).

Outcome 2: D-068 — ii′-5e DESIGN COMPLETE

The partial-fraction identity assembly plan. TWO CORRECTIONS to the D-067 §6 sketch found by the pre-build survey:

• (C1) the circle series bound is O((log R)³), not O((log R)²) — the correct split is by the RADIAL distance ||s|−|ρ|| with the γ-gap needed only in the critical annulus [R±2] (the naive |s−ρ| ≥ 1 bound over the ≍ R log R annulus zeros gives O(R log R) — fatal; recorded with the fix).
• (C2) the near-axis left-plane digamma bound is a SEPARATE build (5d's bound needs 2 ≤ |im w| for the slit-plane FTC; the circle's near-real-axis left part has w = s/2 with |im w| possibly < 2): recurrence + separated reciprocal sum Σ 1/|w+j| ≤ C·log(m+1) (1-separated real parts + dist(w,−ℕ) ≥ 1/4 ⟹ ≤ 2 per unit bin) + ψ(w+m) via StirlingVert (|im| ≥ 1/2) or compactness (|im| < 1/2, re ∈ [1,2]). Also the right-half re ≥ 2 mild case via the Weierstrass series (Zeta23 DigammaSeries.digamma_series — exists). Sub-stage map 5e-i..v: (i) ×2-rescaled γ-gap circles R_k ∈ [4k+2.5, 4k+3] (the 5c ×10-trick verbatim; R/2 ∈ [2k+1.25, 2k+1.5] ⟹ dist ≥ 1/4 to ℤ automatically); (ii) the C2 digamma bound; (iii) the zero series (summability via the ii′-1a dominator + zero_sum_inv_sq; analytic off the zeros via locally-uniform limits; isolation at each zero); (iv) F entire by principal-part splits (NO removable-singularity theorem, NO Hadamard — at 1 via ii′-1b's zetaA logDeriv; at 0 and −2n via the digamma series splits + zeroMult_neg_two_mul); (v) circle bound O((log R)³) + max-modulus squeeze ⟹ F ≡ const (no Liouville needed). Capstone: ∃ B : ℂ, the identity for s off {zeros} ∪ {0,1} ∪ {−2n}. Plus the 5f preview (D-056's six-piece analysis; the perimeter ZeroCountProp's FIRST use in the R-chain).

Banked gotchas (session 026 additions)

• DifferentiableAt.analyticAt does NOT exist in this Mathlib — for a pointwise-analyticity goal use by fun_prop (AnalyticAt is fun_prop-enabled) or DifferentiableOn + analyticOnNhd on a ball.
• Gammaℝ_eq_zero_iff gives s = -(2 * ↑m) (negation OUTSIDE), not -2 * ↑m — match patterns accordingly.
• riemannZeta_neg_two_mul_nat_add_one (n) : ζ(−2·(↑n+1)) = 0 with the +1 in ℂ — for ζ(−2n), apply at n−1 and rewrite ↑(n−1)+1 = ↑n via ← Nat.cast_add_one + Nat.sub_add_cancel.
• lt_trichotomy exists (le_or_lt does NOT in this Mathlib).
• field_simp may close the goal entirely (again) — check before a trailing ring (second occurrence; journal-024 had the first).
• Finset.analyticAt_fun_prod : (∀ i ∈ s, AnalyticAt 𝕜 (f i) x) → AnalyticAt 𝕜 (fun x => ∏ i ∈ s, f i x) x.

Status / next

ii′-5e prep (5e-0) + design (D-068) COMPLETE. Next: ii′-5e-i (γ-gap circles via the ×2-rescaled midpoint pigeonhole), then 5e-ii (near-axis digamma bound), 5e-iii (series), 5e-iv (F entire), 5e-v (capstone). Then ii′-5f (tight analysis → 10.5/48, D-056), ii′-3b, ii′-3c, ii′-6, ii′-7.