CoreGapRemoval

Counting the deleted edges

theorem Nibble.AX1.card_clique2_sdiff_le {V : Type} [Fintype V] [DecidableEq V] (G G' : SimpleGraph V) [DecidableRel G.Adj] [DecidableRel G'.Adj] (hle : G' ≤ G) : ↑(G.cliqueFinset 2 \ G'.cliqueFinset 2).card ≤ ↑G.edgeFinset.card - ↑G'.edgeFinset.card

The 2-cliques lost when passing to a subgraph are at most the edges lost: the endpoint map Sym2 V → Finset V sends the deleted edges onto the deleted 2-cliques.

theorem Nibble.AX1.nu3star_eq_zero_of_cliqueFree {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (h : G.CliqueFree 3) : YusterE.nu3star G ≤ 0

A triangle-free graph has fractional triangle packing number 0.

The removal branch

theorem Nibble.AX1.nu3star_le_of_few_triangles {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {ε : ℝ} (hfew : ↑(G.cliqueFinset 3).card < SimpleGraph.triangleRemovalBound ε * ↑(Fintype.card V) ^ 3) : YusterE.nu3star G ≤ ε * ↑(Fintype.card V) ^ 2

The removal branch. A graph with fewer than triangleRemovalBound(ε)·|V|³ triangles has ν₃* ≤ ε|V|².

Mathlib's triangle removal lemma produces a triangle-free spanning subgraph G' obtained by deleting fewer than ε|V|² edges. Since G' has no triangle, every triangle of G contains a deleted edge, so the entire fractional packing is carried by the deleted edges, each of load at most 1.

theorem Nibble.AX1.gap_le_of_few_triangles (ε : ℝ) (hε : 0 < ε) : ∃ (κ : ℝ), 0 < κ ∧ ∀ (V : Type) [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj], ↑(G.cliqueFinset 3).card < κ * ↑(Fintype.card V) ^ 3 → YusterE.nu3star G - ↑(YusterE.nu3 G) ≤ ε * ↑(Fintype.card V) ^ 2

The removal branch, as a packing-gap bound. For every ε > 0 there is κ > 0 such that every graph with fewer than κ|V|³ triangles has packing gap at most ε|V|².

The residual, restricted to triangle-rich graphs

def Nibble.AX1.CoreGapAtRich (ε δ κ : ℝ) : Prop

The core packing-gap statement at parameters (ε, δ), for triangle-rich graphs. As Nibble.AX1.CoreGapAt ε δ, but only for graphs with at least κ|V|³ triangles.

Equations

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

def Nibble.AX1.CoreGapRichResidual : Prop

The residual restricted to triangle-rich graphs, at the removal-lemma threshold.

Equations

• Nibble.AX1.CoreGapRichResidual = ∀ (ε : ℝ), 0 < ε → ∀ (δ : ℝ), 0 < δ → Nibble.AX1.CoreGapAtRich ε δ (SimpleGraph.triangleRemovalBound ε)

theorem Nibble.AX1.CoreGapAtRich.mono_kappa {ε δ κ κ' : ℝ} (h : CoreGapAtRich ε δ κ) (hκ : κ ≤ κ') : CoreGapAtRich ε δ κ'

Lowering the richness threshold strengthens the statement.

theorem Nibble.AX1.coreGapResidual_of_rich (h : CoreGapRichResidual) : CoreGapResidual

The reduction. The full core residual follows from its triangle-rich restriction: the triangle-poor instances are discharged outright by the removal branch.

theorem Nibble.AX1.rich_of_coreGapResidual (h : CoreGapResidual) : CoreGapRichResidual

The converse. The restricted residual is a weakening of the full one, so the two are equivalent: no strength has been smuggled in.

theorem Nibble.AX1.ax1_of_coreGapRichResidual (h : CoreGapRichResidual) : AX1Statement

AX1 from the triangle-rich residual.

WeightedNibble

theorem Nibble.exists_maximum_packing {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : ∃ (M : Finset (Finset (Finset V))), Hypergraph.IsMatching (YusterE.triangleHypergraphE G) M ∧ M.card = YusterE.nu3 G

The maximum in the definition of ν₃ is attained: there is a triangle packing of size exactly ν₃ G.

theorem Nibble.exists_mem_of_maximum_packing {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {M : Finset (Finset (Finset V))} (hM : Hypergraph.IsMatching (YusterE.triangleHypergraphE G) M) (hcard : M.card = YusterE.nu3 G) {T : Finset (Finset V)} (hT : T ∈ YusterE.triangleHypergraphE G) : ∃ e ∈ M.biUnion id, e ∈ T

Every triangle of G shares an edge with a maximum packing: otherwise it could be added.

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

ν₃* ≤ 3·ν₃. The 3ν₃ edges covered by a maximum triangle packing form a triangle cover, and the total weight of any fractional packing is at most the number of edges in a cover.

theorem Nibble.edge_card_le_half_card_sq {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : ↑(G.cliqueFinset 2).card ≤ ↑(Fintype.card V) ^ 2 / 2

|E(G)| ≤ |V|²/2, sharpening Nibble.YusterE.edge_card_le_card_sq.

theorem Nibble.nu3star_sub_nu3_le_ninth {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : YusterE.nu3star G - ↑(YusterE.nu3 G) ≤ ↑(Fintype.card V) ^ 2 / 9

An unconditional n²/9 bound on the packing gap. Since a maximum packing covers a set of 3ν₃ edges meeting every triangle, ν₃* ≤ 3ν₃, so the gap is at most ⅔ν₃*; and ν₃* ≤ |E|/3 ≤ |V|²/6.

theorem Nibble.AX1.coreGapAt_of_ninth {ε δ : ℝ} (hε : 1 / 9 ≤ ε) : CoreGapAt ε δ

CoreGapAt ε δ for every ε ≥ 1/9, unconditionally — a genuine extension of the previously proved range ε ≥ 1/3 (Nibble.AX1.coreGapAt_of_third).

The degree of the edge-based triangle hypergraph

theorem Nibble.triangleHypergraphE_degree_le_card {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (e : Finset V) : ↑(Hypergraph.degree (YusterE.triangleHypergraphE G) e) ≤ ↑(Fintype.card V)

The triangle hypergraph has maximum degree at most |V|: a triangle through a fixed edge e is insert v e for one of the |V| vertices v.

theorem Nibble.nu3star_nonneg {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : 0 ≤ YusterE.nu3star G

ν₃* ≥ 0.

A proved instance of the weighted nibble: the near-regular case

theorem Nibble.fracMatching_sum_le {W : Type} [Fintype W] [DecidableEq W] {H : Finset (Finset W)} {r : ℕ} (hr : Hypergraph.IsUniform H r) {w : Finset W → ℝ} (hcon : ∀ (v : W), ∑ T ∈ H with v ∈ T, w T ≤ 1) : ↑r * ∑ T ∈ H, w T ≤ ↑(Fintype.card W)

Every fractional matching of an r-uniform hypergraph has total weight at most |W|/r.

theorem Nibble.fracNibble_nearlyRegular (r : ℕ) (hr : 2 ≤ r) (β : ℝ) (hβ : 0 < β) : ∃ (μ : ℝ), 0 < μ ∧ ∃ (η : ℝ), 0 < η ∧ ∃ (d₀ : ℝ), 0 < d₀ ∧ ∀ {W : Type} [inst : Fintype W] [inst_1 : DecidableEq W] (H : Finset (Finset W)) (w : Finset W → ℝ) (d : ℝ), 0 < d → d₀ ≤ d → Hypergraph.IsUniform H r → Hypergraph.NearlyRegularMost H d μ η → Hypergraph.CodegreeBounded H (μ * d) → (∀ (x : W), ↑(Hypergraph.degree H x) ≤ (1 + μ) * d) → (∀ (T : Finset W), 0 ≤ w T) → (∀ (v : W), ∑ T ∈ H with v ∈ T, w T ≤ 1) → ∃ (M : Finset (Finset W)), Hypergraph.IsMatching H M ∧ (1 - β) * ∑ T ∈ H, w T ≤ ↑M.card

The weighted nibble holds for nearly regular hypergraphs, as an immediate consequence of the proved regular nibble Nibble.nibbleTheoremMostCeil_holds: the matching it produces already covers all but a β-fraction of the ground set, and every fractional matching has total weight at most |W|/r. This conclusion relies on the stated near-regularity hypotheses.

CoreGapNearComplete

Edge counting

theorem Nibble.AX1.card_clique2_le_card_edgeFinset {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : ↑(G.cliqueFinset 2).card ≤ ↑G.edgeFinset.card

The number of 2-cliques is at most the number of edges.

theorem Nibble.AX1.card_lowDeg_mul_le {V : Type} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (t : ℝ) : ↑{v : V | ↑(G.degree v) < t}.card * (↑(Fintype.card V) - t) ≤ ↑(Fintype.card V) ^ 2 - 2 * ↑G.edgeFinset.card

Few vertices of low degree in an edge-rich graph. With L the set of vertices of degree below t, one has |L|·(|V| − t) ≤ |V|² − 2|E|.

The deletion at a set of vertices

theorem Nibble.AX1.card_deleted_restrictAway_le {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (L : Finset V) : ↑(G.cliqueFinset 2 \ (restrictAway G L).cliqueFinset 2).card ≤ ↑L.card * ↑(Fintype.card V)

Deleting all edges at the vertices of L destroys at most |L|·|V| edges.

theorem Nibble.AX1.degree_restrictAway_ge {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {L : Finset V} {x : V} (hx : x ∉ L) : ↑(G.degree x) - ↑L.card ≤ ↑((restrictAway G L).degree x)

Deleting the edges at L lowers each degree outside L by at most |L|.

The near-complete branch

theorem Nibble.AX1.gap_le_of_near_complete (ε : ℝ) (hε : 0 < ε) : ∃ (η : ℝ), 0 < η ∧ ∃ (n₀ : ℕ), ∀ (V : Type) [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj], n₀ ≤ Fintype.card V → (1 / 2 - η) * ↑(Fintype.card V) ^ 2 ≤ ↑(G.cliqueFinset 2).card → YusterE.nu3star G - ↑(YusterE.nu3 G) ≤ ε * ↑(Fintype.card V) ^ 2

The near-complete branch. For every ε > 0 there is η > 0 such that every large graph with at least (1/2 − η)|V|² edges has packing gap at most ε|V|².

A universal constant below 1/9

theorem Nibble.AX1.exists_gap_const_lt_ninth : ∃ (c : ℝ), 0 < c ∧ c < 1 / 9 ∧ ∃ (n₀ : ℕ), ∀ (V : Type) [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj], n₀ ≤ Fintype.card V → YusterE.nu3star G - ↑(YusterE.nu3 G) ≤ c * ↑(Fintype.card V) ^ 2

A universal packing-gap constant below 1/9. There is c < 1/9 with ν₃* − ν₃ ≤ c|V|² for every large graph: near-complete graphs are handled by Nibble.AX1.gap_le_of_near_complete, all others by ν₃* ≤ |E|/3 together with ν₃* ≤ 3ν₃.

theorem Nibble.AX1.coreGapAt_of_lt_ninth : ∃ (c : ℝ), 0 < c ∧ c < 1 / 9 ∧ ∀ (ε δ : ℝ), c ≤ ε → CoreGapAt ε δ

CoreGapAt ε δ for every δ and every ε above a constant c < 1/9, strictly improving Nibble.AX1.coreGapAt_of_ninth.

CoreGapRegularDegrees

def Nibble.AX1.edgeTriangleDegree {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (e : Finset V) : ℕ

The triangle degree of an edge: the number of triangles of G containing it.

Equations

• Nibble.AX1.edgeTriangleDegree G e = {t ∈ G.cliqueFinset 3 | e ⊆ t}.card

theorem Nibble.AX1.edgeTriangleDegree_eq {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (E : YusterE.EdgeV G) : Hypergraph.degree (YusterE.triangleHypergraphSub G) E = edgeTriangleDegree G ↑E

The triangle degree of an edge is its degree in the edge-based triangle hypergraph.

theorem Nibble.AX1.gap_le_of_regular_triangle_degrees (ε : ℝ) (hε : 0 < ε) : ∃ (μ : ℝ), 0 < μ ∧ ∃ (η : ℝ), 0 < η ∧ ∃ (d₀ : ℝ), 0 < d₀ ∧ ∀ (V : Type) [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj] (d : ℝ) (Exc : Finset (Finset V)), d₀ ≤ d → ↑Exc.card ≤ η * ↑(G.cliqueFinset 2).card → (∀ e ∈ G.cliqueFinset 2, ↑(edgeTriangleDegree G e) ≤ (1 + μ) * d) → (∀ e ∈ G.cliqueFinset 2, e ∉ Exc → (1 - μ) * d ≤ ↑(edgeTriangleDegree G e)) → YusterE.nu3star G - ↑(YusterE.nu3 G) ≤ ε * ↑(Fintype.card V) ^ 2

The near-regular branch. For every ε > 0 there are μ, η > 0 and d₀ > 0 such that any graph whose edges all have triangle degree at most (1+μ)d, and at least (1−μ)d outside an exceptional set of at most η|E| edges, for some d ≥ d₀, has packing gap at most ε|V|².

The triangle hypergraph is 3-uniform with codegree at most 1 ≤ μd, so these hypotheses are exactly the input of the unconditional nibble Nibble.nibbleTheoremMostCeil_holds; the resulting matching covers all but a 3ε-fraction of the edges, which is the packing-gap accounting Nibble.AX1.gap_le_of_sub_matching.

theorem Nibble.AX1.gap_le_of_regular_triangle_degrees' (ε : ℝ) (hε : 0 < ε) : ∃ (μ : ℝ), 0 < μ ∧ ∃ (d₀ : ℝ), 0 < d₀ ∧ ∀ (V : Type) [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj] (d : ℝ), d₀ ≤ d → (∀ e ∈ G.cliqueFinset 2, (1 - μ) * d ≤ ↑(edgeTriangleDegree G e) ∧ ↑(edgeTriangleDegree G e) ≤ (1 + μ) * d) → YusterE.nu3star G - ↑(YusterE.nu3 G) ≤ ε * ↑(Fintype.card V) ^ 2

The near-regular branch, no exceptional edges.

theorem Nibble.AX1.gap_le_of_regular_triangle_degrees_core (ε : ℝ) (hε : 0 < ε) : ∃ (μ : ℝ), 0 < μ ∧ ∃ (η : ℝ), 0 < η ∧ ∃ (d₀ : ℝ), 0 < d₀ ∧ ∀ (V : Type) [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj] (G' : SimpleGraph V) (x : DecidableRel G'.Adj) (d : ℝ) (Exc : Finset (Finset V)), G' ≤ G → ↑(G.cliqueFinset 2 \ G'.cliqueFinset 2).card ≤ ε / 2 * ↑(Fintype.card V) ^ 2 → d₀ ≤ d → ↑Exc.card ≤ η * ↑(G'.cliqueFinset 2).card → (∀ e ∈ G'.cliqueFinset 2, ↑(edgeTriangleDegree G' e) ≤ (1 + μ) * d) → (∀ e ∈ G'.cliqueFinset 2, e ∉ Exc → (1 - μ) * d ≤ ↑(edgeTriangleDegree G' e)) → YusterE.nu3star G - ↑(YusterE.nu3 G) ≤ ε * ↑(Fintype.card V) ^ 2

The near-regular branch, up to a small deletion. If a graph becomes near-regular in its triangle degrees after deleting at most (ε/2)|V|² edges, its packing gap is at most ε|V|²: deleting k edges moves ν₃* by at most k and can only decrease ν₃ (Nibble.AX1.gap_le_core_gap).

This is to Nibble.AX1.gap_le_of_regular_triangle_degrees what Nibble.AX1.nibbleGap_of_dense_core is to the dense branch.

The complementary branch: uniformly small triangle degrees

theorem Nibble.AX1.gap_le_of_small_triangle_degrees (ε : ℝ) (hε : 0 < ε) : ∃ (ρ : ℝ), 0 < ρ ∧ ∀ (V : Type) [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj], (∀ e ∈ G.cliqueFinset 2, ↑(edgeTriangleDegree G e) ≤ ρ * ↑(Fintype.card V)) → YusterE.nu3star G - ↑(YusterE.nu3 G) ≤ ε * ↑(Fintype.card V) ^ 2

The small-degree branch. For every ε > 0 there is ρ > 0 such that a graph all of whose edges lie in at most ρ|V| triangles has packing gap at most ε|V|².

The handshake identity ∑_e t(e) = 3·#triangles turns the degree bound into #triangles ≤ ρ|V|³/6, which is the removal branch Nibble.AX1.nu3star_le_of_few_triangles. Together with Nibble.AX1.gap_le_of_regular_triangle_degrees this leaves only the graphs whose triangle degrees are simultaneously large somewhere and far from regular.

Deleting the heavy edges

def Nibble.AX1.deleteHeavy {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (c : ℝ) : SimpleGraph V

G with every edge of triangle degree above c deleted.

Equations

• Nibble.AX1.deleteHeavy G c = { Adj := fun (x y : V) => G.Adj x y ∧ ↑(Nibble.AX1.edgeTriangleDegree G {x, y}) ≤ c, symm := ⋯, loopless := ⋯ }

@[instance_reducible]

noncomputable instance Nibble.AX1.instDecidableRelDeleteHeavy {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (c : ℝ) : DecidableRel (deleteHeavy G c).Adj

Equations

• Nibble.AX1.instDecidableRelDeleteHeavy G c x y = { decide := decide (G.Adj x y) && decide (↑(Nibble.AX1.edgeTriangleDegree G {x, y}) ≤ c), reflects_decide := ⋯ }

theorem Nibble.AX1.deleteHeavy_adj {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (c : ℝ) (x y : V) : (deleteHeavy G c).Adj x y ↔ G.Adj x y ∧ ↑(edgeTriangleDegree G {x, y}) ≤ c

theorem Nibble.AX1.deleteHeavy_le {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (c : ℝ) : deleteHeavy G c ≤ G

theorem Nibble.AX1.deleted_subset_heavy {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (c : ℝ) : G.cliqueFinset 2 \ (deleteHeavy G c).cliqueFinset 2 ⊆ {e ∈ G.cliqueFinset 2 | c < ↑(edgeTriangleDegree G e)}

The 2-cliques deleted by Nibble.AX1.deleteHeavy are exactly heavy edges.

theorem Nibble.AX1.edgeTriangleDegree_mono {V : Type} [Fintype V] [DecidableEq V] (G G' : SimpleGraph V) [DecidableRel G.Adj] [DecidableRel G'.Adj] (hle : G' ≤ G) (e : Finset V) : edgeTriangleDegree G' e ≤ edgeTriangleDegree G e

Triangle degrees only decrease when passing to a subgraph.

theorem Nibble.AX1.gap_le_of_few_heavy_edges (ε : ℝ) (hε : 0 < ε) : ∃ (ρ : ℝ), 0 < ρ ∧ ∀ (V : Type) [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj], ↑{e ∈ G.cliqueFinset 2 | ρ * ↑(Fintype.card V) < ↑(edgeTriangleDegree G e)}.card ≤ ε / 2 * ↑(Fintype.card V) ^ 2 → YusterE.nu3star G - ↑(YusterE.nu3 G) ≤ ε * ↑(Fintype.card V) ^ 2

The few-heavy-edges branch. For every ε > 0 there is ρ > 0 such that if the edges lying in more than ρ|V| triangles number at most (ε/2)|V|², then the packing gap is at most ε|V|²: delete them (which costs at most that many edges of the gap) and apply Nibble.AX1.gap_le_of_small_triangle_degrees to what is left.

So the only graphs left open are those with at least (ε/2)|V|² edges each lying in more than ρ|V| triangles.

CoreGapRegularDecomp

Colour classes of an edge colouring

def Nibble.AX1.edgeSelect {V : Type} [DecidableEq V] (G : SimpleGraph V) (P : Finset V → Prop) : SimpleGraph V

The spanning subgraph of G consisting of the edges e with P e.

Equations

• Nibble.AX1.edgeSelect G P = { Adj := fun (x y : V) => G.Adj x y ∧ P {x, y}, symm := ⋯, loopless := ⋯ }

@[instance_reducible]

noncomputable instance Nibble.AX1.instDecidableRelEdgeSelect {V : Type} [DecidableEq V] (G : SimpleGraph V) (P : Finset V → Prop) : DecidableRel (edgeSelect G P).Adj

Equations

• Nibble.AX1.instDecidableRelEdgeSelect G P x✝¹ x✝ = Classical.dec ((Nibble.AX1.edgeSelect G P).Adj x✝¹ x✝)

theorem Nibble.AX1.edgeSelect_adj {V : Type} [DecidableEq V] (G : SimpleGraph V) (P : Finset V → Prop) (x y : V) : (edgeSelect G P).Adj x y ↔ G.Adj x y ∧ P {x, y}

theorem Nibble.AX1.edgeSelect_le {V : Type} [DecidableEq V] (G : SimpleGraph V) (P : Finset V → Prop) : edgeSelect G P ≤ G

noncomputable def Nibble.AX1.colorPart {V : Type} [DecidableEq V] (G : SimpleGraph V) (col : Finset V → ℕ) (i : ℕ) : SimpleGraph V

The i-th colour class of the edge colouring col.

Equations

• Nibble.AX1.colorPart G col i = Nibble.AX1.edgeSelect G fun (e : Finset V) => col e = i

@[instance_reducible]

noncomputable instance Nibble.AX1.instDecidableRelColorPart {V : Type} [DecidableEq V] (G : SimpleGraph V) (col : Finset V → ℕ) (i : ℕ) : DecidableRel (colorPart G col i).Adj

Equations

• Nibble.AX1.instDecidableRelColorPart G col i = Nibble.AX1.instDecidableRelEdgeSelect G fun (e : Finset V) => col e = i

theorem Nibble.AX1.colorPart_le {V : Type} [DecidableEq V] (G : SimpleGraph V) (col : Finset V → ℕ) (i : ℕ) : colorPart G col i ≤ G

theorem Nibble.AX1.colorPart_hyperedge_color {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) (col : Finset V → ℕ) (i : ℕ) {T : Finset (Finset V)} (hT : T ∈ YusterE.triangleHypergraphE (colorPart G col i)) (e : Finset V) : e ∈ T → col e = i

Every edge of a triangle of the i-th colour class has colour i.

theorem Nibble.AX1.triangleHypergraphE_nonempty_of_mem {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {T : Finset (Finset V)} (hT : T ∈ YusterE.triangleHypergraphE G) : T.Nonempty

Hyperedges of a triangle hypergraph are nonempty.

theorem Nibble.AX1.nu3_sum_colorParts_le {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (col : Finset V → ℕ) (k : ℕ) : ∑ i ∈ Finset.range k, YusterE.nu3 (colorPart G col i) ≤ YusterE.nu3 G

Superadditivity of ν₃ over the colour classes of an edge colouring. The colour classes are edge-disjoint, so maximum packings of the classes unite to a packing of G.

The nibble, as a lower bound on ν₃

theorem Nibble.AX1.nu3_ge_of_regular_triangle_degrees (β : ℝ) (hβ : 0 < β) : ∃ (μ : ℝ), 0 < μ ∧ ∃ (η : ℝ), 0 < η ∧ ∃ (d₀ : ℝ), 0 < d₀ ∧ ∀ (V : Type) [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj] (d : ℝ) (Exc : Finset (Finset V)), d₀ ≤ d → ↑Exc.card ≤ η * ↑(G.cliqueFinset 2).card → (∀ e ∈ G.cliqueFinset 2, ↑(edgeTriangleDegree G e) ≤ (1 + μ) * d) → (∀ e ∈ G.cliqueFinset 2, e ∉ Exc → (1 - μ) * d ≤ ↑(edgeTriangleDegree G e)) → (1 - β) * (↑(G.cliqueFinset 2).card / 3) ≤ ↑(YusterE.nu3 G)

The nibble as an integral packing bound. For every β > 0 there are μ, η > 0 and d₀ such that a graph with near-regular triangle degrees at a scale d ≥ d₀ has ν₃ ≥ (1−β)|E|/3.

The structural residual

def Nibble.AX1.RegularDecompAt (ε μ η d₀ : ℝ) : Prop

A near-regular decomposition at parameters (ε, μ, η, d₀). Every large graph carries an edge colouring whose colour classes have near-regular triangle degrees — each at its own scale d i ≥ d₀, with the lower bound allowed to fail on at most an η-fraction of that class's edges — and whose total edge count is at least 3ν₃*(G) − 3ε|V|².

Equations

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

def Nibble.AX1.RegularDecompResidual : Prop

The structural residual: a near-regular decomposition at every window of parameters.

Equations

• Nibble.AX1.RegularDecompResidual = ∀ (ε : ℝ), 0 < ε → ∀ (μ : ℝ), 0 < μ → ∀ (η : ℝ), 0 < η → ∀ (d₀ : ℝ), 0 < d₀ → Nibble.AX1.RegularDecompAt ε μ η d₀

theorem Nibble.AX1.coreGapResidual_of_regularDecomp (h : RegularDecompResidual) : CoreGapResidual

The reduction. A near-regular decomposition of every large graph implies the AX1 core residual: the nibble packs each colour class up to a (1−β)-fraction of its edges (Nibble.AX1.nu3_ge_of_regular_triangle_degrees), the classes are edge-disjoint so the packings unite (Nibble.AX1.nu3_sum_colorParts_le), and the decomposition's edge count recovers ν₃*.

theorem Nibble.AX1.ax1_of_regularDecomp (h : RegularDecompResidual) : AX1Statement

AX1 from the structural residual.

The residual is satisfiable: the one-colour witness

theorem Nibble.AX1.colorPart_const {V : Type} [DecidableEq V] (G : SimpleGraph V) : colorPart G (fun (x : Finset V) => 0) 0 = G

Colouring every edge 0 leaves the graph unchanged.

theorem Nibble.AX1.regularDecomp_witness_of_regular {V : Type} [Fintype V] [DecidableEq V] (ε μ η d₀ : ℝ) (hε : 0 ≤ ε) (G : SimpleGraph V) [DecidableRel G.Adj] (d : ℝ) (Exc : Finset (Finset V)) (hd : d₀ ≤ d) (hExc : ↑Exc.card ≤ η * ↑(G.cliqueFinset 2).card) (hhi : ∀ e ∈ G.cliqueFinset 2, ↑(edgeTriangleDegree G e) ≤ (1 + μ) * d) (hlo : ∀ e ∈ G.cliqueFinset 2, e ∉ Exc → (1 - μ) * d ≤ ↑(edgeTriangleDegree G e)) : ∃ (k : ℕ) (col : Finset V → ℕ) (dd : ℕ → ℝ), (∀ i < k, d₀ ≤ dd i) ∧ (∀ i < k, ∀ e ∈ (colorPart G col i).cliqueFinset 2, ↑(edgeTriangleDegree (colorPart G col i) e) ≤ (1 + μ) * dd i) ∧ (∀ i < k, ∃ (Exc' : Finset (Finset V)), ↑Exc'.card ≤ η * ↑((colorPart G col i).cliqueFinset 2).card ∧ ∀ e ∈ (colorPart G col i).cliqueFinset 2, e ∉ Exc' → (1 - μ) * dd i ≤ ↑(edgeTriangleDegree (colorPart G col i) e)) ∧ YusterE.nu3star G ≤ ∑ i ∈ Finset.range k, ↑((colorPart G col i).cliqueFinset 2).card / 3 + ε * ↑(Fintype.card V) ^ 2

The one-colour witness. A graph whose own triangle degrees are near-regular at a scale d ≥ d₀ satisfies the requirement of Nibble.AX1.RegularDecompAt with the trivial one-colour decomposition. So the structural residual is exactly the assertion that every large graph can be edge-coloured into near-regular classes without losing more than ε|V|² of the fractional optimum: it is a genuine statement about colourings, non-vacuous and satisfied by the regular graphs.

CoreGapRegularFamily

Edge-disjoint families and the colouring they induce

def Nibble.AX1.EdgeDisjointFamily {V : Type} (H : ℕ → SimpleGraph V) (k : ℕ) : Prop

The first k members of the family H are pairwise edge-disjoint.

Equations

• Nibble.AX1.EdgeDisjointFamily H k = ∀ i < k, ∀ j < k, i ≠ j → ∀ (x y : V), (H i).Adj x y → ¬(H j).Adj x y

theorem Nibble.AX1.pair_mem_cliqueFinset_two {V : Type} [Fintype V] [DecidableEq V] (H : SimpleGraph V) [DecidableRel H.Adj] {x y : V} (hxy : x ≠ y) : {x, y} ∈ H.cliqueFinset 2 ↔ H.Adj x y

A pair {x, y} of distinct vertices is a 2-clique of H iff x and y are adjacent.

theorem Nibble.AX1.cliqueFinset_congr_graph {V : Type} [Fintype V] [DecidableEq V] {G₁ G₂ : SimpleGraph V} [DecidableRel G₁.Adj] [DecidableRel G₂.Adj] (h : G₁ = G₂) (n : ℕ) : G₁.cliqueFinset n = G₂.cliqueFinset n

The 2-cliques of two equal graphs agree, whatever the decidability instances.

theorem Nibble.AX1.edgeTriangleDegree_congr_graph {V : Type} [Fintype V] [DecidableEq V] {G₁ G₂ : SimpleGraph V} [DecidableRel G₁.Adj] [DecidableRel G₂.Adj] (h : G₁ = G₂) (e : Finset V) : edgeTriangleDegree G₁ e = edgeTriangleDegree G₂ e

Triangle degrees of two equal graphs agree, whatever the decidability instances.

noncomputable def Nibble.AX1.familyColoring {V : Type} [Fintype V] [DecidableEq V] (H : ℕ → SimpleGraph V) (k : ℕ) (e : Finset V) : ℕ

The edge colouring induced by an edge-disjoint family: an edge gets the index of the member of the family containing it, and the junk colour k if there is none.

Equations

• Nibble.AX1.familyColoring H k e = if h : ∃ i < k, e ∈ (H i).cliqueFinset 2 then Nat.find h else k

theorem Nibble.AX1.colorPart_familyColoring {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) (H : ℕ → SimpleGraph V) (k : ℕ) (hle : ∀ i < k, H i ≤ G) (hdisj : EdgeDisjointFamily H k) {i : ℕ} (hi : i < k) : colorPart G (familyColoring H k) i = H i

The colour classes of Nibble.AX1.familyColoring are exactly the members of the family.

The family form of the structural residual

def Nibble.AX1.HasNearRegularFamily {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (ε μ η d₀ : ℝ) : Prop

A near-regular family for G at parameters (ε, μ, η, d₀): pairwise edge-disjoint subgraphs H 0, …, H (k−1) of G, each with near-regular triangle degrees at its own scale d i ≥ d₀ (the lower bound being allowed to fail on at most an η-fraction of that member's edges), whose total edge count is at least 3ν₃*(G) − 3ε|V|².

Equations

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

theorem Nibble.AX1.HasNearRegularFamily.mono_eps {V : Type} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {ε ε' μ η d₀ : ℝ} (h : HasNearRegularFamily G ε μ η d₀) (hεε' : ε ≤ ε') : HasNearRegularFamily G ε' μ η d₀

Weakening the accuracy of a near-regular family.

theorem Nibble.AX1.HasNearRegularFamily.mono_of_le {V : Type} [Fintype V] [DecidableEq V] {G G' : SimpleGraph V} [DecidableRel G.Adj] [DecidableRel G'.Adj] {ε c μ η d₀ : ℝ} (hle : G' ≤ G) (hgap : YusterE.nu3star G ≤ YusterE.nu3star G' + c * ↑(Fintype.card V) ^ 2) (h : HasNearRegularFamily G' ε μ η d₀) : HasNearRegularFamily G (ε + c) μ η d₀

A family for a spanning subgraph is a family for the graph. If G' ≤ G and the fractional optimum drops by at most c|V|² when passing to G', a near-regular family for G' is one for G at accuracy ε + c.

theorem Nibble.AX1.hasNearRegularFamily_of_few_triangles {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {ε μ η d₀ : ℝ} (hfew : ↑(G.cliqueFinset 3).card < SimpleGraph.triangleRemovalBound ε * ↑(Fintype.card V) ^ 3) : HasNearRegularFamily G ε μ η d₀

The triangle-poor branch. A graph with fewer than triangleRemovalBound(ε)·|V|³ triangles has ν₃* ≤ ε|V|², so the empty family is already a near-regular family.

From families to colourings

theorem Nibble.AX1.regularDecomp_data_of_family {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {ε μ η d₀ : ℝ} (h : HasNearRegularFamily G ε μ η d₀) : ∃ (k : ℕ) (col : Finset V → ℕ) (d : ℕ → ℝ), (∀ i < k, d₀ ≤ d i) ∧ (∀ i < k, ∀ e ∈ (colorPart G col i).cliqueFinset 2, ↑(edgeTriangleDegree (colorPart G col i) e) ≤ (1 + μ) * d i) ∧ (∀ i < k, ∃ (Exc : Finset (Finset V)), ↑Exc.card ≤ η * ↑((colorPart G col i).cliqueFinset 2).card ∧ ∀ e ∈ (colorPart G col i).cliqueFinset 2, e ∉ Exc → (1 - μ) * d i ≤ ↑(edgeTriangleDegree (colorPart G col i) e)) ∧ YusterE.nu3star G ≤ ∑ i ∈ Finset.range k, ↑((colorPart G col i).cliqueFinset 2).card / 3 + ε * ↑(Fintype.card V) ^ 2

A near-regular family gives the data required by Nibble.AX1.RegularDecompAt.

theorem Nibble.AX1.regularDecompAt_of_family {ε μ η d₀ : ℝ} (h : ∃ (n₀ : ℕ), ∀ (V : Type) [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj], n₀ ≤ Fintype.card V → HasNearRegularFamily G ε μ η d₀) : RegularDecompAt ε μ η d₀

The reduction to the family form. If every large graph has a near-regular family, then the structural residual Nibble.AX1.RegularDecompAt holds.

theorem Nibble.AX1.hasNearRegularFamily_of_regularDecomp {ε μ η d₀ : ℝ} (h : RegularDecompAt ε μ η d₀) : ∃ (n₀ : ℕ), ∀ (V : Type) [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj], n₀ ≤ Fintype.card V → HasNearRegularFamily G ε μ η d₀

The converse. A colour decomposition is an edge-disjoint family, so the family form is equivalent to Nibble.AX1.RegularDecompAt: nothing has been smuggled in.

Cleaning: passing to the regularity-reduced graph

theorem Nibble.AX1.hasNearRegularFamily_of_reduced {V : Type} [Fintype V] [DecidableEq V] [Nonempty V] (G : SimpleGraph V) [DecidableRel G.Adj] {ε ε₁ μ η d₀ : ℝ} (hε₁ : 0 < ε₁) (P : Finpartition Finset.univ) (hP : P.IsEquipartition) (hPl : 4 / ε₁ ≤ ↑P.parts.card) (hPu : P.IsUniform G (ε₁ / 8)) (h : HasNearRegularFamily (SimpleGraph.regularityReduced P G (ε₁ / 8) (ε₁ / 4)) ε μ η d₀) : HasNearRegularFamily G (ε + ε₁) μ η d₀

The cleaning step. Mathlib's SimpleGraph.regularityReduced keeps only the edges lying in an ε₁/8-uniform pair of parts of density at least ε₁/4; for a uniform equipartition with enough parts it discards fewer than ε₁|V|² edges (SimpleGraph.regularityReduced_edges_card_aux), and deleting m edges costs the fractional optimum at most m (Nibble.AX1.nu3star_le_add_deleted). So a near-regular family for the reduced graph is one for G, at accuracy ε + ε₁.

The reduced residual

def Nibble.AX1.ReducedFamilyAt (ε μ η d₀ ε₁ : ℝ) : Prop

The reduced residual at parameters (ε, μ, η, d₀) and regularity scale ε₁: every regularity-reduced graph — the subgraph of a large graph G consisting of the edges inside the ε₁/8-uniform pairs of density at least ε₁/4 of an ε₁/8-uniform equipartition P with a bounded number of parts — which is triangle-rich carries a near-regular family recovering 3ν₃* up to 3ε|V|².

This is what remains of Nibble.AX1.RegularDecompResidual after Szemerédi regularity and the triangle removal lemma have been applied: all pairs of parts carrying edges are uniform and dense, so the missing mathematics is the Haxell–Rödl splitting of each uniform pair among the cluster triples together with the sparsification making the triangle degrees of each triple concentrate at a common scale.

Equations

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

def Nibble.AX1.ReducedFamilyResidual : Prop

The reduced residual: at every window of parameters, for some regularity scale ε₁ as small as one likes. The scale is existentially quantified — the cleaning loss it causes is paid for out of the accuracy ε — so a proof is free to run the regularity lemma as finely as it needs.

Equations

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

theorem Nibble.AX1.regularDecompResidual_of_reducedFamily (h : ReducedFamilyResidual) : RegularDecompResidual

The reduction of the structural residual to the reduced one. Given ε, apply Szemerédi's regularity lemma at the scale ε₁ ≤ ε/2 supplied by the residual; the reduced graph is either triangle-poor — and then the empty family already works, by the triangle removal lemma — or triangle-rich, and then the reduced residual applies. Cleaning costs at most ε₁|V|² ≤ (ε/2)|V|² of the fractional optimum.

theorem Nibble.AX1.reducedFamilyResidual_of_regularDecompResidual (h : RegularDecompResidual) : ReducedFamilyResidual

The converse. The reduced residual is a weakening of Nibble.AX1.RegularDecompResidual (reduced graphs are graphs), so by Nibble.AX1.regularDecompResidual_of_reducedFamily the two are equivalent: the passage to regularity-reduced graphs smuggles in no strength.

theorem Nibble.AX1.ax1_of_reducedFamily (h : ReducedFamilyResidual) : AX1Statement

AX1 from the reduced residual.