Decorated four-cycle cuts at order fifteen

Two compact sparse-cut certificates used by the endpoint shared-star census. The four-cycle itself misses the order-15 cut inequality by one edge; adjoining one parent, or two adjacent parents, supplies exactly the missing slack.

@[instance_reducible]

noncomputable def ACMax.decoratedCycleFinDecidableEq {n : ℕ} : DecidableEq (Fin n)

Use the same finite-set decisions as the classical graph certificates.

Equations

• ACMax.decoratedCycleFinDecidableEq = Classical.decEq (Fin n)

theorem ACMax.decorated_c4_same_parent_fires (G : SimpleGraph (Fin 15)) (p x y b₁ b₂ : Fin 15) (hS : {p, x, y, b₁, b₂}.card = 5) (hxy : {x, y}.card = 2) (hpbb : {p, b₁, b₂}.card = 3) (hdp : G.degree p ≤ 4) (hdx : G.degree x ≤ 4) (hdy : G.degree y ≤ 4) (hdb1 : G.degree b₁ ≤ 3) (hdb2 : G.degree b₂ ≤ 3) (hpx : G.Adj p x) (hpy : G.Adj p y) (hxb1 : G.Adj x b₁) (hxb2 : G.Adj x b₂) (hyb1 : G.Adj y b₁) (hyb2 : G.Adj y b₂) : algConn G ≤ 2

A K_{2,2} whose degree-at-most-four vertices share a degree-at-most-four parent gives a five-vertex order-15 sparse cut.

theorem ACMax.decorated_c4_adjacent_parents_fires (G : SimpleGraph (Fin 15)) (p q x y b₁ b₂ : Fin 15) (hS : {p, q, x, y, b₁, b₂}.card = 6) (hqx : {q, x}.card = 2) (hpy : {p, y}.card = 2) (hpbb : {p, b₁, b₂}.card = 3) (hqbb : {q, b₁, b₂}.card = 3) (hxy : {x, y}.card = 2) (hdp : G.degree p ≤ 4) (hdq : G.degree q ≤ 3) (hdx : G.degree x ≤ 4) (hdy : G.degree y ≤ 4) (hdb1 : G.degree b₁ ≤ 3) (hdb2 : G.degree b₂ ≤ 3) (hpq : G.Adj p q) (hpx : G.Adj p x) (hqy : G.Adj q y) (hxb1 : G.Adj x b₁) (hxb2 : G.Adj x b₂) (hyb1 : G.Adj y b₁) (hyb2 : G.Adj y b₂) : algConn G ≤ 2

A K_{2,2} whose two degree-at-most-four vertices have adjacent parents of degrees at most four and three gives a six-vertex order-15 sparse cut.

theorem ACMax.order14_sparse_triangle_fires (G : SimpleGraph (Fin 14)) (x y z : Fin 14) (hxy : G.Adj x y) (hyz : G.Adj y z) (hxz : G.Adj x z) (hdeg : G.degree x + G.degree y + G.degree z ≤ 10) : algConn G ≤ 2

At order fourteen, a triangle whose degree sum is at most ten is a weighted-cut certificate.