The hub-cross firing law and the big-clean-twin structure

The spectral closer for the hub–hub mediation channel of the m-bound, together with the rigidity of the twin population it controls.

Main results

• algConn_le_two_of_hub_cross_pair — the hub-cross firing law: two non-adjacent degree-3 vertices u ≠ v with no common neighbour, partners all of degree ≤ 4 (hub degrees D, D' ≥ 4 unbounded), and whose only possible N(u)–N(v) edge is the hub–hub edge g ~ g', force algConn G ≤ 2. It strictly extends the cross-free usable far-pair law: instantiating the weighted double-star master with au = av = 1, hub weights s = 1/(D−1) and a balance-shifted partner weight makes the hub leak-identity (1−s)² + (D−2)s² = 1 − s yield worst-case slack −(s+s') (the hub–hub cross is spectrally cheap).
• usable_twin_partners_deg_le_four — σ-rigidity: a usable degree-3 twin of a degree-≥ 9 hub has both other partners of degree ≤ 4 (σ(9) + σ(5) + σ(4) > 2). So the firing law applies to every cross-cloud twin pair mediated only by a hub–hub edge.
• bigCleanTwins and its structure lemmas bigCleanTwins_nbr_deg (neighbours have degree 4 or ≥ 9), bigCleanTwins_unique_big (exactly one big neighbour, two degree-4 partners), sum_big_inc_le, sum_small_inc_le — the bipartite incidence counts feeding the hub-cross coverage argument.

theorem ACMax.usable_twin_partners_deg_le_four {V : Type u_1} [Fintype V] (G : SimpleGraph V) (t g w w' : V) (ht3 : G.degree t = 3) (htg : G.Adj t g) (htw : G.Adj t w) (htw' : G.Adj t w') (hgw : w ≠ g) (hgw' : w' ≠ g) (hww' : w ≠ w') (hD : 9 ≤ G.degree g) (husable : sigS G t ≤ 2) (hw4 : 4 ≤ G.degree w) (hw'4 : 4 ≤ G.degree w') : G.degree w ≤ 4 ∧ G.degree w' ≤ 4

σ-rigidity of big-hub twins. A usable degree-3 vertex t (sigS ≤ 2) adjacent to a hub g of degree ≥ 9 has both partners of degree ≤ 4, provided neither partner is degree-3 (i.e. off the M-cluster): σ(9) + σ(5) + σ(4) = 6/7 + 2/3 + 1/2 = 85/42 > 2.

theorem ACMax.algConn_le_two_of_hub_cross_pair {V : Type u_1} [Fintype V] [Nonempty V] (G : SimpleGraph V) (u v g g' : V) (hu3 : G.degree u = 3) (hv3 : G.degree v = 3) (hne : u ≠ v) (huv : ¬G.Adj u v) (hcap : ∀ (w : V), ¬(G.Adj u w ∧ G.Adj v w)) (hgu : G.Adj u g) (hg'v : G.Adj v g') (hD : 4 ≤ G.degree g) (hD' : 4 ≤ G.degree g') (hpart : ∀ (w : V), G.Adj u w → w ≠ g → G.degree w ≤ 4) (hpart' : ∀ (w : V), G.Adj v w → w ≠ g' → G.degree w ≤ 4) (hcross : ∀ (w w' : V), G.Adj u w → G.Adj v w' → G.Adj w w' → w = g ∧ w' = g') : algConn G ≤ 2

The hub-cross firing law. u ≠ v degree-3, non-adjacent, no common neighbour; g ∈ N(u), g' ∈ N(v) hubs of degree ≥ 4 (unbounded above); all other neighbours (partners) of u and of v have degree ≤ 4; and every N(u)–N(v) edge is the hub–hub edge (g, g'). Then algConn G ≤ 2 — the single hub–hub cross is spectrally cheap and cannot block the double-star certificate. Weights: au = av = 1, hub weights 1/(deg−1), u-partners ½, v-partners ½ + (s−s')/2; worst-case quadratic slack = −(s+s') (edge present) resp. −(s+s')−2ss' (absent).

Big clean twins

The big clean twins bigCleanTwins G = {u : deg u = 3 ∧ sigS u ≤ 2 ∧ (∃ x ~ u, deg x ≥ 9) ∧ (∀ x ~ u, deg x ≠ 3)} are the usable degree-3 vertices with a big neighbour and no degree-3 neighbour. By σ-rigidity their neighbourhoods are completely determined (bigCleanTwins_nbr_deg, bigCleanTwins_unique_big), and the bipartite incidence counts sum_big_inc_le / sum_small_inc_le feed the hub-cross pair-coverage count.

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

The big clean twins: usable degree-3 vertices with a degree-≥ 9 neighbour and no degree-3 neighbour.

Equations

• ACMax.bigCleanTwins G = {u : Fin n | G.degree u = 3 ∧ ACMax.sigS G u ≤ 2 ∧ (∃ x ∈ G.neighborFinset u, 9 ≤ G.degree x) ∧ ∀ x ∈ G.neighborFinset u, G.degree x ≠ 3}

theorem ACMax.mem_bigCleanTwins {n : ℕ} {G : SimpleGraph (Fin n)} {u : Fin n} : u ∈ bigCleanTwins G ↔ G.degree u = 3 ∧ sigS G u ≤ 2 ∧ (∃ x ∈ G.neighborFinset u, 9 ≤ G.degree x) ∧ ∀ x ∈ G.neighborFinset u, G.degree x ≠ 3

theorem ACMax.bigCleanTwins_nbr_deg {n : ℕ} (G : SimpleGraph (Fin n)) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) {u : Fin n} (hu : u ∈ bigCleanTwins G) {x : Fin n} (hx : x ∈ G.neighborFinset u) : G.degree x = 4 ∨ 9 ≤ G.degree x

Neighbourhood rigidity. Every neighbour of a big clean twin has degree 4 or degree ≥ 9.

theorem ACMax.bigCleanTwins_unique_big {n : ℕ} (G : SimpleGraph (Fin n)) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) {u : Fin n} (hu : u ∈ bigCleanTwins G) : ∃ g ∈ G.neighborFinset u, 9 ≤ G.degree g ∧ ∀ x ∈ G.neighborFinset u, x ≠ g → G.degree x = 4

Unique big neighbour. A big clean twin has exactly one big neighbour: there is a big neighbour g, and every other neighbour has degree ≤ 4.

theorem ACMax.sum_nbr_inter_comm {n : ℕ} (G : SimpleGraph (Fin n)) (s t : Finset (Fin n)) : ∑ w ∈ s, (G.neighborFinset w ∩ t).card = ∑ u ∈ t, (G.neighborFinset u ∩ s).card

Bipartite incidence exchange (indicator double count): Σ_{w ∈ s} |N(w) ∩ t| = Σ_{u ∈ t} |N(u) ∩ s|.

theorem ACMax.sum_big_inc_le {n : ℕ} (G : SimpleGraph (Fin n)) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) : ∑ w : Fin n with 9 ≤ G.degree w, (G.neighborFinset w ∩ bigCleanTwins G).card ≤ (bigCleanTwins G).card

Big-incidence exchange. The incidences between big vertices and big clean twins number at most |bigCleanTwins| — each twin has exactly one big neighbour.

theorem ACMax.sum_small_inc_le {n : ℕ} (G : SimpleGraph (Fin n)) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) : ∑ w : Fin n with G.degree w ≤ 8, (G.neighborFinset w ∩ bigCleanTwins G).card ≤ 2 * (bigCleanTwins G).card

Small-incidence exchange. The incidences between degree-≤ 8 vertices and big clean twins number at most 2·|bigCleanTwins| — each twin has exactly two degree-4 partners.

theorem ACMax.deg3_with_deg3_nbr_card_le_two {n : ℕ} (G : SimpleGraph (Fin n)) (huniq : ∀ (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₄}) : {u : Fin n | G.degree u = 3 ∧ ∃ x ∈ G.neighborFinset u, G.degree x = 3}.card ≤ 2

The M-population under the dichotomy: at most 2 degree-3 vertices have a degree-3 neighbour.