LeanPool.AsymptoticTrianglePacking.Internal — hypergraph foundations and the handshake identity

Standalone, Mathlib-only. Destined for a Mathlib PR. Foundation for the Rödl-nibble project. A r-uniform hypergraph on a vertex type V is modelled as a Finset (Finset V) all of whose edges have cardinality r.

Goals of this module:

• A1 — definitions: degree, codegree, IsMatching.
• A2 — the handshake identity ∑_v degree v = r * H.card and the codegree double-count.

Everything here must be placeholder-free and axiom-clean [propext, Classical.choice, Quot.sound].

def Hypergraph.degree {V : Type u_1} [DecidableEq V] (H : Finset (Finset V)) (v : V) : ℕ

The degree of a vertex v in a hypergraph H: the number of edges containing v.

Equations

• Hypergraph.degree H v = {e ∈ H | v ∈ e}.card

def Hypergraph.codegree {V : Type u_1} [DecidableEq V] (H : Finset (Finset V)) (x y : V) : ℕ

The codegree of a pair x y: the number of edges containing both.

Equations

• Hypergraph.codegree H x y = {e ∈ H | x ∈ e ∧ y ∈ e}.card

def Hypergraph.IsUniform {V : Type u_1} (H : Finset (Finset V)) (r : ℕ) : Prop

H is r-uniform: every edge has exactly r vertices.

Equations

• Hypergraph.IsUniform H r = ∀ e ∈ H, e.card = r

structure Hypergraph.IsMatching {V : Type u_1} (H M : Finset (Finset V)) : Prop

A matching M in H: a subfamily of pairwise-disjoint edges.

• subset : M ⊆ H
• disjoint (e : Finset V) : e ∈ M → ∀ f ∈ M, e ≠ f → Disjoint e f

theorem Hypergraph.sum_degree {V : Type u_1} [DecidableEq V] [Fintype V] (H : Finset (Finset V)) {r : ℕ} (hr : IsUniform H r) : ∑ v : V, degree H v = r * H.card

A2 — handshake identity. For an r-uniform hypergraph, ∑_v degree v = r * |H|. Proof idea: double count the set of incidences {(v, e) : v ∈ e ∈ H}; summing over v gives ∑ degree, while summing over e gives ∑_{e} |e| = r|H|.

theorem Hypergraph.sum_codegree {V : Type u_1} [DecidableEq V] [Fintype V] (H : Finset (Finset V)) {r : ℕ} (hr : IsUniform H r) : ∑ x : V, ∑ y : V, codegree H x y = r * r * H.card

A2' — codegree double-count. ∑_v (degree H v).choose 2 = ∑ over unordered pairs … stated here in the convenient ordered form: the number of (edge, ordered pair-in-edge) incidences equals ∑_e |e|*(|e|-1) = r*(r-1)*|H| for an r-uniform hypergraph.