[{"type":"thinking","thinking":"The user wants to continue to 5f-iii: the assembly of the six pieces into `Rexpr_decomp`'s norm chain + the pinch lemma + the capstone `logDeriv_riemannZeta_sub_nearZeros_le_tight (hZC) (hZC2) (hNLZ)`.\n\nLet me plan 5f-iii carefully.\n\n**The pieces (all proved in LiTightR.lean):**\n1. Piece 1: `dirichletC2_le_one : dirichletC2 ≤ 1` — bounds ‖logDeriv ζ s₀‖ at s₀ = 2+it (via `norm_logDeriv_zeta_le_dirichlet` from LiCircleBound: ‖ζ′/ζ‖ ≤ dirichletC2 for re ≥ 2).\n2. Piece 2: `near_sum_refPoint_le (hZC2) : ‖∑ ρ ∈ nearZerosSub t, m/(s₀−ρ)‖ ≤ 0.6·log(t+2) + 0.886·loglog(t+2) + 2.7`.\n3. Piece 3: `far_series_le (hZC) (hNLZ) : ‖far series‖ ≤ 12.1284·C0hat(t+1) + 7.2425`.\n4/5. Pieces 4/5: `one_div_diff_le : ‖1/s − 1/s₀‖ ≤ 0.045 ∧ ‖1/(s−1) − 1/(s₀−1)‖ ≤ 0.045`.\n6. Piece 6: `digamma_diff_le : ‖(ψ(s/2) − ψ(s₀/2))/2‖ ≤ 6/t`.\n\n**The decomposition:** `Rexpr_decomp (hZC : ZeroCountProp) {s s₀} (conditions) (t : ℝ)`:\nlogDeriv ζ s − Σ_{nearZerosSub t} m/(s−ρ) = logDeriv ζ s₀ − Σ_{nearZerosSub t} m/(s₀−ρ) + far-series − (1/s − 1/s₀) − (1/(s−1) − 1/(s₀−1)) − (ψ(s/2) − ψ(s₀/2))/2.\n\n**The capstone (D-069 §5):**\n```\ntheorem logDeriv_riemannZeta_sub_nearZeros_le_tight\n    (hZC : ZeroCountProp) (hZC2 : ZeroCountProp2) (hNLZ : NoLowZeros)\n    {t : ℝ} (ht : 10 ≤ t) {s : ℂ}\n    (hσ : -5/2 ≤ s.re ∧ s.re ≤ 3) (him : s.im = t)\n    (hζ : riemannZeta s ≠ 0) :\n    ‖logDeriv riemannZeta s\n        - ∑ ρ ∈ nearZerosSub t, (zeroMult ρ.1 : ℂ) / (s - ρ.1)‖\n      ≤ 10.5 * Real.log (|t| + 2) + 48\n```\nWait — D-069's capstone statement uses `nearZeros t` (the ambient near finset) but our decomposition uses `nearZerosSub t` (the subtype finset). The D-069 capstone says `∑ ρ ∈ nearZeros t, (zeroMult ρ : ℂ) / (s - ρ)` — nearZeros is the LiDisc ambient finset. Hmm — our Rexpr_decomp uses nearZerosSub. For the capstone, I should state it with nearZerosSub (cleaner for ii′-6 per the journal: \"the capstone's near sum is over the SUBTYPE finset — cleaner for ii′-6\"). Let me check what nearZeros is vs nearZerosSub... From LiDisc: nearZeros t is probably the ambient set/finset {ρ : IsNontrivialZero ρ ∧ |γ−t| < 1}. The journal-035 says the capstone uses the SUBTYPE finset. So state with nearZerosSub.\n\n**The assembly:**\n‖LHS‖ ≤ ‖logDeriv ζ s₀‖ + ‖near sum at s₀‖ + ‖far series‖ + ‖1/s − 1/s₀‖ + ‖1/(s−1) − 1/(s₀−1)‖ + ‖ψ-diff/2‖\n≤ 1 + (0.6L + 0.886LL + 2.7) + (12.1284·C0hat(t+1) + 7.2425) + 0.045 + 0.045 + 6/t\n\nwhere L = log(t+2), LL = log log(t+2), and C0hat(t+1) = 0.433·log(t+3) + 0.886·loglog(t+3) + 2.9.\n\nNeed: ≤ 10.5·log(t+2) + 48 (note |t| = t for t ≥ 10).\n\n**The fold:** C0hat(t+1) = 0.433·log(t+3) + 0.886·loglog(t+3) + 2.9. Convert to L/LL: log(t+3) ≤ L + 1/12 (t ≥ 10: log(t+3) = log(t+2) + log(1+1/(t+2)) ≤ L + 1/(t+2) ≤ L + 1/12); loglog(t+3) ≤ LL + (1/12)/log(t+2) ≤ LL + 1/(12·log 12) = LL + 0.03351 (log(t+2) ≥ log 12 ≥ 2.4849 — need log 12 ≥ 2.4849: 12 ≥ e^2.4849 = 12.0001·... hmm — e^2.4849 ≈ 12.0009 > 12 — so log 12 < 2.4849. Need log 12 ≥ 2.4848: e^2.4848 ≈ 11.9997 ≤ 12 ✓. Or log 12 ≥ 2.48: e^2.48 ≈ 11.94 ≤ 12 ✓. Use log 12 ≥ 2.4848 → 1/(12·2.4848) = 0.03353. Hmm — let me just use the D-069 journal's constants: \"C₀ = C0hat(t+1) ≤ 0.433L + 0.886LL + 2.9662 (the L' conversion)\". Check: 0.433·(L+1/12) + 0.886·(LL+0.0335) + 2.9 = 0.433L+0.886LL+2.9+0.0361+0.0297 = 0.433L+0.886LL+2.9658. The journal said 2.9662 (they used loglog-slack 0.0335·0.886 = 0.02969 + 0.433/12 = 0.03608: 2.9+0.03608+0.02969 = 2.96577 ≈ 2.9658). I'll use 2.9658.\n\nSo: piece3 ≤ 12.1284·(0.433L + 0.886LL + 2.9658) + 7.2425 = 5.2516L + 10.7461LL + 35.9650 + 7.2425 = 5.2516L + 10.7461LL + 43.2075.\n\nHmm wait — 12.1284·2.9658 = 35.9638·... let me compute: 12.1284·2.9658 = 35.9647·... 12·2.9658 = 35.5896; 0.1284·2.9658 = 0.38081; total 35.9704?? — let me compute carefully: 12.1284 × 2.9658: 12.1284 × 2 = 24.2568; ×0.9 = 10.91556; ×0.06 = 0.727704; ×0.005 = 0.060642; ×0.0008 = 0.0097027. Sum: 24.2568+10.91556+0.727704+0.060642+0.0097027 = 35.97041. Hmm — that's 35.9704, not 35.9638 (my earlier quick calc). Let me redo: 12.1284 × 2.9658 = 12.1284 × 2.9658. 12 × 2.9658 = 35.5896. 0.1284 × 2.9658 = 0.380809. Total = 35.97041. So piece3 ≤ 5.2516L + 10.7461LL + 35.9704 + 7.2425 = 5.2516L + 10.7461LL + 43.2129.\n\nAssembly: 1 + (0.6L+0.886LL+2.7) + (5.2516L+10.7461LL+43.2129) + 0.09 + 6/t ≤ 5.8516L + 11.6321LL + 47.0029 + 6/t.\n\nAt t = 10 (worst for the 6/t term): 6/10 = 0.6: total ≤ 5.8516L + 11.6321LL + 47.6029. And 6/t ≤ 0.6 for t ≥ 10 ✓ (uniformly).\n\nNeed ≤ 10.5L + 48 ⟺ 11.6321·LL − 4.6484·L ≤ 0.3971 for L ≥ log 12.\nf(L) = 11.6321·log L − 4.6484·L. f′(L) = 11.6321/L − 4.6484 = 0 at L* = 11.6321/4.6484 = 2.50240. f(L*) = 11.6321·log(2.50240) − 4.6484·2.50240 = 11.6321·0.916863 − 11.63215 = 10.66467 − 11.63215 = −0.96748. So f ≤ −0.9675 ≤ 0.3971 ✓ with margin ≈ 1.36.\n\n**The pinch lemma:** 11.6321·LL − 4.6484·L ≤ 0.3971 for all L ≥ log 12. Wait — I should double-check the boundary at L = log 12: f(log 12) = 11.6321·log(log 12) − 4.6484·log 12 = 11.6321·0.90939 − 11.55179 = 10.57873 − 11.55179 = −0.97306 ≤ 0.3971 ✓. And f has max −0.9675 at L*. So the pinch is: ∀ L ≥ log 12, 11.6321·log L − 4.6484·L ≤ 0.3971. Since max is −0.9675, the margin is 1.3646.\n\nProve: f(L*) ≤ 0.3971 where f attains its max at L* = 11.6321/4.6484 ≈ 2.50240. Actually — cleanest: prove f(L) ≤ −0.9 for L ≥ log 12 (giving margin), or directly f(L) ≤ 0.3971. The interior-max calculus: f′(L) = 11.6321/L − 4.6484: positive for L < L*, negative for L > L* ⟹ max at L*. Then evaluate f(L*) = 11.6321·(log(11.6321/4.6484) − 1) = 11.6321·(log L* − 1). Need log L* ≤ 1 + 0.3971/11.6321 = 1.034137 ⟺ L* ≤ e^1.034137 = 2.8133?? — no wait: f(L*) = 11.6321·log L* − 4.6484·L* with L* = 11.6321/4.6484 = 2.50240: = 11.6321·log(2.50240) − 11.6321 = 11.6321·(log 2.50240 − 1) = 11.6321·(0.916863 − 1) = 11.6321·(−0.083137) = −0.96705. So f(L*) = 11.6321·(log L* − 1) and I need 11.6321·(log L* − 1) ≤ 0.3971 ⟺ log L* ≤ 1 + 0.3971/11.6321 = 1.034137 ⟺ L* ≤ e^1.034137. But L* = 2.50240 ≤ e^1.034137 ≈ 2.81333 ✓ trivially with big margin. Even simpler: f(L*) = 11.6321·(log L* − 1) and log L* ≤ log 2.51 ≤ 0.92 (2.51 ≤ e^0.92 = 2.5093·... hmm e^0.92 = 2.50929 < 2.51 ✗ — log 2.51 ≥ 0.92: log L* = log(11.6321/4.6484) — bound L* ≤ 2.5024 ⟹ log L* ≤ log 2.5024 ≤ 0.9169 (2.5024 ≤ e^0.9169 = 2.50148·... ✗). Let me use: L* = 11.6321/4.6484 = 2.502399 ≤ 2.5024 ⟹ log L* ≤ log 2.5024 ≤ 0.91687: e^0.91687 = 2.50152·... < 2.5024 ✗ — need e^0.91687 ≥ 2.5024: e^0.91687 = 2.50152·... hmm the computation: e^0.91687 = ? e^0.9 = 2.459603, e^0.01687 = 1.017013: 2.459603·1.017013 = 2.501454 < 2.5024 ✗. So log 2.5024 > 0.91687. Use 0.9169: e^0.9169 = 2.501529·... still < 2.5024 ✗. log 2.5024 = 0.916872·... — so log L* ≈ 0.91687 exactly-ish. Then f(L*) = 11.6321·(0.91687 − 1) = −0.96748·... wait: 11.6321·(−0.08313) = −0.96717. So f(L*) ≈ −0.9672 ≤ 0.3971 ✓ with margin 1.36.\n\nFor the Lean proof, the cleanest pinch: prove f(L) ≤ −0.96 for L ≥ log 12 (margin 1.36 vs the needed 0.3971). Via: f(L) = 11.6321·log L − 4.6484·L; f has a unique critical point L* = 11.6321/4.6484 (f′ changes + to −); f(L*) = 11.6321·(log L* − 1) ≤ 11.6321·(0.9169 − 1) = −0.9666 ≤ −0.96?? — −0.9666 ≤ −0.96 ✓ barely — hmm tight. Let me not fixate: state the pinch as f(L) ≤ 0.3971 with the certified evaluation log L* ≤ 0.9169 giving f(L*) ≤ −0.9666 ≤ 0.3971 (margin 1.36 — the bound 0.3971 has margin; the certified log L* ≤ 0.9169 has margin ~3e-5 over true 0.916872... — need e^0.9169 ≥ L* = 2.50240: e^0.9169 = 2.50153·... < 2.5024 ✗✗ — log L* is EXACTLY 0.91687, and I need an UPPER bound on log L* — need e^U ≥ L* with U slightly larger: U = 0.917: e^0.917 = 2.459603·e^0.017 = 2.459603·1.017145 = 2.501779 < 2.5024 ✗. U = 0.9173: e^0.9173 = 2.459603·e^0.0173 = 2.459603·1.017451 = 2.502527 ≥ 2.5024 ✓. So log L* ≤ 0.9173. Then f(L*) ≤ 11.6321·(0.9173−1) = 11.6321·(−0.0827) = −0.96197. Hmm — that's −0.962, worse than −0.967 (the slack from the crude log bound). Then f ≤ −0.962 ≤ 0.3971 ✓ margin 1.359. Fine.\n\nHmm — actually, proving the pinch via the interior-max calculus in Lean is the painful part (finding/proving the critical point structure). ALTERNATIVE cleaner formulation: avoid the exact L*: prove f(L) ≤ −0.9 for L ≥ log 12 by a cruder argument:\n- For L ≥ 2.6: f(L) = 11.6321·log L − 4.6484·L ≤ 11.6321·(L/e·e·...)·... — log L ≤ L/2 for L ≥ 2.6? log L ≤ L/2 ⟺ 2 log L ≤ L ⟺ L² ≤ e^L: at L = 2.6: L² = 6.76 ≤ e^2.6 = 13.464 ✓ and (L²/e^L)′ = (2L−L²)/e^L = L(2−L)/e^L < 0 for L > 2 ⟹ L²/e^L decreasing ⟹ L²/e^L ≤ 6.76/13.464 = 0.5021 < 1 for L ≥ 2.6 ✓ hmm that gives L² ≤ e^L·0.5021-ish — not directly. log L ≤ L/2: at L = 2.6: log 2.6 = 0.9555 ≤ 1.3 ✓; and (L/2 − log L)′ = 1/2 − 1/L > 0 for L > 2 ✓ increasing ⟹ log L ≤ L/2 for L ≥ 2.6 ✓.\n  Then f(L) ≤ 11.6321·L/2 − 4.6484·L = L·(5.81605 − 4.6484) = 1.16765·L — POSITIVE and increasing — useless for large L. NO — that bound is too weak (log L ≤ L/2 loses too much; f → −∞ but the bound → +∞).\n- The max-calculus IS needed. OK.\n\nFor the interior max: the cleanest Lean approach: show f(L) ≤ f(L₀) + (integral of f′ where positive)?? no. Standard approach: f(L) ≤ max{f(log 12), f(L*)} evaluated — via: f is concave (f″(L) = −11.6321/L² < 0) ⟹ f ≤ tangent-line bound at any point: f(L) ≤ f(a) + f′(a)(L−a) for all L. Choose a = L* (f′(L*) = 0): f(L) ≤ f(L*). But proving f′(L*) = 0 needs L* = 11.6321/4.6484 exactly — and log L* ≤ 0.9173. So:\n- f concave: f″(L) < 0 (deriv of f′ = −11.6321/L² < 0).\n- f′(L) = 11.6321/L − 4.6484.\n- f(L) ≤ f(2.5024) for L ≥ log 12: case L ≤ 2.5024: f increasing on [log 12, 2.5024] ⟹ f(L) ≤ f(2.5024); case L ≥ 2.5024: f decreasing ⟹ f(L) ≤ f(2.5024).\n- f(2.5024) = 11.6321·log(2.5024) − 4.6484·2.5024 ≤ 11.6321·0.9173 − 11.63209 = 10.67218 − 11.63209 = −0.95991·... hmm: 4.6484·2.5024 = 11.63210·... (4.6484·2.5024 = 11.6320964·... interesting — 4.6484·2.5024 ≈ 11.6321 — because L* = 11.6321/4.6484 = 2.5023994·... so 4.6484·2.5024 = 11.63210·... = 11.6321025. And 11.6321·0.9173 = 10.67213·... f(2.5024) = 10.67213 − 11.63210 = −0.95997. So f(2.5024) ≤ −0.95997 ≤ 0.3971 ✓ margin 1.357.\n  Actually — I realize I can avoid the increasing/decreasing split: concavity gives f(L) ≤ f(a) + f′(a)(L−a) for ANY a. At a = 2.5024: f′(2.5024) = 11.6321/2.5024 − 4.6484 = 4.64836·... − 4.6484 = −0.00004·... ≈ −0.000035 — nearly zero but not exactly. f(L) ≤ f(2.5024) + f′(2.5024)·(L − 2.5024): for L ≥ 2.5024: f′ < 0-ish (negative tiny) ⟹ ≤ f(2.5024) + (negative)·(positive) ≤ f(2.5024) + small. Hmm — the tangent at a where f′(a) ≈ 0 but not exactly 0 — the tangent bound f(L) ≤ f(a) + f′(a)(L−a) holds for concave f at ALL L ✓ regardless of sign: for L ≥ a: f′(a)·(L−a) = (−0.000035)·(L−a) ≤ 0-ish ⟹ f(L) ≤ f(2.5024) ✓; for L ≤ a: f′(a)·(L−a) = (−0.000035)·(negative) = small positive ⟹ f(L) ≤ f(2.5024) + 0.000035·(a − log 12) ≤ f(2.5024) + 0.000035·0.0175 = tiny ✓. So f(L) ≤ f(2.5024) + 0.000001 ≤ 0.3971 ✓.\n  \n  Even simpler: choose a slightly off so f′(a) is EXACTLY describable: a = 2.5: f′(2.5) = 11.6321/2.5 − 4.6484 = 4.65284 − 4.6484 = 0.00444. Tangent at 2.5: f(L) ≤ f(2.5) + 0.00444·(L−2.5). For L ≥ 2.5: f decreasing after 2.5024 — the tangent bound still holds ✓: f(L) ≤ f(2.5) + 0.00444·(L−2.5): for L > L* this is f(2.5) + small·(L−2.5) — grows with L — USELESS for large L!! The tangent at a non-critical point is only useful one-sided. So the two-sided argument (increasing to L*, decreasing after) is needed, or the critical-point tangent (a = 2.5024 with f′ ≈ −0.00004: for L ≥ 2.5024: f′(a)(L−a) ≤ 0 ✓ f(L) ≤ f(2.5024); for log 12 ≤ L ≤ 2.5024: f′(a)(L−a) = (−0.00004)(L−2.5024) = 0.00004·(2.5024−L) ≤ 0.00004·(2.5024−2.4849) = 0.0000007 ✓). So with a = 2.5024: f(L) ≤ f(2.5024) + 0.0000007 for ALL L ≥ log 12 ✓. \n\nHmm — but f′(2.5024) = 11.6321/2.5024 − 4.6484 — I need to prove f′(2.5024) ≤ 0 (for the L ≥ 2.5024 side): 11.6321/2.5024 ≤ 4.6484 ⟺ 11.6321 ≤ 4.6484·2.5024 = 11.6321025·... ⟺ 11.6321 ≤ 11.6321025·... — 4.6484·2.5024 = 11.63210 (4.6484·2.5024 = 11.63210 16 — let me compute exactly: 4.6484 × 2.5024 = 4.6484 × 2.5 + 4.6484 × 0.0024 = 11.621 + 0.01115616 = 11.63215616·... wait: 4.6484×2.5 = 11.621; 4.6484×0.0024 = 0.01115616; sum = 11.63215616. So 11.6321 ≤ 11.63215616 ✓ TRUE (margin 5.6e-5). So f′(2.5024) ≤ 0 ✓ certified by norm_num on rationals ✓.\n\nOK so the pinch proof structure (one-variable calculus, no interior-max hunting):\n- f(L) := 11.6321·log L − 4.6484·L.\n- f′(L) = 11.6321/L − 4.6484.\n- For L ≥ 2.5024: f′(L) ≤ f′(2.5024) ≤ 0 (11.6321/L decreasing) ⟹ f decreasing on [2.5024, ∞) ⟹ f(L) ≤ f(2.5024).\n- For log 12 ≤ L ≤ 2.5024: f′(L) ≥ f′(2.5024) — that gives f′(L) ≥ (negative tiny) — NOT ≥ 0! f′(2.4849) = 11.6321/2.4849 − 4.6484 = 4.68036 − 4.6484 = 0.03196 ≥ 0; f′(2.5024) = −0.000035 ≤ 0. So f′ changes sign in [2.4849, 2.5024] — f increases then decreases — max somewhere in between, bounded by the tangent at 2.5024: f(L) ≤ f(2.5024) + f′(2.5024)·(L−2.5024) = f(2.5024) + (−0.000035)·(negative) = f(2.5024) + tiny ✓. The tangent-line bound f(L) ≤ f(a) + f′(a)(L−a) for concave f — this is `ConcaveOn.le_tangent`? Does Mathlib have concave-tangent lemmas? There might be `ConcaveOn.le_of_deriv...` or I prove it via the FTC: f(L) = f(a) + ∫_a^L f′(x)dx ≤ f(a) + f′(a)(L−a) (f′ decreasing ⟹ for x between a and L: f′(x) ≤ f′(a) when x ≥ a (L ≥ a); when L < a: f′(x) ≥ f′(a) for x ∈ [L, a], and ∫_L^a f′ ≥ f′(a)(a−L) ⟹ f(L) = f(a) − ∫_L^a f′ ≤ f(a) − f′(a)(a−L) = f(a) + f′(a)(L−a) ✓ same bound ✓). Provable via intervalIntegral with f′ decreasing (antitoneOn). That's the concave-tangent machine — I'd need to build it (~80 lines): \n  lemma tangent_bound (f f' : ℝ → ℝ) (hf'anti : AntitoneOn f' s) (hderiv : ∀ x ∈ interior s, HasDerivAt f (f' x) x) (ha : a ∈ s) (hL : L ∈ s) (convex s) : f L ≤ f a + f' a * (L − a).\n  Via: for L ≥ a: ∫_a^L f' ≤ f' a·(L−a) (integral_mono_on with f' x ≤ f' a on [a, L] using anti) ⟹ f L − f a ≤ f' a (L−a) ⟹ f L ≤ f a + f' a(L−a) ✓. For L ≤ a: ∫_L^a f' ≥ f' a·(a−L) ⟹ f a − f L ≥ f' a(a−L) ⟹ f L ≤ f a − f' a(a−L) = f a + f' a(L−a) ✓.\n  With the FTC for both directions (integral_eq_sub_of_hasDerivAt ✓ used all over this file).\n\n- f(2.5024) ≤ 0.3971: f(2.5024) = 11.6321·log 2.5024 − 11.63215616·... ≤ 11.6321·0.9173 − 11.63215616 = 10.672126 − 11.632156 = −0.960030·... compute: 11.6321·0.9173 = 10.672126·... (11.6321·0.9173 = 10.67212·... 11.6321·0.9173: 11.6321·0.9 = 10.46889; ·0.0173 = 0.201235: sum 10.670125·... hmm let me recompute: 11.6321 × 0.9173: 11.6321 × 0.9 = 10.46889; 11.6321 × 0.017 = 0.1977457; 11.6321 × 0.0003 = 0.00348963; total 10.46889+0.1977457+0.00348963 = 10.67012533. And 4.6484·2.5024 = 11.63215616. f(2.5024) = 10.67012533 − 11.63215616 = −0.96203083. So f(2.5024) ≤ −0.96203 ≤ 0.3971 ✓ margin 1.359.\n  Certified: log 2.5024 ≤ 0.9173 ⟺ 2.5024 ≤ e^0.9173: e^0.9173 ≥ Σ_{k<8} 0.9173^k/k! = ? e^0.9173 ≈ 2.502527. Partial sum k<8: 1+0.9173+0.420719+0.128645+0.029507+0.005413+0.000828+0.000108 = 2.502520 ≥ 2.5024 ✓ margin 1.2e-4 ✓.\n\nSo the pinch: ∀ L ≥ log 12: 11.6321·log L − 4.6484·L ≤ 0.3971 (via the tangent at a = 2.5024, f(2.5024) ≤ −0.96203, plus the tangent-correction for L ∈ [log 12, 2.5024]: f(L) ≤ f(2.5024) + f′(2.5024)·(L − 2.5024) with f′(2.5024) = 11.6321/2.5024 − 4.6484 ≤ −0.00005-ish: for L ≤ 2.5024: correction = f′(2.5024)·(L−2.5024) = (negative)·(negative) = positive tiny: |correction| ≤ |f′(2.5024)|·(2.5024 − 2.4849) ≤ 0.00005·0.0175 = 0.0000009 ✓ negligible — the total ≤ −0.96203 + 0.0000009 ≤ 0.3971 ✓.\n\nHmm wait — I need f′(2.5024) EXACTLY: f′(2.5024) = 11.6321/2.5024 − 4.6484 = 4.6483785·... − 4.6484 = −0.0000215·... let me compute: 11.6321/2.5024 = 4.648378·... 2.5024·4.6484 = 11.63215616 (from before): so 11.6321/2.5024 = 11.6321/2.5024: since 2.5024·4.6484 = 11.63215616 > 11.6321, we have 11.6321/2.5024 < 4.6484 ⟹ f′(2.5024) = 11.6321/2.5024 − 4.6484 < 0 ✓ — and the exact value: 11.6321/2.5024 = 11.6321/2.5024 ≈ 4.6483746: f′ ≈ −0.0000254. |correction| ≤ 0.0000254·0.0175 = 4.4e-7 ✓.\n\nFor the tangent bound applied to L ∈ [log 12, 2.5024]: f(L) ≤ f(2.5024) + f′(2.5024)·(L−2.5024): f′(2.5024) = 11.6321/2.5024 − 4.6484 — is that ≤ 0? need 11.6321 ≤ 4.6484·2.5024 = 11.63215616 ✓ (margin 5.6e-5 ✓ norm_num). So f′(2.5024) ≤ 0: then for L ≤ 2.5024: f′(2.5024)·(L−2.5024) = (neg)·(nonpos) ≥ 0 — bounded by |f′|·(2.5024−log 12): |f′(2.5024)| = 4.6484 − 11.6321/2.5024 = (4.6484·2.5024 − 11.6321)/2.5024 = (11.63215616 − 11.6321)/2.5024 = 0.00005616/2.5024 = 0.00002244. ×0.0175 = 3.9e-7 ✓. So f(L) ≤ f(2.5024) + 3.9e-7 ≤ −0.96203 + 0.0000004 ≤ 0.3971 ✓.\n\nHmm — actually the tangent bound already handles both sides uniformly: f(L) ≤ f(a) + f′(a)(L−a) for ALL L (concavity). For L ∈ [log 12, 2.5024]: f′(a)·(L−a) ≤ |f′(a)|·(a − log 12) ≤ 3.9e-7; for L ≥ 2.5024: f′(a)·(L−a) ≤ 0 ✓ (f′(a) ≤ 0, L−a ≥ 0). So f(L) ≤ f(a) + max(0, |f′(a)|·(a − log 12)) ≤ −0.96203 + 0.0000004 ≤ 0.3971. In Lean: state as f(L) ≤ f(a) + f′(a)·(L−a) (the tangent lemma) then bound the correction case-split.\n\nHmm — actually simpler: f(L) ≤ f(2.5024) + f′(2.5024)·(L−2.5024) — for L ≥ 2.5024: the correction is ≤ 0 ⟹ f(L) ≤ f(2.5024) ≤ −0.96203 ≤ 0.3971 ✓. For L ∈ [log 12, 2.5024]: correction ≤ |f′(2.5024)|·0.0175 ≤ 3.9e-7 ⟹ f(L) ≤ −0.96203+3.9e-7 ≤ 0.3971 ✓. Good.\n\nHmm, wait — actually, let me reconsider whether I even need the tangent machinery. ALTERNATIVE simpler pinch: use f(L) ≤ max over the two-sided split:\n- On [log 12, 2.5024]: f(L) ≤ f(2.5024) + (max f′ on the interval)·(L − ...)·... no — f(L) ≤ f(2.5024) + max(0, sup f′)·0.0175: f′ on [log 12, 2.5024] ≤ f′(log 12) = 0.03196 (f′ decreasing) ⟹ f(L) = f(2.5024) − ∫_L^{2.5024} f′ ≥ f(2.5024) − 0.03196·0.0175·... NO: f(L) ≤ f(2.5024) requires ∫_L^{2.5024} f′ ≥ 0 — but f′ goes negative near 2.5024 — so f(L) could exceed f(2.5024)?? No wait — if f increases to L* then decreases: for L < L*: f(L) < f(L*) — the max is at L*, not 2.5024. f(L*) − f(2.5024) = ∫_{L*}^{2.5024} f′ ≤ 0·... = negative — so f(L*) ≥ f(2.5024)!! The max f(L*) > f(2.5024) by ∫_{L*}^{2.5024}(−f′) = small. So the bound f ≤ f(2.5024) + (area between) — the area = ∫_{L*}^{2.5024} (−f′) ≤ |f′(2.5024)|·(2.5024−L*)·... = the triangle ½·|f′(2.5024)|·(2.5024−L*) — L* ≈ 2.502399, 2.5024−L* ≈ 0.0000006 — TINY. So f(L*) ≈ f(2.5024) + ε with ε ≈ ½·0.0000254·0.0000006 ≈ 8e-12 — negligible.\n  The CLEANEST uniform statement: f(L) ≤ f(2.5024) + 0.0000005 for L ≥ log 12 — via: for L ∈ [log 12, 2.5024]: f(L) − f(2.5024) = −∫_L^{2.5024} f′(x)dx ≤ ∫_L^{2.5024} |f′(x)| dx ≤ 0.03196·0.0175 = 0.00056 — hmm that gives f(L) ≤ f(2.5024)+0.00056 — the 0.03196 bound is at the LEFT edge (loose). The tighter: |f′| on [log 12, 2.5024] ≤ max(f′(log 12), |f′(2.5024)|) = max(0.03196, 0.0000254) = 0.03196: area ≤ 0.03196·0.0175 = 0.000559 — so f(L) ≤ f(2.5024)+0.000559 ≤ −0.96203+0.000559 = −0.96147 ≤ 0.3971 ✓ margin 1.359. GOOD — this avoids the tangent lemma subtleties: \n  - For L ∈ [log 12, 2.5024]: f(L) ≤ f(2.5024) + ∫_L^{2.5024} |f′| ≤ f(2.5024) + 0.03196·0.0175. (The ∫ of |f′| — messy to formalize with abs; alternative: f(L) − f(2.5024) = −∫_L^{2.5024} f′ — and f′(x) ≥ f′(2.5024) for x ≤ 2.5024 (f′ decreasing ⟹ f′(x) ≥ f′(2.5024)?? f′ decreasing means x smaller ⟹ f′(x) LARGER: for x ∈ [L, 2.5024]: f′(x) ≥ f′(2.5024) — so −f′(x) ≤ −f′(2.5024) = |f′(2.5024)| ≈ 0.0000254: f(L) − f(2.5024) = −∫ f′ ≤ −f′(2.5024)·(2.5024−L) ≤ 0.0000254·0.0175 = 4.4e-7 ✓✓ — even better and NO abs needed: f(L) ≤ f(2.5024) + (−f′(2.5024))·(2.5024−L) with −f′(2.5024) = 4.6484 − 11.6321/2.5024 = 0.0000254-ish ≥ 0.)\n  - For L ≥ 2.5024: f(L) ≤ f(2.5024) (f decreasing: f′(x) ≤ f′(2.5024) ≤ 0 for x ≥ 2.5024).\n\nSo the pinch formalization needs:\n(i) f and f′ with HasDerivAt (log/differentiable pieces).\n(ii) f′ antitone on Ici (log 12) (11.6321/L antitone + const).\n(iii) The FTC direction bounds (both sides) — via integral_eq_sub_of_hasDerivAt + integral_mono_on with the f′ bounds.\n(iv) f(2.5024) ≤ −0.96203 (certified: log 2.5024 ≤ 0.9173 via exp partial sums + 4.6484·2.5024 ≥ 11.6321 norm_num).\n(v) f′(2.5024) ≤ 0 certified (11.6321 ≤ 4.6484·2.5024 = 11.63215616 norm_num).\n\nThen the FINAL capstone assembly:\n‖LHS‖ ≤ 1 + (0.6L+0.886LL+2.7) + (12.1284·C0hat(t+1)+7.2425) + 0.045+0.045+6/t\nwith C0hat(t+1) ≤ 0.433·(L+1/12) + 0.886·(LL+0.0335) + 2.9 = 0.433L+0.886LL+2.9658.\nHmm wait — the loglog(t+3) conversion: loglog(t+3) ≤ LL + 0.0335: loglog(t+3) = log(log(t+3)) ≤ log(log(t+2) + 1/12) ≤ loglog(t+2) + (1/12)/log(t+2) = LL + 1/(12·log(t+2)) ≤ LL + 1/(12·log 12) = LL + 0.03350 (log 12 ≥ 2.4848: 12 ≥ e^2.4848 ⟺ e^2.4848 ≤ 12: e^2.4848 = e²·e^0.4848 ≤ 7.3890566·1.6238 = 11.9982 ≤ 12 ✓ (e^0.4848 ≤ 1.6238: partial sums? e^0.4848 ≈ 1.62381 — need e^0.4848 ≤ 1.6239: partial sum Σ_{k<7}: 1+0.4848+0.117516+0.018992+0.002302+0.000223 = 1.623833 ≤ 1.6239 ✓; then 7.3890566·1.6239 = 11.99931 ≤ 12 ✓). Hmm — need log 12 ≥ 2.4848: 1/(12·2.4848) = 0.03351. So loglog-slack ≤ 0.03351. And log(t+3) ≤ L + 1/12: log(t+3) = log((t+2)(1+1/(t+2))) = L + log(1+1/(t+2)) ≤ L + 1/(t+2) ≤ L + 1/12 ✓ (log(1+u) ≤ u; 1/(t+2) ≤ 1/12 ✓).\nC0hat(t+1) ≤ 0.433·(L+1/12) + 0.886·(LL+0.03351) + 2.9 = 0.433L+0.886LL+2.9+0.036083+0.029690 = 0.433L+0.886LL+2.965773. Use C0hat(t+1) ≤ 0.433L+0.886LL+2.9658.\n\nHmm — actually, is it cleaner to AVOID the L/LL conversion and state the pinch DIRECTLY in terms of log(t+3)/loglog(t+3)? The assembly becomes:\ntotal ≤ 1 + (0.6·log(t+2)+0.886·loglog(t+2)+2.7) + (12.1284·(0.433·log(t+3)+0.886·loglog(t+3)+2.9)+7.2425) + 0.09 + 6/t\n≤ 10.5·log(t+2) + 48.\nThe mixed forms (log(t+2) vs log(t+3)) — the pinch would need to relate them anyway. The L/LL conversion is cleaner. Let me do the conversion as a lemma:\n```\nlemma C0hat_le_of_ten_le {t : ℝ} (ht : 10 ≤ t) :\n    C0hat (t + 1) ≤ 0.433 * (Real.log (t + 2) + 1 / 12)\n      + 0.886 * (Real.log (Real.log (t + 2)) + 0.03351) + 2.9\n```\nThen piece3 ≤ 12.1284·(0.433·(L+1/12)+0.886·(LL+0.03351)+2.9)+7.2425 = 12.1284·(0.433L+0.886LL+2.96578)+7.2425 — with 0.433/12 = 0.036083 and 0.886·0.03351 = 0.029690: 2.9+0.036083+0.029690 = 2.965773.\n= 5.2516L + 10.7461LL + 35.96864 + 7.2425 = 5.2516L + 10.7461LL + 43.21114.\nTotal: 1 + (0.6L+0.886LL+2.7) + (5.2516L+10.7461LL+43.21114) + 0.09 + 6/t\n= 5.8516L + 11.6321LL + 47.00114 + 6/t ≤ 5.8516L + 11.6321LL + 47.60114 (6/t ≤ 0.6).\nNeed ≤ 10.5L + 48 ⟺ 11.6321·LL − 4.6484·L ≤ 0.39886.\nPinch: 11.6321·LL − 4.6484·L ≤ 0.39886 for L ≥ log 12 — max −0.962 ✓ margin 1.36 ✓.\n\nSo the pinch lemma to prove: `pinch_tight_R : ∀ L ≥ Real.log 12, 11.6321 * Real.log L - 4.6484 * L ≤ 0.3989`.\n\nAnd the pieces for the final theorem:\n- piece 1: ‖logDeriv riemannZeta (2+tI)‖ ≤ dirichletC2 ≤ 1: `norm_logDeriv_zeta_le_dirichlet` (LiCircleBound: ‖ζ′/ζ‖ ≤ dirichletC2 for re ≥ 2: re(2+tI) = 2 ✓) + dirichletC2_le_one.\n- piece 2: near_sum_refPoint_le hZC2 ht.\n- piece 3: far_series_le hZC hNLZ ht hσlo hσhi him hζ.\n- pieces 4/5: one_div_diff_le ht hσlo hσhi him hs0 (s ≠ 0 — from hζ: s ≠ 0 since ζ(0) = ... hmm — s ≠ 0: one_div_diff_le needs hs0 : s ≠ 0: s = 0 ⟹ ζ(0) = −1/2 ≠ 0?? — ζ(0) = −1/2 (riemannZeta_zero : riemannZeta 0 = −1/2 ✓) — so hζ : ζ s ≠ 0 doesn't exclude s = 0!! If s = 0: ζ(0) = −1/2 ≠ 0 ✓ consistent — so s could be 0?? — but s.im = t ≥ 10 ⟹ s ≠ 0 ✓ (im ≠ 0). Prove s ≠ 0 via im: s.im = t ≥ 10 ≠ 0 ⟹ s ≠ 0 ✓.)\n- piece 6: digamma_diff_le ht hσlo hσhi him.\n\nThe decomposition Rexpr_decomp (hZC) (hs : ζ s ≠ 0) (hs0 : s ≠ 0) (hs1 : s ≠ 1) (hst : ∀ n ≥ 1, s ≠ −2n) (hs₀ : ζ s₀ ≠ 0) (hs₀0 : s₀ ≠ 0) (hs₀1 : s₀ ≠ 1) (hs₀t : ∀ n ≥ 1, s₀ ≠ −2n) (t):\n- s's conditions: hζ ✓ (given), s ≠ 0 (via im), s ≠ 1 (im = t ≠ 0 ⟹ s ≠ 1 ✓), s ≠ −2n (im = t ≠ 0 ⟹ ✓).\n- s₀ = 2+tI's conditions: ζ s₀ ≠ 0 (re s₀ = 2: ζ ≠ 0 for re > 1: `riemannZeta_ne_zero_of_one_le_re` (banked from session-033 usage: takes ONLY re ✓): re(2+tI) = 2 ≥ 1 ✓); s₀ ≠ 0 (re = 2); s₀ ≠ 1 (re = 2); s₀ ≠ −2n (re = 2 > 0 ✓ vs −2n ≤ −2 ✓).\n\nThen:\n‖logDeriv ζ s − near-sum‖ = ‖logDeriv ζ s₀ − near-sum₀ + far − elem1 − elem2 − digdiff‖\n≤ ‖logDeriv ζ s₀‖ + ‖near-sum₀‖ + ‖far‖ + ‖elem1‖ + ‖elem2‖ + ‖digdiff‖\nvia the norm-chain (Rexpr_decomp's equality + norm_add/sub chains).\n\nLet me now also figure out the pinch's formalization concretely. The pinch lemma:\n```\nlemma pinch_tight_R {L : ℝ} (hL : Real.log 12 ≤ L) :\n    11.6321 * Real.log L - 4.6484 * L ≤ 0.3989 := by\n  -- f := fun L => 11.6321·log L − 4.6484·L\n  -- f' := fun L => 11.6321/L − 4.6484\n  -- HasDerivAt f (f' x) x for x > 0\n  -- f' antitone on Ici (log 12)\n  -- case split at 2.5024\n  · for L ≥ 2.5024: f decreasing ⟹ f(L) ≤ f(2.5024) ≤ −0.96203 ≤ 0.3989\n  · for log 12 ≤ L ≤ 2.5024: f(L) ≤ f(2.5024) + (−f′(2.5024))·(2.5024−L) ≤ −0.96203+0.0001 ≤ 0.3989\n```\nThe FTC bounds:\n- L ≥ 2.5024: f(L) − f(2.5024) = ∫_{2.5024}^L f′ ≤ ∫_{2.5024}^L 0·... hmm — need ∫_{2.5024}^L f′(x)dx ≤ 0: f′(x) ≤ f′(2.5024) ≤ 0 for x ≥ 2.5024 (f′ antitone: x ≥ a ⟹ f′(x) ≤ f′(a) ✓) — so ∫ ≤ 0 via integral_nonpos_of_nonpos? or integral_mono_on with the zero function: ∫ f′ ≤ ∫ 0 = 0 (f′(x) ≤ f′(2.5024) ≤ 0 — bound by f′(2.5024) ≤ 0: ∫ f′ ≤ f′(2.5024)·(L−2.5024) ≤ 0 ✓ — or directly f′(x) ≤ 0 ⟹ ∫ ≤ 0 ✓ — cleanest: intervalIntegral.integral_nonpos_of_nonpos (integrable) (∀ x, f′ x ≤ 0 on [2.5024, L])? — there's `intervalIntegral.integral_nonpos_of_nonpos`? or use integral_mono_on with g = 0.\n- log 12 ≤ L ≤ 2.5024: f(L) − f(2.5024) = −∫_L^{2.5024} f′ and f′(x) ≥ f′(2.5024) for x ≤ 2.5024 (f′ antitone: x ≤ a ⟹ f′(x) ≥ f′(a) ✓): −∫_L^{2.5024} f′ ≤ −f′(2.5024)·(2.5024−L) (integral_mono_on with f′(x) ≥ f′(2.5024): ∫_L^{2.5024} f′ ≥ f′(2.5024)·(2.5024−L) ⟹ −∫ ≤ −f′(2.5024)·(2.5024−L) ✓).\n\nSo I need a small FTC+monotone-integral lemma pair, or just inline both via integral_eq_sub_of_hasDerivAt + intervalIntegral.integral_mono_on. The integral_eq_sub_of_hasDerivAt (used all over) gives ∫_a^L f′ = f(L) − f(a). Then:\n- L ≥ a: ∫_a^L f′ ≤ ∫_a^L (fun _ => f′ a) = f′ a·(L−a): intervalIntegral.integral_mono_on (h : a ≤ L) (hf'int) (hconst-int) (∀ x ∈ Icc a L, f′ x ≤ f′ a) — with f′ antitone on Icc a L: x ≥ a ⟹ f′ x ≤ f′ a ✓.\n- L ≤ a: ∫_L^a f′ ≥ ∫_L^a (fun _ => f′ a) = f′ a·(a−L): intervalIntegral.integral_mono_on (h : L ≤ a) ... (∀ x ∈ Icc L a, f′ a ≤ f′ x) — f′ antitone: x ≤ a ⟹ f′ a ≤ f′ x ✓. Then f(L) − f(a) = −∫_L^a f′ ≤ −f′ a·(a−L) ✓.\n\nThe f′ antitone on Ici (log 12): f′(x) = 11.6321/x − 4.6484: 11.6321/x antitone for x > 0 (one_div_le_one_div_of_le + const-mul nonneg) ✓.\n\nAnd f(2.5024) ≤ −0.96203: 11.6321·log 2.5024 − 4.6484·2.5024: log 2.5024 ≤ 0.9173 (exp partial sums, e^0.9173 ≥ 2.5024) and 4.6484·2.5024 ≥ 11.6321 (norm_num: 4.6484·2.5024 = 11.63215616 ≥ 11.6321 ✓): 11.6321·log 2.5024 − 4.6484·2.5024 ≤ 11.6321·0.9173 − 11.63215616·... wait — 4.6484·2.5024 = 11.63215616: f(2.5024) = 11.6321·log(2.5024) − 11.63215616 ≤ 11.6321·0.9173 − 11.63215616 = 10.670125 − 11.632156 = −0.962031 ≤ −0.96203. Hmm — the certified: 11.6321·0.9173 = 10.67013·... norm_num: 11.6321·0.9173 = 10.67012·... let me compute exactly: 11.6321 × 0.9173 = 10.67012·... 116321 × 9173 = 116321×9000 = 1,046,889,000; ×173 = 20,123,533; total 1,067,012,533 → 10.67012533. So f(2.5024) ≤ 10.67012533 − 11.63215616 = −0.96203083 ≤ −0.96203 (norm_num can verify −0.96203083 ≤ −0.96203?? — −0.96203083 < −0.96203 ✓ since −0.96203083 is more negative ✓).\n\nAnd f′(2.5024) ≤ 0: 11.6321/2.5024 ≤ 4.6484 ⟺ 11.6321 ≤ 4.6484·2.5024 = 11.63215616 ✓ norm_num.\n\nNow the capstone:\n```\ntheorem logDeriv_riemannZeta_sub_nearZeros_le_tight\n    (hZC : ZeroCountProp) (hZC2 : ZeroCountProp2) (hNLZ : NoLowZeros)\n    {t : ℝ} (ht : 10 ≤ t) {s : ℂ}\n    (hσlo : -5 / 2 ≤ s.re) (hσhi : s.re ≤ 3) (him : s.im = t)\n    (hζ : riemannZeta s ≠ 0) :\n    ‖logDeriv riemannZeta s\n        - ∑ ρ ∈ nearZerosSub t, (zeroMult ρ.1 : ℂ) / (s - ρ.1)‖\n      ≤ 10.5 * Real.log (|t| + 2) + 48\n```\n(note |t| = t for t ≥ 10: abs_of_nonneg.)\n\nThe assembly:\n```\n  have hdec := Rexpr_decomp hZC hs hs0 hs1 hst hs₀ hs₀0 hs₀1 hs₀t t\n  -- hdec : logDeriv ζ s − nearsum = logDeriv ζ s₀ − nearsum₀ + far − e1 − e2 − dig\n  have h1 : ‖logDeriv riemannZeta (2 + t * Complex.I)‖ ≤ dirichletC2 :=\n    norm_logDeriv_zeta_le_dirichlet (by simp : (2 : ℝ) ≤ (2 + t * Complex.I).re)\n  have h1b := dirichletC2_le_one\n  have h2 := near_sum_refPoint_le hZC2 ht\n  have h3 := far_series_le hZC hNLZ ht hσlo hσhi him hζ\n  have h45 := one_div_diff_le ht hσlo hσhi him hs0\n  have h6 := digamma_diff_le ht hσlo hσhi him\n  -- the norm chain\n  have hnorm : ‖logDeriv riemannZeta s - ∑ ρ ∈ nearZerosSub t, (zeroMult ρ.1 : ℂ) / (s - ρ.1)‖\n      ≤ ‖logDeriv riemannZeta (2 + t * Complex.I)‖\n        + ‖∑ ρ ∈ nearZerosSub t, (zeroMult ρ.1 : ℂ) / ((2 + t * Complex.I) - ρ.1)‖\n        + ‖∑' ρ : {ρ : ℂ // IsNontrivialZero ρ}, if ρ ∈ nearZerosSub t then (0:ℂ) else seriesDiffTerm s (2 + t * Complex.I) ρ‖\n        + ‖1 / s - 1 / (2 + t * Complex.I)‖\n        + ‖1 / (s - 1) / ... wait — the decomposition has − (1/s − 1/s₀) − (1/(s−1) − 1/(s₀−1)) − (ψ-diff)/2 — norms of each ✓\n        + ‖(Complex.digamma (s / 2) - Complex.digamma ((2 + t * Complex.I) / 2)) / 2‖ := by\n    rw [hdec]\n    -- norm of the RHS sum\n    ...norm_add_le chains...\n  -- the fold\n  ...\n```\nThe norm chain: ‖A + B + C + D + E‖ ≤ ‖A‖+‖B‖+‖C‖+‖D‖+‖E‖ where the decomposition's RHS is (logDeriv ζ s₀ − nearsum₀) + far − e1 − e2 − dig: write as A + far − e1 − e2 − dig with A = logDeriv ζ s₀ − nearsum₀: ‖A‖ ≤ ‖logDeriv ζ s₀‖ + ‖nearsum₀‖; ‖A + far − e1 − e2 − dig‖ ≤ ‖A‖+‖far‖+‖e1‖+‖e2‖+‖dig‖ via norm_add_le/norm_sub_le chains. Then the fold with the pieces.\n\nHmm — the decomposition's exact form (Rexpr_decomp):\n```\nlogDeriv ζ s − nearsum\n  = logDeriv ζ s₀ − nearsum₀ + far − (1/s − 1/s₀) − (1/(s−1) − 1/(s₀−1)) − (ψ(s/2) − ψ(s₀/2))/2\n```\nSo: LHS norm = ‖logDeriv ζ s₀ − nearsum₀ + far − e1 − e2 − dig‖.\n\nThe final numeric assembly:\n‖LHS‖ ≤ 1 + (0.6L + 0.886LL + 2.7) + (12.1284·C0hat(t+1) + 7.2425) + 0.045 + 0.045 + 6/t\nwith C0hat(t+1) ≤ 0.433·(L+1/12)+0.886·(LL+0.03351)+2.9:\n= 1 + 0.6L+0.886LL+2.7 + (12.1284·(0.433·(L+1/12)+0.886·(LL+0.03351)+2.9)+7.2425) + 0.09 + 6/t\nLet me compute the constants:\n12.1284·(0.433·(L+1/12)) = 5.2516·L + 12.1284·0.433/12 = 5.2516L + 0.437513.\n12.1284·(0.886·(LL+0.03351)) = 10.7461·LL + 12.1284·0.886·0.03351 = 10.7461LL + 0.360137.\n12.1284·2.9 = 35.17236.\npiece3 ≤ 5.2516L + 10.7461LL + (0.437513+0.360137+35.17236+7.2425) = 5.2516L+10.7461LL+43.21251.\nTotal: 1 + 0.6L+0.886LL+2.7 + 5.2516L+10.7461LL+43.21251 + 0.09 + 0.6 (6/t ≤ 0.6)\n= 5.8516L + 11.6321LL + 47.60251.\nNeed ≤ 10.5L + 48 ⟺ 11.6321·LL − 4.6484·L ≤ 0.39749.\nPinch: 11.6321·LL − 4.6484·L ≤ 0.39749 for L ≥ log 12. Max −0.962 ✓ margin 1.36 ✓. So the pinch bound 0.39749 works — use 0.3975 for cleanliness.\n\nHmm — wait, earlier I computed piece3's constant differently (43.21114 vs 43.21251). Let me recompute carefully: piece3 ≤ 12.1284·C0hat(t+1) + 7.2425 with C0hat(t+1) ≤ 0.433·(L+1/12)+0.886·(LL+0.03351)+2.9:\n12.1284·0.433 = 5.25161·... (12.1284·0.433 = 5.25161·... compute: 12.1284·0.433 = 5.25161·... 12.1284·0.4 = 4.85136; ·0.03 = 0.363852; ·0.003 = 0.0363852: total 4.85136+0.363852+0.0363852 = 5.2515972. So 5.2515972 ≈ 5.2516.)\n12.1284·0.433/12 = 5.2515972/12 = 0.4376331.\n12.1284·0.886 = 10.7457624·... (12.1284·0.886 = 10.745762·... 12.1284·0.8 = 9.70272; ·0.08 = 0.970272; ·0.006 = 0.0727704: total 10.7457624.)\n12.1284·0.886·0.03351 = 10.7457624·0.03351 = 0.360090·... (10.7457624·0.03351 = 0.360091·... 10.7457624·0.03 = 0.3223729; ·0.003 = 0.0322373; ·0.0005 = 0.00537288; ·0.00001 = 0.000107458: total 0.3223729+0.0322373+0.00537288+0.000107458 = 0.360090538.)\n12.1284·2.9 = 35.17236.\npiece3-constant: 0.4376331+0.3600905+35.17236+7.2425 = 43.2125836.\nTotal: 1+2.7+43.2125836+0.09+0.6 = 47.6025836. Need ≤ 48 ⟺ 11.6321·LL − 4.6484·L ≤ 48 − 47.6025836 = 0.3974164. Use pinch bound 0.3975 ✓ margin 1.36.\n\nAlso — wait — the LL coefficient: 0.886 (piece 2) + 10.7461 (piece 3) = 11.6321 ✓. And L coefficient: 0.6+5.2516 = 5.8516 ✓ 10.5−5.8516 = 4.6484 ✓.\n\nNow the loglog-slack 0.03351: loglog(t+3) ≤ LL + 1/(12·log(t+2)) with log(t+2) ≥ log 12 ≥ 2.4848: 1/(12·2.4848) = 0.033505·... compute: 1/(12·2.4848) = 1/29.8176 = 0.033537·... hmm: 12·2.4848 = 29.8176: 1/29.8176 = 0.0335371. So the slack is 0.03354 not 0.03351!! Let me recompute: log(t+3) ≤ L + 1/(t+2) ≤ L + 1/12. loglog(t+3) = log(log(t+3)) ≤ log(L + 1/12) ≤ LL + (1/12)/L (log(a+c) ≤ log a + c/a with a = L, c = 1/12) ≤ LL + 1/(12·L) ≤ LL + 1/(12·log 12) = LL + 1/(12·2.4848) = LL + 0.0335371. So slack = 0.03354. Then C0hat(t+1) ≤ 0.433·(L+1/12)+0.886·(LL+0.03354)+2.9 = 0.433L+0.886LL+2.9+0.0360833+0.0297164 = 0.433L+0.886LL+2.9657997. piece3-constant: 12.1284·2.9657997 = 35.96999·... = 12.1284·0.433/12 + 12.1284·0.886·0.03354 + 12.1284·2.9: 0.4376331 + 10.7457624·0.03354 (0.360394) + 35.17236 = 0.4376331+0.3603944+35.17236 = 35.9703875. +7.2425 = 43.2128875. Total: 1+2.7+43.2128875+0.09+0.6 = 47.6028875. Need ⟺ f ≤ 0.3971125. Pinch bound 0.3975 ✓ still fine (margin 1.36).\n\nAnd log 12 ≥ 2.4848: certify: 12 ≥ e^2.4848 ⟺ e^2.4848 ≤ 12: e^2.4848 = e²·e^0.4848: e^0.4848 ≤ 1.6239 (partial sums Σ_{k<7} 0.4848^k/k! = 1+0.4848+0.117516+0.018992+0.002302+0.000223+0.0000180 = 1.623851 ≤ 1.6239 ✓); 7.3890566·1.6239 = 11.99931 ≤ 12 ✓. So log 12 ≥ 2.4848 via Real.le_log_iff_exp_le (12 > 0): 12 ≥ e^2.4848 ⟹ log 12 ≥ 2.4848 ✓.\n\nHmm wait — for the pinch I need L ≥ log 12 (not just 2.4848): the pinch is stated for L = log(t+2) ≥ log 12 ✓ (t ≥ 10 ⟹ t+2 ≥ 12 ✓ log monotone).\n\nAlso for the pinch's antitone domain Ici (log 12) — f′ antitone on Ici (log 12) ✓ (11.6321/x antitone for x ≥ log 12 > 0 ✓).\n\nLet me also decide the pinch statement form: `pinch_tight_R {L : ℝ} (hL : Real.log 12 ≤ L) : 11.6321 * Real.log L - 4.6484 * L ≤ 0.3975`.\n\nThe capstone's final fold:\n```\n  have hfin : 5.8516 * L + 11.6321 * LL + 47.6029 ≤ 10.5 * L + 48 := by\n    have hpinch := pinch_tight_R hL\n    linarith [hpinch]\n```\n— linarith with the pinch (11.6321·LL − 4.6484·L ≤ 0.3975 as atoms LL, L) ✓ linear ✓.\n\nLet me now write the whole 5f-iii as section 20. Structure:\n1. `log_twelve_ge : (2.4848 : ℝ) ≤ Real.log 12` (via e^2.4848 ≤ 12: e²·e^0.4848 ≤ 7.3890566·1.6239 ≤ 12 — reuse he2sq-ish pattern).\n2. `C0hat_le_of_ten_le {t} (ht : 10 ≤ t) : C0hat (t + 1) ≤ 0.433 * (Real.log (t + 2) + 1 / 12) + 0.886 * (Real.log (Real.log (t + 2)) + 0.03354) + 2.9`.\n3. The FTC-machine for the pinch: f, f', HasDerivAt, f' antitone, the two-sided bounds.\n4. `log_two_point_five_zero_two_four_le : Real.log 2.5024 ≤ 0.9173` (exp partial sums).\n5. `pinch_tight_R`.\n6. The capstone `logDeriv_riemannZeta_sub_nearZeros_le_tight`.\n\nFor the FTC machine — let me write a generic lemma:\n```\nlemma pinch_of_antitone {f f' : ℝ → ℝ} {a L : ℝ}\n    (hf'anti : AntitoneOn f' (Set.Ici a))\n    (hderiv : ∀ x ∈ Set.Ici a, HasDerivAt f (f' x) x)\n    (hL : a ≤ L) :\n    f L ≤ f a + f' a * (L - a) := by\n  -- FTC: f L − f a = ∫_a^L f′\n  have hint : ∫ x in a..L, f' x = f L - f a := by\n    rw [intervalIntegral.integral_eq_sub_of_hasDerivAt (fun x hx => hderiv x (by\n      have h := hx\n      rw [Set.uIcc_of_le hL] at h\n      exact h.1 : x ∈ Set.Ici a)]\n  -- hmm — integral_eq_sub_of_hasDerivAt wants the derivatives on uIcc a L: with a ≤ L: uIcc = Icc: hderiv x (Ici-member from Icc) ✓\n  -- and the integrability\n  ...\n  -- bound: ∫_a^L f′ ≤ f′ a·(L−a) via f′(x) ≤ f′(a) for x ≥ a (antitone)\n  have hbound : ∫ x in a..L, f' x ≤ f' a * (L - a) := by\n    rw [← intervalIntegral.integral_const (f' a)]\n    apply intervalIntegral.integral_mono_on hL _ _ (fun x hx => hf'anti (by\n      have h1 : a ≤ a := le_rfl\n      exact h1 : a ∈ Set.Ici a) (by\n      have h2 : a ≤ x := hx.1\n      exact h2 : x ∈ Set.Ici a) hx.1)\n  linarith [hint, hbound]\n```\nHmm — intervalIntegral.integral_const : ∫ x in a..b, c = c·(b−a) ✓ exists. And integral_mono_on (h : a ≤ b) (hf : IntervalIntegrable f) (hg : IntervalIntegrable g) (hfg : ∀ x ∈ Icc a b, f x ≤ g x) ✓ as used before. The integrability of f′ on [a, L]: f′ is continuous (11.6321/x + const with x ≥ a > 0) ⟹ ContinuousOn.intervalIntegrable ✓ — need a > 0 (a = log 12 > 0 ✓).\n\nFor the L ≤ a direction — I realize I can avoid it: the pinch domain is L ≥ log 12 with the split at 2.5024: for L ≥ 2.5024 use the generic lemma with a := 2.5024 (giving f(L) ≤ f(2.5024) + f′(2.5024)·(L−2.5024) ≤ f(2.5024) since f′(2.5024) ≤ 0 and L−2.5024 ≥ 0); for L ∈ [log 12, 2.5024] use the generic lemma with a := 2.5024, L := L — the lemma needs a ≤ L — DOESN'T APPLY. So I DO need the reverse direction or a mirrored lemma:\n```\nlemma pinch_of_antitone_le {f f' : ℝ → ℝ} {a L : ℝ}\n    (hf'anti : AntitoneOn f' (Set.Ici L))\n    (hderiv : ∀ x ∈ Set.Icc L a, HasDerivAt f (f' x) x)\n    (hL : L ≤ a) :\n    f L ≤ f a + (-f' a) * (a - L) := by\n  -- f L − f a = −∫_L^a f′; ∫_L^a f′ ≥ f′ a·(a−L) (f′(x) ≥ f′(a) for x ≤ a)\n```\nHmm — f′ antitone: x ≤ a ⟹ f′(x) ≥ f′(a) ✓: ∫_L^a f′ ≥ f′ a·(a−L) ⟹ f(L) − f(a) = −∫ ≤ −f′ a·(a−L) = (−f′ a)·(a−L) ✓.\n\nBoth need the FTC integrability of f′ on the relevant interval (ContinuousOn of f′: 11.6321/x + const, x ≥ log 12 > 0 ✓).\n\nLet me write the two lemmas as one with case analysis inside, or just inline them in pinch_tight_R directly. Actually simplest: inline both cases in pinch_tight_R with a shared HasDerivAt-family + antitone + the FTC-mono applications. Let me write it.\n\nFor the HasDerivAt of f := fun L => 11.6321·log L − 4.6484·L: ((Real.hasDerivAt_log hx0).const_mul 11.6321).sub (hasDerivAt_id' x).const_mul 4.6484): derivative 11.6321/x − 4.6484 ✓.\n\nNow write section 20. Also need `log_twelve_ge` and `log_2_5024_le`. For e^0.9173 ≥ 2.5024: partial sums Σ_{k<8} 0.9173^k/k! ≥ 2.5024: compute: k=0: 1; k=1: 0.9173; k=2: 0.841439/2 = 0.4207195; k=3: 0.385862/6 = 0.0643103; k=4: 0.353863/24 = 0.0147443; k=5: 0.324555/120 = 0.0027046; k=6: 0.297685/720 = 0.0004135; k=7: 0.273071/5040 = 0.0000542. Sum: 1+0.9173+0.4207195+0.0643103+0.0147443+0.0027046+0.0004135+0.0000542 = 2.4202464?? — that's < 2.5024!! Let me recompute the powers: 0.9173² = 0.84144·... 0.9173² = 0.84143929; /2 = 0.42071965. 0.9173³ = 0.84143929·0.9173 = 0.771852·... = 0.77185227; /6 = 0.12864205. ⁴ = 0.77185227·0.9173 = 0.708016·... = 0.70801609; /24 = 0.02950067. ⁵ = 0.70801609·0.9173 = 0.649463·... = 0.64946316; /120 = 0.00541219. ⁶ = 0.64946316·0.9173 = 0.595757·... = 0.59575656; /720 = 0.00082744. ⁷ = 0.59575656·0.9173 = 0.546487·... = 0.54648749; /5040 = 0.00010843. Sum: 1+0.9173+0.42071965+0.12864205+0.02950067+0.00541219+0.00082744+0.00010843 = 2.50251073 ≥ 2.5024 ✓ (margin 1.1e-4 ✓).\n\nFor log 12 ≥ 2.4848: e^2.4848 ≤ 12: e^2.4848 = e²·e^0.4848: e^0.4848 ≤ 1.6239: Σ_{k<7} 0.4848^k/k!: 1+0.4848+0.117516+0.018992+0.002302+0.000223+0.0000180 = 1.623851 ≤ 1.6239 ✓; e² ≤ 7.3890566 (he2sq value — wait, he2sq is inside log_fourteen_ge's proof — I need it standalone: Real.exp 1 * Real.exp 1 ≤ 7.3890566 via mul_le_mul he2 he2 ✓); 7.3890566·1.6239 = 11.99932·... compute: 7.3890566·1.6239 = 7.3890566·1.6 = 11.82249; ·0.0239 = 0.176598: total 11.999088 ≤ 12 ✓. So log 12 ≥ 2.4848 via Real.le_log_iff_exp_le (by norm_num : (0:ℝ) < 12): 12 ≥ e^2.4848 ⟹ 2.4848 ≤ log 12 ✓.\n\nLet me now also double check the pinch's tangent-point choice a = 2.5024 and the antitone domain: f′ antitone on Ici (log 12): for the L ≥ a case I need f′ antitone on Ici a (a = 2.5024 ≥ log 12 ✓); for the L ≤ a case on Ici L (L ≥ log 12 ✓). Use Ici (log 12) for both (antitoneOn.mono).\n\nOne more piece for the capstone: the elem conditions for s and s₀ (Rexpr_decomp's hypotheses):\n- hs : ζ s ≠ 0 ✓ (hζ).\n- hs0 : s ≠ 0: s.im = t ≥ 10 ⟹ s ≠ 0 (im ≠ 0 ⟹ ≠ 0 ✓ — via: s = 0 ⟹ s.im = 0 ≠ t).\n- hs1 : s ≠ 1: s.im = t ≠ 0 = im 1 ⟹ s ≠ 1 ✓.\n- hst : ∀ n ≥ 1, s ≠ −2n: −2n has im = 0 ≠ t ⟹ s ≠ −2n ✓ (n ≥ 1: −2n : ℂ = −2·(n:ℂ): im = −2·n·0 = 0 — ((−2)·(n:ℂ)).im = 0 ✓).\n- hs₀ : ζ s₀ ≠ 0: s₀ = 2+tI: re = 2 ≥ 1: `riemannZeta_ne_zero_of_one_le_re` — banked from session-033: \"riemannZeta_ne_zero_of_one_le_re takes ONLY re\" ✓ — its form: riemannZeta_ne_zero_of_one_le_re (h : 1 ≤ s.re) : riemannZeta s ≠ 0 ✓.\n- hs₀0 : s₀ ≠ 0: re = 2 ≠ 0 ✓.\n- hs₀1 : s₀ ≠ 1: re = 2 ≠ 1 ✓.\n- hs₀t : ∀ n ≥ 1, s₀ ≠ −2n: re(s₀) = 2 > 0, re(−2n) = −2n ≤ −2 < 0... wait re(−2n) = −2n·... −2·n (real): for n ≥ 1: −2n ≤ −2 < 0 < 2 ✓ re-differ ✓.\n\nAlso for one_div_diff_le: needs hs0 : s ≠ 0 ✓ (have).\n\nLet me write section 20 now. It's the final section of 5f. Estimated ~450 lines.","signature":""},{"type":"text","text":"Continuing to 5f-iii. Plan: the pinch lemma (concave f with a certified tangent point) + the six-piece assembly into the capstone. Let me first update the todo and check two API details."},{"type":"tool_use","id":"TodoWrite_270","name":"TodoWrite","input":{"todos":[{"content":"5f-iii-a: pinch lemma (log 12 >= 2.4848, log 2.5024 <= 0.9173, concave tangent machine, pinch_tight_R)","status":"in_progress","activeForm":"Building the pinch lemma"},{"content":"5f-iii-b: C0hat(t+1) L/LL conversion lemma","status":"pending","activeForm":"Building C0hat conversion"},{"content":"5f-iii-c: capstone logDeriv_riemannZeta_sub_nearZeros_le_tight (six-piece assembly)","status":"pending","activeForm":"Building the capstone"},{"content":"5f-iii-d: build green + axiom audit + commit","status":"pending","activeForm":"Building, auditing, committing"}]},"extra_content":null}]