Edge-based triangle hypergraph

def Nibble.YusterE.triangleHypergraphE {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : Finset (Finset (Finset V))

The edge-based triangle hypergraph: ground set = edges of G (as 2-subsets), hyperedges = the three edges of each triangle. Its matchings are the edge-disjoint triangle packings (ν₃).

Equations

• Nibble.YusterE.triangleHypergraphE G = Finset.image (fun (t : Finset V) => Finset.powersetCard 2 t) (G.cliqueFinset 3)

theorem Nibble.YusterE.triangleHypergraphE_uniform {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : Hypergraph.IsUniform (triangleHypergraphE G) 3

The edge-based triangle hypergraph is 3-uniform (every triangle has exactly three edges).

theorem Nibble.YusterE.triangleHypergraphE_codegree_le_one {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {e e' : Finset V} (hne : e ≠ e') : Hypergraph.codegree (triangleHypergraphE G) e e' ≤ 1

Y2 (edge-based) — codegree ≤ 1. Two distinct edges lie in at most one common triangle (they determine its three vertices), so the edge-based triangle hypergraph has codegree ≤ 1. This is the CodegreeBounded H (μd) input the nibble wants — here in its sharpest form.

theorem Nibble.YusterE.mem_iff_mem_powersetCard_two {V : Type u_1} {u : Finset V} (hu : 2 ≤ u.card) (x : V) : x ∈ u ↔ ∃ e ∈ Finset.powersetCard 2 u, x ∈ e

Membership in a set of card ≥ 2 is witnessed by a 2-subset.

theorem Nibble.YusterE.powersetCard_two_inj {V : Type u_1} {s t : Finset V} (hs : 2 ≤ s.card) (ht : 2 ≤ t.card) (h : Finset.powersetCard 2 s = Finset.powersetCard 2 t) : s = t

Faithful representation. The triangle→edges map t ↦ t.powersetCard 2 is injective on sets of card ≥ 2; hence distinct triangles give distinct hyperedges, and matchings of triangleHypergraphE correspond to edge-disjoint triangle packings.

theorem Nibble.YusterE.triangleHypergraphE_degree {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (e : Finset V) : Hypergraph.degree (triangleHypergraphE G) e = {t ∈ G.cliqueFinset 3 | e ∈ Finset.powersetCard 2 t}.card

Y3-edge — degree = number of triangles through the edge. The degree of a vertex e (an edge) in the edge-based triangle hypergraph equals the number of triangles of G having e among their three edges. Szemerédi regularity makes these counts (nearly) uniform — the near-regularity input to the nibble.

noncomputable def Nibble.YusterE.nu3 {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : ℕ

Y4 — the integral triangle-packing number ν₃(G): the maximum size of a matching of the edge-based triangle hypergraph, i.e. the maximum number of edge-disjoint triangles.

Equations

• Nibble.YusterE.nu3 G = {M ∈ (Nibble.YusterE.triangleHypergraphE G).powerset | Hypergraph.IsMatching (Nibble.YusterE.triangleHypergraphE G) M}.sup Finset.card

theorem Nibble.YusterE.nu3_ge {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {M : Finset (Finset (Finset V))} (hM : Hypergraph.IsMatching (triangleHypergraphE G) M) : M.card ≤ nu3 G

Y4 — the nibble output lower-bounds ν₃. Any matching of the triangle hypergraph witnesses a lower bound on ν₃. NibbleTheorem produces a large matching, hence a large ν₃.

def Nibble.YusterE.IsFracPacking {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (w : Finset (Finset V) → ℝ) : Prop

A fractional triangle packing: nonnegative weights on the triangle hyperedges with total weight through every edge ≤ 1 (Paper III §2.2).

Equations

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

noncomputable def Nibble.YusterE.nu3star {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : ℝ

Y4 — the fractional triangle-packing number ν₃*(G).

Equations

• Nibble.YusterE.nu3star G = sSup {x : ℝ | ∃ (w : Finset (Finset V) → ℝ), Nibble.YusterE.IsFracPacking G w ∧ x = ∑ T ∈ Nibble.YusterE.triangleHypergraphE G, w T}

theorem Nibble.YusterE.nu3star_bddAbove {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : BddAbove {x : ℝ | ∃ (w : Finset (Finset V) → ℝ), IsFracPacking G w ∧ x = ∑ T ∈ triangleHypergraphE G, w T}

The fractional-packing value set is bounded above by |H| (each weight is ≤ 1).

theorem Nibble.YusterE.nu3_le_nu3star {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : ↑(nu3 G) ≤ nu3star G

Y4 — weak duality ν₃ ≤ ν₃*. The indicator of a maximum matching is a fractional packing of value ν₃, so ν₃ ≤ ν₃*.