Uniform bound ℓ(a) ≤ −159/100 on [a₋, a₊]. ℓ = 2log(a/2) + (1/3)J₀ + (4/3)J₁ − (1/3)J₅ with J₀ = −a, J₁ = −log(2/(1+U₁)) − (U₁−1), J₅ = −5log(10/(5+U₅)) − (U₅−5), U_c = √(c²+a²). Each term is bounded separately by monotonicity in a (U₁ ∈ [2647/1250, 105881/50000], U₅ ∈ [266853/50000, 533707/100000]), the three logs by log_le/log_ge'. Upper bound obtained: −1.60135. Data: tools/b2_numerics.py.

theorem Zeta32.Fstar.B2.log_aPlus_half : Real.log (186663 / 100000 / 2) ≤ -6901 / 100000

theorem Zeta32.Fstar.B2.log_U1_ge : -44393 / 100000 ≤ Real.log (2 / (1 + 105881 / 50000))

theorem Zeta32.Fstar.B2.log_U5_le : Real.log (10 / (5 + 266853 / 50000)) ≤ -663 / 20000

theorem Zeta32.Fstar.B2.ell_upper {a : ℝ} (h1 : aMinus ≤ a) (h2 : a ≤ aPlus) : ellA a ≤ -159 / 100