[{"type":"thinking","thinking":"`analyticOrderAt_eq_nat_iff_iteratedDeriv_eq_zero (hf : AnalyticAt 𝕜 f z₀) : analyticOrderAt f z₀ = n ↔ (∀ k < n, iteratedDeriv k f z₀ = 0) ∧ iteratedDeriv n f z₀ ≠ 0`.\n\nSo the plan for `zeroMult_conj`:\n1. Prove `iteratedDeriv_riemannZeta_conj : ∀ (n : ℕ) {z : ℂ} (hz : z ≠ 1), iteratedDeriv n riemannZeta (starRingEnd ℂ z) = starRingEnd ℂ (iteratedDeriv n riemannZeta z)` by induction, using a general conj-deriv lemma.\n2. Then analyticOrderAt ζ (conj ρ) = analyticOrderAt ζ ρ via analyticOrderAt_eq_nat_iff_iteratedDeriv_eq_zero: order at conj ρ = n ⟺ (∀ k < n, itD k ζ (conj ρ) = 0) ∧ itD n ζ (conj ρ) ≠ 0 ⟺ (conj of itD k ζ ρ = 0 ⟺ itD k ζ ρ = 0) ⟺ same condition at ρ ⟺ order at ρ = n. Need both ≠ ⊤ (zeta_order_ne_top_of_ne, ρ ≠ 1 and conj ρ ≠ 1) and the equality as ℕ-valued: set n := analyticOrderNatAt ζ ρ; order at ρ = ↑n (Nat.cast_analyticOrderNatAt); show order at conj ρ = ↑n via the iff; then analyticOrderNatAt both = toNat of equal ℕ∞.\n\nzeroMult := analyticOrderNatAt ζ · = (analyticOrderAt ζ ·).toNat ✓.\n\nFor the conj-deriv lemma I need ζ differentiable: at z ≠ 1: `differentiableAt_riemannZeta`? Let me check — there should be `DifferentiableAt.riemannZeta`? In Mathlib: `differentiableAt_riemannZeta : z ≠ 1 → DifferentiableAt ℂ riemannZeta z`? Something like that exists (riemannZeta is analytic off 1: `analyticAt_riemannZeta` was used in the codebase: `analyticAt_riemannZeta hρ1` (LiContour one_le_zeroMult) ✓, and analytic ⟹ differentiable: AnalyticAt.differentiableAt ✓).\n\nAlso need: iteratedDeriv n ζ differentiable/analytic at z ≠ 1: analyticAt_riemannZeta.iteratedDeriv? — `AnalyticAt.iteratedDeriv` exists? There's `AnalyticAt.deriv` (Mathlib: AnalyticAt.deriv : AnalyticAt 𝕜 (deriv f) x) and iterated: `AnalyticAt.iteratedDeriv` probably exists. Or just .differentiableAt on the iterated: `AnalyticAt.iteratedDeriv` — I saw `analyticOrderAt_iterated_deriv` uses deriv^[k]. For the induction I need DifferentiableAt ℂ (iteratedDeriv n ζ) z — from (analyticAt_riemannZeta hz).iteratedDeriv n? Let me assume `AnalyticAt.iteratedDeriv` exists (Mathlib has `AnalyticAt.iteratedDeriv : AnalyticAt 𝕜 f x → AnalyticAt 𝕜 (iteratedDeriv n f) x` — I believe yes).\n\nThe conj-deriv lemma — general form:\n```\nlemma hasDerivAt_conj_of_conj_eq {f : ℂ → ℂ} {z : ℂ} (hconj : ∀ s, f (starRingEnd ℂ s) = starRingEnd ℂ (f s))\n    (hdiff : DifferentiableAt ℂ f z) :\n    HasDerivAt f (starRingEnd ℂ (deriv f z)) (starRingEnd ℂ z)\n```\nProof: hdiff.hasDerivAt gives HasDerivAt f (deriv f z) z. Convert to slope-tendsto, compose with conj-maps as planned, convert back. \n\nAlternatively — a slicker route via `HasFDerivAt` with conjLIE: the function g := conj ∘ f ∘ conj is ℂ-differentiable at conj z with deriv conj(deriv f z)... g = f pointwise. Hmm, proving g ℂ-differentiable needs the same slope argument. The tendsto composition is the way.\n\nThen the induction:\n```\nlemma iteratedDeriv_riemannZeta_conj (n : ℕ) {z : ℂ} (hz : z ≠ 1) :\n    iteratedDeriv n riemannZeta (starRingEnd ℂ z) = starRingEnd ℂ (iteratedDeriv n riemannZeta z)\n| 0 => riemannZeta_conj z   -- iteratedDeriv_zero: iteratedDeriv 0 f = f ✓ (riemannZeta_conj states ζ (conj z) = conj (ζ z) ✓)\n| n+1 => \n  rw [iteratedDeriv_succ, iteratedDeriv_succ]\n  -- deriv (iteratedDeriv n ζ) (conj z) = conj (deriv (iteratedDeriv n ζ) z)\n  apply HasDerivAt.deriv\n  apply hasDerivAt_conj_of_conj_eq (fun s => iteratedDeriv_riemannZeta_conj n (by ... : s ≠ 1))\n  exact ((analyticAt_riemannZeta hz).iteratedDeriv n).differentiableAt\n```\nWait — the hconj for f := iteratedDeriv n ζ needs ∀ s, s ≠ 1 — the identity only holds for s ≠ 1 (ζ analytic there; at s = 1 both sides junk-ish but actually riemannZeta_conj holds at ALL s (it's a global identity? `riemannZeta_conj : riemannZeta (conj s) = conj (riemannZeta s)` — probably ∀ s). And iteratedDeriv at 1: junk values — the identity iteratedDeriv n ζ (conj s) = conj(iteratedDeriv n ζ s) at s = 1 is NOT needed for the slope argument at z ≠ 1 (only a NEIGHBORHOOD of z matters, and z ≠ 1 has a neighborhood avoiding 1 ✓ — but the lemma as stated quantifies ∀ s. For the slope-tendsto I only need the identity EVENTUALLY near z — better to state hasDerivAt_conj_of_conj_eq with (hconj : ∀ᶠ s in 𝓝 z, ...) or ∀ s in a ball. Simplest: require ∀ s (global) and prove the ζ instance for s ≠ 1... at s = 1 the identity might FAIL (junk). Hmm — does riemannZeta_conj hold at s = 1? ζ(1) = junk = 0? conj(0) = 0 ✓ and ζ(conj 1) = ζ(1) = 0 ✓ — probably holds (both junk 0). For iteratedDeriv n ζ at 1 (n ≥ 1): deriv of ζ at 1 — ζ not differentiable at 1, deriv gives 0 (junk); iteratedDeriv n ζ (conj 1) = iteratedDeriv n ζ 1 = 0 = conj 0 ✓ holds trivially. So the ∀ s version might actually hold for all s! But proving it at s = 1 for the induction step needs... the inductive proof only differentiates NEAR z ≠ 1. Cleaner: state the hconj hypothesis as (hconj : ∀ s, f (starRingEnd ℂ s) = starRingEnd ℂ (f s)) and for the ζ induction prove the identity ∀ s with s ≠ 1 restriction handled... ugh. \n\nSIMPLEST: make the global-in-s lemma by noting the identity holds at every s ≠ 1, and at s = 1 both sides are 0 (junk): for the induction, prove P(n) : ∀ z, iteratedDeriv n ζ (conj z) = conj (iteratedDeriv n ζ z) for ALL z — by induction: P(0) = riemannZeta_conj (all s ✓). P(n+1): for z ≠ 1: the deriv argument (needs f-conj-identity only near z — and P(n) gives it GLOBALLY ✓ fine). For z = 1: iteratedDeriv (n+1) ζ 1: ζ not differentiable at 1 — deriv (iteratedDeriv n ζ) 1 = 0 (deriv of non-differentiable = 0 via `deriv_zero_of_not_differentiableAt`)? Is ζ's iteratedDeriv n differentiable at 1? ζ has a pole at 1 — NOT analytic/differentiable there (analyticAt_riemannZeta needs ≠ 1). So deriv _ 1 = 0 (junk convention) and conj 0 = 0 ✓. So P(n+1) at z = 1: LHS = deriv (itD n ζ) (conj 1) = deriv (itD n ζ) 1 = 0 (not differentiable), RHS = conj (deriv (itD n ζ) 1) = conj 0 = 0 ✓.\n  Need: ¬DifferentiableAt ℂ (iteratedDeriv n ζ) 1. Hmm — is that easy? If itD n ζ were differentiable at 1, then... ζ meromorphic with a pole: for n = 0: differentiableAt_riemannZeta at 1 is false — is there a lemma `not_differentiableAt_riemannZeta_one`? Probably not directly. ζ → ∞ at 1 (tendsto_riemannZeta_nhds_one? `riemannZeta_tendsto_nhds_one`?) ⟹ not continuous ⟹ not differentiable. For n ≥ 1: itD n ζ also blows up at 1 (the pole persists under differentiation...) — harder. \n\n  AVOID the z = 1 case entirely: I only need the identity at nontrivial zeros (re ∈ (0,1) ⟹ z ≠ 1 ✓). So prove P(n) only for z ≠ 1, with the conj-deriv lemma taking the identity as an EVENTUALLY hypothesis near z:\n```\nlemma hasDerivAt_conj_of_conj_eq {f : ℂ → ℂ} {z : ℂ} (hconj : ∀ s, f (starRingEnd ℂ s) = starRingEnd ℂ (f s)) (hdiff : DifferentiableAt ℂ f z) : HasDerivAt f ...\n```\n— global hconj is FINE as a hypothesis form; for the ζ induction I prove the identity for all s ≠ 1... no wait, the hconj needs to hold at the points the slope-tendsto visits = near z, all ≠ 1 if I restrict... but hconj ∀ s can't be satisfied if the identity fails at s = 1. Does it fail at s = 1 for itD n ζ? As computed: both sides junk-0 at 1 ✓ HOLDS (probably). But to be safe, use (hconj : ∀ᶠ s in 𝓝 z, ...)? The slope-quotient rewrite needs the identity at conj x for x near conj z, i.e. at points near z ✓ eventually form works.\n\nActually — cleanest: state the identity hypothesis as ∀ s ∈ (𝓝 z)-eventually. But the induction's hconj for f = itD n ζ would be: ∀ᶠ s in 𝓝 z, itD n ζ (conj s) = conj (itD n ζ s) — from P(n)'s ∀-form restricted... if P(n) is stated for z ≠ 1 only: ∀ {z}, z ≠ 1 → itD n ζ (conj z) = conj(...): then eventually near z ≠ 1 (s ≠ 1 eventually ✓, apply P(n)) ✓.\n\nOK the design is settled. The conj-deriv lemma with eventually hconj. Hmm wait — actually let me double check: does `riemannZeta_conj` exist with the starRingEnd form? It was used in isNontrivialZero_conj: `rw [_root_.riemannZeta_conj, hρ.1, map_zero]` ✓ — riemannZeta_conj : ζ ((starRingEnd ℂ) s) = (starRingEnd ℂ) (ζ s) presumably.\n\nNow — WAIT. Before building this conj machinery, let me reconsider whether the left tail really needs it. The left-tail fiber count: fibers on the subtype with γ < 0. The mult-weighted sum. Hmm — alternatively bound the left-tail sum NOT via per-window C0hat counts but... the fiber ℓ has |γ| ∈ [ℓ, ℓ+1), γ < 0. The window zerosIn(ℓ−1, ℓ+1)-ish on the POSITIVE side won't contain these. The conj map on the SUBTYPE: σ : subtype → subtype, σ ρ = ⟨conj ρ.1, isNontrivialZero_conj ρ.2⟩ — an involution. Σ_{fiber_ℓ} zeroMult ρ.1 = Σ_{σ '' fiber_ℓ} zeroMult (σ⁻¹ ρ').1 = Σ_{fiber'_ℓ} zeroMult (conj ρ'.1) — needs zeroMult(conj) = zeroMult. Yes, unavoidable. OK, build it.\n\nEstimated conj machinery: ~120 lines. Fine.\n\nNOW — let me also reconsider the overall size of this piece-3 build and organize sub-stages:\n\n**3a** (this session's first commit): the numeric bricks (§9). Pure real analysis, self-contained:\n- farW + basic properties.\n- S₃ ≤ 1.3476 (tsum version + Ico version).\n- RW₀ (Σ_{k≥11} 1/k² ≤ 0.1), RW₁ (log k/k² ≤ 0.3303), RW₂ (loglog k/k² ≤ 0.3679·0.3303 — pointwise trick, needs log 10 ≤ 2.3026 & 1/e ≤ 0.3679 & the log u ≤ u/e lemma).\n- LA₀ (1/(j+10)² ≤ 1/23), LA₁ (log j/(j+10)² ≤ 0.1687), LA₂ (≤ 0.3679·0.1687 pointwise).\n- Certified numerics: log 10 ≤ 2.3026, log 13 ≤ 2.565, log(23/13) ≤ 0.571, log(17/14) ≤ 0.1942, log 2.3 ≤ 0.833, log 11 ≥ 2.3978, log 14 ≥ 2.639, 1/e ≤ 0.3679, log 2 ≤ 0.6932 (exists: log_two_lt_d9), sqrt bounds.\n**3b**: C0hat bridges + conj machinery (zeroMult_conj). \n**3c**: the far-series machine (g, summability, per-term bound, norm reduction, main finset + unit_family_le, two tail tsum machines, assembly `far_series_le`).\n\nLet me now write §9. I'll append to LiTightR.lean. First the certified numerics — patterns from this file: log 3 ≤ 1.1 via `Real.sum_le_exp_of_nonneg` (partial sums, k < 6). For log 10 ≤ 2.3026: need e^2.3026 ≥ 10: partial sum Σ_{k<K} 2.3026^k/k! ≥ 10 — e^2.3026 ≈ 9.9998·... hmm wait: e^2.3026 = 10.00003-ish (log 10 = 2.302585, so e^2.3026 = 10·e^0.000015 ≈ 10.00015). Partial sums to reach ≥ 10: need enough terms: e^2.3026 = Σ 2.3026^k/k!: terms up to k ≈ 12: let me compute numerically how many terms needed for the partial sum to exceed 10.\n\nSimilarly log 13 ≤ 2.565: e^2.565 ≥ 13 — partial sums. log(23/13) ≤ 0.571: e^0.571 ≥ 23/13 = 1.76923 — e^0.571 ≈ 1.77001 ✓ partial sums easy. log(17/14) ≤ 0.1942: e^0.1942 ≥ 17/14 = 1.214286: e^0.1942 ≈ 1.214414 ✓. log 2.3 ≤ 0.833: e^0.833 ≥ 2.3: e^0.833 ≈ 2.30043 ✓. log 11 ≥ 2.3978: e^2.3978 ≤ 11 — UPPER bound on exp — harder via partial sums (partial sums are LOWER bounds for positive args). For exp upper: e^2.3978 = 1/e^{−2.3978} ≤ 1/(Σ_{k<K} (−2.3978)^k/k!)... alternating — messy. ALTERNATIVE: e^2.3978 ≤ 11 ⟺ 2.3978 ≤ log 11 — prove log 11 ≥ 2.3978 via: 11 ≥ e^2.3978 ⟺ 11·e^{−2.3978} ≥ 1... Alternatively use a DIFFERENT route: log 11 = log(10·1.1) = log 10 + log 1.1 ≥ 2.3025 + 0.0953 = 2.3978 ✓!! log 10 ≥ 2.3025 (10 ≤ e^2.3025? e^2.3025 ≈ 9.99977 ≤ 10 ✓ — needs exp UPPER again... e^2.3025 ≤ 10 ⟺ log 10 ≥ 2.3025 — circular. Hmm: log 10 ≥ 2.3025 ⟺ 10 ≥ e^2.3025. e^2.3025 ≤ 10: via e^2.3025 = e^2·e^0.3025 ≤ e^2·(1+0.3025+0.3025²/2+...)·... the exp-partial-sum gives LOWER bounds. For upper bounds on exp: e^x ≤ 1/(1−x) for x ∈ (0,1)-ish? e^x (1−x) ≤ 1 for 0 ≤ x < 1? e^x ≤ 1/(1−x) ✓ true for x ∈ [0,1) (since e^{−x} ≥ 1−x ⟹ e^x ≤ 1/(1−x)). So e^0.3025 ≤ 1/(1−0.3025) = 1.4337. e^2 ≤ 7.389 (Real.exp_one_lt_d9: e < 2.7182818286; e² ≤ 2.7183² = 7.3892). e^2.3025 = e²·e^0.3025 ≤ 7.3892·1.4337 = 10.5927 > 10 ✗ too loose.\n  Better: e^0.3025 via partial sums from BELOW gives e^0.3025 ≥ ..., not ≤. For ≤ : e^x = (e^{x/2})² and e^{x/2} ≤ 1/(1−x/2): e^0.3025 ≤ 1/(1−0.15125)² = 1/0.84875² = 1.3877: e^2.3025 ≤ 7.3892·1.3877 = 10.2546 ✗ still > 10.\n  e^0.3025 ≤ 1/(1−0.075625)⁴: (1/0.924375)⁴ = 1.08181⁴ = 1.36966·... 1.08181² = 1.17031, squared = 1.36963: e^2.3025 ≤ 7.3892·1.36963 = 10.1204 ✗.\n  Hmm. The issue: e^{0.3025} true ≈ 1.3533. 1/(1−x/2^m)^{2^m} → e^x from ABOVE? (1−x/n)^{−n} DECREASES to e^x? No — (1−x/n)^{-n} ↓ e^x as n ↑ (for 0 < x < 1): at n=1: 1/(1−x) = 1.4337; n=2: 1.3877; n=4: 1.3696; n=8: (1−0.0378)^{-8} = 1.36124·... 1/0.96219^8: 0.96219^8 = e^{8·ln0.96219} = e^{8·(−0.03854)} = e^{−0.30831} = 0.73471: 1/0.73471 = 1.36108. True e^0.3025 = 1.35328. Still 0.6% high. n=16: ≈ 1.35717. Meh — converges slowly. e^2.3025 ≤ 7.3892·1.35717 = 10.0279 ✗ still > 10.\n  \n  DIFFERENT approach for log 10 ≥ 2.3025: use log 10 = log 2 + log 5: log 2 ≥ 0.6931 (log_two_gt_d9 ✓ exists in Mathlib) and log 5 ≥ 1.6094: log 5 = log(10/2)... circular. log 5: 5 ≥ e^1.6094 ⟺ ... same exp-upper problem. \n  \n  Hmm — what about using the exp partial sums for the LOWER bound on log via a DIFFERENT inversion: log x ≥ L ⟺ x ≥ e^L ⟺ x·e^{−L} ≥ 1: e^{−L} = 1/e^L and e^L ≤ U (upper) ⟹ e^{−L} ≥ 1/U — circular again.\n  \n  OK — the clean classical trick: log x ≥ L via the INTEGRAL/series: log x = −log(1/x) and log(1−y) ≤ −y − y²/2 − ... : log x ≥ partial series: log x = −log(1/x) = −log(1 − (1−1/x)) = Σ (1−1/x)^k/k ≥ Σ_{k≤K} (1−1/x)^k/k. For x = 10: 1−1/10 = 0.9: Σ 0.9^k/k converges SLOWLY (0.9^k: k=20: 0.12). Bad.\n  log x ≥ L via log((1+u)/(1−u)) = 2(u+u³/3+u⁵/5+...) with u = (x−1)/(x+1): for x = 10: u = 9/11 = 0.8182 — also slow-ish but alternating-free (all positive terms — LOWER bounds valid!): 2·(0.8182+0.8182³/3+0.8182⁵/5+...): 0.8182³ = 0.5477/3 = 0.1826; ⁵ = 0.3666/5 = 0.0733; ⁷ = 0.2455/7 = 0.0351; ⁹ = 0.1644/9 = 0.0183; ¹¹ = 0.1101/11 = 0.0100; ¹³: 0.0737/13 = 0.0057; ¹⁵: 0.0494/15 = 0.0033; sum: 0.8182+0.1826+0.0733+0.0351+0.0183+0.0100+0.0057+0.0033 = 1.1465; ×2 = 2.293 < 2.3025. More terms: ¹⁷: 0.0331/17 = 0.0019; ¹⁹: 0.0222/19 = 0.00117; ²¹: 0.0148/21 = 0.000707; total ≈ 1.1503×2 = 2.3006 — still < 2.3025. ~30 terms needed. Painful.\n  \n  ALTERNATIVE: log 11 ≥ 2.3978 — maybe I can just AVOID needing a tight log-11 lower bound! The usage: 0.833/log 11 ≤ 0.3475 ⟸ log 11 ≥ 0.833/0.3475 = 2.39712. So I need log 11 ≥ 2.3972 (slack from 2.3978). Similarly log 14 ≥ 0.1942/0.0736 = 2.63859. Hmm, still needs lower bounds on log 11/14 ≈ 2.397/2.639.\n  \n  Lower bound for log 11: log 11 = log(e²·(11/e²)) = 2 + log(11/e²) = 2 + log(11/7.3891) = 2 + log(1.48895). log 1.48895 ≥ ?: via log(1+x) ≥ x − x²/2 (alternating: log(1+x) ≥ x−x²/2 for x ≥ 0 ✓ standard): x = 0.48895: 0.48895 − 0.11954 = 0.36941 — too weak (need 0.3972). log(1+x) ≥ x − x²/2 + x³/3 − x⁴/4: 0.48895−0.11954+0.03897−0.01428 = 0.39410 — still short. +x⁵/5: 0.39410+0.00559 = 0.39969 − x⁶/6 = 0.39969−0.00455 = 0.39514... oscillating, converging to 0.39722·... true log 1.48895 = 0.39722. Partial alternating bounds: the even-stop gives lower bounds (log(1+x) ≥ Σ_{k≤2m}(−1)^{k+1}x^k/k ✓): need Σ up to k = 2m with value ≥ 0.3972 — the series converges to 0.39722 — the lower bounds approach from below; need ≥ 0.3972: infinitely close — the alternating bound NEVER reaches 0.3972 if the true value is 0.39722... k=8: 0.39514+0.00042−... ≈ 0.3965; k=10: ≈ 0.3969; k=20: ≈ 0.39719. Painful — 20 terms. Doable via norm_num on rationals (x = 0.48895 = 11/e²−1 — but e² is irrational... use x ≤ 0.4890 rational upper: log(1+x) is increasing: log(11/e²) ≤ log(1.4890)... wait I need LOWER bound on log: log(11/e²) ≥ log(1+x₀) requires 11/e² ≥ 1+x₀ ⟺ 11 ≥ (1+x₀)·e² — need e² UPPER: e² ≤ 7.3891 (e ≤ 2.7182818286 → e² ≤ 7.38906·... (2.7182818286)² = 7.389056 — norm_num can compute 2.7182818286² = 7.3890560990·... ≤ 7.3891 ✓). So 11/7.3891 ≥ 1.48868·... 11/7.3891 = 1.488681. log(1.488681) ≥ alternating sum at x = 0.488681: need ≥ 0.3972: k ≤ 20-ish. UGH.\n\n  BETTER: log 11 ≥ 2.3972 ⟺ log 121 ≥ 4.7944 ⟺ ... or: 11 = 10·1.1: log 11 = log 10 + log 1.1. log 10 ≥ 2.3025: hmm same problem. log 1.1 ≥ 0.0953: log(1.1) ≥ 0.1−0.005+0.000333 = 0.095333 ✓ EASY (x = 0.1 small — alternating converges fast ✓). So need log 10 ≥ 2.3024-ish (2.3972−0.0953 = 2.3019). log 10 ≥ 2.3019: 10 = e·(10/e) = 1+log(10/e) = 1+log(3.67879): log 3.67879 ≥ 1.3019: log 3.67879 = log(3.67879) — hmm. 10/e = 3.678794. log(3.678794) = log(4·0.919699) = log 4 + log(0.919699) = 2·log 2 + log(1−0.080301): log 2 ≥ 0.6931 (Mathlib log_two_gt_d9: 0.6931471803 < log 2 ✓ so log 2 ≥ 0.69314). log(1−y) ≥ −y−y²/2−y³/3−...−(y^K/K)·(1/(1−y))-ish (the tail bound: Σ_{k>K} y^k/k ≤ y^{K+1}/((K+1)(1−y))): with y = 0.080301: −log(1−y) = y+y²/2+y³/3+... ≤ 0.080301+0.003224+0.000173+... = 0.0837 — so log(0.919699) ≥ −0.0837. log 10 = 1+2·0.69314−0.0837 = 1+1.38628−0.0837 = 1.30258... wait: log 10 = 1 + log(10/e) = 1 + log(3.678794) = 1 + 2log2 + log(0.919699) = 1+1.38628−0.0837 = 2.30258 ✓ ≥ 2.3025 ✓!!\n  Then log 11 = log 10 + log 1.1 ≥ 2.3025+0.0953 = 2.3978 ✓ (using log 1.1 ≥ 0.0953: log(1.1) ≥ 0.1 − 0.1²/2 + 0.1³/3 − 0.1⁴/4 = 0.1−0.005+0.0003333−0.000025 = 0.0953083 ≥ 0.0953 ✓).\n  And log 14 ≥ 2.639: log 14 = log 2 + log 7: log 7 = log(7): 7 = e²·(7/e²) = 2 + log(7/7.389056...) hmm 7/e² = 0.94717 < 1: log 7 = 2 + log(0.94717) ≥ 2 − (y+y²/2+...) with y = 1−0.94717 = 0.05283: −log(1−y) ≤ y+y²/2+y³/3+y⁴/4·(1/(1−y))·... ≤ 0.05283+0.001395+0.0000491+0.00000195/0.947 ≈ 0.054277. log 7 ≥ 2−0.05428 = 1.94572. log 14 = log 2+log 7 ≥ 0.69314+1.94572 = 2.63886 ≥ 2.6388 — hmm need 2.63859: 2.63886 ≥ 2.63859 ✓✓.\n\n  These are all provable but each is a small norm_num festival. The pattern: log(1+x) alternating bounds — does Mathlib have `Real.log_le_sub_one_of_pos` (log x ≤ x−1) and for lower bounds... there's `Real.log_le_sub_one_of_pos`, and maybe `Real.one_sub_le_log`? Hmm: for log(1+x) ≥ x − x²/2: could prove via integral: log(1+x) = ∫₀^x dt/(1+t) ≥ ∫₀^x (1−t)dt = x−x²/2 (1/(1+t) ≥ 1−t ✓). Via intervalIntegral with the comparison — the LiTightR file has integral machinery (intervalIntegral.norm_integral_le...) but a direct ∫ comparison: `intervalIntegral.integral_mono_on` with 1/(1+t) ≥ 1−t on [0,x] and ∫(1−t) = x−x²/2 — need the antiderivative pattern. There's likely `Real.log_one_add_ge`? hmm. Mathlib has `Real.log_le_sub_one_of_pos : 0 < x → log x ≤ x − 1` and `Real.one_sub_le_log`? Let me not gamble — I'll prove a bespoke lemma `log_one_add_ge_alt : 0 ≤ x → x - x^2/2 + x^3/3 - x^4/4 ≤ log (1+x)` via the integral comparison (1/(1+t) ≥ 1−t+t²−t³ on t ≥ 0: 1 ≥ (1−t+t²−t³)(1+t) = 1−t⁴ ✓). The integral: ∫₀^x (1−t+t²−t³) dt = x − x²/2 + x³/3 − x⁴/4 ✓. And ∫₀^x dt/(1+t) = log(1+x) — `integral_one_div_one_add`? There's `integral_inv_one_add`? or via hasDerivAt log(1+x) — the pattern `intervalIntegral.integral_eq_sub_of_hasDerivAt`. Fine.\n\n  For −log(1−y) ≤ y+y²/2+...+y^{K}/K + tail: log(1−y) ≥ ... : via 1/(1−t) ≤ 1+t+t²+...+t^{K}+t^{K+1}/(1−y) on [0,y]: ∫₀^y dt/(1−t) = −log(1−y) ≤ y+y²/2+...+y^{K+1}/((K+1)(1−y)). Also provable via integral comparison. Or simpler: −log(1−y) = log(1/(1−y)) ≤ (1/(1−y)) − 1 = y/(1−y) via log z ≤ z−1!! For the y values here: y/(1−y): y = 0.080301: 0.080301/0.919699 = 0.087313 — then log 10 = 1+2·0.69314−0.087313·... wait: log(0.919699) = −log(1/0.919699) ≥ −(1/0.919699−1) = −0.087313. log 10 ≥ 1+1.38628−0.087313 = 2.298967 < 2.3025 ✗ TOO WEAK. So I do need the finer −log(1−y) series bound. OK: −log(1−y) ≤ y/(1−y)·... no: −log(1−y) = y + y²/2 + y³/3·(tail factor): the bound −log(1−y) ≤ y + y²/(2(1−y)): since −log(1−y) = ∫₀^y dt/(1−t) ≤ ∫₀^y (1 + t/(1−y)) dt = y + y²/(2(1−y)) (1/(1−t) ≤ 1+t/(1−y) for t ∈ [0,y] ⟺ 1 ≤ (1−t)+t(1−t)/(1−y)·... hmm check: 1/(1−t) ≤ 1 + t/(1−y) ⟺ 1 ≤ (1−t)(1+t/(1−y)) = 1−t + t(1−t)/(1−y) ⟺ t ≤ t(1−t)/(1−y) ⟺ 1 ≤ (1−t)/(1−y) ⟺ 1−y ≤ 1−t ⟺ t ≤ y ✓). So −log(1−y) ≤ y + y²/(2(1−y)): y = 0.080301: 0.080301+0.0064483/(2·0.919699) = 0.080301+0.0035055 = 0.0838065. log 10 ≥ 1+1.38628−0.0838065 = 2.3024735 — need ≥ 2.3025?? 2.3024735 < 2.3025 ✗ BARELY SHORT. Argh!! Use one more term: 1/(1−t) ≤ 1+t+t²/(1−y): −log(1−y) ≤ y+y²/2+y³/(3(1−y)) = 0.080301+0.003224+0.00017255·... = 0.080301+0.0032242+0.0001877 = 0.0837129. log 10 ≥ 1+1.38628−0.0837129 = 2.3025671 ≥ 2.3025 ✓✓ (margin 6.7e-5 — thin but OK).\n  \n  Hmm wait — actually let me double-check the decomposition: log 10 = 1 + log(10/e) — needs 10/e as a clean number: 10/e = 10/e — in Lean: log 10 = log(e·(10/e)) = log e + log(10/e) = 1 + log(10/e) — needs 10/e > 0 ✓ and the exp/log manipulations with e as Real.exp 1. And 10/e = 4·(2.5/e)·... hmm I decomposed 10/e = 4·(10/(4e)) = 4·(2.5/e): log(10/e) = 2 log 2 + log(2.5/e). And 2.5/e = 0.919699 — as (2.5 : ℝ)/Real.exp 1. Then 1 − 2.5/e = (e−2.5)/e — with e ∈ [2.7182818, 2.7182819]: y = 1−2.5/e ∈ [1−2.5/2.7182818, 1−2.5/2.7182819] = [0.08031·...]: compute: 2.5/2.7182818 = 0.919699: y ≤ 0.080301 (using e ≥ 2.7182818: 2.5/e ≤ 0.919699 ⟹ y = 1−2.5/e ≥ 0.080301 — WAIT direction: y = 1−2.5/e, e bigger ⟹ 2.5/e smaller ⟹ y bigger. e ≤ 2.7182819 ⟹ 2.5/e ≥ 0.919698 ⟹ y ≤ 0.080302. So y ≤ 0.080302 and 1−y ≥ 0.919698. −log(1−y) ≤ y+y²/2+y³/(3(1−y)) with y ≤ 0.080302, 1−y ≥ 0.919698: ≤ 0.080302+0.0032243+0.0001877 = 0.083714. log 10 ≥ 1+2·0.693147−0.083714 = 2.30258 ✓.\n  \n  Also for the LOWER bound I need log(2.5/e) ≥ −(that) — i.e. log z ≥ −(1/z−1)-series — the lemma: for 0 < z < 1: log z ≥ (z−1) − (z−1)²/(2z²)·... I'll engineer: log z = −log(1/z) and 1/z = 1/(1−y) with −log(1−y) ≤ y+y²/2+y³/(3(1−y)) where 1−y = z. Direct lemma: `neg_log_one_sub_le : 0 ≤ y → y < 1 → -Real.log (1-y) ≤ y + y^2/2 + y^3/(3*(1-y))` via ∫₀^y dt/(1−t) ≤ ∫₀^y (1+t+t²/(1−y)) dt. The integral ∫₀^y dt/(1−t) = −log(1−y): antiderivative −log(1−t) ✓ (hasDerivAt log.comp).\n\nOK — the certified numerics are all feasible but each is fiddly. Let me organize §9 as:\n\n§9a: misc certified numerics (log/exp/sqrt bounds):\n- `log_two_ge` : log 2 ≥ 0.693147 (Mathlib log_two_gt_d9 ✓ direct)\n- `log_ten_ge` : log 10 ≥ 2.3025 (the decomposition above)\n- `log_ten_le` : log 10 ≤ 2.3026 (10 ≥ e^2.3026?? no: log 10 ≤ 2.3026 ⟺ 10 ≤ e^2.3026: exp partial sums ≥ 10: Σ_{k<14} 2.3026^k/k! ≥ 10? — compute numerically how many terms.)\n- `log_eleven_ge` : log 11 ≥ 2.3978 (log 10 + log 1.1 route: needs log_one_add lower bound: log 1.1 ≥ 0.0953 via the ∫ comparison with 1−t+t²−t³)\n- `log_thirteen_le` : log 13 ≤ 2.565 (13 ≤ e^2.565: partial sums)\n- `log_fourteen_ge` : log 14 ≥ 2.6388 (log 2 + log 7: log 7 = 2 + log(7/e²): −log(e²/7)−ish: log(7/e²) = −log(e²/7), e²/7 = 1.055579: log ≤ y/(1−y)-ish or the series: −log(1−y) ≤ y+y²/2+y³/(3(1−y)) with y = 1−7/e² = 0.052828: ≤ 0.052828+0.001395+0.0000492 = 0.054272: log 7 ≥ 2−0.054272 = 1.945728: log 14 ≥ 0.693147+1.945728 = 2.638875 ≥ 2.6388 ✓)\n- `log_23_13_le` : log(23/13) ≤ 0.571 (23/13 ≤ e^0.571: partial sums)\n- `log_17_14_le` : log(17/14) ≤ 0.1942 (17/14 ≤ e^0.1942)\n- `log_2_3_le` : log 2.3 ≤ 0.833 (2.3 ≤ e^0.833)\n- `one_div_e_le` : 1/e ≤ 0.3679 (e ≥ 2.7182: 1/2.7182 = 0.36789·... ≤ 0.3679 ✓)\n- `log_one_sub_ge`/integral lemmas: `log_one_add_ge`, `neg_log_one_sub_le` (the ∫-comparison machines)\n- sqrt lower bounds: `sqrt_two_ge : 1.414 ≤ √2` etc. via Real.le_sqrt.\n- `log_log_le` : log(log x) ≤ (1/e)·log x — via log u ≤ u/e (u = log x): log u ≤ u/e ⟸ log(u/e) ≤ u/e − 1 (Real.log_le_sub_one_of_pos) ✓.\n\n§9b: the weight farW + S₃ + the tsum bricks.\n\nThis is a lot of numerical grind. To economize: for the exp-upper-bound-partial-sums, the pattern from this file (`log 3 ≤ 1.1` via Real.sum_le_exp_of_nonneg with 6 terms). For e^2.3026 ≥ 10 and e^2.565 ≥ 13, more terms needed — let me compute the required K numerically right now. Also e^0.571, e^0.1942, e^0.833.\n\nActually — WAIT. Much better idea for log-upper bounds: log x ≤ U ⟺ x ≤ e^U. Instead of exp partial sums (needs many terms for x ~ 2.3), use e^U = (e^{U/4})^4 with e^{U/4} ≥ partial sum of the SMALL argument U/4: for U = 2.3026: U/4 = 0.57565: e^0.57565 ≥ Σ_{k<7} 0.57565^k/k! — 7 terms of a small arg. Then e^2.3026 ≥ that^4. Compute numerically whether Σ_{k<7} 0.57565^k/k! ^4 ≥ 10. e^0.57565 = 1.77840·... Σ_{k<7}: 1+0.57565+0.16569+0.03179+0.004576+0.0005269+0.00005057 = 1.77828. ^4: 1.77828² = 3.16228; ^4 = 3.16228² = 10.0000·... = 10.00001 ✓ MARGINAL — need more terms: Σ_{k<8}: +0.57565⁷/5040 = +0.0000042: 1.77829^4 ≈ 10.00005·... — cutting it close. Use U/8 = 0.287825: e^0.287825 ≥ Σ_{k<5} = 1+0.287825+0.041422+0.003974+0.000286 = 1.333507: ^8: 1.333507² = 1.778241; ^4 = 3.162140; ^8 = 9.999124 ✗ < 10. More terms: Σ_{k<6}: +0.287825⁵/120 = +0.00001647: 1.333524^8: 1.333524² = 1.778286, ^4 = 3.162301, ^8 = 10.00014 ✓. So e^2.3026 ≥ (Σ_{k<6} 0.287825^k/k!)^8 ≥ 10.00014 ≥ 10 ✓. Hmm — this squaring approach works but norm_num on (1.333524)^8 ≥ 10 is a big-but-finite rational computation ✓ fine.\n\nSimilarly e^2.565 ≥ 13: U/4 = 0.64125: e^0.64125 ≥ Σ_{k<6}: 1+0.64125+0.20560+0.04396+0.007047+0.000904 = 1.898761: ^4: 1.898761² = 3.605293, ^4 = 12.99814 ✗ < 13. Σ_{k<7}: +0.64125⁶/720 = +0.0000966: 1.898858^4: 1.898858² = 3.605662, ^4 = 13.00080 ✓ ≥ 13 ✓.\ne^0.571 ≥ 23/13 = 1.769231: Σ_{k<5}: 1+0.571+0.163021+0.031042+0.004434 = 1.769497 ✓ ≥ 1.769231 ✓ (margin 2.7e-4 — thin; k<6: +0.0005066: 1.770003 ✓ safer).\ne^0.1942 ≥ 17/14 = 1.214286: Σ_{k<5}: 1+0.1942+0.018857+0.001221+0.0000593 = 1.214337 ✓.\ne^0.833 ≥ 2.3: Σ_{k<7}: 1+0.833+0.346945+0.096328+0.020059+0.003342+0.000464 = 2.300138 ✓ (margin 1.4e-4; k<8: +0.0000644: 2.300202 ✓).\n\nOK — all numerics verified feasible. Now let me get to writing. Given the volume, I'll write §9 in chunks and test-compile each chunk with `lake env lean`. The workflow per handoff: from research/lean/NguyenRH1 dir, `lake env lean NguyenRH1/LiTightR.lean` for single-file iteration (foreground; it takes a while for a big file but OK).\n\nActually — since this file is getting big (820 + ~1000 lines), compile times will grow. Alternative: put piece 3 in a NEW file LiTightR3.lean importing LiTightR? The journal says \"piece 3 in LiTightR.lean\" — follow the journal. But actually — hmm, LiTightR is not yet root-imported (journal: \"not yet root-imported\"). Adding piece 3 there is fine; root-import comes at 5f-iii.\n\nLet me start writing §9. I'll write it in 3 chunks: (9a) certified numerics; (9b) farW + S₃; (9c) the six tail bricks. Let me draft chunk 9a now.\n\nKey lemmas to write (chunk 9a):\n\n```lean\n/-! ## 9. Piece 3a: the certified numerics for the far-sum bricks -/\n\n/-- ∫ comparison lower bound: log(1+x) ≥ x − x²/2 + x³/3 − x⁴/4 for x ≥ 0\n(1/(1+t) ≥ 1 − t + t² − t³ on [0, x]). -/\nlemma log_one_add_ge {x : ℝ} (hx : 0 ≤ x) :\n    x - x^2/2 + x^3/3 - x^4/4 ≤ Real.log (1 + x) := by\n  -- ∫₀^x (1−t+t²−t³) dt ≤ ∫₀^x dt/(1+t) = log(1+x)\n  ...\n```\n\nThe integral ∫₀^x dt/(1+t) = log(1+x): pattern — `intervalIntegral.integral_eq_sub_of_hasDerivAt` with F = log(1+·), F' = 1/(1+·): HasDerivAt (log ∘ (1+·)) (1/(1+t)) t: (hasDerivAt_id' t).const_add 1 |> Real.hasDerivAt_log (1+t ≠ 0).comp? For real log: `Real.hasDerivAt_log (hx : x ≠ 0) : HasDerivAt Real.log x⁻¹ x` ✓ .comp.\nThen the comparison: intervalIntegral.integral_mono_on (a ≤ b) (integrable) (integrable) (∀ t ∈ Icc, f t ≤ g t).\n1−t+t²−t³ ≤ 1/(1+t) ⟺ (1−t+t²−t³)(1+t) ≤ 1 ⟺ 1−t⁴ ≤ 1 ✓ (needs 1+t > 0 ✓).\n\nSimilarly:\n```lean\n/-- ∫ comparison upper bound: −log(1−y) ≤ y + y²/2 + y³/(3(1−y)) for 0 ≤ y < 1\n(1/(1−t) ≤ 1 + t + t²/(1−y) on [0, y]). -/\nlemma neg_log_one_sub_le {y : ℝ} (hy0 : 0 ≤ y) (hy1 : y < 1) :\n    -Real.log (1 - y) ≤ y + y^2/2 + y^3/(3*(1-y))\n```\n∫₀^y dt/(1−t) = −log(1−y): antiderivative −log(1−t): HasDerivAt (−log(1−·)) (1/(1−t)) t: Real.hasDerivAt_log (1−t ≠ 0) at (1−t): deriv = (1−t)⁻¹·(−1) = −1/(1−t), negated: 1/(1−t) ✓.\n1/(1−t) ≤ 1+t+t²/(1−y) ⟺ 1 ≤ (1−t)(1+t+t²/(1−y)) = 1−t² + t²(1−t)/(1−y): ⟺ t² ≤ t²(1−t)/(1−y) ⟺ (for t > 0) 1−y ≤ 1−t ⟺ t ≤ y ✓ (t = 0 trivial ✓).\n\nThen the log bounds:\n```lean\nlemma log_one_point_one_ge : (0.0953 : ℝ) ≤ Real.log 1.1  -- log_one_add_ge with x = 0.1: 0.1−0.005+0.000333−0.000025 = 0.095308 ≥ 0.0953\nlemma log_ten_ge : (2.3025 : ℝ) ≤ Real.log 10\n  -- log 10 = 1 + 2·log 2 + log(2.5/e); log(2.5/e) = −log(e/2.5) ≥ −(y+y²/2+y³/(3(1−y))) with 1−y = 2.5/e\nlemma log_ten_le : Real.log 10 ≤ 2.3026  -- 10 ≤ e^2.3026 via (Σ_{k<6} 0.287825^k/k!)^8\nlemma log_eleven_ge : (2.3978 : ℝ) ≤ Real.log 11  -- = log 10 + log 1.1\nlemma log_thirteen_le : Real.log 13 ≤ 2.565  -- 13 ≤ e^2.565 via (Σ_{k<7} 0.64125^k/k!)^4\nlemma log_fourteen_ge : (2.6388 : ℝ) ≤ Real.log 14  -- log 2 + (2 + log(7/e²)); log(7/e²) = −log(e²/7) ≥ −(...)\nlemma log_23_13_le : Real.log (23/13) ≤ 0.571\nlemma log_17_14_le : Real.log (17/14) ≤ 0.1942\nlemma log_two_point_three_le : Real.log 2.3 ≤ 0.833\nlemma one_div_exp_one_le : (1 : ℝ)/Real.exp 1 ≤ 0.3679\nlemma log_log_le_div_e {x : ℝ} (hx : 1 < x) : Real.log (Real.log x) ≤ (1/Real.exp 1) * Real.log x\n```\n\nHmm wait — for log_ten_ge I use 10/e = 4·(2.5/e): log(10/e) = log 4 + log(2.5/e) = 2 log 2 + log(2.5/e). log(2.5/e): 2.5/e < 1: = −log(e/2.5): e/2.5 = 1/(1−y) with 1−y = 2.5/e ⟺ y = (e−2.5)/e = 1−2.5/e. −log(e/2.5) = −(−log(2.5/e)) = log(2.5/e)... let me redo: log(2.5/e) = −log(e/2.5). And e/2.5 = 1/(2.5/e) = 1/(1−y) with 1−y := 2.5/e. So log(e/2.5) = −log(1−y) ≤ y+y²/2+y³/(3(1−y)). So log(2.5/e) ≥ −[y+y²/2+y³/(3(1−y))].\nNumbers: e ≤ 2.7182819 (Real.exp_one_lt_d9: exp 1 < 2.7182818286 — use 2.7182819 as the rational upper) and e ≥ 2.7182818 (Real.exp_one_gt_d9: 2.7182818283 < exp 1 ✓). 1−y = 2.5/e ≥ 2.5/2.7182819 = 0.919698; y = 1−2.5/e ≤ 1−2.5/2.7182819 = 0.0803017·... compute: 2.5/2.7182819 = 0.91969793·... y ≤ 0.08030207. And 1−y ≥ 0.9196979. Bound: y+y²/2+y³/(3(1−y)) ≤ 0.0803021+0.00322421+0.00018773 = 0.08371405. log(2.5/e) ≥ −0.0837141. log 10 = 1+2·log 2+log(2.5/e) ≥ 1+2·0.6931471−0.0837141 = 2.3025801 ≥ 2.3025 ✓.\n\n(log 2 ≥ 0.6931471: Mathlib `Real.log_two_gt_d9 : 0.6931471803 < log 2` ✓.)\n\nFor log_fourteen_ge: log 14 = log 2 + log 7; log 7 = 2 + log(7/e²) (7 = e²·(7/e²)); log(7/e²) = −log(e²/7); e²/7 = 1/(7/e²) = 1/(1−y') with 1−y' = 7/e². e² ≤ 7.3890562 (e ≤ 2.7182819 ⟹ e² ≤ 2.7182819² = 7.3890561·... = 7.38905620 compute: 2.7182819² = 7.38905619·... norm_num). 7/e² ≥ 7/7.3890562 = 0.947346·... = 0.947347·... compute: 7/7.3890562 = 0.94734654·... So 1−y' ≥ 0.9473465, y' ≤ 0.0526535. Hmm — earlier I used y = 0.052828 (from e² ≥ 7.389 — direction: y' = 1−7/e², e² BIGGER ⟹ 7/e² smaller ⟹ y' BIGGER. e² ≤ 7.3890562 ⟹ y' ≤ 1−7/7.3890562 = 0.0526535. And y' ≥ 1−7/7.3890560 = 0.0526590·... whatever: y' ≤ 0.05266). −log(1−y') ≤ y'+y'²/2+y'³/(3(1−y')) ≤ 0.05266+0.00138655+0.00005134 = 0.05409789. log 7 ≥ 2−0.0540979 = 1.9459021. log 14 ≥ 0.6931471+1.9459021 = 2.6390492 ≥ 2.6388 ✓ (margin 2.5e-4 ✓). Then 0.1942/log 14 ≤ 0.1942/2.6388 = 0.073594 ≤ 0.0736 ✓.\n\nFor log_eleven_ge: log 11 = log 10 + log(11/10) = log 10 + log 1.1 ≥ 2.3025+0.0953083 = 2.3978083 ≥ 2.3978 ✓ (margin 8e-6 — VERY thin!! Let me double-check: log_one_add_ge with x = 0.1: 0.1−0.1²/2+0.1³/3−0.1⁴/4 = 0.1−0.005+0.000333333−0.000025 = 0.095308333. Sum: 2.3025+0.095308333 = 2.397808333 ≥ 2.3978 ✓ margin 8.3e-6. Thin but the pieces are exact: log 10 ≥ 2.3025 has margin 8e-5, log 1.1 ≥ 0.09530833 exact. If I want more margin: use log 11 = log 10 + log 1.1 with log 10 ≥ 2.30258 (the computed bound 2.3025801): state log_ten_ge as 2.3025 but internally it's 2.30258 — the sum ≥ 2.3978 has total margin 8.8e-5+8.3e-6 = ~9e-5 if I use the internal values: 1+2·0.6931471−0.0837141+0.0953083 = 2.3025801+0.0953083 = 2.3978884 ≥ 2.3978 ✓ margin 8.8e-5 ✓ FINE — as long as log_eleven_ge's proof uses the SHARPER internal bounds, not the rounded lemma statements.)\n\nThen 0.833/log 11 ≤ 0.833/2.3978 = 0.34740 ≤ 0.3475 ✓.\n\nOK. And the S₃ sqrt bounds and the farW machinery — chunk 9b. And the six bricks — 9c, using:\n- `AntitoneOn.tsum_comp_add_le_integral` (pattern in this file at tsum_log_div_sq_tail_le).\n- RW₂/LA₂ via the pointwise loglog ≤ (1/e)·log trick + tsum_le_tsum.\n\nLet me now also decide the exact brick statements (they'll feed 3c):\n- `farW : ℕ → ℝ := fun k => 1/((k:ℝ)·Real.sqrt (1+(k:ℝ)^2))`\n- `farW_nonneg`, `farW_le_inv_sq : farW k ≤ 1/(k:ℝ)^2`.\n- S₃: `farW_tsum_le : ∑' k, farW (k+1) ≤ 1.3476` and `farW_Ico_le : ∀ K, ∑ k ∈ Finset.Ico 1 (K+1), farW k ≤ 1.3476`.\n- RW₀: `tail11_inv_sq_le : ∑' k, (1:ℝ)/((k:ℝ)+11)^2 ≤ 0.1`.\n- RW₁: `tail11_log_div_sq_le : ∑' k, Real.log ((k:ℝ)+11)/((k:ℝ)+11)^2 ≤ 0.3303`.\n- RW₂: `tail11_loglog_div_sq_le : ∑' k, Real.log (Real.log ((k:ℝ)+11))/((k:ℝ)+11)^2 ≤ 0.3679 * 0.3303` — hmm, or give the numeric 0.12151: 0.3679·0.3303 = 0.12151227. Use the factored form (1/e)·0.3303 — cleaner for assembly: the assembly uses 0.886·(0.3475·W₀+W₂): with W₂ ≤ (1/e)·W₁ ≤ 0.3679·0.3303. I'll state with 0.3679·0.3303 literal or compute. Keep factored.\n- LA₀: `tail14_inv_add_sq_le : ∑' j, (1:ℝ)/((j:ℝ)+14+10)^2 ≤ 1/23` — hmm the (j+14+10) vs (j+24): the antitone integral gives ∑'_{j} f(j+14) ≤ ∫₁₃^∞ f with f = 1/(x+10)². So the tsum is over f(j+14) = 1/(j+24)². State: ∑' j, (1:ℝ)/(((j:ℝ)+14)+10)^2 ≤ 1/23.\n- LA₁: `tail14_log_div_add_sq_le : ∑' j, Real.log ((j:ℝ)+14)/(((j:ℝ)+14)+10)^2 ≤ 0.1687`.\n- LA₂: ≤ 0.3679·0.1687.\n\nHmm — the tsum index forms (j:ℝ)+14 vs ↑(j+14): the `AntitoneOn.tsum_comp_add_le_integral` gives ∑'_{n:ℕ} f(n+c+1) where the cast is ↑(n+c+1) — need the congr to ((n:ℝ)+14) form — the file already has this pattern (tsum_log_div_sq_tail_le with ↑(n+3+1) = (n:ℝ)+4 bridge ✓ clone).\n\nTime to write. I'll draft chunk 9a + 9b and compile. Actually, let me write the whole §9 draft in one Write-append, then compile and fix errors iteratively. The file is edited via Edit (append before `end NguyenRH1`).\n\nOne more design decision: where does the digamma piece 6's section end — the file ends with `end NguyenRH1` then `end`. I'll insert §9 before `end NguyenRH1`.\n\nLet me draft chunk 9a (certified numerics). For the exp-partial-sum upper bounds on log (log x ≤ U ⟺ x ≤ e^U), pattern from this file's log 3 ≤ 1.1:\n```\nhave h3le : (3 : ℝ) ≤ Real.exp 1.1 := by\n  have h := Real.sum_le_exp_of_nonneg (show (0:ℝ) ≤ 1.1 by norm_num) 6\n  rw [Finset.sum_range_succ, ... unfold ...] at h\n  norm_num at h\n  linarith [h]\nhave h2 : Real.log 3 ≤ Real.log (Real.exp 1.1) := Real.log_le_log (by norm_num) h3le\nrwa [Real.log_exp] at h2\n```\n`Real.sum_le_exp_of_nonneg (hx : 0 ≤ x) (n : ℕ) : ∑ k in range n, x^k/k! ≤ exp x`? The usage: `Real.sum_le_exp_of_nonneg (show (0:ℝ) ≤ 1.1 by norm_num) 6` gave Σ_{k<6} 1.1^k/k! ≤ e^1.1 ✓.\n\nFor e^2.3026 ≥ 10 via the 8th-power route: \n```\nhave hbase : (1.333524 : ℝ) ≤ Real.exp 0.287825 := Σ_{k<6} 0.287825^k/k! ≥ 1.333524 (norm_num)\nhave h2 : (1.333524 : ℝ)^8 ≤ (Real.exp 0.287825)^8 := pow_le_pow_left₀ ...\nhave h3 : (Real.exp 0.287825)^8 = Real.exp 2.3026 := by rw [← Real.exp_nat_mul... \n```\nHmm: (exp 0.287825)^8 = exp (8·0.287825) = exp 2.3026: `Real.exp_nat_mul`? there's `Real.exp_nat_mul (x : ℝ) (n : ℕ) : exp (n * x) = (exp x)^n`? or `Real.exp_nsmul`? Probably `Real.exp_nat_mul : exp (n * x) = exp x ^ n`. Then 8·0.287825 = 2.3026 by norm_num. And (1.333524)^8 ≥ 10 by norm_num (big rational — norm_num should handle 1.333524^8: it's (1333524/1000000)^8 — big numerators but OK... might be slow; alternative chain: 1.333524² ≥ 1.778287 (norm_num), 1.778287² ≥ 3.162304, 3.162304² ≥ 10.00016 ✓ stepwise squaring, each norm_num-friendly).\n\nFor e^2.565 ≥ 13: (Σ_{k<7} 0.64125^k/k!) ≥ 1.898858: ^4 via two squarings: 1.898858² ≥ 3.605662, 3.605662² ≥ 13.00080 ✓.\n\nFor e^0.571 ≥ 23/13: Σ_{k<6} 0.571^k/k! ≥ 1.77 ≥ 23/13 (23/13 = 1.7692308; 1.77 ≥ 23/13 ⟺ 1.77·13 = 23.01 ≥ 23 ✓ norm_num).\nFor e^0.1942 ≥ 17/14: Σ_{k<5} ≥ 1.2143 ≥ 17/14 (1.2143·14 = 17.0002 ≥ 17 ✓).\nFor e^0.833 ≥ 2.3: Σ_{k<8} 0.833^k/k! ≥ 2.3002 ≥ 2.3 ✓.\n\nLet me precompute the partial sums precisely to make sure the norm_num targets are valid:\n- Σ_{k<6} 0.287825^k/k!: computed above ≈ 1.333524 (1+0.287825+0.041422+0.003974+0.000286 = 1.333507+... let me recompute carefully: k=0: 1; k=1: 0.287825; k=2: 0.287825²/2 = 0.082842/2 = 0.041421; k=3: 0.041421·0.287825/3 = 0.011923/3 = 0.003974; k=4: 0.003974·0.287825/4 = 0.001144/4 = 0.000286; k=5: 0.000286·0.287825/120 = 0.0000823/120 = 0.0000007. Sum: 1+0.287825+0.041421+0.003974+0.000286+0.0000007 = 1.3335067. Hmm — so Σ_{k<6} ≈ 1.3335067, NOT 1.333524 (I mis-added before). 1.3335067^8: 1.3335067² = 1.778240; ^4 = 3.162137; ^8 = 9.999110 ✗ < 10!!! Need more terms: k=6: 0.0000007·0.287825/6·... = 0.00000003: no help. So e^2.3026 ≥ (1.3335067)^8 = 9.99911 < 10 ✗ FAILS.\n  Use U/2 = 1.1513: e^1.1513 ≥ Σ_{k<8}: 1+1.1513+0.662745+0.254348+0.073205+0.016855+0.003234+0.000532 = 3.162219: ² = 9.999630 ✗ < 10. k<9: +0.0000875: 3.162307² = 10.000187 ✓ ≥ 10 ✓. So e^2.3026 ≥ (Σ_{k<9} 1.1513^k/k!)² ≥ 3.162307² ≥ 10.000187. Norm_num: 3.162307² = 10.000187 ✓.\n  Hmm wait, let me double check e^1.1513: true e^1.1513 = 3.162306·... (e^1.1513 = e^1·e^0.1513 = 2.71828·1.16335 = 3.16229). And e^2.3026 = (e^1.1513)² ✓. Σ_{k<9} 1.1513^k/k!: terms: k=0: 1; k=1: 1.1513; k=2: 1.325491/2 = 0.6627455; k=3: 0.6627455·1.1513/3 = 0.763017/3 = 0.254339; k=4: 0.254339·1.1513/4 = 0.292813/4 = 0.0732033; k=5: 0.0732033·1.1513/5 = 0.084279/5 = 0.0168558; k=6: 0.0168558·1.1513/6 = 0.019406/6 = 0.0032343; k=7: 0.0032343·1.1513/7 = 0.0037237/7 = 0.0005320; k=8: 0.0005320·1.1513/8 = 0.0006125/8 = 0.0000766. Sum: 1+1.1513+0.6627455+0.254339+0.0732033+0.0168558+0.0032343+0.0005320+0.0000766 = 3.1622865. ² = 10.000056 ✓ ≥ 10 (margin 5.6e-5 — thin but valid; true e^1.1513 = 3.162306 vs partial 3.162287).\n  Even safer: use log 10 ≤ 2.3026 via log 10 = log 2 + log 5 with log 5 ≤ 1.6095 (5 ≤ e^1.6095): e^1.6095 ≥ 5: e^1.6095 = e·e^0.6095: e^0.6095 ≥ Σ_{k<7}: 1+0.6095+0.185745+0.037737+0.005749+0.000701 = 1.839432: e^1.6095 ≥ 2.7182818·1.839432 = 5.0000064 ✓ ≥ 5 (margin 6e-6 — thin!). Σ_{k<8}: +0.0000712: 1.839503: ×2.7182818 = 5.000200 ✓ better. log 5 ≤ 1.6095 ⟹ log 10 = log 2+log 5 ≤ 0.6932+1.6095 = 2.3027 ✗ > 2.3026!! DAMN. log 2 ≤ 0.69315 (log_two_lt_d9: log 2 < 0.6931471809): log 10 ≤ 0.6931472+1.6095 = 2.3026472 ✗. Tighter log 5: log 5 ≤ 1.60945: e^1.60945 ≥ 5: e^0.60945: Σ_{k<8}: 1+0.60945+0.185715+0.037728+0.005747+0.000701+0.0000712 = 1.839412: ×2.7182818 = 4.9999433 ✗ < 5. k<9: +0.0000072: 1.839419: ×2.7182818 = 4.9999627 ✗. k<10: +0.00000063: ≈ 4.999975 ✗. TRUE e^1.60945 = 4.9999865·... < 5! So log 5 > 1.60945 — the bound log 5 ≤ 1.60945 is FALSE. True log 5 = 1.6094379. So log 5 ≤ 1.60944: log 10 ≤ 0.6931472+1.60944 = 2.3025872 ≤ 2.3026 ✓. e^1.60944 ≥ 5: e^0.60944 ≥ 5/2.7182818 = 1.8393972: Σ_{k<8} 0.60944^k/k!: 1+0.60944+0.185709+0.037724+0.005746+0.000700+0.0000711 = 1.8393901 ✗ < 1.8393972. k<9: +0.0000072: 1.8393973 ✓ ≥ 1.8393972 (margin 1e-7!!! way too thin). Hmm. This constant is genuinely tight: log 10 = 2.3025851 and 2.3026 gives only 1.5e-5 of room, i.e. e^2.3026 = 10.00015 — need the partial-sum route with e^2.3026 directly: (Σ_{k<9} 1.1513^k/k!)² = 3.1622865² = 10.0000563 ≥ 10 ✓ margin 5.6e-5 ✓ THAT's the better one. Let me double-check the partial sum 3.1622865²: 3.1622865² = 10.000056·... 3.1622865² = 10.00005635 ✓ ≥ 10 ✓.\n  Actually — even simpler and safer: log 10 ≤ 2.3026 via log 10 = log(10) and 10 ≤ 10.000056 = partial² ✓ as computed. GOOD.\n\n- e^2.565 ≥ 13 via (Σ_{k<7} 0.64125^k/k!)^4: partial ≈ 1.898858 (recompute: k=0: 1; k=1: 0.64125; k=2: 0.411201/2 = 0.2056008; k=3: 0.2056008·0.64125/3 = 0.131841/3 = 0.043947; k=4: 0.043947·0.64125/4 = 0.028181/4 = 0.0070453; k=5: 0.0070453·0.64125/5 = 0.0045178/5 = 0.0009036; k=6: 0.0009036·0.64125/6 = 0.0005794/6 = 0.0000966. Sum: 1+0.64125+0.2056008+0.043947+0.0070453+0.0009036+0.0000966 = 1.8988433. ^4: 1.8988433² = 3.6056054; ^4 = 13.000393 ✓ ≥ 13 ✓ margin 4e-4 ✓.\n\nGood. Now write the code. Also needed: `Real.exp_one_gt_d9`/`lt_d9` names: used in this file: `Real.exp_one_lt_d9.le` (line 289) ✓ and presumably `Real.exp_one_gt_d9`. \n\nLet me now write chunk 9a. I'll write the whole section and compile.","signature":""},{"type":"text","text":"All patterns confirmed. Now I'll write §9 (piece 3a: certified numerics + weight bricks). Appending to LiTightR.lean before the final `end`."},{"type":"tool_use","id":"Edit_39","name":"Edit","input":{"replace_all":false,"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiTightR.lean","old_string":"end NguyenRH1\n\nend","new_string":"/-! ## 9. Piece 3a: certified numerics for the far-sum bricks\n\nThe integral-comparison machines (`log_one_add_ge`, `neg_log_one_sub_le`)\nand the certified log/exp bounds feeding the interval-count bridges and\nthe weight-sum bricks. -/\n\n/-- log(1+x) ≥ x − x²/2 + x³/3 − x⁴/4 for x ≥ 0 (1/(1+t) ≥ 1−t+t²−t³ on\n[0, x], since 1 − (1−t+t²−t³)(1+t) = t⁴ ≥ 0). -/\nlemma log_one_add_ge {x : ℝ} (hx : 0 ≤ x) :\n    x - x ^ 2 / 2 + x ^ 3 / 3 - x ^ 4 / 4 ≤ Real.log (1 + x) := by\n  have hF : ∀ t ∈ Set.uIcc 0 x,\n      HasDerivAt (fun y => Real.log (1 + y)) (1 / (1 + t)) t := by\n    intro t ht\n    have ht0 : (0 : ℝ) ≤ t := by\n      have h := ht.1\n      rwa [Set.uIcc_of_le hx, Set.mem_Icc] at h\n    exact (Real.hasDerivAt_log (by linarith : (1 : ℝ) + t ≠ 0)).comp t\n      ((hasDerivAt_id' t).const_add 1)\n  have hG : ∀ t ∈ Set.uIcc 0 x,\n      HasDerivAt (fun y => y - y ^ 2 / 2 + y ^ 3 / 3 - y ^ 4 / 4)\n        (1 - t + t ^ 2 - t ^ 3) t := by\n    intro t ht\n    have h1 := (hasDerivAt_id' t).sub (((hasDerivAt_pow 2 t).div_const 2))\n    have h2 := h1.add (((hasDerivAt_pow 3 t).div_const 3))\n    have h3 := h2.sub (((hasDerivAt_pow 4 t).div_const 4))\n    rw [show (fun y => y - y ^ 2 / 2 + y ^ 3 / 3 - y ^ 4 / 4)\n        = (fun y => y - y ^ 2 / 2 + y ^ 3 / 3) - fun y => y ^ 4 / 4 from by\n          ext y; simp only [Pi.sub_apply]] at *\n    rw [show (1 : ℝ) - t + t ^ 2 - t ^ 3\n        = (1 - 2 * t / 2 + 3 * t ^ 2 / 3) - 4 * t ^ 3 / 4 from by ring]\n    convert h3 using 2 <;> ring\n  have hInt1 : ∫ t in (0 : ℝ)..x, 1 / (1 + t) = Real.log (1 + x) := by\n    rw [intervalIntegral.integral_eq_sub_of_hasDerivAt hF]\n    · simp [Real.log_one]\n    · apply Continuous.intervalIntegrable\n      exact continuous_const.div (continuous_const.add continuous_id)\n        (fun t => by positivity)\n  have hInt2 : ∫ t in (0 : ℝ)..x, (1 - t + t ^ 2 - t ^ 3)\n      = x - x ^ 2 / 2 + x ^ 3 / 3 - x ^ 4 / 4 := by\n    rw [intervalIntegral.integral_eq_sub_of_hasDerivAt hG]\n    · ring_nf\n    · exact Continuous.intervalIntegrable (by fun_prop)\n  have hmono : ∫ t in (0 : ℝ)..x, (1 - t + t ^ 2 - t ^ 3)\n      ≤ ∫ t in (0 : ℝ)..x, 1 / (1 + t) := by\n    apply intervalIntegral.integral_mono_on hx.le\n    · exact Continuous.intervalIntegrable (by fun_prop)\n    · apply Continuous.intervalIntegrable\n      exact continuous_const.div (continuous_const.add continuous_id)\n        (fun t => by positivity)\n    · intro t ht\n      rw [Set.mem_Icc] at ht\n      have h1 : (0 : ℝ) < 1 + t := by linarith [ht.1]\n      rw [div_le_iff₀ h1]\n      have h2 : (1 - t + t ^ 2 - t ^ 3) * (1 + t) = 1 - t ^ 4 := by ring\n      rw [h2]\n      have h3 : t ^ 4 ≥ 0 := by positivity\n      linarith [ht.1]\n  rw [hInt1, hInt2] at hmono\n  exact hmono\n\n/-- −log(1−y) ≤ y + y²/2 + y³/(3(1−y)) for 0 ≤ y < 1\n(1/(1−t) ≤ 1 + t + t²/(1−y) on [0, y]). -/\nlemma neg_log_one_sub_le {y : ℝ} (hy0 : 0 ≤ y) (hy1 : y < 1) :\n    -Real.log (1 - y) ≤ y + y ^ 2 / 2 + y ^ 3 / (3 * (1 - y)) := by\n  have hF : ∀ t ∈ Set.uIcc 0 y,\n      HasDerivAt (fun x => -Real.log (1 - x)) (1 / (1 - t)) t := by\n    intro t ht\n    have ht1 : t < 1 := by\n      have h := ht.2\n      rwa [Set.uIcc_of_le hy0, Set.mem_Icc] at h\n    have h1 := (Real.hasDerivAt_log (by linarith : (1 : ℝ) - t ≠ 0)).comp t\n      ((hasDerivAt_id' t).const_sub 1)\n    have h2 := h1.neg\n    rw [show (fun x => -Real.log (1 - x))\n        = -(Real.log ∘ fun x => 1 - x) from by ext x; simp [Function.comp_def]] at *\n    rw [show (1 : ℝ) / (1 - t) = -((1 - t)⁻¹ * -1) from by field_simp]\n    convert h2 using 2 <;> ring\n  have hG : ∀ t ∈ Set.uIcc 0 y,\n      HasDerivAt (fun x => x + x ^ 2 / 2 + x ^ 3 / (3 * (1 - y)))\n        (1 + t + t ^ 2 / (1 - y)) t := by\n    intro t ht\n    have h1 := (hasDerivAt_id' t).add (((hasDerivAt_pow 2 t).div_const 2))\n    have h2 := h1.add (((hasDerivAt_pow 3 t).div_const (3 * (1 - y))))\n    rw [show (fun x => x + x ^ 2 / 2 + x ^ 3 / (3 * (1 - y)))\n        = (fun x => x + x ^ 2 / 2) + fun x => x ^ 3 / (3 * (1 - y)) from by\n          ext x; simp only [Pi.add_apply]] at *\n    rw [show (1 : ℝ) + t + t ^ 2 / (1 - y)\n        = (1 + 2 * t / 2) + 3 * t ^ 2 / (3 * (1 - y)) from by ring]\n    convert h2 using 2 <;> ring\n  have hInt1 : ∫ t in (0 : ℝ)..y, 1 / (1 - t) = -Real.log (1 - y) := by\n    rw [intervalIntegral.integral_eq_sub_of_hasDerivAt hF]\n    · simp [Real.log_one]\n    · apply Continuous.intervalIntegrable\n      exact continuous_const.div (continuous_const.sub continuous_id)\n        (fun t => by\n          have h1 : t ≠ 1 ∨ (1 : ℝ) - t ≠ 0 := by\n            by_contra h\n            push_neg at h\n            exact absurd h.1 (sub_ne_zero.mp h.2)\n          obtain h1 | h1 := h1\n          · intro h2\n            rw [sub_eq_zero] at h2\n            exact h1 h2\n          · exact h1)\n  have hInt2 : ∫ t in (0 : ℝ)..y, (1 + t + t ^ 2 / (1 - y))\n      = y + y ^ 2 / 2 + y ^ 3 / (3 * (1 - y)) := by\n    rw [intervalIntegral.integral_eq_sub_of_hasDerivAt hG]\n    · ring_nf\n    · exact Continuous.intervalIntegrable (by fun_prop)\n  have hmono : ∫ t in (0 : ℝ)..y, 1 / (1 - t)\n      ≤ ∫ t in (0 : ℝ)..y, (1 + t + t ^ 2 / (1 - y)) := by\n    apply intervalIntegral.integral_mono_on hy0\n    · apply Continuous.intervalIntegrable\n      exact continuous_const.div (continuous_const.sub continuous_id)\n        (fun t => sub_ne_zero.mpr (by linarith [hy1] : t ≠ 1))\n    · exact Continuous.intervalIntegrable (by fun_prop)\n    · intro t ht\n      rw [Set.mem_Icc] at ht\n      have h1 : (0 : ℝ) < 1 - t := by linarith [ht.2, hy1]\n      have h2 : (0 : ℝ) < 1 - y := by linarith [hy1]\n      rw [le_div_iff₀ h1]\n      have h3 : (1 + t + t ^ 2 / (1 - y)) * (1 - t)\n          = 1 - t ^ 2 + t ^ 2 * (1 - t) / (1 - y) := by field_simp; ring\n      rw [h3]\n      have h4 : t ^ 2 * (1 - t) / (1 - y) ≥ t ^ 2 := by\n        have h5 : (1 - y) ≤ (1 - t) := by linarith [ht.2]\n        have h6 : (0 : ℝ) ≤ t ^ 2 := by positivity\n        rw [div_le_iff₀ h2]\n        calc t ^ 2 * (1 - y) ≤ t ^ 2 * (1 - t) :=\n              mul_le_mul_of_nonneg_left h5 h6\n          _ = t ^ 2 * (1 - t) * 1 := (mul_one _).symm\n      linarith\n  rw [hInt1, hInt2] at hmono\n  exact hmono\n\n/-- log 1.1 ≥ 0.0953 (the x = 0.1 alternating bound). -/\nlemma log_one_point_one_ge : (0.0953 : ℝ) ≤ Real.log 1.1 := by\n  have h := log_one_add_ge (show (0 : ℝ) ≤ (0.1 : ℝ) by norm_num)\n  have h2 : (1 : ℝ) + (0.1 : ℝ) = 1.1 := by norm_num\n  rw [h2] at h\n  norm_num at h ⊢\n  linarith [h]\n\n/-- log 10 ≥ 2.3025: log 10 = 1 + 2·log 2 + log(2.5/e), with\nlog(2.5/e) ≥ −(y + y²/2 + y³/(3(1−y))), y = 1 − 2.5/e ≤ 0.0803021. -/\nlemma log_ten_ge : (2.3025 : ℝ) ≤ Real.log 10 := by\n  have hlog2 : (0.6931471 : ℝ) ≤ Real.log 2 := Real.log_two_gt_d9.le.trans (by norm_num)\n  have he1 : (2.7182818 : ℝ) ≤ Real.exp 1 := Real.exp_one_gt_d9.le.trans (by norm_num)\n  have he2 : Real.exp 1 ≤ (2.7182819 : ℝ) := Real.exp_one_lt_d9.le.trans (by norm_num)\n  -- y := 1 − 2.5/e and its bounds\n  set y : ℝ := 1 - 2.5 / Real.exp 1 with hy\n  have hylo : (0 : ℝ) ≤ y := by\n    rw [hy]\n    have h : (2.5 : ℝ) / Real.exp 1 ≤ 2.5 / 2.7182818 :=\n      div_le_div_of_nonneg_left (by norm_num) (by linarith [Real.exp_pos 1])\n        (by exact_mod_cast he1)\n    have h2 : (2.5 : ℝ) / 2.7182818 ≤ 1 := by norm_num\n    linarith [Real.exp_pos 1, h, h2]\n  have hyub : y ≤ (0.0803021 : ℝ) := by\n    rw [hy]\n    have h : (2.5 : ℝ) / 2.7182819 ≤ 2.5 / Real.exp 1 :=\n      div_le_div_of_nonneg_left (by norm_num) (by norm_num)\n        (by exact_mod_cast he2)\n    have h2 : (0.9196979 : ℝ) ≤ 2.5 / 2.7182819 := by norm_num\n    have h3 := h2.trans h\n    linarith\n  have h1my : (0.9196979 : ℝ) ≤ 1 - y := by\n    rw [hy]\n    have h : (2.5 : ℝ) / Real.exp 1 ≤ 2.5 / 2.7182818 :=\n      div_le_div_of_nonneg_left (by norm_num) (by linarith [Real.exp_pos 1])\n        (by exact_mod_cast he1)\n    have h2 : (2.5 : ℝ) / 2.7182818 ≤ 0.91969793 := by norm_num\n    have h3 := h.trans h2\n    linarith\n  have hy1 : y < 1 := by\n    have h : (0 : ℝ) < 2.5 / Real.exp 1 := by positivity\n    rw [hy]\n    linarith\n  have hmain := neg_log_one_sub_le hylo hy1\n  -- −log(1−y) ≤ 0.0837141\n  have hub : -Real.log (1 - y) ≤ (0.0837141 : ℝ) := by\n    have h1 : y + y ^ 2 / 2 + y ^ 3 / (3 * (1 - y))\n        ≤ (0.0803021 : ℝ) + 0.0803021 ^ 2 / 2 + 0.0803021 ^ 3 / (3 * 0.9196979) := by\n      have h2 : y ^ 3 / (3 * (1 - y)) ≤ 0.0803021 ^ 3 / (3 * 0.9196979) := by\n        have h3 : (0 : ℝ) ≤ y ^ 3 := by positivity\n        have h4 : (0 : ℝ) < 3 * (1 - y) := by positivity\n        rw [div_le_div_iff₀ h4 (by positivity : (0 : ℝ) < 3 * 0.9196979)]\n        have h5 : y ^ 3 ≤ 0.0803021 ^ 3 := by\n          exact pow_le_pow_left₀ hylo hyub 3\n        have h6 : (3 * 0.9196979 : ℝ) ≤ 3 * (1 - y) := by linarith [h1my]\n        nlinarith [h5, h6, h3]\n      have h7 : y ^ 2 ≤ 0.0803021 ^ 2 := pow_le_pow_left₀ hylo hyub 2\n      linarith [h2, h7]\n    have h8 : (0.0803021 : ℝ) + 0.0803021 ^ 2 / 2 + 0.0803021 ^ 3 / (3 * 0.9196979)\n        ≤ 0.0837141 := by norm_num\n    linarith [hmain, h1, h8]\n  -- log(2.5/e) = log(1−y) ≥ −0.0837141\n  have hlog25 : Real.log (2.5 / Real.exp 1) = Real.log (1 - y) := by\n    rw [hy]\n    ring_nf\n  -- the decomposition log 10 = 1 + 2 log 2 + log(2.5/e)\n  have hdecomp : Real.log 10 = 1 + 2 * Real.log 2 + Real.log (2.5 / Real.exp 1) := by\n    have h1 : (10 : ℝ) = Real.exp 1 * 2 * 2 * (2.5 / Real.exp 1) := by\n      field_simp [Real.exp_ne_zero 1]\n      ring\n    rw [h1, Real.log_mul (Real.exp_ne_zero 1) (by norm_num : (2 : ℝ) * 2 * (2.5 / Real.exp 1) ≠ 0),\n      Real.log_exp]\n    have h2 : Real.log (2 * 2 * (2.5 / Real.exp 1))\n        = Real.log (2 * 2) + Real.log (2.5 / Real.exp 1) :=\n      Real.log_mul (by norm_num) (by positivity : (2.5 : ℝ) / Real.exp 1 ≠ 0)\n    rw [h2, Real.log_mul (by norm_num : (2 : ℝ) ≠ 0) (by norm_num : (2 : ℝ) ≠ 0)]\n    ring\n  linarith [hdecomp, hlog2, hub, hlog25]\n\n/-- log 10 ≤ 2.3026: 10 ≤ (Σ_{k<9} 1.1513ᵏ/k!)² ≤ e^{1.1513·2} = e^{2.3026}. -/\nlemma log_ten_le : Real.log 10 ≤ (2.3026 : ℝ) := by\n  have hbase : (3.1622865 : ℝ) ≤ Real.exp 1.1513 := by\n    have h := Real.sum_le_exp_of_nonneg (show (0 : ℝ) ≤ 1.1513 by norm_num) 9\n    rw [Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_succ,\n      Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_succ,\n      Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_succ,\n      Finset.sum_range_zero] at h\n    norm_num at h\n    linarith [h]\n  have hsq : (10 : ℝ) ≤ Real.exp 1.1513 * Real.exp 1.1513 := by\n    have h1 : (3.1622865 : ℝ) * 3.1622865 ≤ Real.exp 1.1513 * Real.exp 1.1513 :=\n      mul_le_mul hbase hbase (by norm_num) (Real.exp_pos 1).le\n    have h2 : (3.1622865 : ℝ) * 3.1622865 ≥ 10 := by norm_num\n    exact h2.trans h1\n  have h2 : Real.exp 1.1513 * Real.exp 1.1513 = Real.exp (1.1513 + 1.1513) := by\n    rw [Real.exp_add]\n  rw [h2] at hsq\n  have h3 : (1.1513 : ℝ) + 1.1513 = 2.3026 := by norm_num\n  rw [h3] at hsq\n  have h4 : Real.log 10 ≤ Real.log (Real.exp 2.3026) :=\n    Real.log_le_log (by norm_num : (0 : ℝ) < 10) hsq\n  rwa [Real.log_exp] at h4\n\n/-- log 11 ≥ 2.3978 (log 11 = log 10 + log 1.1). -/\nlemma log_eleven_ge : (2.3978 : ℝ) ≤ Real.log 11 := by\n  have h1 : (11 : ℝ) = 10 * 1.1 := by norm_num\n  have h2 : Real.log 11 = Real.log 10 + Real.log 1.1 := by\n    rw [h1]\n    exact Real.log_mul (by norm_num : (10 : ℝ) ≠ 0) (by norm_num : (1.1 : ℝ) ≠ 0)\n  have h3 := log_ten_ge\n  have h4 := log_one_point_one_ge\n  linarith [h2, h3, h4]\n\n/-- log 13 ≤ 2.565: 13 ≤ (Σ_{k<7} 0.64125ᵏ/k!)⁴ ≤ e^{2.565}. -/\nlemma log_thirteen_le : Real.log 13 ≤ (2.565 : ℝ) := by\n  have hbase : (1.8988433 : ℝ) ≤ Real.exp 0.64125 := by\n    have h := Real.sum_le_exp_of_nonneg (show (0 : ℝ) ≤ 0.64125 by norm_num) 7\n    rw [Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_succ,\n      Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_succ,\n      Finset.sum_range_succ, Finset.sum_range_zero] at h\n    norm_num at h\n    linarith [h]\n  have hsq2 : (1.8988433 : ℝ) * 1.8988433 ≤ Real.exp 0.64125 * Real.exp 0.64125 :=\n    mul_le_mul hbase hbase (by norm_num) (Real.exp_pos 0.64125).le\n  have hsq2n : (1.8988433 : ℝ) * 1.8988433 ≥ 3.6056054 := by norm_num\n  have hsq4 : (3.6056054 : ℝ) * 3.6056054\n      ≤ (Real.exp 0.64125 * Real.exp 0.64125) * (Real.exp 0.64125 * Real.exp 0.64125) := by\n    have h1 : (3.6056054 : ℝ) ≤ Real.exp 0.64125 * Real.exp 0.64125 := hsq2n.trans hsq2\n    exact mul_le_mul h1 h1 (by norm_num) (by positivity)\n  have hsq4n : (3.6056054 : ℝ) * 3.6056054 ≥ 13 := by norm_num\n  have h2 : (Real.exp 0.64125 * Real.exp 0.64125) * (Real.exp 0.64125 * Real.exp 0.64125)\n      = Real.exp (0.64125 * 4) := by\n    rw [← Real.exp_nat_mul]\n    ring_nf\n    rw [Real.exp_add, Real.exp_add]\n  have h3 : (0.64125 : ℝ) * 4 = 2.565 := by norm_num\n  have h13 : (13 : ℝ) ≤ Real.exp 2.565 := by\n    have h4 := hsq4n.trans hsq4\n    rw [h2, h3] at h4\n    exact h4\n  have h5 : Real.log 13 ≤ Real.log (Real.exp 2.565) :=\n    Real.log_le_log (by norm_num : (0 : ℝ) < 13) h13\n  rwa [Real.log_exp] at h5\n\n/-- log 14 ≥ 2.6388: log 14 = log 2 + 2 + log(7/e²), with\nlog(7/e²) ≥ −(y + y²/2 + y³/(3(1−y))), y = 1 − 7/e² ≤ 0.05266. -/\nlemma log_fourteen_ge : (2.6388 : ℝ) ≤ Real.log 14 := by\n  have hlog2 : (0.6931471 : ℝ) ≤ Real.log 2 := Real.log_two_gt_d9.le.trans (by norm_num)\n  have he1 : (2.7182818 : ℝ) ≤ Real.exp 1 := Real.exp_one_gt_d9.le.trans (by norm_num)\n  have he2 : Real.exp 1 ≤ (2.7182819 : ℝ) := Real.exp_one_lt_d9.le.trans (by norm_num)\n  have he2sq : Real.exp 1 * Real.exp 1 ≤ (7.3890562 : ℝ) := by\n    have h := mul_le_mul he2 he2 (by norm_num) (Real.exp_pos 1).le\n    have h2 : (2.7182819 : ℝ) * 2.7182819 ≤ 7.3890562 := by norm_num\n    exact h.trans h2\n  have he1sq : (7.3890559 : ℝ) ≤ Real.exp 1 * Real.exp 1 := by\n    have h := mul_le_mul he1 he1 (by norm_num) (Real.exp_pos 1).le\n    have h2 : (7.3890559 : ℝ) ≤ 2.7182818 * 2.7182818 := by norm_num\n    exact h2.trans h\n  set y : ℝ := 1 - 7 / (Real.exp 1 * Real.exp 1) with hy\n  have hylo : (0 : ℝ) ≤ y := by\n    rw [hy]\n    have h : (7 : ℝ) / (Real.exp 1 * Real.exp 1) ≤ 7 / 7.3890559 :=\n      div_le_div_of_nonneg_left (by norm_num) (by positivity) he1sq\n    have h2 : (7 : ℝ) / 7.3890559 ≤ 1 := by norm_num\n    have h3 := h.trans h2\n    linarith\n  have hyub : y ≤ (0.05266 : ℝ) := by\n    rw [hy]\n    have h : (7 : ℝ) / 7.3890562 ≤ 7 / (Real.exp 1 * Real.exp 1) :=\n      div_le_div_of_nonneg_left (by norm_num) (by norm_num) he2sq\n    have h2 : (0.94734 : ℝ) ≤ 7 / 7.3890562 := by norm_num\n    have h3 := h2.trans h\n    linarith\n  have h1my : (0.94734 : ℝ) ≤ 1 - y := by\n    rw [hy]\n    have h : (7 : ℝ) / (Real.exp 1 * Real.exp 1) ≤ 7 / 7.3890559 :=\n      div_le_div_of_nonneg_left (by norm_num) (by positivity) he1sq\n    have h2 : (7 : ℝ) / 7.3890559 ≤ 0.9473466 := by norm_num\n    have h3 := h.trans h2\n    linarith\n  have hy1 : y < 1 := by\n    have h : (0 : ℝ) < 7 / (Real.exp 1 * Real.exp 1) := by positivity\n    rw [hy]\n    linarith\n  have hmain := neg_log_one_sub_le hylo hy1\n  have hub : -Real.log (1 - y) ≤ (0.0540979 : ℝ) := by\n    have h1 : y + y ^ 2 / 2 + y ^ 3 / (3 * (1 - y))\n        ≤ (0.05266 : ℝ) + 0.05266 ^ 2 / 2 + 0.05266 ^ 3 / (3 * 0.94734) := by\n      have h2 : y ^ 3 / (3 * (1 - y)) ≤ 0.05266 ^ 3 / (3 * 0.94734) := by\n        have h3 : (0 : ℝ) ≤ y ^ 3 := by positivity\n        have h4 : (0 : ℝ) < 3 * (1 - y) := by positivity\n        rw [div_le_div_iff₀ h4 (by positivity : (0 : ℝ) < 3 * 0.94734)]\n        have h5 : y ^ 3 ≤ 0.05266 ^ 3 := pow_le_pow_left₀ hylo hyub 3\n        have h6 : (3 * 0.94734 : ℝ) ≤ 3 * (1 - y) := by linarith [h1my]\n        nlinarith [h5, h6, h3]\n      have h7 : y ^ 2 ≤ 0.05266 ^ 2 := pow_le_pow_left₀ hylo hyub 2\n      linarith [h2, h7]\n    have h8 : (0.05266 : ℝ) + 0.05266 ^ 2 / 2 + 0.05266 ^ 3 / (3 * 0.94734)\n        ≤ 0.0540979 := by norm_num\n    linarith [hmain, h1, h8]\n  have hlog7 : Real.log (7 / (Real.exp 1 * Real.exp 1)) = Real.log (1 - y) := by\n    rw [hy]\n  have hdecomp : Real.log 14\n      = Real.log 2 + 2 + Real.log (7 / (Real.exp 1 * Real.exp 1)) := by\n    have h1 : (14 : ℝ) = 2 * (Real.exp 1 * Real.exp 1) * (7 / (Real.exp 1 * Real.exp 1)) := by\n      field_simp [Real.exp_ne_zero 1]\n      ring\n    rw [h1, Real.log_mul (by norm_num : (2 : ℝ) ≠ 0)\n      (by positivity : (Real.exp 1 * Real.exp 1) * (7 / (Real.exp 1 * Real.exp 1)) ≠ 0)]\n    have h2 : Real.log ((Real.exp 1 * Real.exp 1) * (7 / (Real.exp 1 * Real.exp 1)))\n        = Real.log (Real.exp 1 * Real.exp 1) + Real.log (7 / (Real.exp 1 * Real.exp 1)) :=\n      Real.log_mul (by positivity : (Real.exp 1 * Real.exp 1) ≠ 0)\n        (by positivity : (7 : ℝ) / (Real.exp 1 * Real.exp 1) ≠ 0)\n    rw [h2, Real.log_exp]\n    ring\n  linarith [hdecomp, hlog2, hub, hlog7]\n\n/-- log(23/13) ≤ 0.571: 23/13 ≤ e^{0.571}. -/\nlemma log_23_13_le : Real.log (23 / 13) ≤ (0.571 : ℝ) := by\n  have hbase : (23 / 13 : ℝ) ≤ Real.exp 0.571 := by\n    have h := Real.sum_le_exp_of_nonneg (show (0 : ℝ) ≤ 0.571 by norm_num) 6\n    rw [Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_succ,\n      Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_succ,\n      Finset.sum_range_zero] at h\n    norm_num at h\n    linarith [h]\n  have h2 : Real.log (23 / 13) ≤ Real.log (Real.exp 0.571) :=\n    Real.log_le_log (by norm_num : (0 : ℝ) < 23 / 13) hbase\n  rwa [Real.log_exp] at h2\n\n/-- log(17/14) ≤ 0.1942: 17/14 ≤ e^{0.1942}. -/\nlemma log_17_14_le : Real.log (17 / 14) ≤ (0.1942 : ℝ) := by\n  have hbase : (17 / 14 : ℝ) ≤ Real.exp 0.1942 := by\n    have h := Real.sum_le_exp_of_nonneg (show (0 : ℝ) ≤ 0.1942 by norm_num) 5\n    rw [Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_succ,\n      Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_zero] at h\n    norm_num at h\n    linarith [h]\n  have h2 : Real.log (17 / 14) ≤ Real.log (Real.exp 0.1942) :=\n    Real.log_le_log (by norm_num : (0 : ℝ) < 17 / 14) hbase\n  rwa [Real.log_exp] at h2\n\n/-- log 2.3 ≤ 0.833: 2.3 ≤ e^{0.833}. -/\nlemma log_two_point_three_le : Real.log 2.3 ≤ (0.833 : ℝ) := by\n  have hbase : (2.3 : ℝ) ≤ Real.exp 0.833 := by\n    have h := Real.sum_le_exp_of_nonneg (show (0 : ℝ) ≤ 0.833 by norm_num) 8\n    rw [Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_succ,\n      Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_succ,\n      Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_zero] at h\n    norm_num at h\n    linarith [h]\n  have h2 : Real.log 2.3 ≤ Real.log (Real.exp 0.833) :=\n    Real.log_le_log (by norm_num : (0 : ℝ) < 2.3) hbase\n  rwa [Real.log_exp] at h2\n\n/-- 1/e ≤ 0.3679. -/\nlemma one_div_exp_one_le : (1 : ℝ) / Real.exp 1 ≤ 0.3679 := by\n  have he1 : (2.7182818 : ℝ) ≤ Real.exp 1 := Real.exp_one_gt_d9.le.trans (by norm_num)\n  have h1 : (1 : ℝ) / Real.exp 1 ≤ 1 / 2.7182818 :=\n    div_le_div_of_nonneg_left one_pos.le (Real.exp_pos 1) he1\n  have h2 : (1 : ℝ) / 2.7182818 ≤ 0.3679 := by norm_num\n  exact h1.trans h2\n\n/-- log u ≤ u/e for u > 0 (the tangent at u = e). -/\nlemma log_le_div_exp (u : ℝ) (hu : 0 < u) : Real.log u ≤ u / Real.exp 1 := by\n  have h := Real.log_le_sub_one_of_pos (x := u / Real.exp 1)\n    (div_pos hu (Real.exp_pos 1))\n  have h2 : Real.log (u / Real.exp 1) = Real.log u - 1 := by\n    rw [Real.log_div hu.ne' (Real.exp_ne_zero 1), Real.log_exp]\n  rw [h2] at h\n  have h3 : u / Real.exp 1 = u / Real.exp 1 := rfl\n  linarith [h]\n\n/-- log log x ≤ (1/e)·log x for x > 1. -/\nlemma log_log_le_div_exp {x : ℝ} (hx : 1 < x) :\n    Real.log (Real.log x) ≤ (1 / Real.exp 1) * Real.log x := by\n  have h1 : (0 : ℝ) < Real.log x := Real.log_pos hx\n  have h2 := log_le_div_exp (Real.log x) h1\n  rw [div_eq_mul_one_div] at h2\n  exact h2\n\nend NguyenRH1\n\nend"},"extra_content":null}]