Session 021 — 2026-08-22 — ii′-4 COMPLETE (L3 + L1 + zeroMult(−2) = 1)

Directive

Work tier ii′ sub-stage ii′-4 (STATE.md NEXT ACTION): L3 zero-avoiding T (pigeonhole on the perimeter unit-window count bound) + L1 kernel bounds, including the trivial-zero residue input zeroMult(−2) = 1 deferred from ii′-1b(iii). All in the new file NguyenRH1/LiContour.lean (freeze protocol: new files + root import only). Three commits: 90ae688 (4a), 33bc5b2 (4b), 5845f6f (4c).

Pre-work (website, non-research — logged in RH-WEBSITE.md §7)

Two website bug fixes at user request (web/ only, research archive untouched): (1) /dashboard/ 500 — git_log subprocess decoded git's UTF-8 commit output as cp1252; the reader thread died on Unicode commit messages and stdout came back None (fixed: encoding="utf-8", errors="replace" + None guard). (2) Roadmap Phase 2/5B checklists rendered as paragraph text — those phases have a note paragraph directly above the list and python-markdown never lets a list interrupt a paragraph (fixed: research_data._restore_interrupted_lists inserts the missing blank line; skips indented continuations and fenced code; archive text still rendered verbatim).

ii′-4a — L3 (exists_zero_avoiding_T)

Design decisions:

• Perimeter hypothesis ZeroCountProp: ∀ t ≥ 2, the number of nontrivial zeros with ordinates in [t, t+1] is ≤ Ĉ₀(t+1) (Nat.card of zeroWindow t; finiteness via Zeta23 zerosIn_finite subset argument; Ĉ₀ = LiSkeleton's C0hat, D-056 §2). This is the Trudgian N(T)/S(T) input in the exact form the assembly consumes.
• Pigeonhole exists_avoiding_midpoint: pure combinatorics — with card S ≤ k, one of the k+1 midpoints a + (2j+1)/(2(k+1)) is ≥ 1/(2(k+1)) from every point of S. Proof via the injective-badness argument (each point kills ≤ 1 midpoint since adjacent midpoints are 1/(k+1) apart; Bad ≤ card S ≤ k < k+1 ⟹ a survivor). Cleaner than the sorted-gap argument (no sorting needed).
• Clearance downgrade 1/(2(k+1)) → 1/(3·Ĉ₀(a+1)) uses Ĉ₀ ≥ 2 (two_le_C0hat: log(t+2) ≥ 1 for t ≥ 1 since t+2 ≥ 3 > e).

ii′-4b — L1 (kernel bounds)

• norm_div_sub_one_le_one: ‖s/(s−1)‖ ≤ 1 ⟺ re s ≤ 1/2 (normSq expansion) ⟹ kFun_norm_le_two.
• Core lemma norm_one_add_one_div_le: ‖1+1/s‖ ≤ 1 + (σ+1)/normSq s via the exact square ‖1+1/s‖² = 1 + (2σ+1)/D ≤ (1+(σ+1)/D)² (needs D + σ + 1 = (σ+½)² + T² + 3/4 > 0).
• kFun_shift_norm_le_exp_four_add_one (horizontals: re s ≤ 3, n ≤ (im s)² ⟹ ≤ (1+4/n)ⁿ ≤ e⁴); kFun_shift_norm_le_exp_sqrt_half_add_one (right vertical: 2√n ≤ re s ⟹ ≤ (1+1/(2√n))ⁿ ≤ e^{√n/2}); both via Real.add_one_le_exp + exp_nat_mul.
• kFun_neg_two + norm_kFun_neg_two_le_one: kFun n (−2) = (2/3)ⁿ − 1, norm ≤ 1 (the trivial-zero contribution).

ii′-4c — zeroMult(−2) = 1 (trivial-zero simplicity)

Route per D-066 §6 / STATE.md: the local factorization ζ(s) = (s+2)·G(s) near −2 with G(s) = Λ(s)/Hfun(s):

• Hfun s = 4·π^{−s/2}·Γ(s/2+2)/s — equals (s+2)·ΓR(s) off {−2,0} (Hfun_eq: Gamma_add_one twice, Γ(s/2) = Γ(s/2+2)/((s/2)(s/2+1))); analytic at −2 (Γ(s/2+2) differentiable on ball(−2,1) since s/2+2 ∈ ball(1, 1/2) avoids the poles {0,−1,…}; the cpow piece via the exp(log π·(−s/2)) bridge); value Hfun_neg_two: Hfun(−2) = −2π ≠ 0.
• Λ(−2) ≠ 0: FE completedRiemannZeta_one_sub to Λ(3) = ΓR(3)·ζ(3) (Zeta23 RvM.completedRiemannZeta_eq_Gammaℝ_mul) with ΓR(3) ≠ 0 (Gammaℝ_eq_zero_iff — note: in Mathlib's junk-value convention ΓR vanishes exactly at {−2n}, so 3 ∉ {−2n} by re-part) and ζ(3) ≠ 0 (riemannZeta_ne_zero_of_one_lt_re).
• The eventuallyEq ζ = (s+2)^1 • G on 𝓝(−2): pointwise on the punctured ball (Λ = ΓR·ζ off {−2n} ∋ the ball; divide by ΓR, multiply by (s+2), use Hfun_eq) + both-sides-zero at −2 (ζ(−2) = 0 by riemannZeta_neg_two_mul_nat_add_one 0).
• AnalyticAt.analyticOrderAt_eq_natCast ⟹ analyticOrderAt = 1; zeroMult = its .toNat (ENat.toNat_one).

Axiom audit + build

Full lake build GREEN (8751 jobs). PrintAxioms sweep of all 17 new theorems: 3 standard axioms only (propext, Classical.choice, Quot.sound), no sorryAx anywhere in the Li chain.

Lean gotchas banked this session (additions to journal-011/019/020 lists)

• have h : AnalyticAt ℂ (fun s => ...) (-2) — the bare fun s => binder in a type ascription DEFAULTS TO ℕ (Neg ℕ / NormedAddCommGroup ℕ synth errors). Always annotate (fun s : ℂ => ...).
• DifferentiableOn ... intro s hs gives DifferentiableWithinAt goals — finish with .differentiableWithinAt.
• rw of an iff under ≠ needs ne_eq first (Ne is not syntactic ¬Eq).
• AnalyticAt.congr (hf : AnalyticAt f x) (h : f =ᶠ[𝓝 x] g) : AnalyticAt g x — direction matters; for .symm use EventuallyEq.symm h (dot notation on the ∀ᶠ form fails with invalidField).
• A dot-projection on the next line after a parenthesized term parses as function application — keep .differentiableWithinAt attached to the closing paren's expression.
• div_eq_div_iff takes ≠ 0 arguments (not positivity).
• Renames hit: pow_le_pow_left → pow_le_pow_left₀; div_le_div_right → div_le_div_iff_of_pos_right; div_le_div_left → div_le_div_iff_of_pos_left.
• mul_div_cancel_left₀ (b) {a} (ha : a ≠ 0) : a * b / a = b — the EXPLICIT argument is the numerator factor; the denominator is implicit.
• Nat.card_coe_set_eq is root-namespace (not Set.Nat.); Set.ncard_eq_toFinset_card _ hfin links ncard to Finite.toFinset.card.
• field_simp needs the side conditions in the EXACT normal form it generates (s + 2 ≠ 0, not s ≠ −2): derive via add_eq_zero_iff_eq_neg.
• Zeta23's product form Λ = ΓR·ζ is RvM.completedRiemannZeta_eq_Gammaℝ_mul (module Zeta23.RvM.CountByIntegral, namespace Zeta23.RvM).

Status

ii′-4 COMPLETE in one session (D-064 estimate: 1 sess ✓). Next: ii′-5 — the R-bound (D-056, A = 10.5, B₀ = 48) via the local route (Borel–Carathéodory + Jensen + Blaschke/StrongPNTPrefix + FE strip bound via riemannZeta_one_sub + Stirling; digamma Lemma D). Estimated 2–3 sessions — the long pole of the remaining ii′ map.