The lower bound for defining sets #
theorem
LatinQuarter.small_clue_coefficient_zero
{n : ℕ}
(P : Finset (Cell n))
(L : Square n)
(e : Fin (n / 2) ⊕ Fin (n - n / 2) ≃ Fin n)
(hP : P.card < n * n / 4)
:
(clueProduct P L (Matrix.of fun (c s : Fin n) => MvPolynomial.X (c, s) + MvPolynomial.C (markedConstant e c s)) * rowMinorProduct P L
(Matrix.of fun (c s : Fin n) => MvPolynomial.X (c, s) + MvPolynomial.C (markedConstant e c s))).coeff
(allTagsExponent (Cell n)) = 0
Below the quarter bound, any balanced choice of marked positions makes the completion polynomial's highest square-free coefficient vanish. No Latin condition on the reference square is required.
theorem
LatinQuarter.defining_set_lower_bound
{n : ℕ}
(P : Finset (Cell n))
(L : Square n)
(h : IsDefining P L)
:
Every defining set in every labelled Latin square has at least the quarter-square number of clues. No restriction on the completed square or on the distribution of its clues is assumed.