Generic rational enclosures used by the point checks of Wt: odd Taylor polynomials bracket arctan on [0, ∞) (monotonicity of the remainder), the shift arctan x = π/4 + arctan ((x-1)/(x+1)), and the Mathlib Taylor remainder bound for log (1 - u). Wt_ge turns four atom bounds into a lower bound for Wt x. Written from scratch.

theorem Zeta32.Fstar.PW.arctan_ge_S4 {t : ℝ} (ht : 0 ≤ t) : t - t ^ 3 / 3 + t ^ 5 / 5 - t ^ 7 / 7 ≤ Real.arctan t

t - t³/3 + t⁵/5 - t⁷/7 ≤ arctan t for t ≥ 0.

theorem Zeta32.Fstar.PW.arctan_le_S3 {t : ℝ} (ht : 0 ≤ t) : Real.arctan t ≤ t - t ^ 3 / 3 + t ^ 5 / 5

arctan t ≤ t - t³/3 + t⁵/5 for t ≥ 0.

theorem Zeta32.Fstar.PW.arctan_shift {x : ℝ} (hx : -1 < x) : Real.arctan x = Real.pi / 4 + Real.arctan ((x - 1) / (x + 1))

arctan x = π/4 + arctan ((x-1)/(x+1)) for x > -1.

theorem Zeta32.Fstar.PW.arctan_ge_shift_pos {x : ℝ} (hx : 1 ≤ x) : 3.141592 / 4 + ((x - 1) / (x + 1) - ((x - 1) / (x + 1)) ^ 3 / 3 + ((x - 1) / (x + 1)) ^ 5 / 5 - ((x - 1) / (x + 1)) ^ 7 / 7) ≤ Real.arctan x

Lower bound for arctan x, x ≥ 1.

theorem Zeta32.Fstar.PW.arctan_ge_shift_neg {x : ℝ} (hx0 : 0 ≤ x) (hx : x ≤ 1) : 3.141592 / 4 - ((1 - x) / (1 + x) - ((1 - x) / (1 + x)) ^ 3 / 3 + ((1 - x) / (1 + x)) ^ 5 / 5) ≤ Real.arctan x

Lower bound for arctan x, 0 ≤ x ≤ 1.

theorem Zeta32.Fstar.PW.log_one_sub_le {u : ℝ} (h : |u| < 1) (n : ℕ) : Real.log (1 - u) ≤ -∑ i ∈ Finset.range n, u ^ (i + 1) / (↑i + 1) + |u| ^ (n + 1) / (1 - |u|)

theorem Zeta32.Fstar.PW.log_one_sub_ge {u : ℝ} (h : |u| < 1) (n : ℕ) : -∑ i ∈ Finset.range n, u ^ (i + 1) / (↑i + 1) - |u| ^ (n + 1) / (1 - |u|) ≤ Real.log (1 - u)

theorem Zeta32.Fstar.PW.log_one_add_ge {t : ℝ} (h0 : 0 ≤ t) (h1 : t < 1) (n : ℕ) : -∑ i ∈ Finset.range n, (-t) ^ (i + 1) / (↑i + 1) - t ^ (n + 1) / (1 - t) ≤ Real.log (1 + t)

Lower bound for log (1 + t), 0 ≤ t < 1.

theorem Zeta32.Fstar.PW.log_le_scaled {y : ℝ} (hy : 0 < y) (k n : ℕ) (hu : |1 - y / 2 ^ k| < 1) : Real.log y ≤ ↑k * 0.6931471808 + (-∑ i ∈ Finset.range n, (1 - y / 2 ^ k) ^ (i + 1) / (↑i + 1) + |1 - y / 2 ^ k| ^ (n + 1) / (1 - |1 - y / 2 ^ k|))

Upper bound for log y after scaling by 2^k.

theorem Zeta32.Fstar.PW.Wt_eq {x : ℝ} (hx : 0 < x) : Wt x = 2 / 3 * (2 * x * Real.arctan x - Real.log (1 + x ^ 2) + Real.pi * x / 4 - x * Real.arctan (x / 5) / 2 + 5 * Real.log (1 + x ^ 2 / 25) / 4)

Wt in the form without arctan (1/x) (the reciprocal identity), for x > 0.

theorem Zeta32.Fstar.PW.Wt_ge {x A L B M : ℝ} (hx : 0 < x) (hA : A ≤ Real.arctan x) (hL : Real.log (1 + x ^ 2) ≤ L) (hB : Real.arctan (x / 5) ≤ B) (hM : M ≤ Real.log (1 + x ^ 2 / 25)) : 2 / 3 * (2 * x * A - L + 3.141592 * x / 4 - x * B / 2 + 5 * M / 4) ≤ Wt x

Four atom bounds give a lower bound for Wt x.