The construction

The coordinate set is V = ι × Fin r, where ι indexes the vertices of a tournament (Arc i j says there is an arc i → j) and Fin r indexes the coordinates inside a block. For i : ι the block B_i is {i} × Fin r.

A gate labelling γ : ι → ι → Fin r picks, for every arc i → j, a coordinate gateCoord γ i j = (j, γ i j) of the block B_j.

The certificate C_i is the subcube cut out by the partial assignment cert Arc γ i:

• every coordinate of B_i is fixed to true;
• for every arc i → j, the gate coordinate (j, γ i j) is fixed to false.

Finally ind Arc γ is the indicator of the union of the C_i.

This file only fixes the definitions and their basic combinatorics; the tournament hypotheses are passed explicitly to the lemmas that need them, so that nothing here depends on the particular (Paley) tournament used later.

Adapted for Lean Pool from Timeroot/BS_Lam at commit 7bd39a8d41ee7910d3296d0477ad18f8fff9d870; ported to Lean Pool with proof and dependency cleanup.

Coordinate blocks

@[reducible, inline]

abbrev BSLambda.Construction.Coord (ι : Type u_2) (r : ℕ) : Type u_2

The coordinate set V = ι × [r] of the construction (Section 3).

Equations

• BSLambda.Construction.Coord ι r = (ι × Fin r)

def BSLambda.Construction.block {ι : Type u_1} {r : ℕ} (i : ι) : Finset (Coord ι r)

The coordinate block B_i = {i} × [r] (Section 3).

Equations

• BSLambda.Construction.block i = {i} ×ˢ Finset.univ

@[simp]

theorem BSLambda.Construction.mem_block {ι : Type u_1} {r : ℕ} {i : ι} {v : Coord ι r} : v ∈ block i ↔ v.1 = i

@[simp]

theorem BSLambda.Construction.card_block {ι : Type u_1} {r : ℕ} (i : ι) : (block i).card = r

theorem BSLambda.Construction.block_nonempty {ι : Type u_1} {r : ℕ} [NeZero r] (i : ι) : (block i).Nonempty

theorem BSLambda.Construction.block_disjoint {ι : Type u_1} {r : ℕ} {i j : ι} (h : i ≠ j) : Disjoint (block i) (block j)

Gate coordinates

def BSLambda.Construction.gateCoord {ι : Type u_1} {r : ℕ} (γ : ι → ι → Fin r) (i j : ι) : Coord ι r

The gate coordinate (j, γ(i,j)) selected by the arc i → j (Section 3.1).

Equations

• BSLambda.Construction.gateCoord γ i j = (j, γ i j)

@[simp]

theorem BSLambda.Construction.gateCoord_fst {ι : Type u_1} {r : ℕ} (γ : ι → ι → Fin r) (i j : ι) : (gateCoord γ i j).1 = j

theorem BSLambda.Construction.gateCoord_injective {ι : Type u_1} {r : ℕ} (γ : ι → ι → Fin r) (i : ι) : Function.Injective (gateCoord γ i)

theorem BSLambda.Construction.gateCoord_fst_eq_self {ι : Type u_1} {r : ℕ} {γ : ι → ι → Fin r} {i : ι} {v : Coord ι r} (h : v.2 = γ i v.1) : gateCoord γ i v.1 = v

A coordinate carrying the gate label of the arc i → v.1 is that gate coordinate.

The certificates

def BSLambda.Construction.cert {ι : Type u_1} {r : ℕ} [DecidableEq ι] (Arc : ι → ι → Bool) (γ : ι → ι → Fin r) (i : ι) : PartialAssign (Coord ι r)

The partial assignment P_i cutting out the certificate C_i (Section 3.2): the owner block B_i is fixed to true, and every outgoing gate coordinate is fixed to false.

Equations

• BSLambda.Construction.cert Arc γ i v = if v.1 = i then some true else if Arc i v.1 = true ∧ v.2 = γ i v.1 then some false else none

theorem BSLambda.Construction.cert_apply {ι : Type u_1} {r : ℕ} [DecidableEq ι] {Arc : ι → ι → Bool} {γ : ι → ι → Fin r} {i : ι} {v : Coord ι r} : cert Arc γ i v = if v.1 = i then some true else if Arc i v.1 = true ∧ v.2 = γ i v.1 then some false else none

The three-way case split describing P_i.

theorem BSLambda.Construction.cert_eq_some_iff {ι : Type u_1} {r : ℕ} [DecidableEq ι] {Arc : ι → ι → Bool} {γ : ι → ι → Fin r} {i : ι} {v : Coord ι r} {b : Bool} : cert Arc γ i v = some b ↔ v.1 = i ∧ b = true ∨ v.1 ≠ i ∧ Arc i v.1 = true ∧ v.2 = γ i v.1 ∧ b = false

The literals of P_i: it fixes v to true on the owner block B_i, and to false on the gate coordinate of an outgoing arc. Every other lemma of this section is a specialisation of this one.

theorem BSLambda.Construction.cert_apply_of_fst_eq {ι : Type u_1} {r : ℕ} [DecidableEq ι] {Arc : ι → ι → Bool} {γ : ι → ι → Fin r} {i : ι} {v : Coord ι r} (h : v.1 = i) : cert Arc γ i v = some true

Inside the owner block, P_i fixes the coordinate to true.

theorem BSLambda.Construction.cert_apply_gateCoord {ι : Type u_1} {r : ℕ} [DecidableEq ι] {Arc : ι → ι → Bool} {γ : ι → ι → Fin r} {i j : ι} (hji : j ≠ i) (hij : Arc i j = true) : cert Arc γ i (gateCoord γ i j) = some false

On a gate coordinate of an outgoing arc, P_i fixes the coordinate to false.

theorem BSLambda.Construction.cert_apply_eq_none {ι : Type u_1} {r : ℕ} [DecidableEq ι] {Arc : ι → ι → Bool} {γ : ι → ι → Fin r} {i : ι} {v : Coord ι r} (h₁ : v.1 ≠ i) (h₂ : ¬(Arc i v.1 = true ∧ v.2 = γ i v.1)) : cert Arc γ i v = none

Away from the owner block and from the outgoing gate coordinates, P_i is free.

theorem BSLambda.Construction.cert_ne_some_true_of_fst_ne {ι : Type u_1} {r : ℕ} [DecidableEq ι] {Arc : ι → ι → Bool} {γ : ι → ι → Fin r} {i : ι} {v : Coord ι r} (h : v.1 ≠ i) : cert Arc γ i v ≠ some true

P_i never fixes a coordinate outside B_i to true.

theorem BSLambda.Construction.arc_and_snd_eq_of_cert_eq_some {ι : Type u_1} {r : ℕ} [DecidableEq ι] {Arc : ι → ι → Bool} {γ : ι → ι → Fin r} {i : ι} {v : Coord ι r} {b : Bool} (h : v.1 ≠ i) (hb : cert Arc γ i v = some b) : Arc i v.1 = true ∧ v.2 = γ i v.1

Outside its owner block, the only coordinates P_i fixes are the gate coordinates (j, γ(i,j)) of its outgoing arcs i → j.

theorem BSLambda.Construction.sat_cert_iff {ι : Type u_1} {r : ℕ} [DecidableEq ι] {Arc : ι → ι → Bool} {γ : ι → ι → Fin r} {i : ι} {x : Input (Coord ι r)} : (cert Arc γ i).Sat x ↔ (∀ (a : Fin r), x (i, a) = true) ∧ ∀ (j : ι), j ≠ i → Arc i j = true → x (gateCoord γ i j) = false

Membership in the certificate subcube C_i, spelled out (Section 3.2).

The fixed coordinates of a certificate

theorem BSLambda.Construction.fixedSet_cert {ι : Type u_1} {r : ℕ} [Fintype ι] [DecidableEq ι] {Arc : ι → ι → Bool} {γ : ι → ι → Fin r} {i : ι} : (cert Arc γ i).fixedSet = block i ∪ Finset.image (gateCoord γ i) (outNbrs Arc i)

The set of coordinates fixed by P_i: the owner block together with the outgoing gate coordinates (Section 3.2). No irreflexivity hypothesis is needed; a self-arc i → i would just put its gate coordinate in the owner block as well.

theorem BSLambda.Construction.disjoint_block_image_gateCoord {ι : Type u_1} {r : ℕ} [Fintype ι] [DecidableEq ι] {Arc : ι → ι → Bool} {γ : ι → ι → Fin r} {i : ι} (hT : IsTournament Arc) : Disjoint (block i) (Finset.image (gateCoord γ i) (outNbrs Arc i))

The owner block B_i is disjoint from the outgoing gate coordinates: the gate coordinate of the arc i → j lies in the block B_j, and j ≠ i.

theorem BSLambda.Construction.codim_cert {ι : Type u_1} {r : ℕ} [Fintype ι] [DecidableEq ι] {Arc : ι → ι → Bool} {γ : ι → ι → Fin r} {i : ι} (hT : IsTournament Arc) : (cert Arc γ i).codim = r + (outNbrs Arc i).card

The codimension of every certificate is r + outdeg(i) (Section 3.2: c = r + d).

The function f

ind is a distinct head symbol from PartialAssign.indUnion, so the simp lemmas of the latter do not fire on it; the three lemmas below restate them for ind.

def BSLambda.Construction.ind {ι : Type u_1} {r : ℕ} [Fintype ι] [DecidableEq ι] (Arc : ι → ι → Bool) (γ : ι → ι → Fin r) : Input (Coord ι r) → Bool

The Boolean function f: the indicator of the union of the certificate subcubes C_i (Section 3.3).

Equations

• BSLambda.Construction.ind Arc γ = BSLambda.PartialAssign.indUnion (BSLambda.Construction.cert Arc γ)

@[simp]

theorem BSLambda.Construction.ind_eq_true_iff {ι : Type u_1} {r : ℕ} [Fintype ι] [DecidableEq ι] {Arc : ι → ι → Bool} {γ : ι → ι → Fin r} {x : Input (Coord ι r)} : ind Arc γ x = true ↔ ∃ (i : ι), (cert Arc γ i).Sat x

A point is positive exactly when some certificate subcube contains it.

@[simp]

theorem BSLambda.Construction.ind_eq_false_iff {ι : Type u_1} {r : ℕ} [Fintype ι] [DecidableEq ι] {Arc : ι → ι → Bool} {γ : ι → ι → Fin r} {x : Input (Coord ι r)} : ind Arc γ x = false ↔ ∀ (i : ι), ¬(cert Arc γ i).Sat x

A point is negative exactly when no certificate subcube contains it.

theorem BSLambda.Construction.ind_eq_true_of_sat {ι : Type u_1} {r : ℕ} [Fintype ι] [DecidableEq ι] {Arc : ι → ι → Bool} {γ : ι → ι → Fin r} {i : ι} {x : Input (Coord ι r)} (h : (cert Arc γ i).Sat x) : ind Arc γ x = true

Every point of a certificate subcube is positive.