The global clue budget

theorem LatinQuarter.quarter_eq (n : ℕ) : n * n / 4 = n / 2 * (n - n / 2)

theorem LatinQuarter.sum_free_columns {n : ℕ} (P : Finset (Cell n)) : ∑ r : Fin n, Fintype.card (FreeColumn P r) + P.card = n * n

theorem LatinQuarter.clue_budget {n : ℕ} (P : Finset (Cell n)) (hP : P.card < n * n / 4) : (n - n / 2) * (n - n / 2) < ∑ r : Fin n, (Fintype.card (FreeColumn P r) - n / 2)

The global clue budget supplies exactly the strict inequality used by the residual-position pigeonhole argument.