Finite edge-set infrastructure for BKLO Lemma 10.7 at r = 2

This module contains only the finite graph vocabulary needed by the pseudorandom simultaneous matching theorem. It is extracted from the independently frozen Paper III development and is kept separate from the theorem-facing API.

def BKLOK2.cliqueEdges {V : Type u_1} [DecidableEq V] (t : Finset V) : Finset (Sym2 V)

The edge set (as Sym2) of a Finset of vertices, viewed as a complete graph on that set: all unordered pairs of distinct vertices of t. For a 3-set this is the triangle's three edges.

Equations

• BKLOK2.cliqueEdges t = {e ∈ t.sym2 | ¬e.IsDiag}

theorem BKLOK2.mem_cliqueEdgesV {V : Type u_1} [DecidableEq V] {t : Finset V} {e : Sym2 V} : e ∈ cliqueEdges t ↔ (∀ x ∈ e, x ∈ t) ∧ ¬e.IsDiag

def BKLOK2.edeg {V : Type u_1} [DecidableEq V] (E : Finset (Sym2 V)) (v : V) : ℕ

The number of edges of E at v.

Equations

• BKLOK2.edeg E v = {e ∈ E | v ∈ e}.card

def BKLOK2.nbhdIn {V : Type u_1} [DecidableEq V] (E : Finset (Sym2 V)) (x : V) (S : Finset V) : Finset V

N_E(x, S): the neighbours of x inside S.

Equations

• BKLOK2.nbhdIn E x S = {y ∈ S | s(x, y) ∈ E}

def BKLOK2.degTo {V : Type u_1} [DecidableEq V] (E : Finset (Sym2 V)) (x : V) (S : Finset V) : ℕ

d_E(x, S) = |N_E(x, S)|.

Equations

• BKLOK2.degTo E x S = (BKLOK2.nbhdIn E x S).card

theorem BKLOK2.mem_nbhdIn {V : Type u_1} [DecidableEq V] {E : Finset (Sym2 V)} {x y : V} {S : Finset V} : y ∈ nbhdIn E x S ↔ y ∈ S ∧ s(x, y) ∈ E

theorem BKLOK2.nbhdIn_subset {V : Type u_1} [DecidableEq V] (E : Finset (Sym2 V)) (x : V) (S : Finset V) : nbhdIn E x S ⊆ S

def BKLOK2.edgesIn {V : Type u_1} [DecidableEq V] (E : Finset (Sym2 V)) (S : Finset V) : Finset (Sym2 V)

E[S]: the edges of E with both ends in S.

Equations

• BKLOK2.edgesIn E S = {e ∈ E | e ∈ S.sym2}

def BKLOK2.edgesBtw {V : Type u_1} [DecidableEq V] (E : Finset (Sym2 V)) (S T : Finset V) : Finset (Sym2 V)

E[S, T]: the edges of E with one end in S and the other in T.

Equations

• BKLOK2.edgesBtw E S T = {e ∈ E | ∃ a ∈ S, ∃ b ∈ T, e = s(a, b)}

def BKLOK2.insideParts {V : Type u_1} [DecidableEq V] (E : Finset (Sym2 V)) (P : Finset (Finset V)) : Finset (Sym2 V)

E − E[P] = ⋃_{W ∈ P} E[W]: the edges of E lying inside a part of P.

Equations

• BKLOK2.insideParts E P = {e ∈ E | ∃ W ∈ P, e ∈ W.sym2}

def BKLOK2.crossParts {V : Type u_1} [DecidableEq V] (E : Finset (Sym2 V)) (P : Finset (Finset V)) : Finset (Sym2 V)

E[P]: the edges of E joining two different parts of P.

Equations

• BKLOK2.crossParts E P = {e ∈ E | ¬∃ W ∈ P, e ∈ W.sym2}

theorem BKLOK2.mem_edgesIn {V : Type u_1} [DecidableEq V] {E : Finset (Sym2 V)} {S : Finset V} {e : Sym2 V} : e ∈ edgesIn E S ↔ e ∈ E ∧ ∀ v ∈ e, v ∈ S

theorem BKLOK2.mem_insideParts {V : Type u_1} [DecidableEq V] {E : Finset (Sym2 V)} {P : Finset (Finset V)} {e : Sym2 V} : e ∈ insideParts E P ↔ e ∈ E ∧ ∃ W ∈ P, ∀ v ∈ e, v ∈ W

theorem BKLOK2.mem_crossParts {V : Type u_1} [DecidableEq V] {E : Finset (Sym2 V)} {P : Finset (Finset V)} {e : Sym2 V} : e ∈ crossParts E P ↔ e ∈ E ∧ ¬∃ W ∈ P, ∀ v ∈ e, v ∈ W

theorem BKLOK2.edgesIn_subset {V : Type u_1} [DecidableEq V] (E : Finset (Sym2 V)) (S : Finset V) : edgesIn E S ⊆ E

def BKLOK2.codegTo {V : Type u_1} [DecidableEq V] (E : Finset (Sym2 V)) (x y : V) (W : Finset V) : ℕ

d_E({x,y}, W) = |N_E(x,W) ∩ N_E(y,W)|, the codegree of the pair x, y inside W.

Equations

• BKLOK2.codegTo E x y W = (BKLOK2.nbhdIn E x W ∩ BKLOK2.nbhdIn E y W).card

def BKLOK2.famEdges {V : Type u_1} [DecidableEq V] (P : Finset (Finset V)) : Finset (Sym2 V)

The edges of a triangle family.

Equations

• BKLOK2.famEdges P = P.biUnion BKLOK2.cliqueEdges

structure BKLOK2.IsMatchingAvoiding {V : Type u_1} (M : Finset (Finset V)) (x : V) : Prop

A Finset (Finset V) is a matching avoiding x: every member is a 2-element set, the members are pairwise disjoint, and none contains x.

• card_two (e : Finset V) : e ∈ M → e.card = 2
• pairwise_disjoint : (↑M).Pairwise Disjoint
• avoids (e : Finset V) : e ∈ M → x ∉ e

def BKLOK2.involutionMatching {V : Type u_1} [DecidableEq V] (S : Finset V) (f : V → V) : Finset (Finset V)

The matching induced by a partner function f on S: the orbit {a, f a} for each a ∈ S.

Equations

• BKLOK2.involutionMatching S f = Finset.image (fun (a : V) => {a, f a}) S

theorem BKLOK2.isMatchingAvoiding_involutionMatching {V : Type u_1} [DecidableEq V] {S : Finset V} {f : V → V} {x : V} (hmap : ∀ a ∈ S, f a ∈ S) (hinv : ∀ a ∈ S, f (f a) = a) (hne : ∀ a ∈ S, f a ≠ a) (hx : x ∉ S) : IsMatchingAvoiding (involutionMatching S f) x

A fixed-point-free involution on S gives a matching of S, avoiding any x ∉ S.

theorem BKLOK2.edgesIn_subset_cliqueEdges_loopless {V : Type u_1} [DecidableEq V] {H : Finset (Sym2 V)} (hloop : ∀ e ∈ H, ¬e.IsDiag) (S : Finset V) : edgesIn H S ⊆ cliqueEdges S

Every edge of H inside S is a clique edge of S, provided H is loopless.

theorem BKLOK2.degTo_le_edeg_edgesIn {V : Type u_1} [DecidableEq V] {H : Finset (Sym2 V)} {S : Finset V} {y : V} (hy : y ∈ S) : degTo H y S ≤ edeg (edgesIn H S) y

The degree of y ∈ S into S is at most its edge degree in H[S].

theorem BKLOK2.card_edgeNeighbors_eq_edeg {V : Type u_1} [DecidableEq V] {A : Finset (Sym2 V)} {N : Finset V} (hAsub : A ⊆ cliqueEdges N) (v : V) : ({z ∈ N | s(v, z) ∈ A}.erase v).card = edeg A v

On a loopless edge set supported on N, counting neighbours of v is the same as counting incident edges. This is the bridge from the BKLO finite-edge vocabulary to the generic spread matching interface.

structure BKLOK2.GoodMatching {V : Type u_1} [DecidableEq V] (H : Finset (Sym2 V)) (W : Finset V) (x : V) (M : Finset (Finset V)) : Prop

The data the greedy sweep produces at an apex x: a perfect matching of N_H(x,W) avoiding x, all of whose edges are edges of H inside N_H(x,W).

• matching : IsMatchingAvoiding M x
• subset (e : Finset V) : e ∈ M → e ⊆ nbhdIn H x W
• covers (a : V) : a ∈ nbhdIn H x W → ∃ e ∈ M, a ∈ e
• edges (e : Finset V) : e ∈ M → cliqueEdges e ⊆ edgesIn H (nbhdIn H x W)

theorem BKLOK2.edeg_le_edeg_sdiff_add_edeg {V : Type u_1} [DecidableEq V] (E F : Finset (Sym2 V)) (v : V) : edeg E v ≤ edeg (E \ F) v + edeg F v

theorem BKLOK2.edeg_sdiff_ge_of_slack {V : Type u_1} [DecidableEq V] {E D : Finset (Sym2 V)} {v : V} {h d : ℕ} (hE : h + d ≤ edeg E v) (hD : edeg D v ≤ d) : h ≤ edeg (E \ D) v

The slack absorbs the used edges. If every vertex has degree ≥ h + d in E (the h + d of Lemma 10.3(ii), h = |N|/2, d the slack) and the used set D has degree ≤ d at v, then the unused part E \ D still has degree ≥ h at v — the hypothesis Dirac needs.

Matchings from involutions

theorem BKLOK2.famEdges_involutionMatching_subset {V : Type u_1} [DecidableEq V] (N : Finset V) (f : V → V) : famEdges (involutionMatching N f) ⊆ Finset.image (fun (a : V) => s(a, f a)) N

The edges of the matching induced by a partner function are among the orbit edges.

theorem BKLOK2.matching_data_of_involution {V : Type u_1} [DecidableEq V] {N : Finset V} {x : V} (hx : x ∉ N) {A : Finset (Sym2 V)} {f : V → V} (hmap : ∀ a ∈ N, f a ∈ N) (hinv : ∀ a ∈ N, f (f a) = a) (hfne : ∀ a ∈ N, f a ≠ a) (hadj : ∀ a ∈ N, s(a, f a) ∈ A) : IsMatchingAvoiding (involutionMatching N f) x ∧ (∀ e ∈ involutionMatching N f, e ⊆ N) ∧ (∀ a ∈ N, ∃ e ∈ involutionMatching N f, a ∈ e) ∧ ∀ e ∈ involutionMatching N f, cliqueEdges e ⊆ A

A partner involution gives all the data of a GoodMatching. This is the second half of BKLO.exists_perfect_matching_in, with the involution supplied from outside.