Session 034 — 2026-08-23 — ii′-5e-v-d COMPLETE: the Schwarz squeeze ⟹

the partial-fraction capstone

Directive

Continue ii′-5e-v per STATE.md: chunk 5e-v-d — the Schwarz squeeze ⟹ the ∃ B capstone partialFraction_identity (LiCircleBound.lean §13 or a new LiSqueeze.lean). User: "Let's start ii′-5e-v-d".

Outcome: 5e-v-d COMPLETE (commit 5a262a1; new file LiSqueeze.lean,

~330 lines, clean elaboration, zero warnings; LiCircleBound + LiSqueeze root-imported; full build GREEN; audit-session034-axioms.txt: 5 decls, 3 standard axioms only)

New file LiSqueeze.lean (imports LiCircleBound; LiCircleBound built for the first time — 51 s — and both now root-imported):

• §1 C0hat_add_two_le: Ĉ₀(R+2) ≤ 5·log R for R ≥ 16002. Via log(R+4) ≤ 2·log R (R+4 ≤ R², Real.log_pow), log log(R+4) ≤ log(2·log R) = log 2 + log log R ≤ 1 + log R ≤ 2·log R (Real.log_le_sub_one_of_pos twice), 2.9 ≤ (1/3)·log R; total 0.433·2 + 0.886·2 + 1/3 ≈ 2.97 ≤ 5.
• §2 not_badPoint_on_gapCircle: the four-way badness split — not nontrivial (session-032's not_isNontrivialZero_on_gapCircle), ≠ 0/1 (norms: ‖s‖ = R ≥ 16002), ≠ −2n (else R/2 = n ∈ ℤ against hgapInt with m := n; Int.cast_natCast bridge, Complex.norm_natCast).
• §3 gentire_circle_le: Gentire s = Fexpr s on the circle (§2 + 5e-iv's gentire_eq_Fexpr) ⟹ the Fexpr_circle_le bound transfers.
• §4 gentire_const (hZC : ZeroCountProp) : Gentire z₀ = Gentire 0. The squeeze: for ε > 0, set C₀' := 2·lowZeroConst + dirichletC2 + ‖Gentire 0‖, C₁ := 2·10⁶·A₀ ( = 400000·A₀·5), c := 2 + (128·C₁ + 2·C₀')·‖z₀‖/ε, M := max (c⁴) (‖z₀‖+1), k := max 4000 ⌈M/4⌉₊; the perimeter gap circle R ∈ [4k+5/2, 4k+3] (exists_gapCircle_radius) has R ≥ M. Max-modulus (Zeta23 AnalyticOn.norm_le_of_norm_le_on_sphere, r = R, analytic from gentire_analyticAt_and_eq.1) lifts the sphere bound to the ball; MapsTo into closedBall (Gentire 0) (RB + ‖Gentire 0‖) by norm_sub_le; the ball-form Schwarz lemma (Complex.dist_le_div_mul_dist_of_mapsTo_ball) gives dist ≤ (RB + ‖Gentire 0‖)/R·‖z₀‖. Growth: RB ≤ C₀' + 64·C₁·Q³ with Q := R^{1/4} (Real.log_le_rpow_div at ε = 1/4 ⟹ log R ≤ 4Q; pow_le_pow_left₀ ⟹ (log R)³ ≤ 64Q³; Ĉ₀(R+2) ≤ 5·log R by §1) and R = Q⁴ (Real.rpow_inv_natCast_pow); Q ≥ c ⟹ the two branches 64·C₁·Q³·‖z₀‖ ≤ (ε/2)·Q⁴ (from 128·C₁·‖z₀‖ ≤ ε·Q) and C₀'·‖z₀‖ ≤ (ε/2)·Q⁴ (from 2·C₀'·‖z₀‖ ≤ ε·Q and ε·Q ≤ (ε/2)·Q⁴ via Q³ ≥ 8); sum ⟹ (RB + ‖Gentire 0‖)·‖z₀‖ ≤ ε·Q⁴ = ε·R. Then dist ≤ ε for all ε ⟹ dist = 0 (le_or_gt rcases + the ε := dist/2 contradiction) ⟹ Gentire z₀ = Gentire 0.
• §5 partialFraction_identity (hZC : ZeroCountProp): ∃ B : ℂ, ∀ s, riemannZeta s ≠ 0 → s ≠ 0 → s ≠ 1 → (∀ n ≥ 1, s ≠ −2n) → logDeriv riemannZeta s = B + seriesFun s − 1/s − 1/(s−1) + (Real.log Real.pi : ℂ)/2 − Complex.digamma (s/2)/2. Proof: ζ s ≠ 0 kills the nontrivial-zero disjunct (IsNontrivialZero.1) ⟹ ¬ badPoint s ⟹ Gentire s = Fexpr s (5e-iv) and Gentire s = Gentire 0 (§4) ⟹ Fexpr s = Gentire 0; unfold Fexpr; linear_combination. B := Gentire 0 (no evaluation needed — D-068 §0: B cancels in 5f's two-point analysis).

This is the first use of the perimeter in the 5e chain (the gap circles need ZeroCountProp; 5c/5d/5e-i..iv were Jensen/unconditional). The capstone is exactly the D-068 §5 target statement.

Inventory verification (all live-checked before writing)

• Complex.dist_le_div_mul_dist_of_mapsTo_ball (Mathlib Schwarz.lean): (hd : DifferentiableOn ℂ f (ball c R₁)) (MapsTo f (ball c R₁) (closedBall (f c) R₂)) (z ∈ ball) ⟹ dist (f z) (f c) ≤ R₂/R₁·dist z c.
• AnalyticOn.norm_le_of_norm_le_on_sphere (Zeta23 StrongPNTPrefix): r ≤ R, AnalyticOn (closedBall 0 R), sphere-r bound, w ∈ closedBall 0 r ⟹ ‖f w‖ ≤ C.
• Real.log_le_rpow_div (0 ≤ x) (0 < ε) : log x ≤ x^ε/ε (Pow/Real).
• Real.pow_rpow_inv_natCast_pow / Real.rpow_inv_natCast_pow (the (c⁴)^{1/4} = c / (R^{1/4})⁴ = R directions).
• pow_le_pow_left₀ (the ₀-suffixed form in this Mathlib; pow_le_pow_left is the preorder one WITHOUT the 0 ≤ a).

Banked gotchas (session 034)

• le_or_lt does NOT exist (recurrence of the session-030/032 gotcha — now banked here too): use le_or_gt (a b) : a ≤ b ∨ a > b. The dist-squeeze close: rcases le_or_gt d 0; the d > 0 branch dies by key (d/2).
• set Q := R ^ ((4:ℝ)⁻¹) with hQ + rw [← hQ] at h after push_cast is the clean (R^{1/4})⁴ = R bridge; write haves with Q in the statement and give R^{1/4} proofs — the set-let defeq makes exact accept them.
• Real.log_le_rpow_div wants the rpow EXPONENT as the ε hypothesis: (4:ℝ)⁻¹ with positivity; the x^ε/ε → 4·x^ε conversion is div_eq_mul_inv + inv_inv + ring.
• push_cast turns rpow_inv_natCast_pow's ((4:ℕ):ℝ)⁻¹ exponent into (4:ℝ)⁻¹ BEFORE the rw [← hQ] match (cast-mismatch rw failure otherwise).
• linarith closes every ≤-chain once the products are pre-formed (div_mul_cancel₀ for the /ε·ε round trips; mul_le_mul_of_nonneg_right for the single-factor lifts); the banked "no add_le_add_left/right" rule kept.
• lake build of a NON-root-imported file's importer fails with a stale "object file does not exist" — lake build NguyenRH1.LiSqueeze builds the dependency chain (LiCircleBound 51 s first time).

Status / next

ii′-5e COMPLETE (5e-0, i, ii, iii, iv, v-a/b/c/d all done). The partial-fraction identity is now Lean-proved modulo ONLY the declared perimeter (ZeroCountProp — Trudgian N(T)/S(T), D-062 §4). Remaining map: ii′-5f (D-056's tight constants A = 10.5, B₀ = 48 from the identity — the partial-fraction R-bound, ~1 session) → ii′-3b (moments) → ii′-3c (crux assembly Sf = Res₁) → ii′-6 (L0) → ii′-7 (closure + paper Appendix B + tag upgrade).