The Hellinger conjecture for Boolean functions under product noise

Claims Theorem 1.1: for every $n\ge1$, every $f:\{-1,1\}^n\to\{-1,1\}$ with $m=\mathbb E f$ and every $\rho\in[-1,1]$, $\sqrt{1-m^2}-\mathbb E\sqrt{1-(T_\rho f)^2}\le1-\sqrt{1-\rho^2}$, with equality for signed coordinates. By the Anantharam et al. implication it reproves the Courtade-Kumar bound (Corollary 8.1). It does NOT treat non-Boolean (soft) functions or non-uniform inputs, and its proof depends on computer-checked arithmetic certificates.

Claims Theorem 1.1: for every $n\ge1$, every $f:\{-1,1\}^n\to\{-1,1\}$ with $m=\mathbb E f$ and every $\rho\in[-1,1]$, $\sqrt{1-m^2}-\mathbb E\sqrt{1-(T_\rho f)^2}\le1-\sqrt{1-\rho^2}$, with equality for signed coordinates. By the Anantharam et al. implication it reproves the Courtade-Kumar bound (Corollary 8.1). It does NOT treat non-Boolean (soft) functions or non-uniform inputs, and its proof depends on computer-checked arithmetic certificates.