Session 031 — 2026-08-23 — ii′-5e-v-b chunk 2 COMPLETE: the far-tail bound

Directive

Continue ii′-5e-v per STATE.md: chunk 2 — the tail bound + (planned) the main series bound. User: "Let's start."

Outcome: the tail bound COMPLETE (commits c26241c, f984afc;

LiCircleBound.lean now ~830 lines, clean elaboration, not yet root-imported)

zero_tail_inv_sq_le (the last new analytic input for the circle bound): for X ≥ 200, Σ_{nontrivial zeros with |γ| > X} m_ρ/(1+γ²) ≤ 16·A0count·log X / X. Route (the dyadic fiber machine, all pieces this session):

• dyadClass X ρ := Nat.log 2 ⌊|im ρ|/X⌋₊ + dyadClass_lower (2^j·X ≤ |γ| when |γ| ≥ X) / dyadClass_upper (|γ| < 2^{j+1}·X) — via Nat.pow_log_le_self / Nat.lt_pow_succ_log_self on the floor.
• dyadClass_fiber_finite (fibers finite via ‖ρ‖ ≤ |re|+|im| ≤ 1 + 2^{j+1}X, the norm_le_abs_re_add_abs_im route — NO square roots).
• fiber_mult_count: Σ over {dyadClass = j ∧ X < |γ|} of zeroMult ≤ A₀·(2^{j+1}X+3)·log(3·2^{j+1}X+5) — the two-window cover (zerosIn(2^jX−1, 2^{j+1}X] ∪ zerosIn(−2^{j+1}X, −2^jX]) + Ncount_le_of_interval_gen + the Subtype.val image bridge (Finset.sum_image, sum_le_sum_of_subset_of_nonneg, sum_union with Finset.disjoint_left) + the finsum_mem_eq_finite_toFinset_sum bridge to Ncount.
• fiber_tail_le: the per-fiber bound Σ ofReal(tailTerm) ≤ ofReal((1/(2^jX)²)·count-bound) — via tsum_subtype (explicit args!)
• tsum_eq_sum + indicator_of_notMem/indicator_of_mem + the filter-split (Finset.sum_filter_add_sum_filter_not) + the per-term 1/(1+γ²) ≤ 1/(2^jX)².
• tsum_dyadic_log: Σ ((j+4)log2 + logX)/2^j = 10 log2 + 2 log X (via hasSum_coe_mul_geometric_of_norm_lt_one for Σ j/2^j = 2 and tsum_geometric_two) + dyadicLog_summable + dyadic_tail_constant ((4A₀/X)(10 log2 + 2 logX) ≤ 16A₀ logX/X for X ≥ 200 — the numerics via Real.exp_one_lt_d9 + norm_num: 2.7182818286^5 ≤ 200).
• tailTerm/tailTerm_nonneg/tailTerm_summable (the 1/(1+im²) ≤ 2/(1+‖γ‖²) comparison vs WeilEF.zero_sum_inv_sq).
• Assembly: ENNReal.tsum_fiberwise over dyadClass + per-fiber bounds + the ofReal_tsum_of_nonneg plumbing both ways.

Banked gotchas (session 031 additions)

• Finset.image / filter / sum_subtype lambdas with a coercion body MUST pin the binder type (fun ρ : {ρ // IsNontrivialZero ρ} => ...) — else the elaborator types ρ : ℂ (identity coe) and the Finset argument mismatches — the journal-028 gotcha recurring in THREE new spots (image, filter predicate, sum_subtype's f). Subtype.val directly is cleanest.
• Unary minus precedence: -(2:ℝ)^(j+1) * X parses as (−2^{j+1})·X — NOT −(2^{j+1}·X) — and abs_neg only matches a top-level Neg. Parenthesize ALL: -((2:ℝ)^(j+1) * X); then abs_neg fires directly. (neg_mul bridges when needed.) Set.Finite.disjoint_ toFinset's output form is the ⊆-based one — use Finset.disjoint_left.
• rw [pow_succ'] closes 2^(j+1) = 2·2^j by rfl — a trailing ring errors "No goals".
• tsum_subtype needs its arguments EXPLICIT (the set + the function) — rw [tsum_subtype] fails to unify the SummationFilter/filter metavariables.
• Set.indicator_of_notMem / Set.indicator_of_mem (camelCase).
• Summable.of_norm_bounded's residual goal KEEPS the norm (‖F j‖ ≤ G j): rw [Real.norm_eq_abs, abs_of_nonneg] ONCE on the LHS only — a second Real.norm_eq_abs fails (no norm left on the RHS).
• Summable-goal elaboration note: the apply form's RHS can be a beta-redex — state split goals with show in reduced form.
• nlinarith CANNOT multiply a hypothesis by a non-constant factor — for the A₀·L·(2^{j+1}X) = 2·A₀·L·(2^jX) alignments, REWRITE with the power identity at the goal and both hypotheses first (rw [hpow] at h1' h2' ⊢), THEN linarith.
• The session-030 parser fragility (nested calc := by in deep case blocks) recurred once — keep calc-with-by blocks at shallow indentation.

Status / next

5e-v-b chunks 1+2 COMPLETE (count bridges, Dirichlet bound, split machinery, lowZeroConst, the tail bound). Next: 5e-v-b chunk 3 — the main seriesFun_norm_le_gapCircle (the ONE tsum split + four finset shell bounds + the threshold numerics 16·Ĉ₀(4k+9/2) < R for k ≥ 4000) — full step-by-step design in STATE.md's NEXT ACTION. Then 5e-v-c (logDeriv/elem assembly ⟹ ‖Fexpr‖ ≤ C(log R)³ on the circles) → 5e-v-d (Schwarz squeeze ⟹ ∃ B capstone) → ii′-5f → ii′-3b → ii′-3c → ii′-6 → ii′-7.