Session 022 — 2026-08-22 — ii′-5a DESIGN (D-067) + ii′-5b COMPLETE (the |ζ| disc bound)

Directive

Work tier ii′ sub-stage ii′-5 (STATE.md NEXT ACTION): the R-bound (D-064 R3, D-056 A = 10.5/B₀ = 48) — the long pole of the remaining ii′ map. Session split into 5a (design) and 5b (the |ζ| polynomial bound), both complete. Commits: de6ab52 (5a design), ab2df3f (5b WIP1: B̃₂ + IBP identity), f607489 (5b complete: representation + disc bound).

ii′-5a — design D-067 (route b″)

Full machinery inventory against vendored Mathlib/Zeta23 (everything verified live — StrongPNTPrefix's BorelCaratheodoryDeriv/ LogOfAnalyticFunction/ZeroFactorization, ZetaBounds' Zeta0EqZeta/ ZetaUpperBnd, StirlingVert's digamma_stirling, RvM product forms). TWO major route decisions:

1. No complex Stirling for Γ needed. The naive route needs |Γ(a+ib)| ~ |b|^{a−1/2}e^{−π|b|/2} (vertical decay) for the FE-side |ζ| bound — a heavy build. ELIMINATED by (i) keeping the disc dip shallow (σ ≥ −1/2) and covering it with ONE extra Euler–Maclaurin level (B̃₂), and (ii) reaching the left strip σ ∈ [−5/2, 1/2] by FE-reflection of the R-bound itself: R(s) = −R(1−s) + digamma bracket — the zero sums cancel EXACTLY (1/(1−s−(1−ρ)) = −1/(s−ρ)).
2. No Hadamard. (already known — disc Blaschke removal instead). Also found: Zeta23's digamma_stirling (‖ψ(w) − log w + 1/(2w)‖ ≤ 3/w.im², re w > 0, |im| ≥ 1/2) SUBSUMES D-056's Lemma D — the digamma remainder never needs separate formalization. Geometry note: every disc covering the |γ−t|<1 zeros dips left of σ = 0 (√(c²+1) > c for any center c+it) — hence the B̃₂ level is unavoidable; chosen R = 5/2 about 2+it.

ii′-5b — LiRBound.lean COMPLETE (~640 lines, all green)

• b2Fun (the periodic Bernoulli primitive (u²−u)/2, u = Int.fract x): periodicity (fract_add_one), range [−1/8, 0], continuity for FREE via ContinuousOn.comp_fract'' (endpoint-matched composition), HasDerivAt (fract x − 1/2) off ℤ, b2Fun = 0 at integers.
• integral_b1_cpow_eq (the level-2 identity, re s > 0): per-unit- interval IBP (integral_mul_deriv_eq_deriv_mul_of_hasDerivAt — the ContinuousOn+Ioo-derivatives variant, exactly fitting B̃₂'s corners), boundary terms vanish at integers, sum to [1,N], N→∞ via intervalIntegral_tendsto_integral_Ioi.
• hasDerivAt_b2Integral (re s > −1): clone of Zeta23's hasDerivAt_Zeta0Integral via hasDerivAt_integral_of_dominated_loc_of_ deriv_le, with ε = (σ+1)/2 and bound x^{−(σ+3)/2}|log x| (their integrable_log_over_pow).
• riemannZeta_eq_level2 (re s > −1, s ≠ 1 — in two im-region variants): ζ(s) = 1/2 + 1/(s−1) − s(s+1)∫₁^∞ B̃₂(x)x^{−s−2}dx. KEY TRICK: instead of proving {re > −1} ∖ {1} connected (the point-avoidance path grind), use the CONVEX regions W± = {re > −1, ±im > 5} — convex ⟹ preconnected, and they contain every application disc (|t| ≥ 10 ⟹ disc B(2+it, 5/2) has |im| ≥ 7.5). Convexity of half-planes via convex_Ioi.linear_preimage reCLM.
• norm_riemannZeta_le_disc: ‖ζ(s)‖ ≤ (3/4)|t|² on B(2+it, 5/2), |t| ≥ 10 — from the representation + ‖∫B̃₂x^{−s−2}‖ ≤ (1/8)/(σ+1) (norm_integral_le_integral_norm + rpow integral) + norm triangle bookkeeping. Full build GREEN (8752 jobs); axiom audit (27 decls): 3 standard axioms only, no sorryAx.

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

• set x := e variables are OPAQUE to linarith (no hypothesis); keep h_def : x = e := rfl and rewrite where needed.
• IntegrableOn.mono' does not exist — use Integrable.mono' (work directly on the restrict measure; IntegrableOn f s μ IS Integrable on the restrict, defeq for exact).
• IntegrableOn.congr_fun h _ measurableSet_Ioi — use apply form so unification instantiates the target function (refine ?_ leaves it uninstantiated). And WATCH Nat casts: Zeta23's Ioi (↑1) vs my Ioi 1 — rw [Nat.cast_one] before congr-rewrites.
• add_le_add_left/add_le_add_right in current Mathlib: _left is the RIGHT-addition form (h : b ≤ c) (a) : b + a ≤ c + a.
• Ico_mem_nhds (not Set.Ico_mem_nhds); natCast_floor_eq_intCast_floor is ROOT-namespace (not Nat.).
• ContinuousOn.comp_fract'' (h : ContinuousOn f (Icc 0 1)) (hf : f 0 = f 1) : Continuous (f ∘ fract) — the endpoint-matching periodic-continuity machine (Topology/Algebra/Order/Floor.lean).
• intervalIntegral.intervalIntegrable_iff' + integrableOn_of_bounded with by fun_prop measurability (B1 is @[fun_prop]-marked in Zeta23).
• hasDerivAt_ofReal_cpow_const (hx : x ≠ 0) (hr : r ≠ 0) and the continuity-only continuousAt_ofReal_cpow_const x y (Or.inr hx0).
• HasDerivAt.congr_deriv (h) (e : f' = g') for derivative-value adjustments; HasDerivAt.const_cpow (hf) (h0 : c ≠ 0 ∨ f x ≠ 0).
• ℂ equations: linarith/nlinarith do NOT apply — use sub_eq_zero/neg_eq_iff_eq_neg/neg_inj chains (journal-011 knew this; it keeps biting in new contexts).
• AnalyticAt.congr (hf : AnalyticAt f x) (h : f =ᶠ[𝓝 x] g) direction; .symm via EventuallyEq.symm as a TERM.

Status

ii′-5b COMPLETE (D-067 estimate ~1 sess ✓). Next: ii′-5c — the Davenport disc argument proper (g = ζ/∏(s−ρₖ)^mₖ, LogOfAnalyticFunction

• BorelCaratheodoryDeriv + the perimeter zero count + the center lower bound via 1/ζ = Σμ(n)n^{−s}) giving the R-bound on σ ∈ [1/2, 7/2]. Then 5d (FE-reflection), 5e (constants fold).