Polynomial coefficients count Latin completions

noncomputable def LatinQuarter.clueProduct {n : ℕ} {R : Type u_1} [CommRing R] (P : Finset (Cell n)) (L : Square n) (Y : Matrix (Fin n) (Fin n) R) : R

The factors contributed by the filled cells to the completion polynomial.

Equations

• LatinQuarter.clueProduct P L Y = ∏ r : Fin n, ∏ c : { c : Fin n // (r, c) ∈ P }, Y (↑c) (L r ↑c)

noncomputable def LatinQuarter.rowMinorProduct {n : ℕ} {R : Type u_1} [CommRing R] (P : Finset (Cell n)) (L : Square n) (Y : Matrix (Fin n) (Fin n) R) : R

The product of row matching determinants over the unfilled cells.

Equations

• LatinQuarter.rowMinorProduct P L Y = ∏ r : Fin n, (Y.submatrix (fun (c : LatinQuarter.FreeColumn P r) => ↑c) fun (c : LatinQuarter.FreeColumn P r) => L r ↑c).det

theorem LatinQuarter.expand_row_matchings {n : ℕ} {R : Type u_1} [CommRing R] [CharP R 2] (P : Finset (Cell n)) (L : Square n) (Y : Matrix (Fin n) (Fin n) R) : clueProduct P L Y * rowMinorProduct P L Y = ∑ σ : RowChoices P, ∏ p : Cell n, Y p.2 (chosenSquare P L σ p.1 p.2)

Expanding the row matching sums enumerates all independent ways to finish the rows. The clue factors restore the full set of cells.

@[reducible, inline]

abbrev LatinQuarter.columnSymbol {n : ℕ} (M : Square n) (p : Cell n) : Cell n

The column-symbol position recording a cell's contribution to its monomial.

Equations

• LatinQuarter.columnSymbol M p = (p.2, M p.1 p.2)

theorem LatinQuarter.columnSymbol_bijective {n : ℕ} {M : Square n} (hM : IsLatin M) : Function.Bijective (columnSymbol M)

theorem LatinQuarter.isLatin_of_columnSymbol_injective {n : ℕ} {M : Square n} (hr : ∀ (r : Fin n), Function.Bijective (M r)) (hi : Function.Injective (columnSymbol M)) : IsLatin M

theorem LatinQuarter.full_coefficient {n : ℕ} (M : Square n) (hr : ∀ (r : Fin n), Function.Bijective (M r)) : (∏ p : Cell n, MvPolynomial.X (columnSymbol M p)).coeff (allTagsExponent (Cell n)) = if IsLatin M then 1 else 0

The full square-free coefficient is one for a Latin square and zero for a row permutation that repeats a symbol in a column.

theorem LatinQuarter.coefficient_eq_sum_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, if IsLatin (chosenSquare P L σ) then 1 else 0

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

theorem LatinQuarter.defining_coefficient_one {n : ℕ} (P : Finset (Cell n)) (L : Square n) (h : IsDefining P 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)) = 1

Adding constants preserves the completion coefficient, and unique completion makes that coefficient exactly one.