Parity of the number of completions

Written by Claude (Anthropic) at Richard Bean's request, October 2026, for version 0.2.0. This is Theorem A of the paper: below the quarter bound, every set of clues taken from a Latin square has an even number of completions.

The coefficient computation in Counting.lean holds for every set of clues, not only for defining sets: the square-free coefficient counts, modulo two, the row choices that produce Latin squares. Those row choices correspond exactly to the completions. The vanishing argument used in LowerBound.lean makes the coefficient zero below the quarter bound.

theorem LatinQuarter.coefficient_eq_card_latin_choices {n : ℕ} (P : Finset (Cell n)) (L : Square n) (hL : IsLatin L) (a : Cell n → ZMod 2) : (clueProduct P L (Matrix.of fun (c s : Fin n) => MvPolynomial.X (c, s) + MvPolynomial.C (a (c, s))) * rowMinorProduct P L (Matrix.of fun (c s : Fin n) => MvPolynomial.X (c, s) + MvPolynomial.C (a (c, s)))).coeff (allTagsExponent (Cell n)) = ↑{σ : RowChoices P | IsLatin (chosenSquare P L σ)}.card

The square-free coefficient counts the Latin row choices modulo two.

theorem LatinQuarter.exists_rowChoices_of_completion {n : ℕ} (P : Finset (Cell n)) (L : Square n) (hL : IsLatin L) (M : Square n) (hM : IsLatin M) (ha : Agrees P L M) : ∃ (σ : RowChoices P), chosenSquare P L σ = M

Every completion arises from one permutation of the free cells in each row.

theorem LatinQuarter.card_completions_eq {n : ℕ} (P : Finset (Cell n)) (L : Square n) (hL : IsLatin L) : (completions P L).card = {σ : RowChoices P | IsLatin (chosenSquare P L σ)}.card

The completions are in bijection with the Latin row choices.

theorem LatinQuarter.completions_card_even {n : ℕ} (P : Finset (Cell n)) (L : Square n) (hL : IsLatin L) (hP : P.card < n * n / 4) : Even (completions P L).card

Theorem A, in the cell form used throughout this package: if fewer than n * n / 4 cells of a Latin square L are given, the number of Latin squares that agree with L on those cells is even.