The limited augmented Zarankiewicz number in three columns

Qi, Cui and Xu define the limited augmented Zarankiewicz number z_L(m, n): start from a C4-free set of z(m, n) cells of the m × n grid and add disjoint pairs of cells subject to two forbidden patterns on the final occupied set. We prove z_L(m, 3) = m + 3 + ⌊(m − 2)/2⌋ for every m ≥ 3, answering Open Problem 1 of arXiv:2608.06050.

Main results

• ZL.z_three: z(m, 3) = m + 3 for m ≥ 3
• ZL.zL_three: z_L(m, 3) = m + 3 + ⌊(m − 2)/2⌋ for m ≥ 3

References

• L. Qi, C. Cui, Y. Xu, arXiv:2604.04111v5 (2026), Def. 2.1.
• L. Qi, J. Löfberg, H. Chen, arXiv:2608.06050v3 (2026), §9 Open Problem 1.

@[reducible, inline]

abbrev ZL.Cell (m n : ℕ) : Type

A cell of the m × n grid.

Equations

• ZL.Cell m n = (Fin m × Fin n)

def ZL.C4Free {m n : ℕ} (E : Finset (Cell m n)) : Prop

E contains no all-occupied rectangle (C₄).

Equations

• ZL.C4Free E = ∀ (i p : Fin m) (j q : Fin n), i ≠ p → j ≠ q → ¬((i, j) ∈ E ∧ (i, q) ∈ E ∧ (p, j) ∈ E ∧ (p, q) ∈ E)

noncomputable def ZL.z (m n : ℕ) : ℕ

The Zarankiewicz number z(m, n): the largest size of a C₄-free set of cells.

Equations

• ZL.z m n = sSup {t : ℕ | ∃ (E : Finset (ZL.Cell m n)), ZL.C4Free E ∧ E.card = t}

def ZL.occ {m n : ℕ} (E₁ : Finset (Cell m n)) (E₂ : Finset (Cell m n × Cell m n)) : Finset (Cell m n)

The occupied set: the fixed cells and both halves of every selected pair.

Equations

• ZL.occ E₁ E₂ = E₁ ∪ Finset.image Prod.fst E₂ ∪ Finset.image Prod.snd E₂

def ZL.Admissible {m n : ℕ} (E₁ : Finset (Cell m n)) (E₂ : Finset (Cell m n × Cell m n)) : Prop

Admissibility of a family of 2-edges over a base E₁ (Definition 2.1, conditions (S), C2, C3; C3 is imposed on every pair, degenerate or not).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ZL.zL (m n : ℕ) : ℕ

The limited augmented Zarankiewicz number z_L(m, n).

Equations

• ZL.zL m n = sSup {t : ℕ | ∃ (E₁ : Finset (ZL.Cell m n)) (E₂ : Finset (ZL.Cell m n × ZL.Cell m n)), ZL.C4Free E₁ ∧ E₁.card = ZL.z m n ∧ ZL.Admissible E₁ E₂ ∧ E₁.card + E₂.card = t}

Rows

def ZL.rowset {m : ℕ} (E : Finset (Cell m 3)) (i : Fin m) : Finset (Fin 3)

The columns occupied in row i.

Equations

• ZL.rowset E i = {j : Fin 3 | (i, j) ∈ E}

theorem ZL.mem_rowset {m : ℕ} {E : Finset (Cell m 3)} {i : Fin m} {j : Fin 3} : j ∈ rowset E i ↔ (i, j) ∈ E

theorem ZL.card_eq_sum_rowset {m : ℕ} (E : Finset (Cell m 3)) : E.card = ∑ i : Fin m, (rowset E i).card

def ZL.prs (R : Finset (Fin 3)) : Finset (Fin 3 × Fin 3)

Column pairs j < q both occupied in the row R.

Equations

• ZL.prs R = {x : Fin 3 × Fin 3 | x.1 < x.2 ∧ x.1 ∈ R ∧ x.2 ∈ R}

def ZL.lt3 : Finset (Fin 3 × Fin 3)

All column pairs j < q.

Equations

• ZL.lt3 = {x : Fin 3 × Fin 3 | x.1 < x.2}

theorem ZL.lt3_card : lt3.card = 3

theorem ZL.row_le (R : Finset (Fin 3)) : R.card ≤ 1 + (prs R).card

theorem ZL.row_eq (R : Finset (Fin 3)) : R.card = 1 + (prs R).card → R.card = 1 ∨ R.card = 2

theorem ZL.lt3_or (j l : Fin 3) : j ≠ l → (j, l) ∈ lt3 ∨ (l, j) ∈ lt3

theorem ZL.third_col (j q : Fin 3) : ∃ (t : Fin 3), t ≠ j ∧ t ≠ q

theorem ZL.prs_disjoint {m : ℕ} {E : Finset (Cell m 3)} (h : C4Free E) (i p : Fin m) (hip : i ≠ p) : Disjoint (prs (rowset E i)) (prs (rowset E p))

theorem ZL.sum_prs {m : ℕ} {E : Finset (Cell m 3)} (h : C4Free E) : ∑ i : Fin m, (prs (rowset E i)).card = (Finset.univ.biUnion fun (i : Fin m) => prs (rowset E i)).card

theorem ZL.biUnion_sub {m : ℕ} (E : Finset (Cell m 3)) : (Finset.univ.biUnion fun (i : Fin m) => prs (rowset E i)) ⊆ lt3

theorem ZL.sum_prs_le {m : ℕ} {E : Finset (Cell m 3)} (h : C4Free E) : ∑ i : Fin m, (prs (rowset E i)).card ≤ 3

theorem ZL.sum_one_add {m : ℕ} (E : Finset (Cell m 3)) : ∑ i : Fin m, (1 + (prs (rowset E i)).card) = m + ∑ i : Fin m, (prs (rowset E i)).card

theorem ZL.card_le_of_c4free {m : ℕ} (E : Finset (Cell m 3)) (h : C4Free E) : E.card ≤ m + 3

(a)

theorem ZL.row_structure {m : ℕ} {E : Finset (Cell m 3)} (h : C4Free E) (hc : E.card = m + 3) : (∀ (i : Fin m), (rowset E i).card = 1 ∨ (rowset E i).card = 2) ∧ ∀ (j l : Fin 3), j ≠ l → ∃ (k : Fin m), (k, j) ∈ E ∧ (k, l) ∈ E

(c)

Construction

def ZL.Rrow : ℕ → Finset (Fin 3)

Row pattern of the extremal base.

Equations

• ZL.Rrow 0 = {0, 1}
• ZL.Rrow 1 = {0, 2}
• ZL.Rrow 2 = {1, 2}
• ZL.Rrow x✝ = {0}

def ZL.Ebase (m : ℕ) : Finset (Cell m 3)

The extremal C₄-free base.

Equations

• ZL.Ebase m = {c : ZL.Cell m 3 | c.2 ∈ ZL.Rrow ↑c.1}

theorem ZL.rowset_Ebase {m : ℕ} (i : Fin m) : rowset (Ebase m) i = Rrow ↑i

theorem ZL.Rrow_inj (a b : ℕ) (j q : Fin 3) : a ≠ b → j ≠ q → j ∈ Rrow a → q ∈ Rrow a → j ∈ Rrow b → q ∈ Rrow b → False

theorem ZL.Ebase_c4 {m : ℕ} : C4Free (Ebase m)

theorem ZL.sum_Rrow (k : ℕ) : ∑ n ∈ Finset.range (k + 3), (Rrow n).card = k + 6

theorem ZL.card_Ebase {m : ℕ} (hm : 3 ≤ m) : (Ebase m).card = m + 3

theorem ZL.z_three {m : ℕ} (hm : 3 ≤ m) : z m 3 = m + 3

(b)

The 2-edges

theorem ZL.subset_occ {m : ℕ} (E₁ : Finset (Cell m 3)) (E₂ : Finset (Cell m 3 × Cell m 3)) : E₁ ⊆ occ E₁ E₂

theorem ZL.pair_props {m : ℕ} {E₁ : Finset (Cell m 3)} {E₂ : Finset (Cell m 3 × Cell m 3)} (ha : Admissible E₁ E₂) {e : Cell m 3 × Cell m 3} (he : e ∈ E₂) {x y : Cell m 3} (hxy : x = e.1 ∧ y = e.2 ∨ x = e.2 ∧ y = e.1) : x ≠ y ∧ x ∉ E₁ ∧ y ∉ E₁ ∧ (x.1 ≠ y.1 → x.2 ≠ y.2 → ¬((x.1, y.2) ∈ occ E₁ E₂ ∧ (y.1, x.2) ∈ occ E₁ E₂)) ∧ ∀ (k : Fin m) (l : Fin 3), k ≠ x.1 → k ≠ y.1 → l ≠ x.2 → l ≠ y.2 → ¬((k, l) ∈ occ E₁ E₂ ∧ (k, x.2) ∈ occ E₁ E₂ ∧ (k, y.2) ∈ occ E₁ E₂ ∧ (x.1, l) ∈ occ E₁ E₂ ∧ (y.1, l) ∈ occ E₁ E₂)

theorem ZL.exists_partner {m : ℕ} {E₁ : Finset (Cell m 3)} {E₂ : Finset (Cell m 3 × Cell m 3)} (ha : Admissible E₁ E₂) {F : Fin m} {j : Fin 3} (hO : (F, j) ∈ occ E₁ E₂) (hn : (F, j) ∉ E₁) : ∃ (y : Cell m 3), (F, j) ≠ y ∧ y ∉ E₁ ∧ (F ≠ y.1 → j ≠ y.2 → ¬((F, y.2) ∈ occ E₁ E₂ ∧ (y.1, j) ∈ occ E₁ E₂)) ∧ ∀ (k : Fin m) (l : Fin 3), k ≠ F → k ≠ y.1 → l ≠ j → l ≠ y.2 → ¬((k, l) ∈ occ E₁ E₂ ∧ (k, j) ∈ occ E₁ E₂ ∧ (k, y.2) ∈ occ E₁ E₂ ∧ (F, l) ∈ occ E₁ E₂ ∧ (y.1, l) ∈ occ E₁ E₂)

theorem ZL.no_two_full {m : ℕ} {E₁ : Finset (Cell m 3)} {E₂ : Finset (Cell m 3 × Cell m 3)} (hrow : ∀ (i : Fin m), 1 ≤ (rowset E₁ i).card ∧ (rowset E₁ i).card ≤ 2) (hcov : ∀ (j l : Fin 3), j ≠ l → ∃ (k : Fin m), (k, j) ∈ E₁ ∧ (k, l) ∈ E₁) (ha : Admissible E₁ E₂) {F G : Fin m} (hFG : F ≠ G) (hF : ∀ (c : Fin 3), (F, c) ∈ occ E₁ E₂) (hG : ∀ (c : Fin 3), (G, c) ∈ occ E₁ E₂) : False

Lemma F: at most one full row.

theorem ZL.card_occ {m : ℕ} {E₁ : Finset (Cell m 3)} {E₂ : Finset (Cell m 3 × Cell m 3)} (ha : Admissible E₁ E₂) : (occ E₁ E₂).card = E₁.card + 2 * E₂.card

theorem ZL.card_E2_le {m : ℕ} (hm : 3 ≤ m) (E₁ : Finset (Cell m 3)) (E₂ : Finset (Cell m 3 × Cell m 3)) (h1 : C4Free E₁) (hc : E₁.card = m + 3) (ha : Admissible E₁ E₂) : 2 * E₂.card ≤ m - 2

(d)

theorem ZL.zL_le {m : ℕ} (hm : 3 ≤ m) : zL m 3 ≤ m + 3 + (m - 2) / 2

(e)

Lower bound: explicit constructions

theorem ZL.sumRows (n : ℕ) (hn : 3 ≤ n) : (∑ i ∈ Finset.range n, if i < 3 then 2 else 1) = n + 3

Odd m = 2N + 3

def ZL.PO (i j : ℕ) : Prop

Membership predicate of the odd base.

Equations

• ZL.PO i j = (i = 0 ∧ j ≤ 1 ∨ i = 1 ∧ j ≠ 1 ∨ i = 2 ∧ 1 ≤ j ∨ 3 ≤ i ∧ j = 0)

@[instance_reducible]

instance ZL.instDecidablePO (i j : ℕ) : Decidable (PO i j)

Equations

• ZL.instDecidablePO i j = id inferInstance

def ZL.baseO (N : ℕ) : Finset (Cell (2 * N + 3) 3)

The odd base.

Equations

• ZL.baseO N = {c : ZL.Cell (2 * N + 3) 3 | ZL.PO ↑c.1 ↑c.2}

def ZL.pairsO (N : ℕ) : Finset (Cell (2 * N + 3) 3 × Cell (2 * N + 3) 3)

The odd pairs.

Equations

• ZL.pairsO N = Finset.image (fun (t : Fin N) => ((⟨3 + 2 * ↑t, ⋯⟩, ⟨1, ZL.pairsO._proof_4⟩), ⟨4 + 2 * ↑t, ⋯⟩, ⟨2, ZL.pairsO._proof_8⟩)) Finset.univ

theorem ZL.mem_baseO (N : ℕ) (c : Cell (2 * N + 3) 3) : c ∈ baseO N ↔ PO ↑c.1 ↑c.2

theorem ZL.mem_occO (N : ℕ) (c : Cell (2 * N + 3) 3) : c ∈ occ (baseO N) (pairsO N) ↔ PO ↑c.1 ↑c.2 ∨ 3 ≤ ↑c.1 ∧ ↑c.1 % 2 = 1 ∧ ↑c.2 = 1 ∨ 4 ≤ ↑c.1 ∧ ↑c.1 % 2 = 0 ∧ ↑c.2 = 2

theorem ZL.card_baseO (N : ℕ) : (baseO N).card = 2 * N + 3 + 3

theorem ZL.c4O (N : ℕ) : C4Free (baseO N)

theorem ZL.admO (N : ℕ) : Admissible (baseO N) (pairsO N)

theorem ZL.card_pairsO (N : ℕ) : (pairsO N).card = N

theorem ZL.exists_odd (N : ℕ) : ∃ (E₁ : Finset (Cell (2 * N + 3) 3)) (E₂ : Finset (Cell (2 * N + 3) 3 × Cell (2 * N + 3) 3)), C4Free E₁ ∧ E₁.card = 2 * N + 3 + 3 ∧ Admissible E₁ E₂ ∧ E₂.card = (2 * N + 3 - 2) / 2

Even m = 2q + 4

def ZL.PE (q i j : ℕ) : Prop

Membership predicate of the even base.

Equations

• ZL.PE q i j = (i = 0 ∧ j ≤ 1 ∨ i = 1 ∧ j ≠ 1 ∨ i = 2 ∧ 1 ≤ j ∨ 3 ≤ i ∧ i ≤ q + 2 ∧ j = 0 ∨ q + 3 ≤ i ∧ j = 1)

@[instance_reducible]

instance ZL.instDecidablePE (q i j : ℕ) : Decidable (PE q i j)

Equations

• ZL.instDecidablePE q i j = id inferInstance

def ZL.baseE (q : ℕ) : Finset (Cell (2 * q + 4) 3)

The even base.

Equations

• ZL.baseE q = {c : ZL.Cell (2 * q + 4) 3 | ZL.PE q ↑c.1 ↑c.2}

def ZL.vertE (q : ℕ) : Finset (Cell (2 * q + 4) 3 × Cell (2 * q + 4) 3)

The vertical pairs.

Equations

• ZL.vertE q = Finset.image (fun (t : Fin q) => ((⟨3 + ↑t, ⋯⟩, ⟨2, ZL.pairsO._proof_8⟩), ⟨q + 3 + ↑t, ⋯⟩, ⟨2, ZL.pairsO._proof_8⟩)) Finset.univ

def ZL.specE (q : ℕ) : Cell (2 * q + 4) 3 × Cell (2 * q + 4) 3

The special pair.

Equations

• ZL.specE q = ((⟨2, ⋯⟩, ⟨0, ZL.specE._proof_4⟩), ⟨2 * q + 3, ⋯⟩, ⟨2, ZL.pairsO._proof_8⟩)

def ZL.pairsE (q : ℕ) : Finset (Cell (2 * q + 4) 3 × Cell (2 * q + 4) 3)

The even pairs.

Equations

• ZL.pairsE q = insert (ZL.specE q) (ZL.vertE q)

theorem ZL.mem_baseE (q : ℕ) (c : Cell (2 * q + 4) 3) : c ∈ baseE q ↔ PE q ↑c.1 ↑c.2

theorem ZL.mem_occE (q : ℕ) (c : Cell (2 * q + 4) 3) : c ∈ occ (baseE q) (pairsE q) ↔ PE q ↑c.1 ↑c.2 ∨ 3 ≤ ↑c.1 ∧ ↑c.2 = 2 ∨ ↑c.1 = 2 ∧ ↑c.2 = 0

theorem ZL.card_baseE (q : ℕ) : (baseE q).card = 2 * q + 4 + 3

theorem ZL.c4E (q : ℕ) : C4Free (baseE q)

theorem ZL.admE (q : ℕ) : Admissible (baseE q) (pairsE q)

theorem ZL.card_pairsE (q : ℕ) : (pairsE q).card = q + 1

theorem ZL.exists_even (q : ℕ) : ∃ (E₁ : Finset (Cell (2 * q + 4) 3)) (E₂ : Finset (Cell (2 * q + 4) 3 × Cell (2 * q + 4) 3)), C4Free E₁ ∧ E₁.card = 2 * q + 4 + 3 ∧ Admissible E₁ E₂ ∧ E₂.card = (2 * q + 4 - 2) / 2

theorem ZL.exists_good {m : ℕ} (hm : 3 ≤ m) : ∃ (E₁ : Finset (Cell m 3)) (E₂ : Finset (Cell m 3 × Cell m 3)), C4Free E₁ ∧ E₁.card = m + 3 ∧ Admissible E₁ E₂ ∧ E₂.card = (m - 2) / 2

Lower-bound construction for every m ≥ 3.

theorem ZL.zL_three {m : ℕ} (hm : 3 ≤ m) : zL m 3 = m + 3 + (m - 2) / 2

Main theorem. z_L(m, 3) = m + 3 + ⌊(m - 2) / 2⌋ for every m ≥ 3.