A monotone counterexample to a question on distributional complexity

For a Boolean function under a product measure, distributional algorithmic complexity is the minimum expected number of adaptive queries needed to determine its value. Distributional subcube partition complexity is the minimum expected number of fixed coordinates in a monochromatic subcube partition. Köhler-Schindler and Steif asked in 2024 whether these quantities are equal for every monotone Boolean function. We answer their Question 2.1 in the negative with the explicit function f(x₀,…,x₄)=x₁x₂x₃ x₀x₄(x₁ x₂ x₃). For independent fair input bits its algorithmic complexity is $13/4$, while its subcube partition complexity is $51/16$. A finite recurrence proves the algorithmic lower bound, and an explicit partition gives the strict inequality. An exact linear-programming dual certificate proves the partition value is optimal. The strict inequality is formalized in Lean; independent exact checkers verify the additional dual certificate. Computer-assisted; not yet reviewed by experts. Produced by AI models under the author's direction.