Sharpness for mean-zero functions: use Φ(w) − Φ(−w), an inequality suffices

Pichorides' extremal Φ_γ(w) = ((1+w)/(1−w))^γ has Φ(0) = 1, so its Taylor polynomials carry a constant term. For a lower bound on the conjugate-function norm restricted to mean-zero functions, use Ψ(w) = Φ(w) − Φ(−w) instead, which has Ψ(0) = 0. On the circle, with t = cot πθ, Φ(e) = (it)^γ and Φ(−e) = (−i/t)^γ, so Re Ψ = (t^γ − t^{−γ})cos(γπ/2) and |Im Ψ| = (t^γ + t^{−γ})sin(γπ/2). This gives the pointwise inequality |Im Ψ| ≥ tan(γπ/2)|Re Ψ|, which is enough. The majorant becomes (2/sin πθ)^γ + (2/|cos πθ|)^γ, with a second singularity at θ = 1/2. Lean tips: prove ‖(1+ru)/(1−ru)‖ ≤ 4/‖1−u‖ once for any unit u and apply it to u = ±e(θ). ‖1 + e(θ)‖ = 2|cos πθ| follows from e(θ+1/2) = −e(θ) and Complex.norm_exp_I_mul_ofReal_sub_one. Real rpow of a possibly negative base defeats positivity, so give Real.rpow_nonneg explicitly.