The quotient (class-vector) master certificate

The opening move of the quotient program for the mid-range 19 ≤ n ≤ 598 693: by Haemers interlacing, for any partition of the vertex set into m classes, λ₂(G) is at most the second eigenvalue of the m×m quotient matrix — and for the second eigenvalue specifically, the quotient bound is witnessed by a class-constant test vector, so it follows from the universal single-vector certificate. The value of the packaging is that the Rayleigh data reduces to aggregate quantities: class sizes and inter-class edge counts, exactly what the campaign's counting machinery produces.

• classSize c i — the size of class i;

• interEdges G c i j — the number of ordered adjacent pairs (u,v) with u in class i and v in class j (interEdges i j = interEdges j i; the diagonal counts internal edges twice but is killed by (x i − x i)² = 0);

• algConn_le_two_of_class_vector — the master: a class-valued vector x with Σᵢ nᵢ xᵢ = 0 and

  Σᵢⱼ Eᵢⱼ (xᵢ − xⱼ)² ≤ 4·Σᵢ nᵢ xᵢ²

  certifies algConn G ≤ 2 (the 4 is 2 × 2: one factor because ordered pairs double-count edges, one from the target λ₂ ≤ 2);

• algConn_le_two_of_sparse_cut — the classical Fiedler cut bound as the m = 2 instance: n·e(S, Sᶜ) ≤ 2·|S|·|Sᶜ| certifies algConn ≤ 2 (stated with the ordered cross count: n·E ≤ 4·|S|·|Sᶜ|);

• degree-class handshake identities on the residual cell, expressing the quotient data of the degree partition {3}/{4}/{≥5} in ledger terms.

Quotient data

noncomputable def ACMax.classSize {V : Type u_1} [Fintype V] {m : ℕ} (c : V → Fin m) (i : Fin m) : ℕ

The size of class i under the class map c.

Equations

• ACMax.classSize c i = {v : V | c v = i}.card

noncomputable def ACMax.interEdges {V : Type u_1} [Fintype V] {m : ℕ} (G : SimpleGraph V) (c : V → Fin m) (i j : Fin m) : ℕ

The number of ordered adjacent pairs from class i to class j.

Equations

• ACMax.interEdges G c i j = {p ∈ {v : V | c v = i} ×ˢ {v : V | c v = j} | G.Adj p.1 p.2}.card

theorem ACMax.sum_classes {V : Type u_1} [Fintype V] {m : ℕ} {M : Type u_2} [AddCommMonoid M] (c : V → Fin m) (f : V → M) : ∑ v : V, f v = ∑ i : Fin m, ∑ v : V with c v = i, f v

Fiberwise decomposition of a vertex sum by classes.

theorem ACMax.sum_sq_classes {V : Type u_1} [Fintype V] {m : ℕ} (c : V → Fin m) (x : Fin m → ℝ) : ∑ v : V, x (c v) ^ 2 = ∑ i : Fin m, ↑(classSize c i) * x i ^ 2

A class-constant square sum aggregates to class sizes.

theorem ACMax.interEdges_eq_sum {V : Type u_1} [Fintype V] {m : ℕ} (G : SimpleGraph V) (c : V → Fin m) (i j : Fin m) : ↑(interEdges G c i j) = ∑ u : V with c u = i, ∑ v : V with c v = j, if G.Adj u v then 1 else 0

The inter-class count as a double indicator sum over the fibers.

theorem ACMax.sum_edge_sq_classes {V : Type u_1} [Fintype V] {m : ℕ} (G : SimpleGraph V) (c : V → Fin m) (x : Fin m → ℝ) : (∑ u : V, ∑ v : V, if G.Adj u v then (x (c u) - x (c v)) ^ 2 else 0) = ∑ i : Fin m, ∑ j : Fin m, ↑(interEdges G c i j) * (x i - x j) ^ 2

The edge quadratic form aggregates to inter-class counts.

The master certificate

theorem ACMax.algConn_le_two_of_class_vector {V : Type u_1} [Fintype V] [Nonempty V] (G : SimpleGraph V) {m : ℕ} (c : V → Fin m) (x : Fin m → ℝ) (hbal : ∑ i : Fin m, ↑(classSize c i) * x i = 0) (hne : ∃ (v : V), x (c v) ≠ 0) (hQ : ∑ i : Fin m, ∑ j : Fin m, ↑(interEdges G c i j) * (x i - x j) ^ 2 ≤ 4 * ∑ i : Fin m, ↑(classSize c i) * x i ^ 2) : algConn G ≤ 2

The quotient master certificate (Haemers interlacing for λ₂). Given a partition into m classes and a class-valued vector x with

• balance: Σᵢ nᵢ·xᵢ = 0,
• some class of nonzero value is inhabited, and
• the aggregate Rayleigh bound Σᵢⱼ Eᵢⱼ·(xᵢ − xⱼ)² ≤ 4·Σᵢ nᵢ·xᵢ² (Eᵢⱼ the ordered inter-class adjacency counts),

we get algConn G ≤ 2. All data is aggregate: sizes and edge counts.

The classical sparse-cut instance (m = 2)

theorem ACMax.algConn_le_two_of_sparse_cut {V : Type u_1} [Fintype V] [Nonempty V] (G : SimpleGraph V) (S : Finset V) (hS : S.Nonempty) (hSc : Sᶜ.Nonempty) (hcut : Fintype.card V * {p ∈ S ×ˢ Sᶜ | G.Adj p.1 p.2}.card ≤ 2 * S.card * Sᶜ.card) : algConn G ≤ 2

The Fiedler sparse-cut bound. For a nonempty proper S ⊆ V with cut count e(S,Sᶜ) (each cross edge counted once, as a pair in S ×ˢ Sᶜ) satisfying the classical n·e(S,Sᶜ) ≤ 2·|S|·|Sᶜ|, we get algConn ≤ 2.

Handshake identities for the quotient data

theorem ACMax.interEdges_symm {V : Type u_1} [Fintype V] {m : ℕ} (G : SimpleGraph V) (c : V → Fin m) (i j : Fin m) : interEdges G c i j = interEdges G c j i

Inter-class counts are symmetric.

The two-cluster law (m = 3)

theorem ACMax.algConn_le_two_of_two_clusters {V : Type u_1} [Fintype V] [Nonempty V] (G : SimpleGraph V) (S₁ S₂ : Finset V) (hS₁ : S₁.Nonempty) (hS₂ : S₂.Nonempty) (hdisj : Disjoint S₁ S₂) (hnc : ∀ u ∈ S₁, ∀ v ∈ S₂, ¬G.Adj u v) (hcut : {p ∈ S₁ ×ˢ (S₁ ∪ S₂)ᶜ | G.Adj p.1 p.2}.card * S₂.card ^ 2 + {p ∈ S₂ ×ˢ (S₁ ∪ S₂)ᶜ | G.Adj p.1 p.2}.card * S₁.card ^ 2 ≤ 2 * S₁.card * S₂.card * (S₁.card + S₂.card)) : algConn G ≤ 2

The two-cluster law. Two disjoint nonempty vertex sets with no edges between them and boundaries ∂₁, ∂₂ (ordered counts of edges leaving each cluster) satisfying

∂₁·|S₂|² + ∂₂·|S₁|² ≤ 2·|S₁|·|S₂|·(|S₁| + |S₂|)

certify algConn ≤ 2. For equal sizes s this reads ∂₁ + ∂₂ ≤ 4s — e.g. two disjoint M-edges with no cross edges fire at the exact tie (∂ = 4 each, s = 2), recovering the cell's 2K₂ exclusion.

The degree-class partition on the residual cell

The two-hub block cut (the endgame seed)

theorem ACMax.algConn_le_two_of_hub_block {V : Type u_1} [Fintype V] [Nonempty V] (G : SimpleGraph V) (g : V) (K : Finset V) (hgK : g ∉ K) (hK : ∀ t ∈ K, G.Adj g t) (hK3 : ∀ t ∈ K, G.degree t = 3) (hSc : (insert g K)ᶜ.Nonempty) (hcut : Fintype.card V * (G.degree g + K.card) ≤ 2 * (K.card + 1) * (insert g K)ᶜ.card) : algConn G ≤ 2

The single-hub block cut. A hub g with k degree-3 twins forms a block {g} ∪ K of size k+1 whose boundary is at most d_g + k (the hub leaks its non-twin degree d−k; each twin leaks its two non-g neighbours). Under n·(d_g + k) ≤ 2·(k+1)·(n−k−1) — asymptotically d_g ≤ k + 2, the capped-class condition as an exact tie — the block fires algConn ≤ 2.

theorem ACMax.algConn_le_two_of_hub_block' {V : Type u_1} [Fintype V] [Nonempty V] (G : SimpleGraph V) (g : V) (K : Finset V) (hgK : g ∉ K) (hK : ∀ t ∈ K, G.Adj g t) (hK3 : ∀ t ∈ K, G.degree t = 3) (hn : K.card + 1 < Fintype.card V) (hcut : Fintype.card V * (G.degree g + K.card) ≤ 2 * (K.card + 1) * (Fintype.card V - (K.card + 1))) : algConn G ≤ 2

Instance-free form of the single-hub block cut: the statement mentions only cardinalities, so it applies verbatim from any DecidableEq context.

theorem ACMax.algConn_le_two_of_double_star {V : Type u_1} [Fintype V] [Nonempty V] (G : SimpleGraph V) (g₁ g₂ : V) (K₁ K₂ : Finset V) (hg₁K₁ : g₁ ∉ K₁) (hg₂K₂ : g₂ ∉ K₂) (hK₁a : ∀ t ∈ K₁, G.Adj g₁ t) (hK₁3 : ∀ t ∈ K₁, G.degree t = 3) (hK₂a : ∀ t ∈ K₂, G.Adj g₂ t) (hK₂3 : ∀ t ∈ K₂, G.degree t = 3) (hdisj : Disjoint (insert g₁ K₁) (insert g₂ K₂)) (hnc : ∀ u ∈ insert g₁ K₁, ∀ v ∈ insert g₂ K₂, ¬G.Adj u v) (hcond : (G.degree g₁ + K₁.card) * (K₂.card + 1) ^ 2 + (G.degree g₂ + K₂.card) * (K₁.card + 1) ^ 2 ≤ 2 * (K₁.card + 1) * (K₂.card + 1) * (K₁.card + K₂.card + 2)) : algConn G ≤ 2

The double-star cut (the v66 tie-breaker). Two non-adjacent hubs with disjoint, mutually non-adjacent twin blocks {gᵢ} ∪ Kᵢ fire the two-cluster law under the exact condition

(d₁+k₁)(k₂+1)² + (d₂+k₂)(k₁+1)² ≤ 2(k₁+1)(k₂+1)(k₁+k₂+2)

— equivalently (ε₁−2)(k₂+1)² + (ε₂−2)(k₁+1)² ≤ 0 for εᵢ = dᵢ − kᵢ, which holds for EVERY DS-unblocked intDeg-pattern once k₁ ≥ k₂. No largeness of n is required.

theorem ACMax.algConn_le_two_of_double_star' {V : Type u_1} [Fintype V] [Nonempty V] (G : SimpleGraph V) (g₁ g₂ : V) (K₁ K₂ : Finset V) (hg₁K₁ : g₁ ∉ K₁) (hg₂K₂ : g₂ ∉ K₂) (hK₁a : ∀ t ∈ K₁, G.Adj g₁ t) (hK₁3 : ∀ t ∈ K₁, G.degree t = 3) (hK₂a : ∀ t ∈ K₂, G.Adj g₂ t) (hK₂3 : ∀ t ∈ K₂, G.degree t = 3) (hne : g₁ ≠ g₂) (hg₁K₂ : g₁ ∉ K₂) (hg₂K₁ : g₂ ∉ K₁) (hKdisj : Disjoint K₁ K₂) (hgg : ¬G.Adj g₁ g₂) (hgt₂ : ∀ t ∈ K₂, ¬G.Adj g₁ t) (hgt₁ : ∀ t ∈ K₁, ¬G.Adj g₂ t) (htt : ∀ t₁ ∈ K₁, ∀ t₂ ∈ K₂, ¬G.Adj t₁ t₂) (hcond : (G.degree g₁ + K₁.card) * (K₂.card + 1) ^ 2 + (G.degree g₂ + K₂.card) * (K₁.card + 1) ^ 2 ≤ 2 * (K₁.card + 1) * (K₂.card + 1) * (K₁.card + K₂.card + 2)) : algConn G ≤ 2

Pointwise form of the double-star cut: all hypotheses are adjacency statements and cardinalities, so it applies verbatim from any DecidableEq context.

theorem ACMax.cherry_centre_fires (n : ℕ) [Nonempty (Fin n)] (hn : 18 ≤ n) (G : SimpleGraph (Fin n)) (y x z : Fin n) (hxz : x ≠ z) (hyx : G.Adj y x) (hyz : G.Adj y z) (hy3 : G.degree y = 3) (hx3 : G.degree x = 3) (hz3 : G.degree z = 3) : algConn G ≤ 2

The cherry-centre fire (the per-n CaseCherry machinery, lifted): a degree-3 vertex with two degree-3 neighbours fires the block cut at every n ≥ 18 — the centre plus its two twins form a {y} ∪ K-block of boundary 5 against 2·3·(n−3)/n. The M-cherry dispatch branches of the per-n proofs are instances of this statement.

theorem ACMax.two_medges_fire (n : ℕ) [Nonempty (Fin n)] (hn : 18 ≤ n) (G : SimpleGraph (Fin n)) (t₁ t₂ t₃ t₄ : Fin n) (h12ne : t₁ ≠ t₂) (h13ne : t₁ ≠ t₃) (h14ne : t₁ ≠ t₄) (h23ne : t₂ ≠ t₃) (h24ne : t₂ ≠ t₄) (h34ne : t₃ ≠ t₄) (h12 : G.Adj t₁ t₂) (h34 : G.Adj t₃ t₄) (h1 : G.degree t₁ = 3) (h2 : G.degree t₂ = 3) (h3 : G.degree t₃ = 3) (h4 : G.degree t₄ = 3) : algConn G ≤ 2

The two-M-edge fire (the hmin branch, lifted): two disjoint degree-3 edges fire at every n ≥ 18 — any cross adjacency creates a cherry centre, and otherwise the four vertices induce a 2K₂ of degree sum 12. On the cell, more than one M-edge is fatal at every size.

theorem ACMax.medges_or_single (n : ℕ) [Nonempty (Fin n)] (hn : 18 ≤ n) (G : SimpleGraph (Fin n)) : algConn G ≤ 2 ∨ ∀ (t₁ t₂ t₃ t₄ : Fin n), G.Adj t₁ t₂ → G.Adj t₃ t₄ → G.degree t₁ = 3 → G.degree t₂ = 3 → G.degree t₃ = 3 → G.degree t₄ = 3 → {t₁, t₂} = {t₃, t₄}

The M-dichotomy (the counting cascade's re-armer): at every n ≥ 18, either the graph fires or all M-edges coincide — two sharing edges make a cherry centre, two disjoint ones a 2K₂-or-cherry.