[{"type":"thinking","thinking":"Section 9 (the certified numerics) compiles clean. Now chunk 9b: the weight `farW` + S₃ bound + the six tail bricks. Let me write those.\n\nfarW := fun k : ℕ => 1/((k:ℝ)·Real.sqrt (1+(k:ℝ)^2)).\n\nNeeded:\n1. `farW_nonneg`\n2. `farW_le_inv_sq : farW k ≤ 1/(k:ℝ)^2` (for k ≥ 1: k·√(1+k²) ≥ k·k = k² ⟹ 1/(k√(1+k²)) ≤ 1/k²).\n3. S₃: `farW_tsum_le : ∑' k : ℕ, farW (k+1) ≤ 1.3476`:\n   - summability of farW (k+1): dominated by 1/(k+1)² — `summable_one_div_nat_pow 2`-ish: Summable (fun n => 1/(n:ℝ)^2)? There's `Real.summable_one_div_nat_pow` : Summable (fun n => 1/(n:ℝ)^p) for 1 < p. For the shifted (k+1): use comparison with that via Summable.of_norm_bounded + the shift... The cleanest: farW (k+1) ≤ 1/(k+1)² and Summable (fun k => (1:ℝ)/((k:ℝ)+1)^2): from Real.summable_one_div_nat_pow via (summable_nat_add_iff 1).mpr-ish: Summable (fun n => 1/((n+1):ℝ)^2) = the (n+1)-shift of summable 1/n² — `(summable_nat_add_iff 1).mpr Real.summable_one_div_nat_pow` — gives Summable (fun n => 1/((n+1:ℕ):ℝ)^2)? The nat_add_iff: Summable (fun n => f (n+k)) ↔ Summable f. With f = fun n => 1/(n:ℝ)^2: f (n+1) = 1/((n+1:ℕ):ℝ)^2 — the cast forms ↑(n+1) vs ↑n+1 — push_cast bridges.\n   Hmm — but actually the telescope dominator is cleaner for the tail: for k ≥ 4: farW k ≤ 1/(k·(k−1))... The S₃ proof: split tsum at 4: ∑' farW(k+1) = Σ_{k ∈ range 4} farW(k+1) + ∑' farW(k+5). Bound the tail: farW (k+5) ≤ 1/((k+5)(k+4)) (since (k+5)·√(1+(k+5)²) ≥ (k+5)(k+4) ⟺ √(1+u²) ≥ u−1 with u = k+5 ✓ trivially since u−1 ≤ u ≤ √(1+u²)). And ∑' 1/((k+5)(k+4)) = 1/4 via telescope.\n   The exact terms: farW 1 ≤ 1/1.414 etc. via Real.le_sqrt.\n   - Telescope: tsum_one_div_mul_sub: ∑' k, 1/((k+5)(k+4)) = 1/4: write 1/((k+5)(k+4)) = 1/(k+4) − 1/(k+5): field_simp. Summable: telescoping with term → 0: `Summable` of differences of a convergent seq: there's `Summable.sub`-self... simplest: hasSum via partial sums: ∑_{k<N} (a k − a (k+1)) = a 0 − a N (Finset.sum_range_sub' — signature: ∑ i in range n, (f i − f (i+1)) = f 0 − f n — `Finset.sum_range_sub'`). Then HasSum (fun k => (1/(k+4) − 1/(k+5))) (1/4 − 0) via Tendsto (a N = 1/(N+4) → 0) + hasSum definition: HasSum f b ⟺ Tendsto (partial sums) → b: partial sum = 1/4 − 1/(N+4) → 1/4 (tendsto_sub tendsto_const_nhds (one_div→0 via tendsto_natCast_atTop + tendsto_inv_atTop_zero...)). Then tsum = 1/4 − 0 = ... wait: HasSum f (1/4 − lim) — the limit of (1/4 − 1/(N+4)) is 1/4 − 0 = 1/4 ✓.\n   The 1/(N+4) → 0: `tendsto_inv_atTop_zero.comp (tendsto_natCast_atTop_atTop.atTop_add ...)` — there's `tendsto_natCast_add_atTop`? Simpler: Tendsto (fun N : ℕ => (1:ℝ)/((N:ℝ)+4)) atTop (𝓝 0): rw [show (fun N => (1:ℝ)/((N:ℝ)+4)) = (fun N => ((N:ℝ)+4)⁻¹)]; apply tendsto_inv_atTop_zero.comp; exact tendsto_atTop_add_const_right... hmm: Tendsto (fun N : ℕ => (N:ℝ)+4) atTop atTop: (tendsto_natCast_atTop_atTop).atTop_add_const? There is `tendsto_natCast_atTop_atTop : Tendsto Nat.cast atTop atTop` and `.atTop_add_const_right 4`? Might be `tendsto_atTop_add_const_right`. I'll work it out in code.\n\n4. Ico version: `farW_Ico_le (K : ℕ) : ∑ k ∈ Finset.Ico 1 (K+1), farW k ≤ 1.3476` — via sum_le_tsum of the nonneg summable: `Summable.sum_le_tsum (s : Finset) (hf : ∀ i ∉ s, 0 ≤ f i) (hs : Summable f)` — with f = fun k => farW (k+1)? The Ico 1 (K+1) sums farW k for k = 1..K — reindex: = ∑ k ∈ range K, farW (k+1) (Finset.sum_Ico_eq_sum_range: ∑_{Ico a b} f = ∑_{range (b−a)} f(a+·)). Then sum_le_tsum with the shifted family ✓.\n\n5. The six bricks:\n   - RW₀: `tail11_inv_sq_le : ∑' k : ℕ, (1:ℝ)/((k:ℝ)+11)^2 ≤ 0.1`:\n     via AntitoneOn.tsum_comp_add_le_integral with f = 1/x² on Ici 10: pattern from tsum_log_div_sq_tail_le:\n     ```\n     have hle := antitoneOn_one_div_sq.tsum_comp_add_le_integral 10 integrable integrable-nonneg\n     ```\n     Need: `antitoneOn_one_div_sq : AntitoneOn (fun x => 1/x^2) (Set.Ici 10)` — direct: intro a ha b hb hab: 1/a² ≤... AntitoneOn f s = ∀ a ∈ s, ∀ b ∈ s, a ≤ b → f b ≤ f a: 1/b² ≤ 1/a² ⟺ a² ≤ b² (positivity): one_div_le_one_div_of_le (0 < a²) (a² ≤ b²) ✓ — wait the banked gotcha: \"one_div_le_one_div_of_le takes the small side's positivity first\": one_div_le_one_div_of_le (ha : 0 < a) (hab : a ≤ b) : 1/b ≤ 1/a ✓.\n     Integrable: ∫₁₀^∞ 1/x² = 1/10: antiderivative −1/x: `integral_Ioi_of_hasDerivAt_of_tendsto'` with F = −x⁻¹: HasDerivAt (−x⁻¹) (x⁻²) x: ((hasDerivAt_id' x).inv (ne)).neg — derivative of x⁻¹ is −x⁻², negated: x⁻² = 1/x² ✓. Tendsto → 0: tendsto_neg_atBot... (−1/x → 0): (tendsto_inv_atTop_zero).neg? −x⁻¹ → −0 = 0: simpa using tendsto_inv_atTop_zero.neg.\n     Then ∑'_{n} f(n+10+1) = ∑' 1/(n+11)² ≤ ∫₁₀^∞ = 1/10 = 0.1 ✓ and the cast bridge ↑(n+10+1) = (n:ℝ)+11 (the tsum_log_div_sq_tail_le pattern).\n   - RW₁: `tail11_log_div_sq_le : ∑' k, Real.log ((k:ℝ)+11)/((k:ℝ)+11)^2 ≤ 0.3303`:\n     f = log x/x²: antitone on Ici 10: `antitoneOn_log_div_sq` (Ici 3) mono to Ici 10: AntitoneOn.mono (subset: Ici 10 ⊆ Ici 3) ✓.\n     Integrable: integrableOn_log_div_sq (Ioi 3) mono to Ioi 10: IntegrableOn.mono_set (Ioi 10 ⊆ Ioi 3) ✓.\n     Integral ∫₁₀^∞ log x/x² = (log 10+1)/10: integral_Ioi_of_hasDerivAt_of_tendsto' (hasDerivAt_neg_log_add_one_div (x ≠ 0)) integrableOn... tendsto_neg_log_add_one_div: F(10) = −(log 10+1)/10: integral = 0 − F(10) = (log 10+1)/10 ≤ (2.3026+1)/10 = 0.33026 ≤ 0.3303 ✓ (log_ten_le).\n     Hmm — the tsum_comp_add_le_integral gives ∑' f(n+11) ≤ ∫_{Ioi 10} f — need the integral value computation: ∫ x in Ioi 10, log x/x² = (log 10+1)/10 — prove like integral_log_div_sq_Ioi_three but at 10.\n   - RW₂: `tail11_loglog_div_sq_le : ∑' k, Real.log (Real.log ((k:ℝ)+11))/((k:ℝ)+11)^2 ≤ (1/Real.exp 1) * 0.3303`:\n     pointwise: loglog(k+11)/(k+11)² ≤ (1/e)·log(k+11)/(k+11)² via log_log_le_div_exp (k+11 > 1 ✓). Then Summable.tsum_le_tsum with RW₁'s summable, RHS = (1/e)·∑' log/²  ≤ (1/e)·0.3303 — tsum_mul_left. Need summability of the loglog family: of_norm_bounded by (1/e)·log-family (nonneg: loglog(k+11) ≥ loglog 11 > 0 ✓ so norm = itself).\n     Actually state: ≤ (1/Real.exp 1) * 0.3303 — or numerically 0.12152 (0.36788·0.3303 = 0.12151...): keep factored (1/exp 1)·0.3303 — in assembly I'll bound 1/exp 1 ≤ 0.3679 via one_div_exp_one_le. Simpler for assembly: state `tail11_loglog_div_sq_le : ... ≤ 0.1216`: 0.3679·0.3303 = 0.12151227 ≤ 0.1216 ✓ — cleaner! Use 0.1216.\n   - LA₀: `tail14_inv_add_sq_le : ∑' j, (1:ℝ)/(((j:ℝ)+14)+10)^2 ≤ 1/23`:\n     f = 1/(x+10)²: antitone on Ici 13 (direct, like RW₀ with shift: 1/((a+10)²) ≥ 1/((b+10)²)), integrable (antiderivative −(x+10)⁻¹: HasDerivAt (−(x+10)⁻¹) ((x+10)⁻²): ((hasDerivAt_id' x).const_add 10).inv.ne... derivative of (x+10)⁻¹ = −(x+10)⁻²·1, negated ✓), ∫₁₃^∞ = 1/23 (0 − (−(13+10)⁻¹) = 1/23 ✓).\n   - LA₁: `tail14_log_div_add_sq_le : ∑' j, Real.log ((j:ℝ)+14)/(((j:ℝ)+14)+10)^2 ≤ 0.1687`:\n     f = log x/(x+10)²: antitone on Ici 13: derivative ((x+10)/x − 2 log x)/(x+10)³ ≤ 0 ⟸ (x+10)/x ≤ 2 log x: at x ≥ 13: (x+10)/x = 1+10/x ≤ 1+10/13 = 23/13 ≤ 1.77; 2 log x ≥ 2·log 13 ≥ 2·2.5649·... — need log 13 ≥ 2.5649 (e^2.5649 ≤ 13: e^2.5649 = ? true log 13 = 2.564949 — so log 13 ≥ 2.5649 ⟺ e^2.5649 ≤ 13: e^2.5649 ≈ 12.99935 ≤ 13 ✓ — exp partial sums LOWER bound gives e^2.5649 ≥ Σ... — that's a lower bound on exp, wrong direction!! For e^2.5649 ≤ 13 need an UPPER bound on exp: e^2.5649 = e²·e^0.5649 ≤ 7.3890566·e^0.5649: e^0.5649 ≤ 1/(1−0.5649)?? = 2.298: 7.3890566·2.298 = 16.98 ✗. e^0.5649 ≤ 1/(1−0.28245)² = 1.9437: 7.389·1.9437 = 14.36 ✗. e^0.5649 ≤ 1/(1−0.141225)⁴ = 1.8380: 7.389·1.8380 = 13.58 ✗. Hmm — need tighter: e^0.5649: true = 1.75916. 7.3890566·1.75916 = 12.9993 ✓. To prove e^0.5649 ≤ 1.7592 via... partial sums give lower bounds only. The 1/(1−x/n)ⁿ route converges slowly (computed above: n=16 gives 1.35717 for e^0.3025 vs true 1.35328 — 0.3% high). For e^0.5649 ≤ 1.7592: (1−0.5649/16)^{-16} = ? ln-side: −16·ln(1−0.03530625) = 16·(0.03530625+0.000623+0.0000147+...) = 16·0.0359508 = 0.575213: e^0.575213 = 1.7776 — hmm that's the value of (1−x/n)^{-n} — need it ≤ 1.7592: 1.7776 > 1.7592 ✗. n=32: −32·ln(1−0.017653) = 32·(0.017653+0.0001558+0.0000018) = 32·0.0178108 = 0.569947: e^0.569947 = 1.76808 ✗ still > 1.7592. This converges like c+const/n — too slow.\n     \n     ALTERNATIVE: log 13 ≥ 2.5649 via log 13 = log 14 − log(14/13) ≥ 2.6388 − log(14/13): log(14/13) ≤ 14/13−1 = 1/13 = 0.076923 (Real.log_le_sub_one_of_pos): log 13 ≥ 2.6388−0.0769 = 2.5619 ✗ < 2.5649. Better: log(14/13) ≤ the neg_log_one_sub route? log(14/13) = −log(13/14) = −log(1−1/14) ≤ y+y²/2+y³/(3(1−y)) with y = 1/14 = 0.0714286: ≤ 0.0714286+0.002551+0.0001309 = 0.0741105. log 13 ≥ 2.6388−0.0741105 = 2.5646895 ✗ < 2.5649 (by 2.1e-4!). Hmm — need log 14 sharper: the internal bound was 2.6390491. log 13 ≥ 2.6390491−0.0741105 = 2.5649386 ≥ 2.5649 ✓ (margin 3.9e-5). So: prove log 13 ≥ 2.5649 as a lemma USING log_fourteen_ge's sharper internals... but log_fourteen_ge only states ≥ 2.6388. Ugh. Make a bespoke: `log_thirteen_ge : (2.5649 : ℝ) ≤ Real.log 13` via log 13 = log 14 − log(14/13) with the sharper log-14 (recompute inside) — OR simpler: log 13 = log 2 + log 6.5 = log 2 + log(13/2): log(13/2) = log 6.5 = log(e·(6.5/e)) = 1+log(6.5/e): 6.5/e = 2.391465·... > 1: log(6.5/e) = −log(e/6.5): e/6.5 = 0.418197·... < 1: −log(1−y) with 1−y = e/6.5?? e/6.5 = 0.418197: −log(0.418197) = log(6.5/e)... I need log(6.5/e) with 6.5/e < 1: log(6.5/e) = −log(e/6.5), and e/6.5 < 1 so log(e/6.5) < 0, −log > 0: −log(e/6.5) = −log(1−y'), y' = 1−e/6.5 = 0.581803: −log(1−y') ≤ y'+y'²/2+y'³/(3(1−y')) — y' = 0.5818 big: 0.5818+0.16925+0.06564/(3·0.4182 = 1.2546) = 0.5818+0.16925+0.05231 = 0.80336: log 6.5 = 1+0.80336 = 1.80336?? true log 6.5 = 1.87180 — the bound 0.80336 vs true 0.87180 — the y³-tail bound is too crude for large y. Use more terms: y'+y'²/2+y'³/3+y'⁴/(4(1−y')): 0.5818+0.16925+0.06565+0.02866/(1.6728) = 0.5818+0.16925+0.06565+0.01713 = 0.83383 — still short. This needs a different series. \n     \n     MUCH SIMPLER: log 13 ≥ 2.5649 ⟺ 13 ≥ e^2.5649 — and I need an UPPER bound on e^2.5649. Use e^2.5649 = (e^0.6405... no. Use e^2.5649 = e^2.565/e^0.0001 ≈ 13.000393/1.0001 = 12.999 — I have e^2.565 ≥ 1.8988433⁴ (LOWER bound on exp — gives log 13 ≤ 2.565, the other direction). For e^2.5649 ≤ 13: e^2.5649 ≤ (partial upper?) — partial sums are lower bounds. BUT: e^2.5649 = 1/e^{−2.5649} and e^{−2.5649} ≥ Σ_{k<K} (−2.5649)^k/k! — ALTERNATING — not a lower bound. Hmm: e^{−x} ≥ 1−x (gives e^x ≤ 1/(1−x)) — for x = 2.5649 invalid (>1). e^{−x} ≥ 1−x+x²/2−x³/3 for x ≥ 0? The alternating bounds: e^{−x} ≥ Σ_{k≤2m+1}(−x)^k/k! (odd stops are LOWER bounds for e^{−x} — TRUE: e^{−x} = 1−x+x²/2−... and the tail after an odd stop is negative... e^{−x} ≥ 1−x+x²/2−x³/6 for x ≥ 0 ✓ (Taylor with remainder: e^{−x} = Σ_{k<4} + e^{−ξ}x⁴/24 ≥ Σ_{k<4} since the x⁴ term is +). So e^{−2.5649} ≥ 1−2.5649+3.28946−2.81232+1.80475·... = 1−2.5649+3.28946−2.81233+1.80468−0.92576·... k=5 term: −2.5649⁵/120 = −0.92576: partial (k≤5): 1−2.5649+3.28946−2.81233+1.80468−0.92576 = −0.20885 — NEGATIVE, useless. e^{−2.5649} ≈ 0.07692 — the alternating series at x = 2.56 oscillates hugely before converging (peak term ~x⁷/7! ≈ 0.47). Partial alternating bounds valid but need k ~ 15+: messy.\n     \n     STEP BACK. For log 13 ≥ 2.5649, the cleanest: 13 ≥ e^2.5649 ⟺ 13⁴ ≥ e^{10.2596}?? no. ⟺ 13 ≥ (e^{0.6405-ish})⁴... I have e^2.565 ≥ 1.8988433⁴ ≥ 13 (log_thirteen_le's proof shows 13 ≤ e^2.565 — wait that gave log 13 ≤ 2.565: e^2.565 ≥ 13). For log 13 ≥ 2.5649 need 13 ≥ e^2.5649: note e^2.5649 = e^2.565·e^{−0.0001}: and e^2.565 = ??? I only have e^2.565 ≥ 1.8988433⁴ (lower). I need e^2.565 UPPER: e^2.565 ≤ 13.0004-ish: via e^2.565 = e²·e^0.565 ≤ 7.3890566·e^0.565: e^0.565 ≤ ?? upper — the (1−x/n)^{-n} route: n = 4: (1−0.14125)^{-4} = 0.85875^{-4} = 1/0.85875⁴: 0.85875² = 0.73745; ⁴ = 0.54384: 1/0.54384 = 1.83877. e^2.565 ≤ 7.3890566·1.83877 = 13.5868 ✗. n=8: (1−0.070625)^{-8}: 0.929375^8 = e^{8 ln 0.929375} = e^{8·(−0.073244)} = e^{−0.585951} = 0.556556: 1/0.556556 = 1.79677: 7.3890566·1.79677 = 13.2756 ✗. n=16: 1.77375: ×7.389 = 13.104 ✗. n=32: 1.76808: ×7.389 = 13.064 ✗. Converges to 13.000-ish but slowly — n=128: ≈1.7602: 13.008. Hopeless for a 13.0004 bound.\n     \n     OK completely different: prove `log_thirteen_ge` via log 13 = log(13) with the LOG-SERIES at a close rational: log(13/8) = log 1.625 = log(1+0.625): alternating at 0.625 — converges moderately: log 1.625: terms 0.625−0.195+0.0814−0.0381+0.0191−0.00995+0.00534−0.00292+0.00163−0.000925+0.000532−0.00031 = 0.48584·... true log 1.625 = 0.485508. log 13 = 3·log 2 + log 1.625 ≥ 3·0.6931471+0.4858 = 2.0794413+0.4858 = 2.5652 ✓ ≥ 2.5649!! With log(1.625) ≥ alternating-partial ≥ 0.4858: log(1+x) ≥ x−x²/2+x³/3−...−x^{2m}/(2m) — need the general even-stop lower bound. My log_one_add_ge is only the 4th-order. Generalizing: log(1+x) ≥ Σ_{k=1}^{2m}(−1)^{k+1}x^k/k via 1/(1+t) ≥ Σ_{k=0}^{2m−1}(−t)^k on [0,x] (finite geometric: (1−(−t)^{2m})/(1+t) ≤ 1/(1+t) ⟺ 1−t^{2m} ≤ 1 ✓ for t ≥ 0... (1−(−t)^{2m})/(1+t) = (1−t^{2m})/(1+t) ≤ 1/(1+t) ⟺ 1−t^{2m} ≤ 1 ✓). The integral of the finite geometric: Σ_{k=0}^{2m−1}(−1)^k x^{k+1}/(k+1) ✓. So a general lemma `log_one_add_ge_series (m : ℕ) (x : ℝ) (hx : 0 ≤ x) : ∑_{k=1}^{2m} (−1)^{k+1} x^k/k ≤ log(1+x)` — prove via the same integral comparison with the finite geometric polynomial. Doable but another integral machine. For m = 6 (12 terms): log 1.625 ≥ Σ_{k=1}^{12}(−1)^{k+1}0.625^k/k = 0.625−0.195313+0.081380−0.038147+0.019073−0.009934+0.005343−0.002936+0.001645−0.000935+0.000539−0.000315 = 0.486134·... let me sum: 0.625−0.195313 = 0.429687; +0.081380 = 0.511067; −0.038147 = 0.472920; +0.019073 = 0.491993; −0.009934 = 0.482059; +0.005343 = 0.487402; −0.002936 = 0.484466; +0.001645 = 0.486111; −0.000935 = 0.485176; +0.000539 = 0.485715; −0.000315 = 0.485400. So ≥ 0.4854: log 13 ≥ 2.0794413+0.4854 = 2.5648413 ✗ < 2.5649 (by 6e-5!). More terms: k=13: +0.000185 = 0.485585; k=14: −0.000109 = 0.485476; k=16: ≈ 0.48552. True = 0.485508. The even stops oscillate around 0.4854–0.4856 — reaching ≥ 2.5649−2.0794413 = 0.4854587 needs the even partial ≥ 0.48546: at k=12: 0.485400 ✗; k=14: 0.485476 ✓!! So m = 7 (14 terms): log 13 ≥ 2.0794413+0.485476 = 2.5649173 ≥ 2.5649 ✓ (margin 1.7e-5 — thin). k=16: 0.485400+0.000185−0.000109+0.000065−0.000039 = 0.485502: 2.5649433 ✓ (m = 8, margin 4.3e-5 — better). True target bound: log 13 ≥ 2.5649 — with m = 8 margin 4.3e-5 ✓.\n     Hmm — 16 terms with alternating signs as a norm_num-fest. Doable: the sum is a rational number (x = 0.625 = 5/8 rational): Σ_{k=1}^{16}(−1)^{k+1}(5/8)^k/k — norm_num can evaluate: state `log_thirteen_ge : (2.5649:ℝ) ≤ Real.log 13 := by have := log_one_add_ge_series 8 (show (0:ℝ) ≤ (1.625−1)...)...` — with log(1.625) ≥ S (rational), log 13 = 3 log 2 + log(13/8): 13 = 8·1.625? 8·1.625 = 13 ✓: log 13 = log 8 + log 1.625 = 3 log 2 + log 1.625 ✓.\n     \n     OK — but do I even NEED log 13 ≥ 2.5649? It's for LA₁'s antitone condition: (x+10)/x ≤ 2 log x for x ≥ 13. Alternative: use a WEAKER antitone threshold: (x+10)/x ≤ 2·2.5649 is needed... what if I prove antitone directly without the tight log: (x+10)/x ≤ 2 log x ⟺ 1+10/x ≤ 2 log x. At x = 13: 1.7692 ≤ 2·2.564949 = 5.1299 ✓ with LOTS of room (1.77 vs 5.13!). So even log 13 ≥ 1 (trivial: 13 > e) suffices: 2 log x ≥ 2 ≥ 1.77 for x ≥ 13 ⟸ log x ≥ 1 ⟺ x ≥ e: 13 ≥ e ✓ (exp_one_lt_d9). MUCH easier!! I overcomplicated: 1+10/13 = 1.7693 ≤ 2 ≤ 2 log x ✓✓. Great — log_thirteen_ge UNNEEDED.\n     Similarly RW₁'s f = log x/x² on Ici 10 — the existing antitoneOn_log_div_sq covers Ici 3 ✓ (used log 3 ≥ 1 ✓ fine).\n     \n   - LA₂: `tail14_loglog_div_add_sq_le : ∑' j, loglog(j+14)/((j+14)+10)² ≤ 0.0621`: pointwise loglog ≤ (1/e)·log: ≤ (1/e)·LA₁-sum ≤ 0.3679·0.1687 = 0.062066 ≤ 0.0621 ✓.\n\n6. Then the C0hat bridges (piece 3b) and the far-series machine (3c).\n\nWait — LA₁'s antitone: derivative of log x/(x+10)²: (1/x·(x+10)² − log x·2(x+10))/(x+10)⁴ = ((x+10)/x − 2 log x)/(x+10)³. Need ≤ 0 on Ici 13: (x+10)/x ≤ 1+10/13 = 23/13 ≤ 1.77 ≤ 2 ≤ 2 log x ✓ (log x ≥ 1 for x ≥ 13 ≥ e ✓). PROVABLE with the antitoneOn_of_deriv_nonpos pattern (needs the interior derivative + continuity — pattern from antitoneOn_log_div_sq in this file ✓ clone).\n\nAnd LA₀'s f = 1/(x+10)² antitone: direct (no calculus): a ≤ b ⟹ (a+10)² ≤ (b+10)² ⟹ 1/(b+10)² ≤ 1/(a+10)² ✓ one_div_le_one_div_of_le + pow_le_pow_left₀.\n\nRW₀'s f = 1/x² on Ici 10: same direct pattern.\n\nAlso LA₁ integrability: ∫₁₃^∞ log x/(x+10)² = 0.16862: antiderivative F(x) = −log x/(x+10) + (1/10)·log(x/(x+10)): HasDerivAt — messy quotient; build from parts: F = −(log x)·(x+10)⁻¹ + (1/10)(log x − log(x+10)): \n  part1: −(log x)·(x+10)⁻¹: HasDerivAt via ((Real.hasDerivAt_log hx0).mul ((hasDerivAt_id' x).const_add 10).inv h10).neg — derivative: −[x⁻¹·(x+10)⁻¹ + log x·(−(x+10)⁻²)] = −1/(x(x+10)) + log x/(x+10)².\n  part2: (1/10)(log x − log(x+10)): derivative (1/10)(1/x − 1/(x+10)) = (1/10)·(10/(x(x+10))) = 1/(x(x+10)).\n  sum: log x/(x+10)² ✓ — the 1/(x(x+10)) cancels ✓.\n  Tendsto F → 0 at ∞: −log x/(x+10) → 0 (log x/(x+10) ≤ log x/x → 0-ish: log x/(x+10) = (log x/x)·(x/(x+10)): log x/x → 0 (have: Real.tendsto_pow_log_div_mul_add_atTop 1 0 1 one_ne_zero — used in this file ✓) and x/(x+10) → 1: product → 0 ✓); (1/10)·log(x/(x+10)) → (1/10)·log 1 = 0: x/(x+10) → 1 (tendsto of the ratio: (1+10/x)⁻¹-ish → 1: Tendsto (fun x => x/(x+10)) atTop (𝓝 1): x/(x+10) = 1/(1+10/x) → 1/(1+0) = 1) and Real.log continuous at 1: (Real.continuousAt_log (by norm_num : (1:ℝ) ≠ 0)).tendsto.comp.\n  F(13) = −log 13/23 + (1/10)·log(13/23): integral = 0 − F(13) = log 13/23 + (1/10)·log(23/13) ≤ 2.565/23+0.571/10 = 0.1115217+0.0571 = 0.1686217 ≤ 0.1687 ✓ (log_thirteen_le ✓ log_23_13_le ✓ — both already proved!).\n\nIntegrableOn for LA₁: the deriv-of-nonneg pattern `integrableOn_Ioi_deriv_of_nonneg'` ✓ (f ≥ 0 for x ≥ 13: log x ≥ 0 ✓).\n\nRW₀'s integral: ∫₁₀^∞ 1/x² = 1/10: integral_Ioi_of_hasDerivAt_of_tendsto' with F = −x⁻¹ ✓.\n\nAlso — the `AntitoneOn.tsum_comp_add_le_integral` signature: from tsum_log_div_sq_tail_le: `antitoneOn_log_div_sq.tsum_comp_add_le_integral 3 integrableOn_log_div_sq (nonneg)` : gives ∑' n, f(n+3+1) ≤ ∫_{Ioi 3} f. The nonneg arg: (fun t ht => ...) over Ici? In that proof: (fun t ht => by have ht3 : 3 < t := ht; positivity-ish) — ht : t ∈ Set.Ioi 3? The signature from Mathlib: `AntitoneOn.tsum_comp_add_le_integral (hs : AntitoneOn f (Ici c)) (hi : IntegrableOn f (Ioi c)) (hf : ∀ x ∈ Ici c, 0 ≤ f x) : ∑' n, f (n + c + 1) ≤ ∫ x in Ioi c, f x`. Hmm — in the file's usage the third arg was (fun t ht => by have ht3 : (3:ℝ) < t := ht; ...) — ht3 : 3 < t from ht : t ∈ Ici?? They wrote `have ht3 : (3 : ℝ) < t := ht` — so ht : 3 < t, i.e. the nonneg is over Ioi?? whatever — clone the exact pattern from tsum_log_div_sq_tail_le ✓.\n\nThe cast bridge: ∑' n, f (↑(n + 10 + 1)) vs my stated form with ((n:ℝ)+11): the hcongr pattern from that lemma ✓.\n\nAlso RW₀'s f = 1/x² antitone — need as a separate lemma (antitoneOn_one_div_sq on Ici 10).\n\nRW₂/LA₂'s summability via domination.\n\nLet me now also plan the exact list of brick statements to write (chunk 9b+9c):\n\n```lean\ndef farW (k : ℕ) : ℝ := 1 / ((k : ℝ) * Real.sqrt (1 + (k : ℝ) ^ 2))\nlemma farW_nonneg (k : ℕ) : 0 ≤ farW k\nlemma farW_le_inv_sq {k : ℕ} (hk : 1 ≤ k) : farW k ≤ 1 / (k : ℝ) ^ 2\nlemma farW_le_inv_mul_sub {k : ℕ} (hk : 4 ≤ k) : farW k ≤ 1 / ((k : ℝ) * ((k : ℝ) - 1))\nlemma farW_one_le : farW 1 ≤ 0.70721\nlemma farW_two_le : farW 2 ≤ 0.22422\nlemma farW_three_le : farW 3 ≤ 0.10549\nlemma farW_four_le : farW 4 ≤ 0.06064\nlemma telescope_tsum : ∑' k : ℕ, (1 : ℝ) / ((k : ℝ) + 5) / ((k : ℝ) + 4) = 1 / 4  -- or the difference form\nlemma farW_shift_summable : Summable (fun k : ℕ => farW (k + 1))\nlemma farW_tsum_le : ∑' k : ℕ, farW (k + 1) ≤ 1.3476\nlemma farW_Ico_le (K : ℕ) : ∑ k ∈ Finset.Ico 1 (K + 1), farW k ≤ 1.3476\n-- RW bricks\nlemma antitoneOn_one_div_sq : AntitoneOn (fun x : ℝ => 1 / x ^ 2) (Set.Ici 10)\nlemma integral_one_div_sq_Ioi_ten : ∫ x in Set.Ioi (10 : ℝ), 1 / x ^ 2 = 1 / 10\nlemma tail11_inv_sq_le : ∑' k : ℕ, (1 : ℝ) / ((k : ℝ) + 11) ^ 2 ≤ 0.1\nlemma integral_log_div_sq_Ioi_ten : ∫ x in Set.Ioi (10 : ℝ), Real.log x / x ^ 2 = (Real.log 10 + 1) / 10\nlemma tail11_log_div_sq_le : ∑' k : ℕ, Real.log ((k : ℝ) + 11) / ((k : ℝ) + 11) ^ 2 ≤ 0.3303\nlemma tail11_loglog_div_sq_le : ∑' k : ℕ, Real.log (Real.log ((k : ℝ) + 11)) / ((k : ℝ) + 11) ^ 2 ≤ 0.1216\n-- LA bricks\nlemma antitoneOn_one_div_add_sq : AntitoneOn (fun x : ℝ => 1 / (x + 10) ^ 2) (Set.Ici 13)\nlemma integral_one_div_add_sq_Ioi_thirteen : ∫ x in Set.Ioi (13 : ℝ), 1 / (x + 10) ^ 2 = 1 / 23\nlemma tail14_inv_add_sq_le : ∑' j : ℕ, (1 : ℝ) / (((j : ℝ) + 14) + 10) ^ 2 ≤ 1 / 23\nlemma antitoneOn_log_div_add_sq : AntitoneOn (fun x : ℝ => Real.log x / (x + 10) ^ 2) (Set.Ici 13)\nlemma integral_log_div_add_sq_Ioi_thirteen : ∫ x in Set.Ioi (13 : ℝ), Real.log x / (x + 10) ^ 2 = Real.log 13 / 23 + Real.log (23 / 13) / 10\nlemma tail14_log_div_add_sq_le : ∑' j : ℕ, Real.log ((j : ℝ) + 14) / (((j : ℝ) + 14) + 10) ^ 2 ≤ 0.1687\nlemma tail14_loglog_div_add_sq_le : ∑' j : ℕ, Real.log (Real.log ((j : ℝ) + 14)) / (((j : ℝ) + 14) + 10) ^ 2 ≤ 0.0621\n```\n\nAlso needed: integrableOn_one_div_sq (Ioi 10), integrableOn_log_div_sq on Ioi 10 (mono from Ioi 3 ✓ existing), integrableOn_one_div_add_sq (Ioi 13), integrableOn_log_div_add_sq (Ioi 13, deriv-of-nonneg pattern).\n\nThat's a big chunk. Let me write it in two edits: (9b) farW + S₃; (9c) the six bricks. Write 9b now.\n\nFor farW_one_le: farW 1 = 1/(1·√2) = 1/√2 ≤ 0.70721: via √2 ≥ 1.414 (Real.le_sqrt : 1.414 ≤ √2 ⟺ 1.414² ≤ 2 — `Real.le_sqrt (hx : 0 ≤ x) : x ≤ Real.sqrt y ↔ x ^ 2 ≤ y`? signature might be Real.le_sqrt (hy : 0 ≤ y)? or (hx)? Let me check: Mathlib `Real.le_sqrt (hx : 0 ≤ x) : x ≤ Real.sqrt y ↔ x ^ 2 ≤ y` — hmm might need (hy : 0 ≤ y). I'll write: \n```\nhave h14 : (1.414 : ℝ) ≤ Real.sqrt 2 := by\n  rw [Real.le_sqrt (by norm_num : (0:ℝ) ≤ 1.414)]\n  norm_num\n```\nIf the signature differs, fix at compile. Then farW 1 = 1/(1·√2) = 1/√2 ≤ 1/1.414 = 0.70721·... : 1/1.414 = 0.7072136 ≤ 0.70721?? 1/1.414 = 0.70721358 > 0.70721!! My constant 0.70721 is too tight (from the earlier computation: 1/1.414 = 0.7072136). The mpmath check: \"exact-term bounds: 0.707213578500707\" — and the SUM bound 1.3475495 ≤ 1.3476 ✓. So individual: farW 1 ≤ 0.70722 (1/1.414 = 0.7072136 ≤ 0.70722 ✓) — hmm or state as 1/1.414 directly and sum: 1/1.414+1/(2·2.23)+1/(3·3.16)+1/(4·4.123)+1/4 = 0.7072136+0.2242152+0.1054852+0.0606355+0.25 = 1.3475495 ≤ 1.3476 ✓. So state farW_one_le : farW 1 ≤ 1/1.414 etc. and the sum bound 1.3476 at the assembly. Cleaner: state each as the rational reciprocal: farW 1 ≤ 1/1.414, farW 2 ≤ 1/4.46, farW 3 ≤ 1/9.48, farW 4 ≤ 1/16.492. Then farW_tsum_le : ≤ 1/1.414+1/4.46+1/9.48+1/16.492+1/4 ≤ 1.3476 (norm_num: 1/1.414 = 0.7072136, 1/4.46 = 0.2242152, 1/9.48 = 0.1054852, 1/16.492 = 0.0606355: sum = 1.3475495 ✓ norm_num verifies ✓).\n\nFor the Ico version: ∑_{Ico 1 (K+1)} farW ≤ ∑' farW(k+1) via reindex + Summable.sum_le_tsum.\n\nThe telescope: ∑' k, (1/((k:ℝ)+4) − 1/((k:ℝ)+5)) = 1/4:\n```\nlemma tsum_one_div_sub_telescope' : ∑' k : ℕ, (1 / ((k : ℝ) + 4) - 1 / ((k : ℝ) + 5)) = 1 / 4\n```\nProof: HasSum via partial sums: ∑_{k<N} (a k − a (k+1)) = a 0 − a N (Finset.sum_range_sub' a N : ∑ i ∈ range N, (f i − f (i+1)) = f 0 − f N — check exact name/direction: `Finset.sum_range_sub' : ∑ i ∈ range n, (f i − f (i + 1)) = f 0 − f n` ✓). With a k = 1/(k+4): partial = 1/4 − 1/(N+4) → 1/4 (Tendsto.sub_const: 1/(N+4) → 0). HasSum → tsum_eq.\n   Tendsto (fun N : ℕ => (1:ℝ)/((N:ℝ)+4)) atTop (𝓝 0): simpa using tendsto_inv_atTop_zero.comp (Tendsto (fun N => (N:ℝ)+4) atTop atTop): Tendsto (fun N:ℕ => (N:ℝ)+4) atTop atTop := tendsto_natCast_atTop_atTop.atTop_add_const_right? — there's `tendsto_atTop_add_const_right (c) (hf : Tendsto f l atTop) : Tendsto (fun x => f x + c) l atTop` ✓ — with f = Nat.cast: tendsto_natCast_atTop_atTop (ordered field version — used in Zeta23?). Then the division form: (1:ℝ)/(N+4) = ((N:ℝ)+4)⁻¹: simp [one_div].\n   Then HasSum a (1/4 − 0): hasSum_iff_tendsto_nat_of_summable? No — HasSum f b ⟺ Tendsto (fun N => ∑_{k<N} f k) atTop (𝓝 b) — `hasSum_nat` : HasSum f b ↔ Tendsto (fun N => partial sums) — the def via `HasSum` directly: Tendsto (fun N => ∑ k in range N, a k) atTop (𝓝 (1/4)): rw (partial = 1/4 − 1/(N+4)) and Tendsto.sub (tendsto_const) (inv→0) : → 1/4 − 0 = 1/4: simpa [sub_eq_add_neg...]. Then `HasSum.tsum_eq`.\n\nLet me write chunk 9b now. Also the summability of farW(k+1): dominated by the telescope family: farW (k+1) ≤ 1/((k+1)·k) for k ≥ 3 hmm — for ALL k: farW(k+1) ≤ 1/((k+1)·√(1+(k+1)²)) hmm circular. farW k ≤ 1/k² (k ≥ 1) and Summable (fun k => 1/((k:ℝ)+1)^2)? — or dominate by telescope from k = 5: farW(k+5) ≤ 1/((k+5)(k+4)) ✓ telescope summable; the first 4 terms finite: Summable via (summable_nat_add_iff 5).mp : Summable (fun k => farW (k+1+...)) hmm — summable_nat_add_iff k : Summable (fun n => f (n + k)) ↔ Summable f: so Summable (fun k => farW (k+1)) ⟺ Summable (fun k => farW (k+1+4)) — with f = fun k => farW (k+1): f (k+4) = farW (k+5) ✓. So: prove Summable (fun k => farW (k+5)) via of_norm_bounded by the telescope summable, then (summable_nat_add_iff 4).mp? — summable_nat_add_iff (k) : (Summable fun n => f (n+k)) ↔ Summable f: .mp : Summable (f(·+k)) → Summable f. So from Summable (fun k => farW(k+1+4))?? I have Summable (fun k => farW (k+5)) = Summable (f (k+4)) with f k = farW (k+1) — f (k+4) = farW (k+4+1) = farW (k+5) ✓ (up to add-assoc cast — need congr). So:\n```\nhave h1 : Summable (fun k : ℕ => farW (k + 5)) := <domination by telescope>\nhave h2 := (summable_nat_add_iff (f := fun k : ℕ => farW (k + 1)) 4).mp ?_\n-- ?_ : Summable (fun k => (fun k => farW (k+1)) (k+4)) = Summable (fun k => farW (k+4+1))\nexact h1.congr (fun k => by ring_nf; congr 1; omega)?? — farW (k+4+1) vs farW (k+5): k+4+1 = k+5 ✓ congr\n```\nfine.\n\nFor the telescope summable: the HasSum proof gives Summable directly (hasSum.summable).\n\nNow write 9b. It's long; let me draft carefully.","signature":""},{"type":"text","text":"Section 9 compiles clean. Now chunk 9b: the farW weight + S₃ bound."},{"type":"tool_use","id":"Edit_70","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":"/-! ## 10. Piece 3b: the far-sum weight and the S₃ brick -/\n\n/-- The far-sum per-interval weight: 1/(k√(1+k²)). -/\ndef farW (k : ℕ) : ℝ := 1 / ((k : ℝ) * Real.sqrt (1 + (k : ℝ) ^ 2))\n\nlemma farW_nonneg (k : ℕ) : (0 : ℝ) ≤ farW k := by\n  rw [farW]\n  positivity\n\n/-- farW k ≤ 1/k² (since √(1+k²) ≥ k). -/\nlemma farW_le_inv_sq {k : ℕ} (hk : 1 ≤ k) : farW k ≤ 1 / (k : ℝ) ^ 2 := by\n  have hk0 : (0 : ℝ) < (k : ℝ) := by exact_mod_cast hk\n  rw [farW]\n  have h1 : (k : ℝ) * (k : ℝ) ≤ (k : ℝ) * Real.sqrt (1 + (k : ℝ) ^ 2) := by\n    apply mul_le_mul_of_nonneg_left _ hk0.le\n    calc (k : ℝ) = Real.sqrt ((k : ℝ) ^ 2) := by\n          rw [Real.sqrt_sq_eq_abs, abs_of_nonneg hk0.le]\n      _ ≤ Real.sqrt (1 + (k : ℝ) ^ 2) :=\n          Real.sqrt_le_sqrt (by linarith [sq_nonneg (k : ℝ)])\n  have h2 : (0 : ℝ) < (k : ℝ) * (k : ℝ) := by positivity\n  have h3 := one_div_le_one_div_of_le (mul_pos hk0 hk0) h1\n  rwa [show (k : ℝ) * (k : ℝ) = (k : ℝ) ^ 2 from by ring] at h3\n\n/-- farW k ≤ 1/(k(k−1)) for k ≥ 1 (since √(1+k²) ≥ k−1). -/\nlemma farW_le_inv_mul_sub {k : ℕ} (hk : 1 ≤ k) :\n    farW k ≤ 1 / ((k : ℝ) * ((k : ℝ) - 1)) := by\n  have hk0 : (0 : ℝ) < (k : ℝ) := by exact_mod_cast hk\n  rw [farW]\n  have h1 : (k : ℝ) * ((k : ℝ) - 1) ≤ (k : ℝ) * Real.sqrt (1 + (k : ℝ) ^ 2) := by\n    apply mul_le_mul_of_nonneg_left _ hk0.le\n    by_cases hk1 : (1 : ℝ) ≤ (k : ℝ)\n    · calc (k : ℝ) - 1 ≤ (k : ℝ) := by linarith\n        _ = Real.sqrt ((k : ℝ) ^ 2) := by\n            rw [Real.sqrt_sq_eq_abs, abs_of_nonneg hk1]\n        _ ≤ Real.sqrt (1 + (k : ℝ) ^ 2) :=\n            Real.sqrt_le_sqrt (by linarith [sq_nonneg (k : ℝ)])\n    · have h2 : (k : ℝ) - 1 ≤ 0 := by linarith\n      exact h2.trans (Real.sqrt_nonneg _)\n  rcases eq_or_ne k 1 with rfl | hk1\n  · norm_num [farW]\n  · have hkk : (1 : ℝ) < (k : ℝ) := by\n      have h1' : (1 : ℕ) < k := lt_of_le_of_ne hk (Ne.symm hk1)\n      exact_mod_cast h1'\n    have h2 : (0 : ℝ) < (k : ℝ) * ((k : ℝ) - 1) := by positivity\n    exact one_div_le_one_div_of_le h2 h1\n\n/-- The telescoping tail: ∑' k, (1/(k+4) − 1/(k+5)) = 1/4. -/\nlemma tsum_one_div_four_sub_telescope :\n    (∑' k : ℕ, (1 / ((k : ℝ) + 4) - 1 / ((k : ℝ) + 5))) = 1 / 4 := by\n  have ha : ∀ k : ℕ, 1 / ((k : ℝ) + 4) - 1 / ((k : ℝ) + 5)\n      = 1 / ((k : ℝ) + 4) / ((k : ℝ) + 5) := by\n    intro k\n    have h1 : ((k : ℝ) + 4) ≠ 0 := by positivity\n    have h2 : ((k : ℝ) + 5) ≠ 0 := by positivity\n    field_simp\n    ring\n  have hsum : ∀ N : ℕ, ∑ k ∈ Finset.range N, (1 / ((k : ℝ) + 4) - 1 / ((k : ℝ) + 5))\n      = 1 / 4 - 1 / ((N : ℝ) + 4) := by\n    intro N\n    have h := Finset.sum_range_sub' (fun k : ℕ => 1 / ((k : ℝ) + 4)) N\n    rw [h]\n    simp\n  have hlim : Filter.Tendsto (fun N : ℕ => 1 / ((N : ℝ) + 4)) Filter.atTop (𝓝 0) := by\n    have h1 : Filter.Tendsto (fun N : ℕ => (N : ℝ) + 4) Filter.atTop Filter.atTop :=\n      Filter.Tendsto.atTop_add_const_right _ _ tendsto_natCast_atTop_atTop\n    have h2 := tendsto_inv_atTop_zero.comp h1\n    simpa [one_div] using h2\n  have hhas : HasSum (fun k : ℕ => 1 / ((k : ℝ) + 4) - 1 / ((k : ℝ) + 5)) (1 / 4) := by\n    rw [HasSum]\n    rw [show (fun N => ∑ k ∈ Finset.range N, (1 / ((k : ℝ) + 4) - 1 / ((k : ℝ) + 5)))\n        = fun N => 1 / 4 - 1 / ((N : ℝ) + 4) from funext hsum]\n    have h3 : (1 : ℝ) / 4 = 1 / 4 - 0 := by ring\n    rw [h3]\n    exact Filter.Tendsto.sub tendsto_const_nhds hlim\n  exact hhas.tsum_eq\n\n/-- farW (k+5) is summable (telescope-dominated). -/\nlemma farW_shift5_summable : Summable (fun k : ℕ => farW (k + 5)) := by\n  have htel : Summable (fun k : ℕ => 1 / ((k : ℝ) + 4) - 1 / ((k : ℝ) + 5)) :=\n    ⟨_, tsum_one_div_four_sub_telescope⟩\n  have htel2 : Summable (fun k : ℕ => 1 / ((k : ℝ) + 4) / ((k : ℝ) + 5)) := by\n    apply htel.congr\n    intro k\n    have h1 : ((k : ℝ) + 4) ≠ 0 := by positivity\n    have h2 : ((k : ℝ) + 5) ≠ 0 := by positivity\n    field_simp\n    ring\n  apply Summable.of_norm_bounded htel2\n  intro k\n  have h1 := farW_le_inv_mul_sub (k := k + 5) (by omega : 1 ≤ k + 5)\n  have h2 : farW (k + 5) ≤ 1 / ((k : ℝ) + 4) / ((k : ℝ) + 5) := by\n    have h3 : ((k + 5 : ℕ) : ℝ) * (((k + 5 : ℕ) : ℝ) - 1)\n        = ((k : ℝ) + 5) * ((k : ℝ) + 4) := by push_cast; ring\n    calc farW (k + 5) ≤ 1 / (((k + 5 : ℕ) : ℝ) * (((k + 5 : ℕ) : ℝ) - 1)) := h1\n      _ = 1 / (((k : ℝ) + 5) * ((k : ℝ) + 4)) := by rw [h3]\n      _ = 1 / ((k : ℝ) + 4) / ((k : ℝ) + 5) := by\n          rw [div_mul_div_comm, mul_comm ((k : ℝ) + 5) ((k : ℝ) + 4), one_mul]\n  rw [Real.norm_eq_abs, abs_of_nonneg (farW_nonneg _),\n    abs_of_nonneg (by positivity : (0 : ℝ) ≤ 1 / ((k : ℝ) + 4) / ((k : ℝ) + 5))]\n  exact h2\n\n/-- farW (k+1) is summable. -/\nlemma farW_shift_summable : Summable (fun k : ℕ => farW (k + 1)) := by\n  have h1 := (summable_nat_add_iff (f := fun k : ℕ => farW (k + 1)) 4).mp ?_\n  · exact h1\n  · apply farW_shift5_summable.congr\n    intro k\n    show farW (k + 4 + 1) = farW (k + 5)\n    rw [show k + 4 + 1 = k + 5 from rfl]\n\n/-- The four exact S₃ terms. -/\nlemma farW_exact_four :\n    farW 1 + farW 2 + farW 3 + farW 4 ≤ 1 / 1.414 + 1 / 4.46 + 1 / 9.48 + 1 / 16.492 := by\n  have hsqrt2 : (1.414 : ℝ) ≤ Real.sqrt 2 := by\n    rw [Real.le_sqrt (by norm_num : (0 : ℝ) ≤ (1.414 : ℝ))]\n    norm_num\n  have hsqrt5 : (2.23 : ℝ) ≤ Real.sqrt 5 := by\n    rw [Real.le_sqrt (by norm_num : (0 : ℝ) ≤ (2.23 : ℝ))]\n    norm_num\n  have hsqrt10 : (3.16 : ℝ) ≤ Real.sqrt 10 := by\n    rw [Real.le_sqrt (by norm_num : (0 : ℝ) ≤ (3.16 : ℝ))]\n    norm_num\n  have hsqrt17 : (4.123 : ℝ) ≤ Real.sqrt 17 := by\n    rw [Real.le_sqrt (by norm_num : (0 : ℝ) ≤ (4.123 : ℝ))]\n    norm_num\n  have h1 : farW 1 ≤ 1 / 1.414 := by\n    rw [farW]\n    norm_num\n    have h2 : (1.414 : ℝ) ≤ Real.sqrt (1 + (1 : ℝ) ^ 2) := by\n      rw [show (1 : ℝ) + (1 : ℝ) ^ 2 = 2 from by ring]\n      exact hsqrt2\n    exact one_div_le_one_div_of_le (by norm_num : (0 : ℝ) < 1.414) h2\n  have h2' : farW 2 ≤ 1 / 4.46 := by\n    rw [farW]\n    have h3 : Real.sqrt (1 + (2 : ℝ) ^ 2) = Real.sqrt 5 := by\n      rw [show (1 : ℝ) + (2 : ℝ) ^ 2 = 5 from by ring]\n    rw [h3]\n    have h4 : (2 : ℝ) * 2.23 ≤ (2 : ℝ) * Real.sqrt 5 :=\n      mul_le_mul_of_nonneg_left hsqrt5 (by norm_num)\n    have h5 : (2 : ℝ) * 2.23 = 4.46 := by norm_num\n    rw [h5] at h4\n    exact one_div_le_one_div_of_le (by norm_num : (0 : ℝ) < 4.46) h4\n  have h3' : farW 3 ≤ 1 / 9.48 := by\n    rw [farW]\n    have h4 : Real.sqrt (1 + (3 : ℝ) ^ 2) = Real.sqrt 10 := by\n      rw [show (1 : ℝ) + (3 : ℝ) ^ 2 = 10 from by ring]\n    rw [h4]\n    have h5 : (3 : ℝ) * 3.16 ≤ (3 : ℝ) * Real.sqrt 10 :=\n      mul_le_mul_of_nonneg_left hsqrt10 (by norm_num)\n    have h6 : (3 : ℝ) * 3.16 = 9.48 := by norm_num\n    rw [h6] at h5\n    exact one_div_le_one_div_of_le (by norm_num : (0 : ℝ) < 9.48) h5\n  have h4' : farW 4 ≤ 1 / 16.492 := by\n    rw [farW]\n    have h5 : Real.sqrt (1 + (4 : ℝ) ^ 2) = Real.sqrt 17 := by\n      rw [show (1 : ℝ) + (4 : ℝ) ^ 2 = 17 from by ring]\n    rw [h5]\n    have h6 : (4 : ℝ) * 4.123 ≤ (4 : ℝ) * Real.sqrt 17 :=\n      mul_le_mul_of_nonneg_left hsqrt17 (by norm_num)\n    have h7 : (4 : ℝ) * 4.123 = 16.492 := by norm_num\n    rw [h7] at h6\n    exact one_div_le_one_div_of_le (by norm_num : (0 : ℝ) < 16.492) h6\n  linarith [h1, h2', h3', h4']\n\n/-- **The S₃ brick**: Σ_{k≥1} 1/(k√(1+k²)) ≤ 1.3476. -/\nlemma farW_tsum_le : (∑' k : ℕ, farW (k + 1)) ≤ 1.3476 := by\n  have hsplit : (∑' k : ℕ, farW (k + 1))\n      = (∑ k ∈ Finset.range 4, farW (k + 1)) + ∑' k : ℕ, farW (k + 1 + 4) :=\n    (farW_shift_summable.sum_add_tsum_nat_add 4).symm\n  have hhead : ∑ k ∈ Finset.range 4, farW (k + 1)\n      = farW 1 + farW 2 + farW 3 + farW 4 := by\n    rw [Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_succ,\n      Finset.sum_range_succ, Finset.sum_range_zero]\n    norm_num\n  have htail : (∑' k : ℕ, farW (k + 1 + 4)) ≤ 1 / 4 := by\n    have h1 : (∑' k : ℕ, farW (k + 1 + 4)) = ∑' k : ℕ, farW (k + 5) := by\n      apply tsum_congr\n      intro k\n      rw [show k + 1 + 4 = k + 5 from rfl]\n    rw [h1]\n    have htel : (∑' k : ℕ, farW (k + 5))\n        ≤ ∑' k : ℕ, (1 / ((k : ℝ) + 4) - 1 / ((k : ℝ) + 5)) := by\n      apply Summable.tsum_le_tsum _ farW_shift5_summable ⟨_, tsum_one_div_four_sub_telescope⟩\n      intro k\n      have h2 := farW_le_inv_mul_sub (k := k + 5) (by omega : 1 ≤ k + 5)\n      have h3 : ((k + 5 : ℕ) : ℝ) * (((k + 5 : ℕ) : ℝ) - 1)\n          = ((k : ℝ) + 5) * ((k : ℝ) + 4) := by push_cast; ring\n      have h4 : 1 / (((k + 5 : ℕ) : ℝ) * (((k + 5 : ℕ) : ℝ) - 1))\n          = 1 / ((k : ℝ) + 4) - 1 / ((k : ℝ) + 5) := by\n        rw [h3]\n        have h5 : ((k : ℝ) + 4) ≠ 0 := by positivity\n        have h6 : ((k : ℝ) + 5) ≠ 0 := by positivity\n        field_simp\n        ring\n      exact h2.trans h4.le\n    rw [tsum_one_div_four_sub_telescope] at htel\n    exact htel\n  have hbound : (∑ k ∈ Finset.range 4, farW (k + 1)) + 1 / 4\n      ≤ (1 / 1.414 + 1 / 4.46 + 1 / 9.48 + 1 / 16.492) + 1 / 4 := by\n    rw [hhead]\n    linarith [farW_exact_four]\n  have hnum : (1 : ℝ) / 1.414 + 1 / 4.46 + 1 / 9.48 + 1 / 16.492 + 1 / 4 ≤ 1.3476 := by\n    norm_num\n  calc (∑' k : ℕ, farW (k + 1))\n      = (∑ k ∈ Finset.range 4, farW (k + 1)) + ∑' k : ℕ, farW (k + 1 + 4) := hsplit\n    _ ≤ (∑ k ∈ Finset.range 4, farW (k + 1)) + 1 / 4 := by linarith [htail]\n    _ ≤ (1 / 1.414 + 1 / 4.46 + 1 / 9.48 + 1 / 16.492) + 1 / 4 := hbound\n    _ ≤ 1.3476 := hnum\n\n/-- The finite-Ico S₃ bound (for the main bucket family). -/\nlemma farW_Ico_le (K : ℕ) : ∑ k ∈ Finset.Ico 1 (K + 1), farW k ≤ 1.3476 := by\n  rw [Finset.sum_Ico_eq_sum_range]\n  have h1 : ∑ x ∈ Finset.range (K + 1 - 1), farW (1 + x)\n      ≤ ∑' k : ℕ, farW (k + 1) := by\n    apply Summable.sum_le_tsum _ _ farW_shift_summable\n    intro i _\n    exact farW_nonneg _\n  have h2 : ∑ x ∈ Finset.range (K + 1 - 1), farW (1 + x)\n      = ∑ x ∈ Finset.range (K + 1 - 1), farW (x + 1) := by\n    apply Finset.sum_congr rfl\n    intro x _\n    rw [add_comm]\n  rw [h2] at h1\n  exact h1.trans farW_tsum_le\n\nend NguyenRH1\n\nend"},"extra_content":null}]