Session 029 — 2026-08-23 — ii′-5e-iv COMPLETE: F entire (LiFEntire.lean)

Directive

Continue the route per STATE.md: ii′-5e-iv (D-068 §4) — F entire by principal-part splits. User: "let's work on the remaining route."

Outcome: 5e-iv COMPLETE (commits 58e03e2 + closure; LiFEntire.lean,

~1130 lines, 30 decls, all audited clean: 3 standard axioms only; full build GREEN 8766 jobs, LiFEntire root-imported)

The difference function Fexpr s := logDeriv ζ s − seriesFun s + 1/s + 1/(s−1) − (log π)/2 + ψ(s/2)/2 extends to an ENTIRE function. Since Mathlib lacks a general removable-singularity theorem AND the pointwise values of Fexpr at the excluded points are junk (0/0-forms), the extension is packaged as the punctured-limit function Gentire s := limUnder (𝓝[≠] s) Fexpr:

• good points (¬badPoint s, where badPoint = nontrivial ∨ 0 ∨ 1 ∨ −2n): Fexpr analytic there (Fexpr_analyticAt_of_not_bad) ⟹ continuous ⟹ the punctured limit is the value (gentire_eq_Fexpr, via tendsto_nhds_limUnder + tendsto_nhds_unique); and a whole ball of good points exists (exists_ball_good_of_not_bad: the ζ ≠ 0 continuity ball ∩ {0,1}-avoidance) ⟹ Gentire =ᶠ Fexpr there ⟹ analytic.
• bad points: an explicit analytic witness W per case with punctured agreement Fexpr =ᶠ[𝓝[≠] s] W; the limUnder uniqueness gives Gentire s = W s, and a small ball is bad-point-free off the center ⟹ Gentire =ᶠ[𝓝 s] W (full nhd) ⟹ analytic at s.

The four witness cases (D-068 §0's residue bookkeeping verified at each):

• nontrivial ρ₀ (Fexpr_eventually_nontrivial): the NF witness logDeriv_zeta_sub_mult_div_eventually (the LiSides NF block: logDeriv ζ − m/(s−ρ₀) =ᶠ logDeriv h punctured, h the order normal form factor) + 5e-iii's seriesFun_sub_polar_analyticAt; the elementary terms analytic since re ρ₀ ∈ (0, 1).
• s = 1 (Fexpr_eventually_one): logDeriv ζ = logDeriv zetaA − 1/(s−1) punctured (zetaA = (s−1)ζ analytic, zetaA 1 = 1 — logDeriv_zeta_eq_logDeriv_zetaA_sub).
• s = 0 (Fexpr_eventually_zero): ψ(s/2)/2 + 1/s = −γ/2 + ½·digammaSeriesPart(s/2) punctured; the series part analytic on ball(0, 1/2) by the M-test (digammaSeriesPart_analyticOn, majorant 1/(j+1)²); logDeriv ζ analytic at 0 (ζ(0) = −1/2).
• s = −2n (Fexpr_eventually_neg_two_mul): logDeriv ζ − 1/(s+2n) analytic (NF + zeroMult_neg_two_mul via the new riemannZeta_neg_two_mul); ψ(s/2)/2 + 1/(s+2n) = ½·H_n(s/2) punctured where H_n = the digamma series with the j = n−1 term dropped (digammaSeriesPartSub, analytic on ball(−n, 1/2) by the eventually M-test, majorant (2n+1)/(j+1)² for j ≥ 2n+1; digammaSeriesPart_eq_sub_add_single the tsum split).

Supporting infrastructure:

• analyticAt_digamma: ψ analytic off {0} ∪ −ℕ (finite-min avoiding ball; Γ differentiable + nonzero there; DifferentiableOn → analyticOnNhd → the deriv/div form of logDeriv Γ).
• zeta_zero_classification: every zero of ζ is nontrivial, 0, or −2n (re ≥ 1 by Mathlib's one_le_re nonvanishing; re ≤ 0 by Gammaℝ_eq_zero_iff + Zeta23's completedRiemannZeta_eq_zero_iff — the LiDisc argument globalized).

Capstone gentire_analyticAt_and_eq: (∀ s, AnalyticAt ℂ Gentire s) ∧ (∀ s ∉ bad set, Gentire s = Fexpr s) — exactly the input 5e-v needs (circle bound on the γ-gap circles — all good points — then the max-modulus squeeze ⟹ Gentire ≡ const =: B).

Banked gotchas (session 029 additions)

• AnalyticAt.comp HOU ambiguity: (analyticAt_digamma h).comp h1 with hg : AnalyticAt ℂ g (s/2) — the f x pattern unifies to the WRONG solution (f := HDiv.hDiv s, x := 2). Pin f: AnalyticAt.comp (f := fun s : ℂ => s / 2) hg h1. And the middle value must be normalized FIRST when it's a non-defeq arithmetic form ((−2↑n)/2 vs −↑n): build hg at the unreduced point via rw [show −2↑n/2 = −↑n by ring] inside the have, then comp.
• AnalyticAt.div with ascribed hg0: apply AnalyticAt.div analyticAt_const _ (h : 0 − 1 ≠ 0) mis-unifies g (HOU on g x = 0−1). Pin g: (g := fun s : ℂ => s − 1).
• Pi-form defeq is reliable for exact ((f − g) x ≡ f x − g x via Pi.sub_apply etc.) but NOT for rw-pattern matching and NOT for apply conclusions involving HOU — the apply-form apply AnalyticAt.div f g h on a lambda goal works, the raw term f.div g h ascription to a lambda type mostly works.
• Complex.norm_ofReal does NOT exist — it's RCLike.norm_ofReal (∀-form; fine in rw). RCLike.norm_natCast, RCLike.norm_ofNat same ∀-form class. Complex.norm_intCast exists (→ ℤ-norm; chain Int.norm_eq_abs).
• Cast-leaf elaboration: ((k + (n:ℤ)) : ℂ) elaborates with the coercion pushed to the LEAVES (↑k + ↑↑n), not a single outer cast — the expected type propagates through +. To force one outer cast pin the inner type: (((k + (n:ℤ)) : ℤ) : ℂ). Same for show (k:ℂ) + ((n:ℤ):ℂ) = (((k:ℝ)+(n:ℝ)):ℂ)-style rewrites — the LHS must match the goal's atom EXACTLY (elaborated forms differ by coercion insertion points). The ROBUST alternative for ‖cast-expr‖ bounds: Complex.abs_re_le_norm + a simp-computed re (Complex.add_re/sub_re/mul_re + natCast_re/ofNat_re) — no norm-of-cast matching needed.
• ContinuousAt.eventually_ne (hg2 : g x ≠ y) has {y} implicit — pin the result type by ascription (have hz0 : ∀ᶠ w in 𝓝 0, ζ w ≠ 0 := ...) or the by-block's norm_num sees a metavariable.
• EventuallyEq vs raw ∀ᶠ: Tendsto.congr'/AnalyticAt.congr want the EventuallyEq wrapper; a raw ∀ᶠ y in l, f y = g y hypothesis is defeq but dot-notation (.symm) fails — bridge with have h' : f =ᶠ[l] g := h. And rw [Metric.eventually_nhds_iff_ball] does NOT see through the =ᶠ wrapper — show ∀ᶠ ... first.
• subst hye with hye : y = s eliminated s (the outer lemma variable!) when both are locals — use rw [hye] on the goal instead (or name the target: subst y).
• nhdsNE_neBot is an @[instance] (NormedField namespace) — 𝓝[≠] s in ℂ is NeBot automatically; no haveI needed.
• simp only [if_pos h]/if_neg rewrites under binders (rw can't); simp at hd on ‖(1:ℂ) − 0‖ < 1/2 needs the explicit norm_one chain — prefer rw [show ‖(1:ℂ)−0‖ = 1 by simp] at hd; linarith.
• file-end convention: end NguyenRH1 then end (noncomputable section wraps the namespace) — confirmed again.

Status / next

ii′-5e-iv COMPLETE. Next: ii′-5e-v (D-068 §5): the circle bound |Gentire| ≤ C(log R_k)³ on 5e-i's γ-gap circles |s| = R_k (inputs: 5c's ‖ζ′/ζ − near‖ ≤ 100000(log|t|)² on σ ∈ [1/2, 7/2], 5d's left version ≤ 200000(log|t|)², the Dirichlet bound for re ≥ 2 (Zeta23 LSeries vonMangoldt), 5e-ii's digamma bounds, 5e-i's circle gaps for the series radial split (log R)³/c) + the difference-quotient max-modulus squeeze ⟹ Gentire ≡ Gentire 0 =: B ⟹ the capstone ∃ B identity. Then ii′-5f (D-056's tight analysis → 10.5/48) → ii′-3b → ii′-3c → ii′-6 → ii′-7.