Boolean degree one functions on the Grassmann scheme

Abstract

Ferdinand Ihringer proved that Boolean degree one functions on the Grassmann scheme $J_q(n,k)$ are trivial when $\min (k,n-k)\ge 2$ and $n$ is large enough. We provide a mostly self-contained exposition of this result. All results were formalized by ChatGPT 5.6 Sol, and are available on GitHub at YuvalFilmus/grassmann-degree-one.

15 pages