Double-open-star certificates and the M-edge dispatch vocabulary

The signed-cut toolbox for two-hub configurations, together with the vocabulary that classifies a residual graph by its M-edges (edges between degree-3 vertices). Two hubs g ≠ h and their degree-3 twins assemble a double open star, whose signed cut bounds algebraic connectivity by 2 under an explicit leak budget.

Vocabulary

deg3Set (the degree-3 set D), hubSet (degree ≥ 4), hubTwins g (degree-3 neighbours of g), privTwins g h / sharedTwins g h (twins of g private to it / shared with h), intDeg g (non-degree-3 neighbours of g), mCross g h, mIncidence (the D–D incidence sum), and isoTwins (degree-3 vertices with no degree-3 neighbour).

Main results

• W1Config, w1_cut_certificate, w1_algConn_le_two — the W1 double-open-star certificate: with P = {g} ∪ privTwins g h and N = {h} ∪ privTwins h g ∪ F (far pads F balancing the sizes), the leak budget |F| + intDeg g + intDeg h + 2·sharedTwins + 2·[g ~ h] + 4·mCross ≤ 4 produces a TwoBlockConfig, hence algConn G ≤ 2.
• eM_trichotomy — mIncidence G ∈ {0, 2} ∨ 4 ≤ mIncidence G, the gate splitting the dispatch into the no-M-edge, single-M-edge and cherry cases.
• SeaFatBoundary, w1Config_of_pair, dsValue — the resource boundary where no hub pair yields a cheap W1 witness, and the firing bridge back into W1Config.
• two_hub_opposite_twin_twoBlock, two_hub_private_pair_twoBlock, star3_leak_le_six — raw six-vertex two-block certificates (over [DecidableEq V]) that tolerate shared twins and M-crosses beyond the W1 master arithmetic, used in the rich-sea regime.

The double-star vocabulary

noncomputable def ACMax.deg3Set {V : Type u_1} [Fintype V] (G : SimpleGraph V) : Finset V

The degree-3 set D.

Equations

• ACMax.deg3Set G = {v : V | G.degree v = 3}

theorem ACMax.mem_deg3Set {V : Type u_1} [Fintype V] {G : SimpleGraph V} {v : V} : v ∈ deg3Set G ↔ G.degree v = 3

noncomputable def ACMax.hubTwins {V : Type u_1} [Fintype V] (G : SimpleGraph V) (g : V) : Finset V

The degree-3 twins of a hub: D3(g) = N(g) ∩ D.

Equations

• ACMax.hubTwins G g = G.neighborFinset g ∩ ACMax.deg3Set G

noncomputable def ACMax.privTwins {V : Type u_1} [Fintype V] (G : SimpleGraph V) (g h : V) : Finset V

The private twins of g against h: D3(g) \ D3(h) — the P-side block body of the double open star.

Equations

• ACMax.privTwins G g h = ACMax.hubTwins G g \ ACMax.hubTwins G h

noncomputable def ACMax.sharedTwins {V : Type u_1} [Fintype V] (G : SimpleGraph V) (g h : V) : Finset V

The shared twins s(g,h) = D3(g) ∩ D3(h).

Equations

• ACMax.sharedTwins G g h = ACMax.hubTwins G g ∩ ACMax.hubTwins G h

noncomputable def ACMax.intDeg {V : Type u_1} [Fintype V] (G : SimpleGraph V) (g : V) : ℕ

The internal degree i(g) = deg g − |D3(g)| — the number of non-degree-3 neighbours (the design's intdeg).

Equations

• ACMax.intDeg G g = (G.neighborFinset g \ ACMax.deg3Set G).card

noncomputable def ACMax.mCross {V : Type u_1} [Fintype V] (G : SimpleGraph V) (g h : V) : ℕ

The M-cross count: the number of edges between the two private sides (each such edge is a D–D edge, i.e. an M-edge; in the residual world e(M) ≤ 1 forces mCross ≤ 1, so this count coincides with the design's [M-cross] indicator).

Equations

• ACMax.mCross G g h = ∑ t ∈ ACMax.privTwins G g h, (G.neighborFinset t ∩ ACMax.privTwins G h g).card

noncomputable def ACMax.adjInd {V : Type u_1} (G : SimpleGraph V) (g h : V) : ℕ

The adjacency indicator [g ~ h].

Equations

• ACMax.adjInd G g h = if G.Adj g h then 1 else 0

noncomputable def ACMax.mIncidence {V : Type u_1} [Fintype V] (G : SimpleGraph V) : ℕ

The D–D incidence sum ∑_{v∈D} |N(v) ∩ D| = 2·e(M).

Equations

• ACMax.mIncidence G = ∑ v ∈ ACMax.deg3Set G, (G.neighborFinset v ∩ ACMax.deg3Set G).card

Vocabulary lemmas

theorem ACMax.privTwins_spec {V : Type u_1} [Fintype V] {G : SimpleGraph V} {g h t : V} : t ∈ privTwins G g h ↔ G.Adj g t ∧ G.degree t = 3 ∧ ¬G.Adj h t

theorem ACMax.sharedTwins_spec {V : Type u_1} [Fintype V] {G : SimpleGraph V} {g h t : V} : t ∈ sharedTwins G g h ↔ G.Adj g t ∧ G.Adj h t ∧ G.degree t = 3

theorem ACMax.sharedTwins_comm {V : Type u_1} [Fintype V] (G : SimpleGraph V) (g h : V) : sharedTwins G g h = sharedTwins G h g

theorem ACMax.privTwins_disjoint {V : Type u_1} [Fintype V] (G : SimpleGraph V) (g h : V) : Disjoint (privTwins G g h) (privTwins G h g)

The two private sides are always disjoint.

theorem ACMax.hubTwins_card_add_intDeg {V : Type u_1} [Fintype V] (G : SimpleGraph V) (g : V) : (hubTwins G g).card + intDeg G g = G.degree g

Twin/internal split of a hub's neighbourhood: |D3(g)| + i(g) = deg g.

theorem ACMax.privTwins_card_add_shared {V : Type u_1} [Fintype V] (G : SimpleGraph V) (g h : V) : (privTwins G g h).card + (sharedTwins G g h).card = (hubTwins G g).card

Private/shared split of the twin set: |priv(g,h)| + |s(g,h)| = |D3(g)|.

Part 1 — the W1 certificate

The leak/cross bookkeeping of the double open star, block by block.

theorem ACMax.doubleStar_center_leak {V : Type u_1} [Fintype V] (G : SimpleGraph V) (g h : V) : (G.neighborFinset g \ insert g (privTwins G g h)).card ≤ (sharedTwins G g h).card + intDeg G g

Centre leak bound. The centre g of P = {g} ∪ priv(g,h) leaks at most s(g,h) + i(g): its neighbourhood is priv(g,h) ⊔ shared(g,h) ⊔ (N(g) \ D), and the private part stays inside P.

theorem ACMax.doubleStar_twin_leak {V : Type u_1} [Fintype V] (G : SimpleGraph V) (g h : V) {t : V} (ht : t ∈ privTwins G g h) : (G.neighborFinset t \ insert g (privTwins G g h)).card ≤ 2

Twin leak bound. Each private twin t ∈ priv(g,h) (degree 3, one edge back to g ∈ P) leaks at most 2 out of P.

theorem ACMax.doubleStar_P_leak {V : Type u_1} [Fintype V] (G : SimpleGraph V) (g h : V) : ∑ p ∈ insert g (privTwins G g h), (G.neighborFinset p \ insert g (privTwins G g h)).card ≤ (sharedTwins G g h).card + intDeg G g + 2 * (privTwins G g h).card

P-side leak bound (assembled): leak(P) ≤ s(g,h) + i(g) + 2·|priv(g,h)|.

theorem ACMax.doubleStar_P_cross {V : Type u_1} [Fintype V] (G : SimpleGraph V) (g h : V) (F : Finset V) (hfar : ∀ f ∈ F, ∀ w ∈ insert g (privTwins G g h) ∪ insert h (privTwins G h g), ¬G.Adj f w) : ∑ p ∈ insert g (privTwins G g h), (G.neighborFinset p ∩ (insert h (privTwins G h g) ∪ F)).card ≤ adjInd G g h + mCross G g h

P-side cross bound: with far pads, the only cross-edges out of P into N = {h} ∪ priv(h,g) ∪ F are the (possible) g–h edge and the M-edges between the private sides: e(P,N) ≤ [g ~ h] + mCross(g,h).

def ACMax.W1Config {V : Type u_1} [Fintype V] (G : SimpleGraph V) : Prop

The W1 (DOUBLE-OPEN-STAR) configuration — the design's DS_pair witness in its exact validated form (scratchpad/general_w1_check.py: 74/74 saved escapers fire, all assembled witnesses re-verified integer-exactly). Data: hubs g ≠ h and a far pad set F (degree-3 vertices with no edge into P₀ ∪ N₀) padding the h-side to equal size, satisfying the master arithmetic

|F| + i(g) + i(h) + 2·s(g,h) + 2·[g ~ h] + 4·mCross(g,h) ≤ 4

(|F| = gap; the 4·mCross count form matches the design's 4·[M-cross] indicator on the whole e(M) ≤ 1 residual world, and is one-sidedly stronger as a hypothesis when mCross ≥ 2, so the certificate below is sound for it verbatim). Instances: TwoHub is the (4,4,2,2,s=0) tie; the clean TwoStar is (d,d,0,0,s=0) at slack 4; blocking a pair needs DS-value ≥ 5. The design's (+2 M-pad) refinement (using the e(M) = 1 edge pair as a 2-pad at cost 4 instead of 6) is NOT formalized — the base ≤ 4 form is the one validated on all 74 + 301 builds.

Equations

• One or more equations did not get rendered due to their size.

theorem ACMax.w1_cut_certificate {V : Type u_1} [Fintype V] (G : SimpleGraph V) (hcfg : W1Config G) : TwoBlockConfig G

The W1 cut certificate (Part 1, the main theorem): a double-open-star witness is a two-block witness. P = {g} ∪ priv(g,h), N = {h} ∪ priv(h,g) ∪ F;

2·e(P,N) + leak(P) + leak(N) ≤ 2([g~h] + mCross) + (s + i(g) + 2·p_g) + (s + i(h) + 2·p_h + 3·|F|) = 4·p_g + (|F| + i(g) + i(h) + 2s + 2[g~h] + 2·mCross) ≤ 4·p_g + 4 = 4|P|

using p_h + |F| = p_g — exactly the master arithmetic (with the crossing M-edges' true cost 2·mCross ≤ 4·mCross).

theorem ACMax.w1_algConn_le_two {V : Type u_1} [Fintype V] [Nonempty V] (G : SimpleGraph V) (h : W1Config G) : algConn G ≤ 2

The W1 configuration closes the graph: algConn G ≤ 2.

Subsumption: TwoHub and TwoStar are W1 instances

The M-edge dispatch predicates

The case predicates of the glue tree, with the mechanical dispatch-direction lemmas: the mIncidence trichotomy that isolates the cherry / single-M-edge / no-M-edge worlds, and the SeaFatBoundary resource gate.

def ACMax.CaseCherry {V : Type u_1} [Fintype V] (G : SimpleGraph V) : Prop

C0 — the cherry world: e(M) ≥ 2 (incidence form). Routed to the per-n cherry constructions (SingleVertex / TwoTwin / HubTriangle).

Equations

• ACMax.CaseCherry G = (4 ≤ ACMax.mIncidence G)

def ACMax.CaseMZero {V : Type u_1} [Fintype V] (G : SimpleGraph V) : Prop

C5 — the e(M) = 0 world. Closing counting: NEEDS-NEW-COUNTING (L5.7; the MaxHub-style extremal counting survives only n ≤ 20).

Equations

• ACMax.CaseMZero G = (ACMax.mIncidence G = 0)

theorem ACMax.eM_trichotomy {V : Type u_1} [Fintype V] (G : SimpleGraph V) : CaseMZero G ∨ mIncidence G = 2 ∨ CaseCherry G

The e(M) dispatch gate: the D–D incidence sum is even (each M-edge is counted from both ends), so every graph is e(M) = 0, e(M) = 1 (mIncidence = 2), or in the cherry world. This is the C0/C5 split of the glue tree.

noncomputable def ACMax.dsValue {V : Type u_1} [Fintype V] (G : SimpleGraph V) (g h : V) : ℕ

The DS value of a hub pair — the design's master-arithmetic left-hand side, with the gap in ℕ-symmetric form (p_g − p_h) + (p_h − p_g) = |p_g − p_h|.

Equations

• One or more equations did not get rendered due to their size.

def ACMax.SeaFatBoundary {V : Type u_1} [Fintype V] (G : SimpleGraph V) : Prop

C2 — the ¬W1-resource boundary predicate (design §2a): every hub pair is DS-blocked (value ≥ 5). The output of the (open) C2 resource LP: ≤ 1 clean deg-4 hub, O(√n) unburied hubs, e_H ≥ (3/2)(|Hub| − O(√n)) — NEEDS-C2-COUNTING.

Equations

• ACMax.SeaFatBoundary G = ∀ (g h : V), 4 ≤ G.degree g → 4 ≤ G.degree h → g ≠ h → 5 ≤ ACMax.dsValue G g h

theorem ACMax.w1Config_of_pair {V : Type u_1} [Fintype V] (G : SimpleGraph V) (g h : V) (F : Finset V) (hg4 : 4 ≤ G.degree g) (hh4 : 4 ≤ G.degree h) (hne : g ≠ h) (hF3 : ∀ f ∈ F, G.degree f = 3) (hfar : ∀ f ∈ F, ∀ w ∈ insert g (privTwins G g h) ∪ insert h (privTwins G h g), ¬G.Adj f w) (hcard : F.card + (privTwins G h g).card = (privTwins G g h).card) (hds : dsValue G g h ≤ 4) : W1Config G

The firing bridge: a hub pair of DS-value ≤ 4 with an exact far-pad supply is a W1 configuration (the master inequality is the DS value with gap = |F|).

noncomputable def ACMax.isoTwins {V : Type u_1} [Fintype V] (G : SimpleGraph V) : Finset V

The M-isolated degree-3 twins (Iso): degree-3 vertices with no degree-3 neighbour.

Equations

• ACMax.isoTwins G = {t ∈ ACMax.deg3Set G | ∀ (w : V), G.Adj t w → G.degree w ≠ 3}

Rich-sea two-block cut certificates

Raw six-vertex two-block certificates over [DecidableEq V], used in the rich-sea regime where shared twins and M-crosses block the clean W1 master arithmetic. The [DecidableEq V] binder lets every ∩/∪ in the statements instantiate to the ambient instance; classical_inter_eq / classical_sdiff_eq bridge it to the Classical instance pinned inside richHubs / mIncidence (DecidableEq is a subsingleton). Key certificates: two_hub_opposite_twin_twoBlock, two_hub_private_pair_twoBlock, and the leak bound star3_leak_le_six.

The classical-instance bridges

theorem ACMax.classical_inter_eq {α : Type u_2} [inst : DecidableEq α] (s t : Finset α) : s ∩ t = s ∩ t

Bridge: Finset.inter under the Classical instance equals ∩ under the ambient open Classical in instance (DecidableEq is a subsingleton).

theorem ACMax.classical_sdiff_eq {α : Type u_2} [inst : DecidableEq α] (s t : Finset α) : s \ t = s \ t

Bridge: Finset.sdiff under the Classical instance equals \ under the ambient instance.

noncomputable def ACMax.hubSet {V : Type u_1} [Fintype V] (G : SimpleGraph V) : Finset V

The hub set: vertices of degree ≥ 4.

Equations

• ACMax.hubSet G = {v : V | 4 ≤ G.degree v}

theorem ACMax.mem_hubSet {V : Type u_1} [Fintype V] {G : SimpleGraph V} {v : V} : v ∈ hubSet G ↔ 4 ≤ G.degree v

theorem ACMax.mem_isoTwins {V : Type u_1} [Fintype V] {G : SimpleGraph V} {t : V} : t ∈ isoTwins G ↔ G.degree t = 3 ∧ ∀ (w : V), G.Adj t w → G.degree w ≠ 3

theorem ACMax.mIncidence_eq_sum {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) : mIncidence G = ∑ v ∈ deg3Set G, (G.neighborFinset v ∩ deg3Set G).card

mIncidence in the ambient-instance sum form.

Iso-twin bookkeeping

theorem ACMax.isoTwins_not_adj {V : Type u_1} [Fintype V] (G : SimpleGraph V) {s t : V} (hs : s ∈ isoTwins G) (ht : t ∈ isoTwins G) : ¬G.Adj s t

Two iso twins are never adjacent.

The certificates

theorem ACMax.nbr_inter_triple_zero {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) (p x y z : V) (hx : ¬G.Adj p x) (hy : ¬G.Adj p y) (hz : ¬G.Adj p z) : (G.neighborFinset p ∩ {x, y, z}).card = 0

Neighbourhood–triple non-adjacency gives a zero cross count.

theorem ACMax.star3_leak_le_six {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) (h a b : V) (hne_ha : h ≠ a) (hne_hb : h ≠ b) (hne_ab : a ≠ b) (hadj_a : G.Adj a h) (hadj_b : G.Adj b h) (hda : G.degree a = 3) (hdb : G.degree b = 3) (hdh : G.degree h ≤ 4) : ∑ p ∈ {h, a, b}, (G.neighborFinset p \ {h, a, b}).card ≤ 6

Open-star boundary count: a hub of degree ≤ 4 with two degree-3 leaves inside its triple leaks at most (4 − 2) + 2 + 2 = 6 — the P-side arithmetic of the two-hub cut, n-independent.

theorem ACMax.two_hub_opposite_twin_twoBlock {V : Type u_1} [Fintype V] (G : SimpleGraph V) (h₁ h₂ a b c d : V) (hdegh₁ : G.degree h₁ ≤ 4) (hdegh₂ : G.degree h₂ ≤ 4) (hdega : G.degree a = 3) (hdegb : G.degree b = 3) (hdegc : G.degree c = 3) (hdegd : G.degree d = 3) (hadj_ah₁ : G.Adj a h₁) (hadj_bh₁ : G.Adj b h₁) (hadj_ch₂ : G.Adj c h₂) (hadj_dh₂ : G.Adj d h₂) (hn_h₁h₂ : ¬G.Adj h₁ h₂) (hn_h₁c : ¬G.Adj h₁ c) (hn_h₁d : ¬G.Adj h₁ d) (hn_ah₂ : ¬G.Adj a h₂) (hn_ac : ¬G.Adj a c) (hn_ad : ¬G.Adj a d) (hn_bh₂ : ¬G.Adj b h₂) (hn_bc : ¬G.Adj b c) (hn_bd : ¬G.Adj b d) (ne_h₁h₂ : h₁ ≠ h₂) (ne_h₁a : h₁ ≠ a) (ne_h₁b : h₁ ≠ b) (ne_h₁c : h₁ ≠ c) (ne_h₁d : h₁ ≠ d) (ne_h₂a : h₂ ≠ a) (ne_h₂b : h₂ ≠ b) (ne_h₂c : h₂ ≠ c) (ne_h₂d : h₂ ≠ d) (ne_ab : a ≠ b) (ne_ac : a ≠ c) (ne_ad : a ≠ d) (ne_bc : b ≠ c) (ne_bd : b ≠ d) (ne_cd : c ≠ d) : TwoBlockConfig G

The two-hub opposite-twin cut, generic V (port of two_hub_opposite_twin_cert_nineteen, output TwoBlockConfig): the boundary tie 2·0 + 6 + 6 = 12 ≤ 4·3. The hub degrees are only required ≤ 4 (slack-tolerant strengthening; the per-n versions used = 4).

theorem ACMax.two_hub_private_pair_twoBlock {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) (h₁ h₂ : V) (hdh₁ : G.degree h₁ = 4) (hdh₂ : G.degree h₂ = 4) (hne : h₁ ≠ h₂) (hnadj : ¬G.Adj h₁ h₂) (hpriv1 : 2 ≤ ((G.neighborFinset h₁ ∩ isoTwins G) \ G.neighborFinset h₂).card) (hpriv2 : 2 ≤ ((G.neighborFinset h₂ ∩ isoTwins G) \ G.neighborFinset h₁).card) : TwoBlockConfig G

Two hubs with 2 + 2 private iso twins give a two-block cut — the positive form of the per-n hno2hub selector (select_finish + two_hub_config): whenever the selector's existential holds, the cut fires.