Completion of a sparse partial Latin array with few symbols

Proved

ProofsInTheBook.Chapter33.lemma2_few_elements_completes

by xiangyazi24 · Sep 12, 2026 · Mathlib c5ea003 (Lean v4.30.0)

auxiliary-lemmabook-chapter-36combinatoricslatin-squareslean4proofs-from-the-book

Write $[n]=\{0,\ldots,n-1\}$ for $n\in\mathbb N$ , with $[0]=\varnothing$ . A partial array of order $n$ is a map $P:[n]^2\to[n]\cup\{\bot\}$ , with $\bot$ denoting an empty cell. Write $F(P)=\{(i,j):P(i,j)\ne\bot\}$ and $U(P)=\{a\in[n]:\exists i,j,\ P(i,j)=a\}$ . It is partial Latin when no symbol repeats within a row or column. A completion is a map $L:[n]^2\to[n]$ injective in each row and column, with $L(i,j)=a$ whenever $P(i,j)=a\ne\bot$ . Let $n\in\mathbb N$ and let $P$ be partial Latin of order $n$ . If

|F(P)|+1\le n,\qquad 2|U(P)|\le n,

then $P$ has a completion of order $n$ .

Preamble

import Init
import Mathlib
import Definitions.Def_P2MAssembly_Chapter33
set_option autoImplicit true
open Finset
open Classical
open ProofsInTheBook.Chapter33

Formal statement

theorem ProofsInTheBook.Chapter33.lemma2_few_elements_completes (n : ℕ)
    (P : Fin n → Fin n → Option (Fin n)) (hP : IsPartialLatin P)
    (hcard : (filledCells P).card + 1 <= n)
    (helem : 2 * (elementsUsed P).card <= n) :
    ∃ L : Fin n → Fin n → Fin n, Completes P L := by sorry

Source

Original formalization: https://github.com/xiangyazi24/proof_in_the_book/blob/88d88d141768cded75e782c525ef1bf04b8fe220/ProofsInTheBook/Chapter33Ryser.lean#L1476. Topic: Aigner and Ziegler, Proofs from THE BOOK, 6th edition, Chapter 36, “Completing Latin squares”, pp. 253–258 (https://doi.org/10.1007/978-3-662-57265-8_36).

View graph