← Session 29 — ii′-5e-v: circle bound (far-tail + series bounds)
thinking (45 chars)
Session 033 complete. Summarize for the user.
**Session 033 COMPLETE — ii′-5e-v-c: the Fexpr circle bound is proved.**
**`Fexpr_circle_le`** (LiCircleBound.lean:3875): on the γ-gap circle ‖s‖ = R (k ≥ 4000),
$$\|\mathrm{Fexpr}\, s\| \;\le\; 2\cdot\mathrm{lowZeroConst} + \mathrm{dirichletC2} + 400000\cdot A_0\cdot \hat C_0(R{+}2)\cdot(\log R)^2$$
Sub-stage commits:
- **c-i** `1c76576` — `logDeriv_Gammaℝ_eq_of_not_neg_nat`: the (G) formula logDeriv ΓR s₀ = −(log π)/2 + ½ψ(s₀/2) at **any** non-pole point, via direct `logDeriv_mul` on `Gammaℝ_def` (digamma := logDeriv Γ by definition) — the im ≠ 0 hypothesis of 5e-ii's (G) was only pole-avoidance. This discharges the real point s = −R with **no continuity argument** (a design-level simplification vs journal-030's plan). Plus `gapCircle_sep` (the arc-analysis separation standalone), `nearZeros_count_le`, `gapCircle_sep_of_mem_nearZeros`.
- **c-ii** `5da957c` — `digamma_right_le` (re ≥ 1.75: 48+23·log) and `digamma_circle_le` (uniform ‖ψ(s/2)‖ ≤ 62+23·log(2+R/2): strip sub-log / right_le / left near-axis via 5e-ii (A) c = 1/8 from the ℤ-clearance — the R+re s = im²/(R−re s) identity avoids all square roots).
- **c-iii** `2fc359f` — `logDeriv_circle_le` (three regions: (i) re ≥ 2 Dirichlet; (ii) re ∈ [−5/2, 2] — |im| ≥ 10 automatic — 5c/5d capstones + near sum ≤ 32Ĉ₀·count; (iii) re < −5/2: `logDeriv_zeta_fe` with all 10 hypotheses discharged + Dirichlet at 1−s + the ΓR bracket) and the six-norm assembly.
- **Closure** `df4e083` — journal-033, STATE, NGUYEN.md, db.
Audit (`audit-session033-axioms.txt`): 14 decls, **3 standard axioms only**. File ~3928 lines, clean, zero warnings, not yet root-imported (by design — the file's capstone lands at 5e-v-d).
**Next (session 034): 5e-v-d** — the Schwarz squeeze: Gentire entire + the circle bound ⟹ MapsTo into closedBall (Gentire 0) (R₂+1) ⟹ `Complex.dist_le_div_mul_dist_of_mapsTo_ball` ⟹ dist (Gentire z₀) (Gentire 0) ≤ (R₂+1)/R·‖z₀‖ → 0 (via Ĉ₀(R+2) ≤ 5 log R and log R ≤ 4·R^{1/4}) ⟹ **Gentire ≡ B** ⟹ the capstone `partialFraction_identity` under `ZeroCountProp`. Then ii′-5f (tight constants) → ii′-3b → ii′-3c → ii′-6 → ii′-7.
raw content_json (database row)
[{"type":"thinking","thinking":"Session 033 complete. Summarize for the user.","signature":""},{"type":"text","text":"**Session 033 COMPLETE — ii′-5e-v-c: the Fexpr circle bound is proved.**\n\n**`Fexpr_circle_le`** (LiCircleBound.lean:3875): on the γ-gap circle ‖s‖ = R (k ≥ 4000),\n$$\\|\\mathrm{Fexpr}\\, s\\| \\;\\le\\; 2\\cdot\\mathrm{lowZeroConst} + \\mathrm{dirichletC2} + 400000\\cdot A_0\\cdot \\hat C_0(R{+}2)\\cdot(\\log R)^2$$\n\nSub-stage commits:\n- **c-i** `1c76576` — `logDeriv_Gammaℝ_eq_of_not_neg_nat`: the (G) formula logDeriv ΓR s₀ = −(log π)/2 + ½ψ(s₀/2) at **any** non-pole point, via direct `logDeriv_mul` on `Gammaℝ_def` (digamma := logDeriv Γ by definition) — the im ≠ 0 hypothesis of 5e-ii's (G) was only pole-avoidance. This discharges the real point s = −R with **no continuity argument** (a design-level simplification vs journal-030's plan). Plus `gapCircle_sep` (the arc-analysis separation standalone), `nearZeros_count_le`, `gapCircle_sep_of_mem_nearZeros`.\n- **c-ii** `5da957c` — `digamma_right_le` (re ≥ 1.75: 48+23·log) and `digamma_circle_le` (uniform ‖ψ(s/2)‖ ≤ 62+23·log(2+R/2): strip sub-log / right_le / left near-axis via 5e-ii (A) c = 1/8 from the ℤ-clearance — the R+re s = im²/(R−re s) identity avoids all square roots).\n- **c-iii** `2fc359f` — `logDeriv_circle_le` (three regions: (i) re ≥ 2 Dirichlet; (ii) re ∈ [−5/2, 2] — |im| ≥ 10 automatic — 5c/5d capstones + near sum ≤ 32Ĉ₀·count; (iii) re < −5/2: `logDeriv_zeta_fe` with all 10 hypotheses discharged + Dirichlet at 1−s + the ΓR bracket) and the six-norm assembly.\n- **Closure** `df4e083` — journal-033, STATE, NGUYEN.md, db.\n\nAudit (`audit-session033-axioms.txt`): 14 decls, **3 standard axioms only**. File ~3928 lines, clean, zero warnings, not yet root-imported (by design — the file's capstone lands at 5e-v-d).\n\n**Next (session 034): 5e-v-d** — the Schwarz squeeze: Gentire entire + the circle bound ⟹ MapsTo into closedBall (Gentire 0) (R₂+1) ⟹ `Complex.dist_le_div_mul_dist_of_mapsTo_ball` ⟹ dist (Gentire z₀) (Gentire 0) ≤ (R₂+1)/R·‖z₀‖ → 0 (via Ĉ₀(R+2) ≤ 5 log R and log R ≤ 4·R^{1/4}) ⟹ **Gentire ≡ B** ⟹ the capstone `partialFraction_identity` under `ZeroCountProp`. Then ii′-5f (tight constants) → ii′-3b → ii′-3c → ii′-6 → ii′-7."}]