Sum of attention outputs: NO rows each ≤ D/(8n), ≥ D YES rows each ≥ 1/2 ⇒ YES sum ≥ 4 × NO sum

For all $\htmlData{mx=1}{n \in \htmlData{mx=0}{\mathbb{N}}}$, $\htmlData{mx=5}{\mathit{oNo}, \mathit{oYes} : \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fin}}\,\htmlData{mx=1}{n}} \mathrel{\htmlData{mx=4}{\to}} \htmlData{mx=3}{\mathbb{R}}}$, $\htmlData{mx=5}{Y \in \htmlData{mx=4}{\htmlData{mx=0}{\operatorname{Finset}}\,\htmlData{mx=3}{\htmlData{mx=1}{\operatorname{Fin}}\,\htmlData{mx=2}{n}}}}$ and $\htmlData{mx=1}{D \in \htmlData{mx=0}{\mathbb{R}}}$, if $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{n}$, $0 \mathrel{\htmlData{mx=1}{\leq}} \htmlData{mx=0}{D}$, $\htmlData{mx=8}{\forall i,\ \htmlData{mx=2}{\htmlData{mx=0}{\mathit{oNo}}(\htmlData{mx=1}{i})} \mathrel{\htmlData{mx=7}{\leq}} \htmlData{mx=6}{\frac{\htmlData{mx=3}{D}}{\htmlData{mx=5}{8\htmlData{mx=4}{n}}}}}$, $\htmlData{mx=0}{D} \mathrel{\htmlData{mx=2}{\leq}} \htmlData{mx=1}{\operatorname{card}}$, $\htmlData{mx=6}{\forall i \in \htmlData{mx=5}{Y},\ \htmlData{mx=0}{\frac{1}{2}} \mathrel{\htmlData{mx=4}{\leq}} \htmlData{mx=3}{\htmlData{mx=1}{\mathit{oYes}}(\htmlData{mx=2}{i})}}$ and $\htmlData{mx=4}{\forall i,\ 0 \mathrel{\htmlData{mx=3}{\leq}} \htmlData{mx=2}{\htmlData{mx=0}{\mathit{oYes}}(\htmlData{mx=1}{i})}}$, then