← Session 29 — ii′-5e-v: circle bound (far-tail + series bounds)
thinking (438 chars)
Session 032 is complete. Summary for the user:
- Chunk 3 (the main series circle bound) COMPLETE: `seriesFun_norm_le_gapCircle` proved — ‖seriesFun s‖ ≤ 2·lowZeroConst + 2900·A₀·Ĉ₀(4k+9/2)·(log R)² on the γ-gap circle (k ≥ 4000).
- LiCircleBound.lean ~2867 lines, clean, zero warnings.
- 6 commits (3a, 3b, 3c-i, 3c-ii, capstone, closure b829c21).
- Axiom audit: 19 decls, 3 standard axioms only.
- Next: 5e-v-c (logDeriv/elem assembly).
**Session 032 COMPLETE — ii′-5e-v-b chunk 3: the series circle bound is proved.**
**`seriesFun_norm_le_gapCircle`** (LiCircleBound.lean:2847): on the γ-gap circle ‖s‖ = R (k ≥ 4000),
$$\|\mathrm{seriesFun}\, s\| \;\le\; 2\cdot\mathrm{lowZeroConst} + 2900\cdot A_0\cdot \hat C_0(4k{+}9/2)\cdot(\log R)^2$$
Sub-stage commits:
- **3a** `787b9c0` — `gapCircle_threshold` (416·Ĉ₀ ≤ 4k+5/2, explicit exp/log arithmetic: 2.7¹⁰ ≥ 16006.5, 2.72⁹ ≤ 16006.5, e^{2.4} ≥ 10.2) + `not_isNontrivialZero_on_gapCircle` (the circle is zero-free: a zero would sit within 1/R of R in ordinate, below the 1/(16Ĉ₀) gap).
- **3b** `727f656` — the per-term identity ‖seriesTerm s ρ‖ = m·R/(‖ρ‖·‖s−ρ‖), the reusable count brick `sum_zeroMult_le_of_im_band` (band [a,b] + sign-separation ⟹ 3·A₀·(b−a+2)·log), the tail ≤ 91·A₀·log R via `zero_tail_inv_sq_le`.
- **3c-i/ii** `d2bfde6`, `222d65d` — `dyadic_family_le` (generic machine via `Finset.sum_fiberwise_of_maps_to`, sidestepping the Fintype-ℕ gap in `sum_fiberwise`) + the four shells: low (2·lowZeroConst), inlo/inhi (60·A₀L² each), up (45·A₀L² — dyadic class reaches J+1).
- **3c-iii** `7b8c433` — `shell_crit` (2688·Ĉ₀·A₀·L: uniform separation 1/(32Ĉ₀) — strip arcs |t−γ| ≥ 1/(32Ĉ₀) from the γ-gap (via conj for γ < 0) + threshold; near-axis arcs ‖s−ρ‖ ≥ √13−1) and the five-way partition assembly.
- **Closure** `b829c21` — journal-032, STATE, NGUYEN.md, db.
Audit (`audit-session032-axioms.txt`): 19 decls, **3 standard axioms only**. File now ~2867 lines, clean elaboration, zero warnings, not yet root-imported (by design — the file's capstone chain lands at 5e-v-d).
**Next (session 033): 5e-v-c** — logDeriv assembly (strip arcs via the 5c/5d capstones + the near-sum via the gap; right near-axis Dirichlet; left near-axis via FE + ΓR brackets) + the elementary terms ⟹ ‖Fexpr‖ ≤ C·(log R)³. Then 5e-v-d (Schwarz squeeze ⟹ the ∃ B capstone). Full design staged in STATE.md.
raw content_json (database row)
[{"type":"thinking","thinking":"Session 032 is complete. Summary for the user:\n\n- Chunk 3 (the main series circle bound) COMPLETE: `seriesFun_norm_le_gapCircle` proved — ‖seriesFun s‖ ≤ 2·lowZeroConst + 2900·A₀·Ĉ₀(4k+9/2)·(log R)² on the γ-gap circle (k ≥ 4000).\n- LiCircleBound.lean ~2867 lines, clean, zero warnings.\n- 6 commits (3a, 3b, 3c-i, 3c-ii, capstone, closure b829c21).\n- Axiom audit: 19 decls, 3 standard axioms only.\n- Next: 5e-v-c (logDeriv/elem assembly).","signature":""},{"type":"text","text":"**Session 032 COMPLETE — ii′-5e-v-b chunk 3: the series circle bound is proved.**\n\n**`seriesFun_norm_le_gapCircle`** (LiCircleBound.lean:2847): on the γ-gap circle ‖s‖ = R (k ≥ 4000),\n$$\\|\\mathrm{seriesFun}\\, s\\| \\;\\le\\; 2\\cdot\\mathrm{lowZeroConst} + 2900\\cdot A_0\\cdot \\hat C_0(4k{+}9/2)\\cdot(\\log R)^2$$\n\nSub-stage commits:\n- **3a** `787b9c0` — `gapCircle_threshold` (416·Ĉ₀ ≤ 4k+5/2, explicit exp/log arithmetic: 2.7¹⁰ ≥ 16006.5, 2.72⁹ ≤ 16006.5, e^{2.4} ≥ 10.2) + `not_isNontrivialZero_on_gapCircle` (the circle is zero-free: a zero would sit within 1/R of R in ordinate, below the 1/(16Ĉ₀) gap).\n- **3b** `727f656` — the per-term identity ‖seriesTerm s ρ‖ = m·R/(‖ρ‖·‖s−ρ‖), the reusable count brick `sum_zeroMult_le_of_im_band` (band [a,b] + sign-separation ⟹ 3·A₀·(b−a+2)·log), the tail ≤ 91·A₀·log R via `zero_tail_inv_sq_le`.\n- **3c-i/ii** `d2bfde6`, `222d65d` — `dyadic_family_le` (generic machine via `Finset.sum_fiberwise_of_maps_to`, sidestepping the Fintype-ℕ gap in `sum_fiberwise`) + the four shells: low (2·lowZeroConst), inlo/inhi (60·A₀L² each), up (45·A₀L² — dyadic class reaches J+1).\n- **3c-iii** `7b8c433` — `shell_crit` (2688·Ĉ₀·A₀·L: uniform separation 1/(32Ĉ₀) — strip arcs |t−γ| ≥ 1/(32Ĉ₀) from the γ-gap (via conj for γ < 0) + threshold; near-axis arcs ‖s−ρ‖ ≥ √13−1) and the five-way partition assembly.\n- **Closure** `b829c21` — journal-032, STATE, NGUYEN.md, db.\n\nAudit (`audit-session032-axioms.txt`): 19 decls, **3 standard axioms only**. File now ~2867 lines, clean elaboration, zero warnings, not yet root-imported (by design — the file's capstone chain lands at 5e-v-d).\n\n**Next (session 033): 5e-v-c** — logDeriv assembly (strip arcs via the 5c/5d capstones + the near-sum via the gap; right near-axis Dirichlet; left near-axis via FE + ΓR brackets) + the elementary terms ⟹ ‖Fexpr‖ ≤ C·(log R)³. Then 5e-v-d (Schwarz squeeze ⟹ the ∃ B capstone). Full design staged in STATE.md."}]