The cherry case (e(M) ≥ 2)

The dispatch for the cherry world CaseCherry G (4 ≤ mIncidence G, i.e. the degree-3 set spans at least two edges), and its unconditional closure in the sea e(M) = 2 regime. A cherry is a degree-3 centre z with two non-adjacent degree-3 neighbours x, y; its three vertices form the N-block of a two-block cut, so any disjoint 3-block P with 2·e(P,N) + leak(P) ≤ 7 closes.

Main results

• exists_cherry, residualCore_cherry — a cherry always exists in the cherry world (either some degree-3 vertex has two degree-3 neighbours, or the M-edges form a ≥ 2-edge matching whose disjoint pairs would give a forbidden 2K₂).
• cherry_assemble and the three cut certificates two_twin_cherry_twoBlock (a degree-≤ 5 hub with two iso twins avoiding the cherry), single_vertex_cherry_twoBlock (an iso apex plus two hub neighbours, boundary 2(c₁+c₂) + deg h₁ + deg h₂ ≤ 8 + 2·[h₁~h₂]) and hub_triangle_cherry_twoBlock (three mutually adjacent hubs, 2·∑cross + ∑deg ≤ 13).
• cherryHubs_card_le_five — at most 5 hubs meet a cherry; shared_twin_hubs_nonadj — two degree-≤ 4 hubs on a common twin are non-adjacent (a (3,4,4)-triangle has ∑deg = 11 ≤ thr(n), n ≥ 18).
• six_richLow_twoBlock, iso_apex_dichotomy — the supply-side pigeonhole: ≥ 6 rich low hubs close the cherry world, and every iso apex either fires the SingleVertex certificate or has ≥ 2 bad neighbours (degree ≥ 5 or cherry-touching).
• caseCherry_dichotomy — under ResidualCore n G and CaseCherry G, either TwoBlockConfig G, or the graph sits in the precisely described blocked cherry corner (a cherry exists, ≤ 5 rich low hubs, every iso twin has ≥ 2 bad neighbours).
• blockedCherryCorner_close, caseCherry_algConn_le_two_of_sea_eM_four — the closure of the blocked corner, and hence of the whole cherry case, in the sea Δ ≤ 4, e(M) = 2 regime for every n ≥ 18.

The cherry

structure ACMax.Cherry {V : Type u_1} [Fintype V] (G : SimpleGraph V) (x z y : V) : Prop

A cherry: a degree-3 centre z with two distinct, non-adjacent degree-3 neighbours x, y — the P₃ inside the degree-3 graph M that every e(M) ≥ 2 residual contains (exists_cherry). The blocks below always use the cherry as the N-side {z, x, y} (leak ≤ 5 for size 3: excess −1, the best small block in the calculus).

• deg_x : G.degree x = 3
• deg_z : G.degree z = 3
• deg_y : G.degree y = 3
• adj_zx : G.Adj z x
• adj_zy : G.Adj z y
• ne_xy : x ≠ y
• nadj_xy : ¬G.Adj x y

theorem ACMax.Cherry.ne_zx {V : Type u_1} [Fintype V] {G : SimpleGraph V} {x z y : V} (h : Cherry G x z y) : z ≠ x

theorem ACMax.Cherry.ne_zy {V : Type u_1} [Fintype V] {G : SimpleGraph V} {x z y : V} (h : Cherry G x z y) : z ≠ y

theorem ACMax.Cherry.card_three {V : Type u_1} [Fintype V] {G : SimpleGraph V} {x z y : V} (h : Cherry G x z y) : {z, x, y}.card = 3

The cherry block {z, x, y} has exactly 3 vertices.

theorem ACMax.Cherry.notMem_isoTwins {V : Type u_1} [Fintype V] {G : SimpleGraph V} {x z y : V} (h : Cherry G x z y) {v : V} (hv : v ∈ isoTwins G) : v ∉ {z, x, y}

No cherry member is M-isolated (each has a degree-3 neighbour).

theorem ACMax.Cherry.iso_cross_zero {V : Type u_1} [Fintype V] {G : SimpleGraph V} {x z y : V} (h : Cherry G x z y) {t : V} (ht : t ∈ isoTwins G) : (G.neighborFinset t ∩ {z, x, y}).card = 0

An M-isolated twin sends no edge into the cherry.

Small Finset helpers

The cherry N-side leak bound and the assembly lemma

theorem ACMax.cherry_leak_le_five {V : Type u_1} [Fintype V] (G : SimpleGraph V) {x z y : V} (hch : Cherry G x z y) : ∑ q ∈ {z, x, y}, (G.neighborFinset q \ {z, x, y}).card ≤ 5

The cherry leaks at most 5: the centre keeps two edges inside (leak ≤ 1), each end keeps one (leak ≤ 2). Size 3, leak 5: excess −1 — the cherry is the canonical twin-anchored small block of the design's block calculus.

theorem ACMax.cherry_assemble {V : Type u_1} [Fintype V] (G : SimpleGraph V) {x z y : V} (hch : Cherry G x z y) (P : Finset V) (hcard : P.card = 3) (hdisj : Disjoint P {z, x, y}) (hbound : 2 * ∑ p ∈ P, (G.neighborFinset p ∩ {z, x, y}).card + ∑ p ∈ P, (G.neighborFinset p \ P).card ≤ 7) : TwoBlockConfig G

The cherry assembly lemma: any 3-block P disjoint from the cherry with 2·e(P, N) + leak(P) ≤ 7 is a two-block witness against the cherry (2·e + leak(P) + leak(N) ≤ 7 + 5 = 12 = 4·3). All three cherry cut certificates below are instances.

The three cherry cut certificates

theorem ACMax.two_twin_cherry_twoBlock {V : Type u_1} [Fintype V] (G : SimpleGraph V) {x z y h t₁ t₂ : V} (hch : Cherry G x z y) (hh4 : 4 ≤ G.degree h) (hh5 : G.degree h ≤ 5) (ht₁ : t₁ ∈ isoTwins G) (ht₂ : t₂ ∈ isoTwins G) (hne : t₁ ≠ t₂) (ha₁ : G.Adj h t₁) (ha₂ : G.Adj h t₂) (hnz : ¬G.Adj h z) (hnx : ¬G.Adj h x) (hny : ¬G.Adj h y) : TwoBlockConfig G

The TwoTwin cherry certificate (port of two_twin_cut_certificate_* / twotwin_assemble_cherry_nineteen, n-generic): a hub h with 4 ≤ deg h ≤ 5 (degree-5 hubs ARE eligible — the slack that kills the fat regime), two M-isolated twins t₁ ≠ t₂, and no edge from h into the cherry, yield a two-block witness P = {h, t₁, t₂} against N = {z, x, y}: leak(P) ≤ (deg h − 2) + 2 + 2 ≤ 7, e(P, N) = 0.

theorem ACMax.single_vertex_cherry_twoBlock {V : Type u_1} [Fintype V] (G : SimpleGraph V) {x z y t h₁ h₂ : V} (hch : Cherry G x z y) (ht : t ∈ isoTwins G) (hne : h₁ ≠ h₂) (ha₁ : G.Adj t h₁) (ha₂ : G.Adj t h₂) (hd₁ : 4 ≤ G.degree h₁) (hd₂ : 4 ≤ G.degree h₂) (hbound : 2 * ((G.neighborFinset h₁ ∩ {z, x, y}).card + (G.neighborFinset h₂ ∩ {z, x, y}).card) + G.degree h₁ + G.degree h₂ ≤ 8 + 2 * adjInd G h₁ h₂) : TwoBlockConfig G

The SingleVertex cherry certificate (port of single_vertex_cut_certificate_*, n-generic): an M-isolated apex t with two hub neighbours h₁ ≠ h₂ satisfying the exact per-n boundary arithmetic

2·(c₁ + c₂) + deg h₁ + deg h₂ ≤ 8 + 2·[h₁ ~ h₂]

(cᵢ = the cherry cross count of hᵢ) yields a two-block witness P = {t, h₁, h₂}: the apex leaks ≤ 1 and crosses 0 (isolated), each hub leaks ≤ deg − 1 − [h₁ ~ h₂].

Cherry extraction

theorem ACMax.exists_cherry (n : ℕ) (hn : 6 ≤ n) (G : SimpleGraph (Fin n)) (hT : ¬HasGoodTriangle n G) (h2k2 : ¬HasDeg3Ind2K2 n G) (hch : CaseCherry G) : ∃ (x : Fin n) (z : Fin n) (y : Fin n), Cherry G x z y

Cherry extraction. In the cherry world (4 ≤ mIncidence, i.e. e(M) ≥ 2) with no good triangle and no induced 2K₂ on degree-3 vertices, a cherry exists: either some degree-3 vertex has two degree-3 neighbours, or M is a matching with ≥ 2 edges whose two edges have no cross adjacency (any cross adjacency would give a vertex two degree-3 neighbours) — an induced 2K₂, excluded. The ends are non-adjacent since a degree-3 triangle has ∑deg = 9, good for every n ≥ 6.

theorem ACMax.residualCore_cherry (n : ℕ) (G : SimpleGraph (Fin n)) (h : ResidualCore n G) (hch : CaseCherry G) : ∃ (x : Fin n) (z : Fin n) (y : Fin n), Cherry G x z y

Cherry extraction from the residual core (the ResidualCore fields supply exactly the needed exclusions; n ≥ 12 ≥ 6).

The counting layer

noncomputable def ACMax.cherryHubs {V : Type u_1} [Fintype V] (G : SimpleGraph V) (x z y : V) : Finset V

The cherry-touching hubs: hubs adjacent to a cherry vertex.

Equations

• ACMax.cherryHubs G x z y = {w ∈ ACMax.hubSet G | G.Adj w z ∨ G.Adj w x ∨ G.Adj w y}

theorem ACMax.mem_cherryHubs {V : Type u_1} [Fintype V] {G : SimpleGraph V} {x z y w : V} : w ∈ cherryHubs G x z y ↔ 4 ≤ G.degree w ∧ (G.Adj w z ∨ G.Adj w x ∨ G.Adj w y)

theorem ACMax.cherryHubs_card_le_five {V : Type u_1} [Fintype V] (G : SimpleGraph V) {x z y : V} (hch : Cherry G x z y) : (cherryHubs G x z y).card ≤ 5

The cherry-touching hub budget — at most 5 hubs meet a cherry: the centre carries ≤ 1 hub (two of its three edges stay in the cherry), each end ≤ 2.

theorem ACMax.shared_twin_hubs_nonadj (n : ℕ) (hn : 18 ≤ n) (G : SimpleGraph (Fin n)) (hT : ¬HasGoodTriangle n G) {t g h : Fin n} (hdt : G.degree t = 3) (hdg : G.degree g ≤ 4) (hdh : G.degree h ≤ 4) (hgt : G.Adj g t) (hht : G.Adj h t) (hne : g ≠ h) : ¬G.Adj g h

Shared-twin hubs are non-adjacent (n ≥ 18): two degree-≤ 4 hubs adjacent to a common degree-3 vertex cannot be adjacent — the (3,4,4)-triangle has ∑deg ≤ 11 = thr(n), a good triangle for every n ≥ 18. The structural atom of the sea-side host-capacity analysis (host pairs of an iso twin are pairwise non-adjacent).

The pigeonholes

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

The rich low hubs: hubs of degree ≤ 5 with at least two M-isolated twins — exactly the TwoTwin-eligible centres.

Equations

• ACMax.richLowHubs G = {w ∈ ACMax.hubSet G | G.degree w ≤ 5 ∧ 2 ≤ (G.neighborFinset w ∩ ACMax.isoTwins G).card}

theorem ACMax.mem_richLowHubs {V : Type u_1} [Fintype V] {G : SimpleGraph V} {w : V} : w ∈ richLowHubs G ↔ 4 ≤ G.degree w ∧ G.degree w ≤ 5 ∧ 2 ≤ (G.neighborFinset w ∩ isoTwins G).card

noncomputable def ACMax.badApexNbrs {V : Type u_1} [Fintype V] (G : SimpleGraph V) (x z y t : V) : Finset V

The bad neighbours of an apex t against a cherry: neighbours of degree ≥ 5 or touching the cherry — the vertices that block the SingleVertex pair selection.

Equations

• ACMax.badApexNbrs G x z y t = {w ∈ G.neighborFinset t | 5 ≤ G.degree w ∨ w ∈ ACMax.cherryHubs G x z y}

theorem ACMax.six_richLow_twoBlock {V : Type u_1} [Fintype V] (G : SimpleGraph V) {x z y : V} (hch : Cherry G x z y) (h6 : 6 ≤ (richLowHubs G).card) : TwoBlockConfig G

The C0 pigeonhole (the design's "fat + cherry → TwoTwin" counting): ≥ 6 rich low hubs close the cherry world — at most 5 hubs touch the cherry, so some rich low hub avoids it and fires the TwoTwin certificate.

theorem ACMax.iso_apex_dichotomy {V : Type u_1} [Fintype V] (G : SimpleGraph V) (hdeg3 : ∀ (v : V), 3 ≤ G.degree v) {x z y t : V} (hch : Cherry G x z y) (ht : t ∈ isoTwins G) : TwoBlockConfig G ∨ 2 ≤ (badApexNbrs G x z y t).card

The sea-side dispatch atom: every M-isolated apex t either fires the SingleVertex certificate outright (two neighbours of degree exactly 4 avoiding the cherry), or has ≥ 2 bad neighbours — degree ≥ 5 or cherry-touching. (The δ ≥ 3 hypothesis makes all of t's three neighbours hubs.)

The dispatch

theorem ACMax.caseCherry_dichotomy (n : ℕ) (G : SimpleGraph (Fin n)) (h : ResidualCore n G) (hch : CaseCherry G) : TwoBlockConfig G ∨ ∃ (x : Fin n) (z : Fin n) (y : Fin n), Cherry G x z y ∧ (richLowHubs G).card ≤ 5 ∧ ∀ t ∈ isoTwins G, 2 ≤ (badApexNbrs G x z y t).card

The cherry dichotomy (the main dispatch of this file): under ResidualCore and CaseCherry, either a TwoBlockConfig exists (via the certificates above), or the graph lies in the sharply-described blocked cherry corner: a cherry with ≤ 5 rich low hubs and every M-isolated twin double-blocked (≥ 2 neighbours of degree ≥ 5 or cherry-touching). The corner predicate is exactly the interface the L4 continuation (the sea-side host-capacity pigeonhole) must close; every adversarial build probed at n ∈ {25, 30, 40} that satisfies it is nevertheless killed by TwoHub ⊂ W1 (scratchpad/general_cherry_sweep.py).

Closing the blocked cherry corner in the sea e(M) = 2 regime

Closes the residual blockedCherryCorner of caseCherry_dichotomy when mIncidence G = 4 (e(M) = 2, so M is exactly the P₃ cherry) and Δ ≤ 4 (the sea), for every n ≥ 18. With e(M) = 2 the cherry carries the whole of M (eM_four_nbrs), so every degree-3 vertex outside {x, z, y} is an iso twin and |Iso| ≥ 5 (eM_four_iso_card). In the sea bad = cherry-touching, so the corner demands ∑_{t∈Iso} |N(t) ∩ CT| ≥ 2|Iso|, forcing ≥ 3 rich cherry-touching hubs, of which z blocks at most one — hence two z-avoiding rich hubs (corner_rich_pair_exists). Such a pair closes (p3_pair_close): the crossing budget vanishes (mCross_eq_zero_of_zavoid) and a short case analysis on |D3| ∈ {3, 4} and adjacency fires W1Config with or without a far pad, or falls back to the raw two_hub_private_pair_twoBlock.

Small helpers

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

The iso-twin neighbours of a hub, as a pinned def so that its instances stay stable across the Fin n / generic-V boundary.

Equations

• ACMax.isoNbrs G g = G.neighborFinset g ∩ ACMax.isoTwins G

theorem ACMax.mem_isoNbrs {V : Type u_1} [Fintype V] {G : SimpleGraph V} {g t : V} : t ∈ isoNbrs G g ↔ G.Adj g t ∧ t ∈ isoTwins G

theorem ACMax.cherry_x_not_iso {V : Type u_1} [Fintype V] (G : SimpleGraph V) {x z y : V} (hch : Cherry G x z y) : x ∉ isoTwins G

The cherry ends and centre are not M-isolated (each has a degree-3 neighbour).

theorem ACMax.cherry_y_not_iso {V : Type u_1} [Fintype V] (G : SimpleGraph V) {x z y : V} (hch : Cherry G x z y) : y ∉ isoTwins G

theorem ACMax.cherry_z_not_iso {V : Type u_1} [Fintype V] (G : SimpleGraph V) {x z y : V} (hch : Cherry G x z y) : z ∉ isoTwins G

The e(M) = 2 structure: the cherry is the whole of M

theorem ACMax.eM_four_nbrs {V : Type u_1} [Fintype V] (G : SimpleGraph V) {x z y : V} (hch : Cherry G x z y) (heM : mIncidence G = 4) : (∀ (w : V), G.Adj x w → G.degree w = 3 → w = z) ∧ (∀ (w : V), G.Adj y w → G.degree w = 3 → w = z) ∧ ∀ (v : V), G.degree v = 3 → v ≠ z → v ≠ x → v ≠ y → v ∈ isoTwins G

The mIncidence = 4 structure theorem. When e(M) = 2, the cherry accounts for the entire D–D incidence sum: the only degree-3 neighbour of each end is the centre z, and every degree-3 vertex other than x, z, y is an M-isolated twin.

theorem ACMax.eM_four_iso_card (n : ℕ) (hn : 8 ≤ n) (G : SimpleGraph (Fin n)) (hm : G.edgeFinset.card = 2 * (n - 2)) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) {x z y : Fin n} (hch : Cherry G x z y) (heM : mIncidence G = 4) : 5 ≤ (isoTwins G).card

The iso-twin supply of the e(M) = 2 world: |Iso| ≥ |D| − 3 ≥ 5.

The pair atoms

theorem ACMax.mCross_eq_zero_of_zavoid {V : Type u_1} [Fintype V] (G : SimpleGraph V) {x z y : V} (hch : Cherry G x z y) (heM : mIncidence G = 4) {g h : V} (hgz : ¬G.Adj g z) (hhz : ¬G.Adj h z) : mCross G g h = 0

The crossing budget vanishes for z-avoiding pairs: in the e(M) = 2 world every M-edge touches the centre z, and z lies in neither private side of a pair of hubs avoiding it — so mCross(g, h) = 0 structurally.

theorem ACMax.sharedTwins_card_le_one_of_zavoid (n : ℕ) (hn : 16 ≤ n) (G : SimpleGraph (Fin n)) (hC4 : ¬HasGoodC4 n G) {x z y : Fin n} (hch : Cherry G x z y) (heM : mIncidence G = 4) {g h : Fin n} (hdg : G.degree g = 4) (hdh : G.degree h = 4) (hne : g ≠ h) (hnadj : ¬G.Adj g h) (hgz : ¬G.Adj g z) : (sharedTwins G g h).card ≤ 1

The share bound for z-avoiding pairs (n ≥ 16): two non-adjacent degree-4 hubs avoiding z share at most one degree-3 twin — any two shared twins live in {x, y} ∪ Iso, hence are non-adjacent, and give the good C₄ Σ = 14.

theorem ACMax.sharedTwins_eq_empty_of_adj (n : ℕ) (hn : 18 ≤ n) (G : SimpleGraph (Fin n)) (hT : ¬HasGoodTriangle n G) {g h : Fin n} (hdg : G.degree g ≤ 4) (hdh : G.degree h ≤ 4) (hadj : G.Adj g h) : sharedTwins G g h = ∅

Adjacent low hubs share nothing (n ≥ 18, wraps shared_twin_hubs_nonadj): an adjacent pair of degree-≤ 4 hubs with a common degree-3 twin is a (3,4,4)-triangle.

theorem ACMax.hubTwins_card_bounds {V : Type u_1} [Fintype V] (G : SimpleGraph V) {g c : V} (hgc : G.Adj g c) (hc3 : G.degree c = 3) (hcIso : c ∉ isoTwins G) : (isoNbrs G g).card + 1 ≤ (hubTwins G g).card

The rich-CT D3-card bound: a hub with a non-iso degree-3 neighbour c has |D3| ≥ |isoNbrs| + 1.

The pair closes

theorem ACMax.p3_pair_close (n : ℕ) (hn : 18 ≤ n) (G : SimpleGraph (Fin n)) (hT : ¬HasGoodTriangle n G) (hC4 : ¬HasGoodC4 n G) {x z y : Fin n} (hch : Cherry G x z y) (heM : mIncidence G = 4) (hIso5 : 5 ≤ (isoTwins G).card) {g h : Fin n} (hne : g ≠ h) (hdg : G.degree g = 4) (hdh : G.degree h = 4) (hgxy : G.Adj g x ∨ G.Adj g y) (hhxy : G.Adj h x ∨ G.Adj h y) (hgz : ¬G.Adj g z) (hhz : ¬G.Adj h z) (hgr : 2 ≤ (isoNbrs G g).card) (hhr : 2 ≤ (isoNbrs G h).card) : W1Config G ∨ TwoBlockConfig G

The z-avoiding rich pair closes (the main pair theorem, n ≥ 18): two distinct rich cherry-touching degree-4 hubs avoiding the centre give a W1Config or a TwoBlockConfig, by the adjacent / equal / gap / two-hub case tree.

The pigeonhole: two z-avoiding rich cherry-touching hubs exist

theorem ACMax.corner_rich_pair_exists {V : Type u_1} [Fintype V] (G : SimpleGraph V) (hsea : ∀ (v : V), G.degree v ≤ 4) {x z y : V} (hch : Cherry G x z y) (hIso5 : 5 ≤ (isoTwins G).card) (hblock : ∀ t ∈ isoTwins G, 2 ≤ (badApexNbrs G x z y t).card) : ∃ (g : V) (h : V), g ≠ h ∧ G.degree g = 4 ∧ G.degree h = 4 ∧ (G.Adj g x ∨ G.Adj g y) ∧ (G.Adj h x ∨ G.Adj h y) ∧ ¬G.Adj g z ∧ ¬G.Adj h z ∧ 2 ≤ (isoNbrs G g).card ∧ 2 ≤ (isoNbrs G h).card

The corner pigeonhole (sea regime): if every iso twin has ≥ 2 bad neighbours and there is no degree-≥ 5 vertex, the ≥ 2|Iso| ≥ 10 cherry-touching incidence demand against the ≤ 5-hub, ≤ 3-each capacity forces ≥ 3 rich cherry-touching hubs, of which at most one is adjacent to the centre z — leaving the two hubs the pair theorem needs.

The corner closure and the C0 assembly

theorem ACMax.blockedCherryCorner_close (n : ℕ) (hn : 18 ≤ n) (G : SimpleGraph (Fin n)) (h : ResidualCore n G) (hsea : ∀ (v : Fin n), G.degree v ≤ 4) (heM : mIncidence G = 4) {x z y : Fin n} (hch : Cherry G x z y) (hblock : ∀ t ∈ isoTwins G, 2 ≤ (badApexNbrs G x z y t).card) : W1Config G ∨ TwoBlockConfig G

THE BLOCKED CHERRY CORNER CLOSES in the e(M) = 2 sea regime (n ≥ 18, Δ ≤ 4, mIncidence = 4): under ResidualCore, a cherry all of whose iso twins are double-blocked forces a W1Config or a TwoBlockConfig — the exact conclusion the caseCherry_dichotomy corner interface asks for.

theorem ACMax.caseCherry_algConn_le_two_of_sea_eM_four (n : ℕ) [Nonempty (Fin n)] (hn : 18 ≤ n) (G : SimpleGraph (Fin n)) (h : ResidualCore n G) (hsea : ∀ (v : Fin n), G.degree v ≤ 4) (heM : mIncidence G = 4) : algConn G ≤ 2

The C0 closure on the e(M) = 2 sea regime (the strongest honest form of caseCherry_algConn_le_two): a ResidualCore graph with Δ ≤ 4 and mIncidence = 4 has algConn G ≤ 2 — unconditionally, for every n ≥ 18. Both branches of caseCherry_dichotomy are discharged: the supply side by the cherry cut certificates, the blocked corner by blockedCherryCorner_close.