Far-pair and apex double-star test-vector certificates

Two reusable spectral certificates that bound the algebraic connectivity of a graph above by 2 from an explicit test vector. They are the workhorses for killing configurations built around a pair of low-degree vertices u, v in the general ACMAX argument.

Main results

• algConn_le_two_of_weighted_double_star — the weighted double-star master certificate. For non-adjacent u ≠ v with disjoint neighbourhoods and nonnegative weight data (au on u, p on N(u), av on v, q on N(v)), the five-valued test vector x = au·𝟙_u + p·𝟙_{N(u)} − av·𝟙_v − q·𝟙_{N(v)} witnesses algConn G ≤ 2 whenever the worst-case quadratic bound Σ (au − p w)² + Σ (av − q w)² + Σ_{cross} (p w + q w')² + Σ leak·p² + Σ leak·q² ≤ 2·(au² + Σ p² + av² + Σ q²) holds (an edge inside N(u) costs at most its two leak-slot charges since the weights are nonnegative).
• algConn_le_two_of_apex_double_star — the same certificate extended to pairs sharing exactly one common neighbour g (the apex, weight 0); the two apex edges u–g, v–g cost au² + av².
• algConn_le_two_of_apex_twin_pair — the apex tie law: two degree-3 vertices sharing a single hub g, with all non-apex partners of degree ≤ 4 and no partner–partner cross edges, force algConn G ≤ 2. With au = av = 1, p = q ≡ ½ the quadratic bound holds with equality (1 + 1 + 4·¼ + 4·(3·¼) = 6 = 2·(1 + ½ + 1 + ½)), so the hypotheses trace out the exact tie boundary.

All three are direct instances of algConn_le_two_of_testvector; no new spectral machinery is introduced.

The weighted double-star master certificate

theorem ACMax.algConn_le_two_of_weighted_double_star {V : Type u_1} [Fintype V] [Nonempty V] (G : SimpleGraph V) (u v : V) (au av : ℝ) (p q : V → ℝ) (hne : u ≠ v) (huv : ¬G.Adj u v) (hcap : ∀ (w : V), ¬(G.Adj u w ∧ G.Adj v w)) (hau : 0 < au) (hp : ∀ w ∈ G.neighborFinset u, 0 ≤ p w) (hq : ∀ w ∈ G.neighborFinset v, 0 ≤ q w) (hbal : au + ∑ w ∈ G.neighborFinset u, p w = av + ∑ w ∈ G.neighborFinset v, q w) (hQ : (∑ w ∈ G.neighborFinset u, (au - p w) ^ 2 + ∑ w ∈ G.neighborFinset v, (av - q w) ^ 2 + ∑ w ∈ G.neighborFinset u, ∑ w' ∈ G.neighborFinset v, if G.Adj w w' then (p w + q w') ^ 2 else 0) + ∑ w ∈ G.neighborFinset u, ↑(G.neighborFinset w \ insert u (G.neighborFinset v)).card * p w ^ 2 + ∑ w ∈ G.neighborFinset v, ↑(G.neighborFinset w \ insert v (G.neighborFinset u)).card * q w ^ 2 ≤ 2 * (au ^ 2 + ∑ w ∈ G.neighborFinset u, p w ^ 2 + (av ^ 2 + ∑ w ∈ G.neighborFinset v, q w ^ 2))) : algConn G ≤ 2

The weighted double-star master certificate. Two vertices u ≠ v, not adjacent, with disjoint neighbourhoods, and nonnegative weights (au on u, p w on w ∈ N(u); av, q on the v-side, negated) that are balanced (au + Σ p = av + Σ q) and satisfy the worst-case quadratic-form bound: then algConn G ≤ 2. Cross edges N(u)–N(v) are allowed and cost (p w + q w')²; each further edge at w ∈ N(u) (to anywhere except u and N(v)) is charged (p w)² per endpoint slot.

The apex double star and the tie law

algConn_le_two_of_apex_double_star extends the master certificate to pairs sharing one apex g (weight 0), the two apex edges u–g, v–g costing au² + av². The tie law algConn_le_two_of_apex_twin_pair applies it to two degree-3 vertices with a single shared hub, partners of degree ≤ 4, and no partner–partner cross edge. This is the certificate behind the A-bound: every same-cloud pair of usable twins of a degree-≥ 9 hub either meets it or shares a degree-4 partner / carries a cross edge, a coverage count that bounds the cloud size.

theorem ACMax.algConn_le_two_of_apex_double_star {V : Type u_1} [Fintype V] [Nonempty V] (G : SimpleGraph V) (u v g : V) (au av : ℝ) (p q : V → ℝ) (hne : u ≠ v) (huv : ¬G.Adj u v) (hgu : G.Adj u g) (hgv : G.Adj v g) (hcap : ∀ (w : V), w ≠ g → ¬(G.Adj u w ∧ G.Adj v w)) (hau : 0 < au) (hp : ∀ w ∈ (G.neighborFinset u).erase g, 0 ≤ p w) (hq : ∀ w ∈ (G.neighborFinset v).erase g, 0 ≤ q w) (hbal : au + ∑ w ∈ (G.neighborFinset u).erase g, p w = av + ∑ w ∈ (G.neighborFinset v).erase g, q w) (hQ : (au ^ 2 + av ^ 2 + ∑ w ∈ (G.neighborFinset u).erase g, (au - p w) ^ 2 + ∑ w ∈ (G.neighborFinset v).erase g, (av - q w) ^ 2 + ∑ w ∈ (G.neighborFinset u).erase g, ∑ w' ∈ (G.neighborFinset v).erase g, if G.Adj w w' then (p w + q w') ^ 2 else 0) + ∑ w ∈ (G.neighborFinset u).erase g, ↑(G.neighborFinset w \ insert u ((G.neighborFinset v).erase g)).card * p w ^ 2 + ∑ w ∈ (G.neighborFinset v).erase g, ↑(G.neighborFinset w \ insert v ((G.neighborFinset u).erase g)).card * q w ^ 2 ≤ 2 * (au ^ 2 + ∑ w ∈ (G.neighborFinset u).erase g, p w ^ 2 + (av ^ 2 + ∑ w ∈ (G.neighborFinset v).erase g, q w ^ 2))) : algConn G ≤ 2

The apex double-star master certificate. Two vertices u ≠ v, not adjacent, with g their only common neighbour (the apex, weight 0), and nonnegative weights (au on u, p w on w ∈ N(u) ∖ {g}; av, q on the v-side, negated) that are balanced and satisfy the worst-case quadratic-form bound — the far-pair bound plus the two apex-edge terms au² + av². Then algConn G ≤ 2.

theorem ACMax.algConn_le_two_of_apex_twin_pair {V : Type u_1} [Fintype V] [Nonempty V] (G : SimpleGraph V) (u v g : V) (hu3 : G.degree u = 3) (hv3 : G.degree v = 3) (hne : u ≠ v) (huv : ¬G.Adj u v) (hgu : G.Adj u g) (hgv : G.Adj v g) (hcap : ∀ (w : V), w ≠ g → ¬(G.Adj u w ∧ G.Adj v w)) (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 → w ≠ g → G.Adj v w' → w' ≠ g → ¬G.Adj w w') : algConn G ≤ 2

The apex-tie twin law. Two degree-3 vertices u ≠ v, non-adjacent, with common neighbour g (of any degree) and no other common neighbour; all other neighbours (partners) of u and of v have degree ≤ 4; and there is no edge between the two partner sides. Then algConn G ≤ 2 — the apex double star at au = av = 1, p = q ≡ ½ sits at the exact tie num = 2·norm.