Session 036 — 2026-08-24 — ii′-5f COMPLETE: piece 3 + 5f-iii capstone

Directive

Continue ii′-5f from the session-035 state: piece 3 (the far-sum interval machine) then 5f-iii (assembly + pinch + capstone). User: "Let's do it now" / "let's continue to 5f-iii now".

Outcome part 1: PIECE 3 COMPLETE (commits 79c506b..52bb2cb)

LiTightR.lean sections 9–19 (~2700 new lines), the far difference series bounded by far_series_le : ‖far‖ ≤ 12.1284·C0hat(t+1) + 7.2425:

• §9 certified numerics: the integral-comparison log machines (log_one_add_ge, neg_log_one_sub_le), all certified log/exp/sqrt bounds (log 10 both sides, log 11/14 below, log 13/2.3/(23/13)/(17/14) above, 1/e ≤ 0.3679, log u ≤ u/e).
• §10 the weight farW + S₃: farW k = 1/(k√(1+k²)); S₃ = Σ_{k≥1} farW k ≤ 1.3476 (4 exact sqrt-rational terms: √2 ≥ 1.414, √5 ≥ 2.23, √10 ≥ 3.16, √17 ≥ 4.123; telescope Σ_{k≥5} 1/(k(k−1)) = 1/4).
• §11/12 the six tail bricks (antitone-integral machine): RW₀ 0.1, RW₁ 0.3303, RW₂ 0.1216 (loglog ≤ (1/e)·log trick); LA₀ 1/23, LA₁ 0.1687 (the F = −log x/(x+10) + (1/10)log(x/(x+10)) antiderivative), LA₂ 0.0621.
• §13 C0hat bridges: C0hat(2k+1) ≤ 0.433(log k+0.833)+0.886(loglog k +0.3475)+2.9 (k ≥ 11), the j+1 form (j ≥ 14: 0.1942/0.0736), and C0hat(2t+1) ≤ C0hat(t+1) + 0.55 (t ≥ 10).
• §14 conj machinery: hasDerivAt_conj_of_conj_eq (the conj-derivative lemma via the slope characterization) → iteratedDeriv_riemannZeta_conj → analyticOrderAt_riemannZeta_conj → zeroMult_conj (the left-tail count bridge).
• §15 farG + norm reduction: farG (4.5m/(x√(1+x²))), farG_summable (dominated by 18(1+t)²·m/(1+‖γ‖²) via the normSq comparison), seriesDiffTerm_norm_eq, the per-term bound (‖s₀−s‖ ≤ 4.5, ‖s−ρ‖ ≥ x, ‖s₀−ρ‖ ≥ √(1+x²)), far_series_norm_le_farG_tsum.
• §16 the main bucket machine: unit_family_le (dyadic_family_le generalized), mainFinset + bucket range, farG_le_farW_mul (the monotone weight chain), main_bucket_count (the two-window perimeter bridge: right via hZC + C0hat_two_t_add_one_le, left via hZC or NoLowZeros emptiness), farG_main_le ≤ 4.5(2C₀+0.55)·1.3476.
• §17/18 the two tail machines (ENNReal fiberwise, cloning the LiCircleBound fiber_tail_le/zero_tail_inv_sq_le pattern): farGLeft_le ≤ 4.5·0.260558 = 1.1729 (left, j ≥ 14, conj + zeroMult_conj); farGRight_le ≤ 4.5·0.607614 = 2.7343 (right, k ≥ ⌊t⌋₊+1, C0hat(2k+1)).
• §19 the tail split + capstone: farG_tail_eq (outside mainFinset, farG = farGRight + farGLeft — the main finset has no γ<0 zeros by NoLowZeros) and far_series_le (main + right + left: 4.5(2C₀+0.55)·1.3476 + 2.7343 + 1.1729 = 12.1284·C₀ + 7.2425).

Outcome part 2: 5f-iii COMPLETE (commit e6d57e1) — ii′-5f DONE

LiTightR.lean sections 20–21 (~550 lines):

• the pinch lemma pinch_tight_R: 11.6318·log L − 4.6484·L ≤ 0.397094 for L ≥ log 12 — the concave tangent at the certified critical point 2.5024: f′ = 11.6318/L − 4.6484 antitone on Ici (log 12), FTC in both directions, f(2.5024) ≤ −0.96231 certified (log 2.5024 ≤ 0.9173 via exp partial sums; 4.6484·2.5024 = 11.63215616 ≥ 11.6318). Correction side ≤ 0.001. Supporting: log 12 = 4 log 2 − log(4/3) ≥ 2.4848 (the 4-term neg_log_one_sub_le_four machine), log 12 ≤ 2.5024, log 3 ≤ 1.0987.
• the C0hat L/LL conversion: C0hat(t+1) ≤ 0.433(L+1/12) + 0.886(LL+0.03354)+2.9.
• THE CAPSTONE logDeriv_riemannZeta_sub_nearZeros_le_tight (hZC) (hZC2) (hNLZ): for σ ∈ [−5/2, 3], t ≥ 10, ζ s ≠ 0: ‖logDeriv ζ s − Σ_{near} m/(s−ρ)‖ ≤ 10.5·log(t+2) + 48 — the six-piece assembly: piece 1 dirichletC2 ≤ 1, piece 2 the honest two-unit near count 0.6L+0.886LL+2.7, piece 3 far_series_le, pieces 4/5 0.045 each, piece 6 digamma_diff_le ≤ 6/t ≤ 0.6; fold: 5.8516L + 11.6318LL + 47.6029 ≤ 10.5L + 48 via the pinch (margin ≈ 1.36 at the worst point L*).

ii′-5f is COMPLETE: the tight R-bound (D-056's Theorem R, A = 10.5, B₀ = 48) is now Lean-proved modulo ONLY the declared perimeter (ZeroCountProp, ZeroCountProp2, NoLowZeros).

Axiom audits

• audit-session036-axioms.txt (piece 3, 22 decls): 3 standard axioms only.
• audit-session036b-axioms.txt (5f-iii, 11 decls): 3 standard axioms only. Full build GREEN (8762 jobs).

Banked gotchas (session 036)

• a * b / c parses as (a·b)/c — with mul_left-coefficient proofs the goal must be written c * (b / d) with explicit parens, else isDefEq explodes (200k+ heartbeats) proving (a·b)/c = a·(b/c) by unfolding. THE key Lean-4 gotcha of the session (reproduced in isolation).
• Decimal literals can default to Float in literal-only statements — pin (x : ℝ) on the first literal when the statement's type isn't otherwise forced.
• rw [lemma] rewrites only the FIRST unifier's instances — a two-sided rewrite (e.g. div_eq_mul_inv on both sides) needs two calls.
• x⁻¹ vs 1/x are different terms (Inv.inv vs HDiv); normalize via one_div/div_eq_mul_inv with care about which form each lemma produces.
• div_le_div_of_nonneg_left (ha : 0≤a) (hc : 0<c) (h : c≤b) : a/b ≤ a/c — the 2nd arg is 0 < (SECOND denominator); div_le_iff₀ (hc : 0<c) : b/c ≤ a ↔ b ≤ a·c; le_div_iff₀ : a ≤ b/c ↔ a·c ≤ b (directions swapped vs naive expectation — banked twice).
• mul_le_mul (h₁ : a≤b) (h₂ : c≤d) (hc : 0≤c) (hb : 0≤b) : a·c ≤ b·d (arg order: (left-ineq)(right-ineq)(0≤right-left)(0≤left-left)).
• Real.exp_one_gt_d9/lt_d9 trans direction: (by norm_num : rounder ≤ d9-const).trans X_gt_d9.le for lower bounds; X_lt_d9.le.trans (by norm_num) for upper bounds — getting these backwards produces Real.log 2 ≤ ?m metavariable goals.
• t ^ 3 needs pow_nonneg ht.1 3 (odd powers aren't positivity-provable); t² is fine.
• Summable.mul_left/add produce lambdas with · inside (not Pi.mul/add) — exact at the term level works; apply Summable.add with function args fails (it takes proofs).
• tsum_add as a rewrite needs beta-rfl bridges: state the goal with from rfl-provable explicit (f x + g x) forms before rw [e1, e2].
• Nat.floor needs exact_mod_cast for mixed ℕ/ℝ conditions; and ⌊t⌋₊+1 vs (⌊t⌋₊:ℝ)+1 bridge via push_cast.
• The farGLeft tail's left interval count needs NoLowZeros for the main-farGLeft emptiness (any γ<0 zero has |γ| ≥ 14 ⟹ x ≥ t+14 ⟹ never in mainFinset).
• two_le_C0hat (ht : 1 ≤ t) is the C0hat nonnegativity source (positivity can't see through C0hat).
• The pinch's coefficient must match the assembly exactly — a rounded-up LL-coefficient with a rounded-up L-coefficient is safe (both LL, L ≥ 0), but a mixed-sign rounding (LL up, L-coeff down via 10.5−L) breaks the pinch for large L (the f−f_actual difference has mixed sign). Use exact coefficients 11.6318/4.6484 with explicit rounding lemmas 5.8515972 ≤ 5.8516, 10.7457624 ≤ 11.6318.

Status / next

ii′-5f COMPLETE. Remaining map (per D-064 §6 + session-035 notes): ii′-3b (the contour moments σ_k = −g^{(k−1)}(0)/(k−1)! — the R-bound is now proved, unblocking the moment estimates) → ii′-3c (assembly of Lagarias (4.10): τ_j = c_j + (−1)ʲσ_{j+1} − (−1)ʲ — the crux identity Sf(n) = Res₁(n)) → ii′-6 (L0 assembly: sides identity + bridge |λ_n(T)| ≤ 2·FAlt(T) (hRH) + |Sf n| ≤ Bn FAlt n on [10⁵, N₁]; D-069 Finding 2's H(T) near-sum repair map lives here) → ii′-7 (closure: theorem sfBoundProp : SfBoundProp; final lambda_pos_finite_height_closed with the 3 perimeter hypotheses only; full axiom audit; paper Appendix B

• tag upgrade; archive closure + D-037 line-63 erratum pointer). NEXT ACTION: Session 037 — ii′-3b (the contour moments).