Session 033 — 2026-08-23 — ii′-5e-v-c COMPLETE: the Fexpr circle bound

Directive

Continue ii′-5e-v per STATE.md: chunk 5e-v-c — the logDeriv/elem assembly ⟹ ‖Fexpr s‖ ≤ C·(log R)³ on the γ-gap circles. User: "let's continue next session".

Outcome: 5e-v-c COMPLETE (commits 1c76576, 5da957c, + capstone;

LiCircleBound.lean now ~3928 lines, clean elaboration, zero warnings, not yet root-imported)

Fexpr_circle_le: for k ≥ 4000, R with the gap-circle properties (4k+5/2 ≤ R ≤ 4k+3, the γ-gap ordinate clearance, the ℤ-clearance dist(R/2,ℤ) ≥ 1/4), ‖s‖ = R: ‖Fexpr s‖ ≤ 2·lowZeroConst + dirichletC2 + 400000·A₀·Ĉ₀(R+2)·(log R)².

Structure realized:

• c-i differentiableAt_Gammaℝ_of_not_neg_nat + logDeriv_Gammaℝ_eq_of_not_neg_nat — the (G) formula logDeriv ΓR s₀ = −(log π)/2 + ½ψ(s₀/2) at ANY s₀ with s₀/2 off the Γ poles: the im ≠ 0 hypothesis of 5e-ii's logDeriv_Gammaℝ_eq was only pole-avoidance, and the direct logDeriv_mul computation on Gammaℝ_def works everywhere (digamma := logDeriv Γ by definition; deriv_comp for the chain rule). This discharges the real point s = −R of the left near-axis arc with NO continuity argument. gapCircle_sep (the shell_crit arc analysis as a standalone statement for ALL nontrivial zeros — the shell range was only used for the term bound), nearZeros_count_le (the near-window mult-count ≤ 3·A₀·log(3·max|t−1||t+1|+5), single zerosIn window), gapCircle_sep_of_mem_nearZeros. New imports: LiDisc, LiReflect, LiDigammaLeft.
• c-ii digamma_right_le (re w ≥ 1.75 ⟹ ‖ψ(w)‖ ≤ 48+23·log(2+‖w‖): sub-log / 5e-ii (B) / 5e-ii (A) c = 1); digamma_circle_le (uniform ‖ψ(s/2)‖ ≤ 62+23·log(2+R/2) on the circle: strip sub-log; right_le; the left near-axis via 5e-ii (A) c = 1/8 from the ℤ-clearance — the R+re s = im²/(R−re s) identity, NO square roots); the small elems (‖1/s‖, ‖1/(s−1)‖, log π ≤ 2, ‖(log π)/2‖ ≤ 1, dirichletC2_nonneg).
• c-iii logDeriv_circle_le (three regions): (i) re s ≥ 2: Dirichlet. (ii) re s ∈ [−5/2, 2] — automatically |im s| ≥ 10 via R−|im| = re²/(R+|im|): the 5c/5d capstones (re ≥ 1/2: 100000·(log|t|)² with a ×2 trans; re < 1/2: 200000) + the near sum ‖Σ m/(s−ρ)‖ ≤ 32·Ĉ₀·(near count) ≤ 192·Ĉ₀·A₀·(log R)². (iii) re s < −5/2: logDeriv_zeta_fe (all 10 hypotheses discharged: ζ s ≠ 0 via zeta_zero_classification + the ℤ-clearance for −2n; Gammaℝ s ≠ 0 via Gammaℝ_eq_zero_iff + hpoles; hpoles itself: im ≠ 0 branch + the s = −R branch via hm2 from congrArg Complex.re) + Dirichlet at 1−s + the ΓR bracket (hbr1/hbr2 via logDeriv_Gammaℝ_eq_of_not_neg_nat — at s = −R too) ≤ 57+23·log R ≤ 100·A₀Ĉ₀L². Uniform: dirichletC2 + 200000·L² + 300·A₀·Ĉ₀·L². Fexpr_circle_le: the six-norm chain (norm_add_le/norm_sub_le haves + linarith — NO add_le_add_*), the Ĉ₀(4k+9/2) → Ĉ₀(R+2) conversion via C0hat_mono, and the absorption (200000·L² ≤ 100000·A₀Ĉ₀L²; 34+12L ≤ 40·A₀Ĉ₀L² via L ≤ L²).

Axiom audit (audit-session033-axioms.txt): 14 declarations, all [propext, Classical.choice, Quot.sound] only.

Banked gotchas (session 033 additions)

• riemannZeta_ne_zero_of_one_le_re takes ONLY the re hypothesis (no s ≠ 1) — apply produces ONE goal; a second bullet errors "No goals".
• div_lt_iff₀ in this Mathlib is a/c < b ↔ a < b·c; for a < b/c use lt_div_iff₀.
• add_le_add_left/right are SWAPPED vs classic (session-025 gotcha recurring in force): add_le_add_left h a : b+a ≤ c+a (changes the LEFT addend); add_le_add_right h a : a+b ≤ a+c (changes the RIGHT). For norm-chain sums, per-step norm_add_le/norm_sub_le haves + linarith is strictly more robust than any add_le_add_* nesting.
• rw [h3 : X = 1*X] rewrites EVERYWHERE (both sides) — use a calc step with the 1·X form isolated instead.
• linear_combination -h discharges the (1−s) = 0/1 ⟺ s = 1/0 bridges — do NOT hand-roll sub_add_cancel chains (rw [h6 : 1 = 1+s] rewrites every literal 1 and explodes the goal).
• congrArg Complex.re + simp is the robust cast-bridge for ↑(-R)/2 vs −↑R/2 forms (cast-of-neg vs neg-of-cast are defeq not syntactic; rw-chains on them are fragile).
• Real.pi_lt_d2 : π < 3.15 (d2-style naming; Real.pi_lt_315 does NOT exist); Real.pi_gt_three : 3 < π.
• abs_one : |1| = 1 for the |x+1| ≤ |x|+1 forms (abs_add_le leaves |1|); abs_neg first for |x−1|.
• Finset.mul_sum's factor is LEFT-nested: keep all shell/count products LEFT-ASSOC ((c·d)·x) through every calc step — a·(b·c) vs (a·b)·c are different atoms to rw/nlinarith/linarith.
• one_div_le_one_div_of_le (ha : 0 < a) (hab : a ≤ b) : 1/b ≤ 1/a takes the SMALL side's positivity first; then .trans_eq (one_div_one_div _).
• Complex.digamma := logDeriv Gamma (rfl def) ⟹ the ΓR logDeriv formula at real non-pole points is a direct logDeriv_mul computation — no identity-principle/continuity detour needed.
• hasDerivAt_id' s₀ |>.div_const 2 + deriv_comp for deriv (Γ(z/2)) = deriv Γ (s₀/2)·(1/2); the eta-rfl bridge (fun z => Γ (z/2)) vs (Γ ∘ fun z => z/2) closes by rfl.

Status / next

5e-v-a ✔, 5e-v-b ✔ (chunks 1+2+3), 5e-v-c ✔. Remaining: 5e-v-d — the Schwarz squeeze: Gentire entire + ‖Gentire‖ ≤ 2·lowZeroConst + dirichletC2 + 400000·A₀·Ĉ₀(R+2)·(log R)² on the gap circles ⟹ dist (Gentire z₀) (Gentire 0) ≤ R₂(R_k)/R_k·|z₀| → 0 (mapsTo into closedBall via AnalyticOn.norm_le_of_norm_le_on_sphere + Complex.dist_le_div_mul_dist_of_mapsTo_ball; (log R)³/R → 0 needs the Ĉ₀(R+2) ~ log R·loglog R growth bound) ⟹ Gentire ≡ Gentire 0 =: B ⟹ the capstone partialFraction_identity (hZC : ZeroCountProp) : ∃ B : ℂ, ∀ s, riemannZeta s ≠ 0 → s ≠ 0 → s ≠ 1 → (∀ n ≥ 1, s ≠ −2n) → logDeriv riemannZeta s = B + seriesFun s − 1/s − 1/(s−1) + (Real.log Real.pi)/2 − Complex.digamma (s/2)/2 (D-068 §5) → ii′-5f → ii′-3b → ii′-3c → ii′-6 → ii′-7.