Session 035 — 2026-08-23 — ii′-5f STARTED: perimeter repair +

P1/P2 declarations + D-069 design (5f-0 COMPLETE)

Directive

Session 035: ii′-5f — the tight R-bound from the partial-fraction identity (D-056's six-piece analysis ⟹ |R(s)| ≤ 10.5·log(|t|+2) + 48, the baked LiSkeleton constants). User: "Let's work on session 035".

Outcome part 1: PERIMETER REPAIR (user-approved, commit 75172e6)

Second ii′-1a-class encoding defect found (at the point of consumption, 5f design): ZeroCountProp was encoded as the UNWEIGHTED set-card Nat.card (zeroWindow t) ≤ C0hat (t+1), but (i) the declared perimeter source (Trudgian 2014 N(T)/S(T), D-062 §4) counts zeros WITH multiplicity, and (ii) the 5f/ii′-6 near sums are zeroMult-weighted (from seriesFun). The unconditional mult-weighted counts (Jensen/A₀) are ~100× looser and would collapse the R-004 margin constants. User chose strengthen in place: ZeroCountProp is now the mult-weighted form (Σ ρ ∈ window, zeroMult ρ : ℝ) ≤ C0hat (t+1). New bridge lemma one_le_zeroMult (IsNontrivialZero ρ ⟹ 1 ≤ zeroMult ρ; analyticAt_riemannZeta + AnalyticAt.analyticOrderAt_ne_zero + ENat.toNat_pos). Consumers adapted via card ≤ Σ mult (Finset.card_eq_sum_ones as a REAL sum — the ascription ((Σ f : ℕ) : ℝ) elaborates to a real sum of casts, so bridge in ℝ directly): exists_zero_avoiding_T (LiContour), exists_gapCircle_radius (LiGapCircles, three window steps). Full build GREEN (8768 jobs); audit-session035-axioms.txt: 5 decls (incl. partialFraction_identity), 3 standard axioms only.

Outcome part 2: TWO FINDINGS + P1/P2 PERIMETER ADDITIONS

(user-approved, commit f850d9a; design D-069)

• Finding 1 (5f-blocking): D-056's piece 2 charges the near sum Σ_{|γ−t|<1} 1/|s₀−ρ| ONE unit-window count C₀(t), but |γ−t|<1 spans TWO unit windows. The per-unit perimeter fold (2·Ĉ₀) breaks 10.5/48 (≈ 11.2·L + 51); the two-unit Trudgian F/S-pair form (N(t+1)−N(t−1), S-pair does NOT double: 0.59231·L + 0.886·LL + 2.591) makes the honest assembly 6.111·L + 12.163·LL + 47.6 ≤ 10.5·L + 48 — FITS, worst point the loglog pinch at t ≈ 13.1 (margin ≈ 0.15–0.4). ⟹ (P1) ZeroCountProp2 declared (two-unit mult-weighted count; same Trudgian source; honesty slack 0.008·L + 0.109).
• Need (P2): the far sum's height-< 14 intervals need a numeric count; Jensen gives ≈ 3.25 (breaks the pinch constants) vs the true 0 ⟹ NoLowZeros declared (no nontrivial zeros with |γ| ≤ 14; Platt-class zero-location certificate — NOT implied by RHUpTo).
• Finding 2 (documented for ii′-6, NOT 5f scope): D-036's H(T) near-sum has the same count gap PLUS a clearance-coverage gap (L3's clearance covers only in-window zeros). Honest H(T) near sum ≈ 7·Ĉ₀² + 8·Ĉ₀ vs baked 3·Ĉ₀² — margin survives (E-028 26× slack) but the crossover/base points move; to be faced at ii′-6 (D-069 §4).

State of 5f (sub-stage map, D-069 §5)

• 5f-0 ✔ (this session): design + P1/P2 + repair.
• 5f-i: reference-point difference identity (partialFraction_identity at s vs s₀ = 2+it, B cancels) + the near/far split (subtype finset nearZerosSub + ℂ tsum_split) + pieces 1 (dirichletC2 ≤ 0.995 via Λ ≤ log + AntitoneOn.tsum_comp_add_le_integral), 2 (P1 × |s₀−ρ| ≥ 1), 4, 5 (‖1/s − 1/s₀‖ ≤ 4.5/|t|² etc.).
• 5f-ii: piece 6 (sharp digamma |r| ≤ 1.2/|w|² via level-2 EM — LiRBound b2Fun machinery) + piece 3 (the far-sum interval machine; conj for γ < 0; P2 for height < 14; Σ 1/(k(k+1)) = 1).
• 5f-iii: assembly + the pinch lemma (12.163·LL ≤ 4.389·L + const, interior max at L ≈ 2.772) + capstone logDeriv_riemannZeta_sub_nearZeros_le_tight + audit.

Banked gotchas (session 035)

• The ascription ((finset.sum f : ℕ) : ℝ) elaborates to a REAL sum of per-term casts (expected-type propagation INTO the sum) — so Nat.cast_le.mpr (cast-of-ℕ-sum) does NOT match; bridge card ≤ Σ in ℝ directly via by simp (card = Σ 1 in ℝ) + Finset.sum_le_sum + exact_mod_cast.
• zerosIn T₁ T₂ is open-below (T₁ < ρ.im): for a |·| ≤ 1 window use zerosIn (t−2) (t+1), NOT (t−1) (the boundary point ρ.im = t−1 is in the abs-window but not in zerosIn (t−1) _).
• le_or_lt absent (banked twice before — now also in journal-034).

Outcome part 3: 5f-i COMPLETE (commits d808f52 + 1eeda9b)

New file LiTightR.lean (~510 lines, clean, zero warnings; not yet root-imported):

• tsum_split_finset_complex (ℂ variant), nearZerosSub + mem_nearZerosSub (the subtype near finset; the capstone's near sum is over the SUBTYPE finset — cleaner for ii′-6), seriesDiffTerm + seriesDiffTerm_summable + seriesFun_sub_seriesFun, Rexpr_decomp (the six-piece reference-point decomposition: partialFraction_identity at s and s₀ = 2+it, B cancels; linear_combination hsid − hs₀id + hdiff + hsplit + hnear).
• near_sum_refPoint_le (piece 2): near sum at s₀ ≤ ZeroCountProp2 count (|s₀−ρ| ≥ 1 from re ρ < 1; subtype→ambient image bridge).
• one_div_diff_le (pieces 4/5): ≤ 4.5/|t|² ≤ 0.045 each.
• dirichletC2_le_one (piece 1): dirichletC2 ≤ 1 — the level-2 integral machinery: hasDerivAt_neg_log_add_one_div (antiderivative −(log x+1)/x), tendsto_neg_log_add_one_div, integrableOn_log_div_sq, integral_log_div_sq_Ioi_three (= (log 3+1)/3 via integral_Ioi_of_hasDerivAt_of_tendsto'), antitoneOn_log_div_sq (deriv (1−2 log x)/x³ ≤ 0 via log 3 ≥ 1), tsum_log_div_sq_tail_le (AntitoneOn.tsum_comp_add_le_integral), then head n ≤ 3 + tail + the numeric fold (log 2 ≤ 0.6932 via log_two_lt_d9; log 3 ≤ 1.1 via e^1.1 ≥ 3.00126 partial-sum).

Banked gotchas (session 035, LiTightR build)

• cpow_natCast needs the (2:ℂ) = ((2:ℕ):ℂ) norm_num bridge first.
• HasDerivAt.div/.neg produce Pi.div/Pi.neg FUNCTION forms — rw [show] bridges (or Pi.neg_apply/Pi.div_apply); NEVER convert on HasDerivAt (HOU instance-goal explosion: Semiring.toModule = ...).
• Set.interior_Ici is the ROOT-namespace interior_Ici.
• differentiableAt_pow takes ONE explicit arg (the exponent).
• Summable.sum_add_tsum_nat_add is the METHOD form; tsum-first needs .symm.
• tsum_congr pointwise goals come as tail-fn n = shifted-h n — show with the tail on the LEFT.
• field_simp [hx0] can CLOSE the goal (no trailing ring).
• Tendsto 1/x: tendsto_inv_atTop_zero + simpa only [one_div]; log x/x → 0: Real.tendsto_pow_log_div_mul_add_atTop 1 0 1 one_ne_zero
• simpa.

Outcome part 4: 5f-ii piece 6 COMPLETE (commit c9c1362)

LiTightR.lean §8 (~290 lines): log_diff_le (the log difference along the constant-im segment, ≤ 5/t — the segment FTC with Complex.hasDerivAt_log.comp + comp_ofReal + intervalIntegral.norm_integral_le_of_norm_le_const) and digamma_diff_le (piece 6): ‖(ψ(s/2) − ψ(s₀/2))/2‖ ≤ 6/t — via the +2 shift (re(w+2) ≥ 3/4 ⟹ StirlingVert.digamma_stirling applies, remainder ≤ 3/(t/2)² each), the recurrence (digamma_add_natCast), and log_diff_le. NOTE: the sharp Lemma-D remainder (|r| ≤ 1.2/|w|²) turned out UNNECESSARY — digamma_stirling's 3/im² form suffices, and the crude |log(1+u)| ≤ 2|u| log bound sufficed because piece 3's sharper interval sum (S₃ ≤ 1.3703 via the k≥4 telescope, not the D-056 √2-form) freed the constant budget: the full assembly is 5.94·L + 11.813·LL + 46.7 ≤ 10.5·L + 48 with the pinch margin ≈ 1.9 (the LL−L function is DECREASING on L ≥ log 12 — max at the boundary).

Banked gotchas (session 035, piece 6)

• (t/2)·I elaborates with the division INSIDE ℂ (↑t·(1/2:ℂ)) — write the real-cast-first form ((t/2 : ℝ) : ℂ)·I for clean re/im.
• re/im ext-goals: explicit per-component rw chains (Complex.add_re + the value haves + ring) — constructor+simp is unpredictable (simp sometimes closes, sometimes leaves arithmetic).
• field_simp [hx0] can CLOSE the goal (no trailing ring) — twice bitten ("No goals to be solved").
• linear_combination -ht1 when goal_diff = −ht1_diff.
• Set.uIoc is the Ι-notation's real name.
• Real.norm_eq_abs after Complex.norm_real for the |c| form (norm_real gives ‖c‖ not |c|).
• The segment-FTC pattern (banked from 5d): Complex.hasDerivAt_log (slit) ∘ (affine via hasDerivAt_id'.mul_const/.const_add) then .comp_ofReal; the comp's point-match needs the product-of-casts segment form (z y = w₀ + ↑y·↑c, NOT ↑(y·c)).

Status / next

5f remaining: piece 3 (the far-sum interval machine, the big one) + 5f-iii (assembly + pinch + capstone). Piece 3 map (journal-035 piece-3 map + D-069 §3): the far difference series Σ_far m·(s₀−s)/ ((s−ρ)(s₀−ρ)) with per-term ≤ 4.5/(x√(1+x²)) ≤ 4.5/(k√(1+k²)) on k ≤ x = |t−γ| < k+1; per-interval C0hat counts (left ≤ C0hat(t+1) via the perimeter; right ≤ C0hat(2t+1) ≤ C0hat(t+1) + 0.55); the negative-γ side via isNontrivialZero_conj; the height-< 14 intervals empty by NoLowZeros; S₃ := Σ_{k≥1} 1/(k√(1+k²)) ≤ 1.3703 via k ≤ 3 exact (√2 ≥ 1.414, √5 ≥ 2.23, √10 ≥ 3.16) + the telescope 1/(k√(1+k²)) ≤ 1/(k(k−1)) for k ≥ 4 (Σ_{k≥4} 1/(k(k−1)) = 1/3 via Finset.sum_range_sub + the limit); the k > t tail ≤ 0.5828 (Σ log(3k)/k² and Σ 1/k² via the same telescopes). Total piece 3 ≤ 4.5·[2·S₃·C₀ + 0.55·S₃ + 0.5828] = 12.333·C₀ + 6.014 with C₀ = C0hat(t+1) ≤ 0.433L + 0.886LL + 2.9662 (the L' conversion). 5f-iii: the assembly (six pieces into Rexpr_decomp's norm chain) + the pinch lemma + the capstone logDeriv_riemannZeta_sub_nearZeros_le_tight (hZC) (hZC2) (hNLZ).