Sparse-boundary cores from internal edge excess

If a vertex set carries more ordered internal adjacent pairs than twice its total degree excess above three, iterative deletion cannot remove every vertex while always deleting a vertex with at least three external neighbors. The surviving set has external degree at most two at every vertex.

@[instance_reducible]

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

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

Equations

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

theorem ACMax.neighbor_sdiff_card_add_le_degree {n : ℕ} (G : SimpleGraph (Fin n)) (S K : Finset (Fin n)) (v : Fin n) (hK : K ⊆ G.neighborFinset v ∩ S) : (G.neighborFinset v \ S).card + K.card ≤ G.degree v

A displayed set of internal neighbors subtracts from the number of edges leaving a vertex set.

noncomputable def ACMax.internalPairCount {n : ℕ} (G : SimpleGraph (Fin n)) (S : Finset (Fin n)) : ℕ

The number of ordered adjacent pairs contained in S.

Equations

• ACMax.internalPairCount G S = {p ∈ S ×ˢ S | G.Adj p.1 p.2}.card

theorem ACMax.internalPairCount_eq_sum {n : ℕ} (G : SimpleGraph (Fin n)) (S : Finset (Fin n)) : internalPairCount G S = ∑ v ∈ S, (G.neighborFinset v ∩ S).card

theorem ACMax.internalPairCount_eq_two_mul {n : ℕ} (G : SimpleGraph (Fin n)) (S : Finset (Fin n)) : ∃ (k : ℕ), internalPairCount G S = 2 * k

The ordered internal-pair count is even: each induced edge contributes its two orientations.

theorem ACMax.internalPairCount_erase {n : ℕ} (G : SimpleGraph (Fin n)) (S : Finset (Fin n)) {v : Fin n} (hv : v ∈ S) : internalPairCount G S = internalPairCount G (S.erase v) + 2 * (G.neighborFinset v ∩ S).card

Removing a vertex deletes twice its internal degree from the ordered-pair count.

theorem ACMax.twice_internal_degree_le_internalPairCount {n : ℕ} (G : SimpleGraph (Fin n)) (S : Finset (Fin n)) {v : Fin n} (hv : v ∈ S) : 2 * (G.neighborFinset v ∩ S).card ≤ internalPairCount G S

The internal degree of one vertex accounts for twice as many ordered internal incidences: once at each endpoint of every incident edge.

theorem ACMax.adj_of_internalPairCount_eq_two {n : ℕ} (G : SimpleGraph (Fin n)) (S : Finset (Fin n)) {u v : Fin n} (hu : u ∈ S) (hv : v ∈ S) (huv : u ≠ v) (huPos : 0 < (G.neighborFinset u ∩ S).card) (hvPos : 0 < (G.neighborFinset v ∩ S).card) (hpairs : internalPairCount G S = 2) : G.Adj u v

If an induced subgraph has exactly one edge, any two of its non-isolated vertices are the endpoints of that edge.

theorem ACMax.internal_degree_le_one_of_pairCount_eq_twice_at {n : ℕ} (G : SimpleGraph (Fin n)) (S : Finset (Fin n)) {u v : Fin n} (hu : u ∈ S) (hv : v ∈ S) (huv : u ≠ v) (hpairs : internalPairCount G S = 2 * (G.neighborFinset u ∩ S).card) : (G.neighborFinset v ∩ S).card ≤ 1

If every induced edge is incident with u, then every other vertex has internal degree at most one. The pair-count equality expresses precisely that the edges incident with u exhaust the induced subgraph.

theorem ACMax.exists_sparse_core_of_twice_excess_lt_pairs {n : ℕ} (G : SimpleGraph (Fin n)) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) (S : Finset (Fin n)) (hlarge : 2 * ∑ v ∈ S, (G.degree v - 3) < internalPairCount G S) : ∃ T ⊆ S, T.Nonempty ∧ ∀ v ∈ T, (G.neighborFinset v \ T).card ≤ 2

If the internal ordered-pair count is larger than twice the total degree excess, some nonempty subset has external degree at most two at every vertex.

theorem ACMax.algConn_le_two_of_sparse_core_clusters {n : ℕ} [Nonempty (Fin n)] (G : SimpleGraph (Fin n)) (S T : Finset (Fin n)) (hSne : S.Nonempty) (hTne : T.Nonempty) (hdisj : Disjoint S T) (hnc : ∀ u ∈ S, ∀ v ∈ T, ¬G.Adj u v) (hS : ∀ u ∈ S, (G.neighborFinset u \ S).card ≤ 2) (hT : ∀ v ∈ T, (G.neighborFinset v \ T).card ≤ 2) : algConn G ≤ 2

Two separated vertex sets certify algConn G <= 2 when every vertex has at most two neighbors outside its own set.

theorem ACMax.algConn_le_two_of_order15_cluster_sum (G : SimpleGraph (Fin 15)) (S : Finset (Fin 15)) (hSne : S.Nonempty) (hcard : S.card = 5 ∨ S.card = 6) (hsum : ∑ v ∈ S, (G.neighborFinset v \ S).card ≤ S.card + 1) : algConn G ≤ 2

On fifteen vertices, a set of size five or six whose edge boundary is at most one more than its order is a sparse cut.

theorem ACMax.algConn_le_two_of_order15_cluster (G : SimpleGraph (Fin 15)) (S : Finset (Fin 15)) (p : Fin 15) (hp : p ∈ S) (hcard : S.card = 5 ∨ S.card = 6) (hpout : (G.neighborFinset p \ S).card ≤ 2) (hother : ∀ v ∈ S, v ≠ p → (G.neighborFinset v \ S).card ≤ 1) : algConn G ≤ 2

Pointwise form of algConn_le_two_of_order15_cluster_sum: one distinguished vertex may send two edges out and every other cluster vertex may send one.