The M-shape analysis and the complete Δ ≤ 4 closure

Closes the e(M) ≥ 3 part of the blocked cherry corner in the sea regime (Δ ≤ 4), and assembles the full Δ ≤ 4 ("sea") closure of the residual core. Under ResidualCore the degree-3 graph M on D = deg3Set has no triangle, no 4-cycle, no induced 2K₂ and Δ(M) ≤ 3, so with e(M) ≥ 3 its support is exactly one of five shapes: P4, claw, chair, S22 (double star) or C5, with every other degree-3 vertex an iso twin.

Main results

• mshape_classify — the M-shape classification of the e(M) ≥ 3 support.
• Two structural atoms: hub_mnbrs_not_adj (a hub sees at most one end of each M-edge; (≤4,3,3)-triangle, n ≥ 9) and hub_no_dist2_pair (a hub never sees two M-vertices at M-distance 2; C₄ ∑ = 13, n ≥ 11), so a rich hub's M-neighbourhood is pairwise M-distance ≥ 3.
• s22_split_twoBlock — the S22 shape splits unconditionally into its two stars (tie 2·1 + 5 + 5 = 12).
• p4_corner_close and the claw/chair/C5 kills — every other shape closes: in claw/chair/C5 a corner-provided rich hub misses a cherry and fires two_twin_cherry_twoBlock; the P4 shape needs the role analysis (β/γ/α* pinned by the two atoms and the share bound hubs_share_le_one) feeding two_hub_opposite_twin_twoBlock or the private-iso pair cut.
• blockedCherryCorner_close_eM_ge3, caseCherry_algConn_le_two_of_sea — the e(M) ≥ 3 corner closure and hence the complete cherry-case closure for Δ ≤ 4.
• residual_sea_algConn_le_two — for every n ≥ 23, a ResidualCore graph with Δ ≤ 4 has algConn G ≤ 2, dispatched by eM_trichotomy: e(M) ≤ 1 via x0_corner_close, e(M) ≥ 2 via caseCherry_algConn_le_two_of_sea. Only the Δ ≥ 5 ("fat") side of ResidualCore remains open.

Small neighbourhood atoms

theorem ACMax.deg3_nbr_pin {V : Type u_1} [Fintype V] (G : SimpleGraph V) {v p q r w : V} (hdv : G.degree v = 3) (hp : G.Adj v p) (hq : G.Adj v q) (hr : G.Adj v r) (hpq : p ≠ q) (hpr : p ≠ r) (hqr : q ≠ r) (hw : G.Adj v w) : w = p ∨ w = q ∨ w = r

A degree-3 vertex with three known distinct neighbours has no others.

theorem ACMax.deg4_nbr_pin {V : Type u_1} [Fintype V] (G : SimpleGraph V) {g p q r s w : V} (hdg : G.degree g = 4) (hp : G.Adj g p) (hq : G.Adj g q) (hr : G.Adj g r) (hs : G.Adj g s) (hpq : p ≠ q) (hpr : p ≠ r) (hps : p ≠ s) (hqr : q ≠ r) (hqs : q ≠ s) (hrs : r ≠ s) (hw : G.Adj g w) : w = p ∨ w = q ∨ w = r ∨ w = s

A degree-4 vertex with four known distinct neighbours has no others.

theorem ACMax.not_iso_of_mnbr {V : Type u_1} [Fintype V] (G : SimpleGraph V) {v w : V} (hvw : G.Adj v w) (hw3 : G.degree w = 3) : v ∉ isoTwins G

An M-vertex (a degree-3 vertex with a degree-3 neighbour) is not iso.

theorem ACMax.deg3_not_adj_iso {V : Type u_1} [Fintype V] (G : SimpleGraph V) {v t : V} (hv3 : G.degree v = 3) (ht : t ∈ isoTwins G) : ¬G.Adj v t

An iso twin is adjacent to no degree-3 vertex (symmetric form).

The exclusion atoms (F0 / F1 / F5 / the universal share bound)

theorem ACMax.deg3_triangle_false (n : ℕ) (hn : 6 ≤ n) (G : SimpleGraph (Fin n)) (hT : ¬HasGoodTriangle n G) {u v w : Fin n} (hdu : G.degree u = 3) (hdv : G.degree v = 3) (hdw : G.degree w = 3) (huv : G.Adj u v) (hvw : G.Adj v w) (huw : G.Adj u w) : False

F0: no triangle of degree-3 vertices (∑ = 9, good from n = 6).

theorem ACMax.hub_mnbrs_not_adj (n : ℕ) (hn : 9 ≤ n) (G : SimpleGraph (Fin n)) (hT : ¬HasGoodTriangle n G) {g t₁ t₂ : Fin n} (hdg : G.degree g ≤ 4) (hd₁ : G.degree t₁ = 3) (hd₂ : G.degree t₂ = 3) (h12 : G.Adj t₁ t₂) (hg1 : G.Adj g t₁) (hg2 : G.Adj g t₂) : False

F1: a degree-≤ 4 hub never sees both ends of an M-edge (∑ ≤ 10, good from n = 9).

theorem ACMax.hub_no_dist2_pair (n : ℕ) (hn : 11 ≤ n) (G : SimpleGraph (Fin n)) (hT : ¬HasGoodTriangle n G) (hC4 : ¬HasGoodC4 n G) {g v t₁ t₂ : Fin n} (hdg : G.degree g = 4) (hdv : G.degree v = 3) (hd₁ : G.degree t₁ = 3) (hd₂ : G.degree t₂ = 3) (hne : t₁ ≠ t₂) (hv1 : G.Adj v t₁) (hv2 : G.Adj v t₂) (hg1 : G.Adj g t₁) (hg2 : G.Adj g t₂) : False

F5: a degree-4 hub never sees two M-vertices at M-distance 2 (the C₄ g−t₁−v−t₂ has ∑ = 13, good from n = 11).

theorem ACMax.hubs_share_le_one (n : ℕ) (hn : 18 ≤ n) (G : SimpleGraph (Fin n)) (hT : ¬HasGoodTriangle n G) (hC4 : ¬HasGoodC4 n G) {g h : Fin n} (hdg : G.degree g = 4) (hdh : G.degree h = 4) (hne : g ≠ h) : (sharedTwins G g h).card ≤ 1

The universal share bound (n ≥ 18): two distinct degree-4 hubs share at most one degree-3 twin — adjacent twins die by the (4,3,3)-triangle, adjacent hubs by the (4,4,3)-triangle, and the rest by the ∑ = 14 good C₄.

theorem ACMax.hubs_share_two_false (n : ℕ) (hn : 18 ≤ n) (G : SimpleGraph (Fin n)) (hT : ¬HasGoodTriangle n G) (hC4 : ¬HasGoodC4 n G) {g h t₁ t₂ : Fin n} (hdg : G.degree g = 4) (hdh : G.degree h = 4) (hne : g ≠ h) (hne12 : t₁ ≠ t₂) (hd₁ : G.degree t₁ = 3) (hd₂ : G.degree t₂ = 3) (hg1 : G.Adj g t₁) (hh1 : G.Adj h t₁) (hg2 : G.Adj g t₂) (hh2 : G.Adj h t₂) : False

Two shared twins force False (extraction form of hubs_share_le_one).

The iso-twin supply and the corner pigeonhole

theorem ACMax.iso_card_of_cover {V : Type u_1} [Fintype V] (G : SimpleGraph V) (S : Finset V) (hS : ∀ (v : V), G.degree v = 3 → v ∉ S → v ∈ isoTwins G) : (deg3Set G).card ≤ (isoTwins G).card + S.card

Iso-twin supply through a covering set: if every degree-3 vertex outside S is iso, then |D| ≤ |Iso| + |S|.

theorem ACMax.corner_rich_bound {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) (hblock : ∀ t ∈ isoTwins G, 2 ≤ (badApexNbrs G x z y t).card) : 2 * (isoTwins G).card ≤ 2 * {w ∈ cherryHubs G x z y | 2 ≤ (isoNbrs G w).card}.card + (cherryHubs G x z y).card

The corner pigeonhole count (sea regime): if every iso twin is double-blocked, then 2·|Iso| ≤ 2·#(rich CT hubs) + |CT|.

theorem ACMax.corner_rich_one {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) (hblock : ∀ t ∈ isoTwins G, 2 ≤ (badApexNbrs G x z y t).card) (hIso : 3 ≤ (isoTwins G).card) : ∃ (g : V), G.degree g = 4 ∧ 2 ≤ (isoNbrs G g).card ∧ (G.Adj g z ∨ G.Adj g x ∨ G.Adj g y)

Extraction: with |Iso| ≥ 3, the corner provides a rich cherry-touching hub: degree exactly 4, ≥ 2 iso twins, adjacent to a cherry vertex.

theorem ACMax.corner_rich_two {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) (hblock : ∀ t ∈ isoTwins G, 2 ≤ (badApexNbrs G x z y t).card) (hIso : 4 ≤ (isoTwins G).card) : ∃ (g : V) (h : V), g ≠ h ∧ (G.degree g = 4 ∧ 2 ≤ (isoNbrs G g).card ∧ (G.Adj g z ∨ G.Adj g x ∨ G.Adj g y)) ∧ G.degree h = 4 ∧ 2 ≤ (isoNbrs G h).card ∧ (G.Adj h z ∨ G.Adj h x ∨ G.Adj h y)

Extraction: with |Iso| ≥ 4, the corner provides two rich cherry-touching hubs.

theorem ACMax.rich_avoiding_twoBlock {V : Type u_1} [Fintype V] (G : SimpleGraph V) {g x' z' y' : V} (hch : Cherry G x' z' y') (hdg : G.degree g = 4) (hr : 2 ≤ (isoNbrs G g).card) (hnz : ¬G.Adj g z') (hnx : ¬G.Adj g x') (hny : ¬G.Adj g y') : TwoBlockConfig G

The TwoTwin fire: a degree-4 hub with ≥ 2 iso twins avoiding a cherry closes the graph (wrapper around two_twin_cherry_twoBlock).

theorem ACMax.cherryHubs_swap {V : Type u_1} [Fintype V] (G : SimpleGraph V) (x z y : V) : cherryHubs G x z y = cherryHubs G y z x

cherryHubs is symmetric in the two cherry ends.

theorem ACMax.badApexNbrs_swap {V : Type u_1} [Fintype V] (G : SimpleGraph V) (x z y t : V) : badApexNbrs G x z y t = badApexNbrs G y z x t

badApexNbrs is symmetric in the two cherry ends.

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

A Cherry with the two ends swapped.

The five M-shapes

Each shape structure records: the degrees, the M-edges, all pairwise distinctness, the M-neighbour pinning of every shape vertex (mnbr_*: its only degree-3 neighbours are its M-partners), and the isolation of every degree-3 vertex outside the shape (iso_rest). These are exactly the facts the classification tree produces and the kill lemmas consume.

structure ACMax.MShapeP4 {V : Type u_1} [Fintype V] (G : SimpleGraph V) (a b c d : V) : Prop

The P4 shape: M is the path a−b−c−d (plus iso twins).

• deg_a : G.degree a = 3
• deg_b : G.degree b = 3
• deg_c : G.degree c = 3
• deg_d : G.degree d = 3
• adj_ab : G.Adj a b
• adj_bc : G.Adj b c
• adj_cd : G.Adj c d
• ne_ac : a ≠ c
• ne_ad : a ≠ d
• ne_bd : b ≠ d
• mnbr_a (w : V) : G.Adj a w → G.degree w = 3 → w = b
• mnbr_b (w : V) : G.Adj b w → G.degree w = 3 → w = a ∨ w = c
• mnbr_c (w : V) : G.Adj c w → G.degree w = 3 → w = b ∨ w = d
• mnbr_d (w : V) : G.Adj d w → G.degree w = 3 → w = c
• iso_rest (v : V) : G.degree v = 3 → v ≠ a → v ≠ b → v ≠ c → v ≠ d → v ∈ isoTwins G

theorem ACMax.MShapeP4.nadj_ac {V : Type u_1} [Fintype V] {G : SimpleGraph V} {a b c d : V} (hs : MShapeP4 G a b c d) : ¬G.Adj a c

theorem ACMax.MShapeP4.nadj_bd {V : Type u_1} [Fintype V] {G : SimpleGraph V} {a b c d : V} (hs : MShapeP4 G a b c d) : ¬G.Adj b d

theorem ACMax.MShapeP4.rev {V : Type u_1} [Fintype V] {G : SimpleGraph V} {a b c d : V} (hs : MShapeP4 G a b c d) : MShapeP4 G d c b a

The reversed path is the same shape.

theorem ACMax.MShapeP4.a_not_iso {V : Type u_1} [Fintype V] {G : SimpleGraph V} {a b c d : V} (hs : MShapeP4 G a b c d) : a ∉ isoTwins G

theorem ACMax.MShapeP4.b_not_iso {V : Type u_1} [Fintype V] {G : SimpleGraph V} {a b c d : V} (hs : MShapeP4 G a b c d) : b ∉ isoTwins G

theorem ACMax.MShapeP4.c_not_iso {V : Type u_1} [Fintype V] {G : SimpleGraph V} {a b c d : V} (hs : MShapeP4 G a b c d) : c ∉ isoTwins G

theorem ACMax.MShapeP4.d_not_iso {V : Type u_1} [Fintype V] {G : SimpleGraph V} {a b c d : V} (hs : MShapeP4 G a b c d) : d ∉ isoTwins G

theorem ACMax.MShapeP4.iso_ge (n : ℕ) (hn : 8 ≤ n) (G' : SimpleGraph (Fin n)) {a b c d : Fin n} (hs : MShapeP4 G' a b c d) (hm : G'.edgeFinset.card = 2 * (n - 2)) (h3 : ∀ (v : Fin n), 3 ≤ G'.degree v) : 4 ≤ (isoTwins G').card

structure ACMax.MShapeClaw {V : Type u_1} [Fintype V] (G : SimpleGraph V) (z₀ x₁ x₂ x₃ : V) : Prop

The claw shape: M is K_{1,3} at centre z₀ with leaves x₁, x₂, x₃.

• deg_z : G.degree z₀ = 3
• deg_1 : G.degree x₁ = 3
• deg_2 : G.degree x₂ = 3
• deg_3 : G.degree x₃ = 3
• adj_1 : G.Adj z₀ x₁
• adj_2 : G.Adj z₀ x₂
• adj_3 : G.Adj z₀ x₃
• ne_12 : x₁ ≠ x₂
• ne_13 : x₁ ≠ x₃
• ne_23 : x₂ ≠ x₃
• mnbr_1 (w : V) : G.Adj x₁ w → G.degree w = 3 → w = z₀
• mnbr_2 (w : V) : G.Adj x₂ w → G.degree w = 3 → w = z₀
• mnbr_3 (w : V) : G.Adj x₃ w → G.degree w = 3 → w = z₀
• iso_rest (v : V) : G.degree v = 3 → v ≠ z₀ → v ≠ x₁ → v ≠ x₂ → v ≠ x₃ → v ∈ isoTwins G

structure ACMax.MShapeChair {V : Type u_1} [Fintype V] (G : SimpleGraph V) (q l₁ l₂ p e : V) : Prop

The chair shape: centre q with leaves l₁, l₂ and the path q−p−e.

• deg_q : G.degree q = 3
• deg_l₁ : G.degree l₁ = 3
• deg_l₂ : G.degree l₂ = 3
• deg_p : G.degree p = 3
• deg_e : G.degree e = 3
• adj_l₁ : G.Adj q l₁
• adj_l₂ : G.Adj q l₂
• adj_p : G.Adj q p
• adj_pe : G.Adj p e
• ne_l₁l₂ : l₁ ≠ l₂
• ne_l₁p : l₁ ≠ p
• ne_l₂p : l₂ ≠ p
• ne_l₁e : l₁ ≠ e
• ne_l₂e : l₂ ≠ e
• ne_qe : q ≠ e
• mnbr_l₁ (w : V) : G.Adj l₁ w → G.degree w = 3 → w = q
• mnbr_l₂ (w : V) : G.Adj l₂ w → G.degree w = 3 → w = q
• mnbr_p (w : V) : G.Adj p w → G.degree w = 3 → w = q ∨ w = e
• mnbr_e (w : V) : G.Adj e w → G.degree w = 3 → w = p
• iso_rest (v : V) : G.degree v = 3 → v ≠ q → v ≠ l₁ → v ≠ l₂ → v ≠ p → v ≠ e → v ∈ isoTwins G

structure ACMax.MShapeS22 {V : Type u_1} [Fintype V] (G : SimpleGraph V) (q₁ q₂ l₁ l₂ m₁ m₂ : V) : Prop

The S22 shape: the double star — adjacent centres q₁ ~ q₂ with leaves l₁, l₂ at q₁ and m₁, m₂ at q₂.

• deg_q₁ : G.degree q₁ = 3
• deg_q₂ : G.degree q₂ = 3
• deg_l₁ : G.degree l₁ = 3
• deg_l₂ : G.degree l₂ = 3
• deg_m₁ : G.degree m₁ = 3
• deg_m₂ : G.degree m₂ = 3
• adj_qq : G.Adj q₁ q₂
• adj_l₁ : G.Adj q₁ l₁
• adj_l₂ : G.Adj q₁ l₂
• adj_m₁ : G.Adj q₂ m₁
• adj_m₂ : G.Adj q₂ m₂
• ne_l₁l₂ : l₁ ≠ l₂
• ne_m₁m₂ : m₁ ≠ m₂
• ne_q₁m₁ : q₁ ≠ m₁
• ne_q₁m₂ : q₁ ≠ m₂
• ne_q₂l₁ : q₂ ≠ l₁
• ne_q₂l₂ : q₂ ≠ l₂
• ne_l₁m₁ : l₁ ≠ m₁
• ne_l₁m₂ : l₁ ≠ m₂
• ne_l₂m₁ : l₂ ≠ m₁
• ne_l₂m₂ : l₂ ≠ m₂
• mnbr_l₁ (w : V) : G.Adj l₁ w → G.degree w = 3 → w = q₁
• mnbr_l₂ (w : V) : G.Adj l₂ w → G.degree w = 3 → w = q₁
• mnbr_m₁ (w : V) : G.Adj m₁ w → G.degree w = 3 → w = q₂
• mnbr_m₂ (w : V) : G.Adj m₂ w → G.degree w = 3 → w = q₂
• iso_rest (v : V) : G.degree v = 3 → v ≠ q₁ → v ≠ q₂ → v ≠ l₁ → v ≠ l₂ → v ≠ m₁ → v ≠ m₂ → v ∈ isoTwins G

structure ACMax.MShapeC5 {V : Type u_1} [Fintype V] (G : SimpleGraph V) (v₀ v₁ v₂ v₃ v₄ : V) : Prop

The C5 shape: M is the 5-cycle v₀−v₁−v₂−v₃−v₄−v₀.

• deg_0 : G.degree v₀ = 3
• deg_1 : G.degree v₁ = 3
• deg_2 : G.degree v₂ = 3
• deg_3 : G.degree v₃ = 3
• deg_4 : G.degree v₄ = 3
• adj_01 : G.Adj v₀ v₁
• adj_12 : G.Adj v₁ v₂
• adj_23 : G.Adj v₂ v₃
• adj_34 : G.Adj v₃ v₄
• adj_40 : G.Adj v₄ v₀
• ne_02 : v₀ ≠ v₂
• ne_03 : v₀ ≠ v₃
• ne_13 : v₁ ≠ v₃
• ne_14 : v₁ ≠ v₄
• ne_24 : v₂ ≠ v₄
• mnbr_0 (w : V) : G.Adj v₀ w → G.degree w = 3 → w = v₁ ∨ w = v₄
• mnbr_1 (w : V) : G.Adj v₁ w → G.degree w = 3 → w = v₀ ∨ w = v₂
• mnbr_2 (w : V) : G.Adj v₂ w → G.degree w = 3 → w = v₁ ∨ w = v₃
• mnbr_3 (w : V) : G.Adj v₃ w → G.degree w = 3 → w = v₂ ∨ w = v₄
• mnbr_4 (w : V) : G.Adj v₄ w → G.degree w = 3 → w = v₃ ∨ w = v₀
• iso_rest (v : V) : G.degree v = 3 → v ≠ v₀ → v ≠ v₁ → v ≠ v₂ → v ≠ v₃ → v ≠ v₄ → v ∈ isoTwins G

The S22 kill: the double star splits into its two stars

P = {q₁, l₁, l₂} vs N = {q₂, m₁, m₂}: the only crossing edge is q₁q₂, each centre leaks ≤ 1, each leaf ≤ 2 — the exact tie 2·1 + 5 + 5 = 12 = 4·3. Unconditional: no corner, no sea, no n-threshold.

theorem ACMax.s22_split_twoBlock {V : Type u_1} [Fintype V] (G : SimpleGraph V) {q₁ q₂ l₁ l₂ m₁ m₂ : V} (hs : MShapeS22 G q₁ q₂ l₁ l₂ m₁ m₂) : TwoBlockConfig G

The S22 split.

The claw / chair / C5 kills: any rich hub TwoTwin-fires

By F1/F5 the M-neighbourhood of a degree-4 hub is a pairwise-M-distance-≥ 3 set — and in these three shapes every such set misses one of the shape's cherries, so a rich hub avoids a full cherry and two_twin_cherry_twoBlock fires. The corner pigeonhole (corner_rich_one) supplies the rich hub.

theorem ACMax.claw_rich_kill (n : ℕ) (hn : 18 ≤ n) (G : SimpleGraph (Fin n)) (hT : ¬HasGoodTriangle n G) (hC4 : ¬HasGoodC4 n G) {z₀ x₁ x₂ x₃ : Fin n} (hs : MShapeClaw G z₀ x₁ x₂ x₃) {g : Fin n} (hdg : G.degree g = 4) (hgr : 2 ≤ (isoNbrs G g).card) : TwoBlockConfig G

The claw rich-hub kill (unconditional in the rich hub).

theorem ACMax.chair_rich_kill (n : ℕ) (hn : 18 ≤ n) (G : SimpleGraph (Fin n)) (hT : ¬HasGoodTriangle n G) (hC4 : ¬HasGoodC4 n G) {q l₁ l₂ p e : Fin n} (hs : MShapeChair G q l₁ l₂ p e) {g : Fin n} (hdg : G.degree g = 4) (hgr : 2 ≤ (isoNbrs G g).card) : TwoBlockConfig G

The chair rich-hub kill.

theorem ACMax.c5_rich_kill (n : ℕ) (hn : 18 ≤ n) (G : SimpleGraph (Fin n)) (hT : ¬HasGoodTriangle n G) (hC4 : ¬HasGoodC4 n G) {v₀ v₁ v₂ v₃ v₄ : Fin n} (hs : MShapeC5 G v₀ v₁ v₂ v₃ v₄) {g : Fin n} (hdg : G.degree g = 4) (hgr : 2 ≤ (isoNbrs G g).card) : TwoBlockConfig G

The C5 rich-hub kill.

The P4 kill

The only shape with genuine corner escapers. Roles for a rich hub g (by F1/F5): B (~b only), C (~c only), A (~a ∧ ~d); anything else avoids the cherry (a,b,c) or (b,c,d) and is TT-killed. The corner pigeonhole gives two rich cherry-touching hubs, double roles are impossible, and each role pair fires an explicit cut.

theorem ACMax.p4_rich_role (n : ℕ) (hn : 18 ≤ n) (G : SimpleGraph (Fin n)) (hT : ¬HasGoodTriangle n G) (hC4 : ¬HasGoodC4 n G) {a b c d : Fin n} (hs : MShapeP4 G a b c d) {g : Fin n} (hdg : G.degree g = 4) (hgr : 2 ≤ (isoNbrs G g).card) : TwoBlockConfig G ∨ G.Adj g b ∧ ¬G.Adj g a ∧ ¬G.Adj g c ∧ ¬G.Adj g d ∨ G.Adj g c ∧ ¬G.Adj g a ∧ ¬G.Adj g b ∧ ¬G.Adj g d ∨ G.Adj g a ∧ G.Adj g d ∧ ¬G.Adj g b ∧ ¬G.Adj g c

The P4 role trichotomy for a rich degree-4 hub.

theorem ACMax.p4_pair_BA (n : ℕ) (hn : 18 ≤ n) (G : SimpleGraph (Fin n)) (hT : ¬HasGoodTriangle n G) (hC4 : ¬HasGoodC4 n G) {a b c d : Fin n} (hs : MShapeP4 G a b c d) {β α : Fin n} (hβ4 : G.degree β = 4) (hβr : 2 ≤ (isoNbrs G β).card) (hβb : G.Adj β b) (hβa : ¬G.Adj β a) : ¬G.Adj β c → ∀ (hβd : ¬G.Adj β d) (hα4 : G.degree α = 4) (hαr : 2 ≤ (isoNbrs G α).card) (hαa : G.Adj α a) (hαd : G.Adj α d) (hαb : ¬G.Adj α b), ¬G.Adj α c → TwoBlockConfig G

The (B,A) pair cut: P = {α, d, k} vs N = {β, b, i} — the opposite-twin two-hub cut with the M-vertices d and b as twins.

theorem ACMax.p4_pair_CA (n : ℕ) (hn : 18 ≤ n) (G : SimpleGraph (Fin n)) (hT : ¬HasGoodTriangle n G) (hC4 : ¬HasGoodC4 n G) {a b c d : Fin n} (hs : MShapeP4 G a b c d) {γ α : Fin n} (hγ4 : G.degree γ = 4) (hγr : 2 ≤ (isoNbrs G γ).card) (hγc : G.Adj γ c) (hγa : ¬G.Adj γ a) (hγb : ¬G.Adj γ b) (hγd : ¬G.Adj γ d) (hα4 : G.degree α = 4) (hαr : 2 ≤ (isoNbrs G α).card) (hαa : G.Adj α a) (hαd : G.Adj α d) (hαb : ¬G.Adj α b) (hαc : ¬G.Adj α c) : TwoBlockConfig G

The (C,A) pair cut: P = {α, a, k} vs N = {γ, c, j}.

theorem ACMax.p4_rich_ahub (n : ℕ) (hn : 18 ≤ n) (G : SimpleGraph (Fin n)) (hT : ¬HasGoodTriangle n G) (hC4 : ¬HasGoodC4 n G) {a b c d : Fin n} (hs : MShapeP4 G a b c d) {α : Fin n} (hα4 : G.degree α = 4) (hαr : 2 ≤ (isoNbrs G α).card) (hαa : G.Adj α a) : TwoBlockConfig G ∨ G.Adj α a ∧ G.Adj α d ∧ ¬G.Adj α b ∧ ¬G.Adj α c

A rich a-hub is TT-killed or is an α* (role A).

theorem ACMax.p4_ahubs (n : ℕ) (G : SimpleGraph (Fin n)) (hmin : ∀ (v : Fin n), 3 ≤ G.degree v) (hsea : ∀ (v : Fin n), G.degree v ≤ 4) {a b c d : Fin n} (hs : MShapeP4 G a b c d) : ∃ (α₁ : Fin n) (α₂ : Fin n), α₁ ≠ α₂ ∧ G.Adj a α₁ ∧ G.Adj a α₂ ∧ G.degree α₁ = 4 ∧ G.degree α₂ = 4 ∧ ∀ (w : Fin n), G.Adj a w → 4 ≤ G.degree w → w = α₁ ∨ w = α₂

The two hubs of a (endpoint of the path).

theorem ACMax.p4_bpin {V : Type u_1} [Fintype V] (G : SimpleGraph V) {a b c d : V} (hs : MShapeP4 G a b c d) {β w : V} (hβb : G.Adj β b) (hβ4 : G.degree β = 4) (hw : G.Adj w b) (hw4 : 4 ≤ G.degree w) : w = β

Any degree-≥ 4 hub of b equals the given one (b has one hub slot).

theorem ACMax.p4_cpin {V : Type u_1} [Fintype V] (G : SimpleGraph V) {a b c d : V} (hs : MShapeP4 G a b c d) {γ w : V} (hγc : G.Adj γ c) (hγ4 : G.degree γ = 4) (hw : G.Adj w c) (hw4 : 4 ≤ G.degree w) : w = γ

Any degree-≥ 4 hub of c equals the given one.

theorem ACMax.badApex_two {V : Type u_1} [Fintype V] (G : SimpleGraph V) (hsea : ∀ (v : V), G.degree v ≤ 4) {x z y t : V} (h2 : 2 ≤ (badApexNbrs G x z y t).card) : ∃ (w₁ : V) (w₂ : V), w₁ ≠ w₂ ∧ (G.Adj t w₁ ∧ 4 ≤ G.degree w₁ ∧ (G.Adj w₁ z ∨ G.Adj w₁ x ∨ G.Adj w₁ y)) ∧ G.Adj t w₂ ∧ 4 ≤ G.degree w₂ ∧ (G.Adj w₂ z ∨ G.Adj w₂ x ∨ G.Adj w₂ y)

Unpack two distinct bad-apex neighbours (sea regime: both cherry-touching).

theorem ACMax.p4_pair_BC (n : ℕ) (hn : 18 ≤ n) (G : SimpleGraph (Fin n)) (hT : ¬HasGoodTriangle n G) (hC4 : ¬HasGoodC4 n G) (hmin : ∀ (v : Fin n), 3 ≤ G.degree v) (hsea : ∀ (v : Fin n), G.degree v ≤ 4) {a b c d : Fin n} (hs : MShapeP4 G a b c d) (hblock : ∀ t ∈ isoTwins G, 2 ≤ (badApexNbrs G a b c t).card) (hIso : 4 ≤ (isoTwins G).card) {β γ : Fin n} (hβ4 : G.degree β = 4) (hβr : 2 ≤ (isoNbrs G β).card) (hβb : G.Adj β b) (hβa : ¬G.Adj β a) (hβc : ¬G.Adj β c) (hβd : ¬G.Adj β d) (hγ4 : G.degree γ = 4) (hγr : 2 ≤ (isoNbrs G γ).card) (hγc : G.Adj γ c) : ¬G.Adj γ a → ∀ (hγb : ¬G.Adj γ b), ¬G.Adj γ d → TwoBlockConfig G

The (B,C) pair closes — private pair, or a pinch/adjacency counting rederivation of a rich a-hub feeding p4_pair_BA.

theorem ACMax.p4_close_main (n : ℕ) (hn : 18 ≤ n) (G : SimpleGraph (Fin n)) (hT : ¬HasGoodTriangle n G) (hC4 : ¬HasGoodC4 n G) (hmin : ∀ (v : Fin n), 3 ≤ G.degree v) (hsea : ∀ (v : Fin n), G.degree v ≤ 4) {a b c d : Fin n} (hs : MShapeP4 G a b c d) (hIso : 4 ≤ (isoTwins G).card) (hblock : ∀ t ∈ isoTwins G, 2 ≤ (badApexNbrs G a b c t).card) : TwoBlockConfig G

The P4 main tree (cherry normalized to (a, b, c)).

theorem ACMax.p4_corner_close (n : ℕ) (hn : 18 ≤ n) (G : SimpleGraph (Fin n)) (h : ResidualCore n G) (hsea : ∀ (v : Fin n), G.degree v ≤ 4) {a b c d : Fin n} (hs : MShapeP4 G a b c d) {x z y : Fin n} (hch : Cherry G x z y) (hblock : ∀ t ∈ isoTwins G, 2 ≤ (badApexNbrs G x z y t).card) : TwoBlockConfig G

The P4 corner closure (arbitrary blocked cherry): normalize the cherry position by the path reversal and end swap, then run the main tree.

The M-shape classification

Under ¬goodTriangle (n ≥ 6), ¬goodC4 (n ≥ 8) and ¬deg3-2K₂, the degree-3 graph with e(M) ≥ 3 is exactly one of the five shapes. The tree: a vertex of M-degree 3 exists (→ claw / chair / S22, by the third-neighbour case analysis) or not (→ P4 / C5, growing the cherry to a path).

theorem ACMax.mC4_false (n : ℕ) (hn : 8 ≤ n) (G : SimpleGraph (Fin n)) (hT : ¬HasGoodTriangle n G) (hC4 : ¬HasGoodC4 n G) {p q r s : Fin n} (h3p : G.degree p = 3) (h3q : G.degree q = 3) (h3r : G.degree r = 3) (h3s : G.degree s = 3) (hpq : G.Adj p q) (hqr : G.Adj q r) (hrs : G.Adj r s) (hsp : G.Adj s p) (hpr : p ≠ r) (hqs : q ≠ s) : False

No 4-cycle among degree-3 vertices (diagonals die by the degree-3 triangle, the induced cycle by the ∑ = 12 good C₄, n ≥ 8).

theorem ACMax.cross_of_no2K2 (n : ℕ) (G : SimpleGraph (Fin n)) (h2k2 : ¬HasDeg3Ind2K2 n G) {u v p q : Fin n} (hu : G.degree u = 3) (hv : G.degree v = 3) (hp : G.degree p = 3) (hq : G.degree q = 3) (huv : G.Adj u v) (hpq : G.Adj p q) (hup : u ≠ p) (huq : u ≠ q) (hvp : v ≠ p) (hvq : v ≠ q) : G.Adj u p ∨ G.Adj u q ∨ G.Adj v p ∨ G.Adj v q

Two vertex-disjoint M-edges have a crossing M-edge (no induced 2K₂).

theorem ACMax.outside_iso (n : ℕ) (G : SimpleGraph (Fin n)) (h2k2 : ¬HasDeg3Ind2K2 n G) (P : Fin n → Prop) {p q : Fin n} (hp3 : G.degree p = 3) (hq3 : G.degree q = 3) (hpq : G.Adj p q) (hpP : P p) (hqP : P q) (hclosed : ∀ (u w : Fin n), P u → G.degree u = 3 → G.degree w = 3 → G.Adj u w → P w) {v : Fin n} (hv3 : G.degree v = 3) (hvP : ¬P v) : v ∈ isoTwins G

Outside vertices are iso: every shape-closed predicate P holding on an M-edge p−q isolates all degree-3 vertices outside P (any outside M-edge would be an induced 2K₂ against p−q).

theorem ACMax.classify_branch1 (n : ℕ) (hn : 8 ≤ n) (G : SimpleGraph (Fin n)) (hT : ¬HasGoodTriangle n G) (hC4 : ¬HasGoodC4 n G) (h2k2 : ¬HasDeg3Ind2K2 n G) {v₀ w₁ w₂ w₃ p : Fin n} (h0 : G.degree v₀ = 3) (h1 : G.degree w₁ = 3) (h2 : G.degree w₂ = 3) (h3 : G.degree w₃ = 3) (hp3 : G.degree p = 3) (ha1 : G.Adj v₀ w₁) (ha2 : G.Adj v₀ w₂) (ha3 : G.Adj v₀ w₃) (h12 : w₁ ≠ w₂) (h13 : w₁ ≠ w₃) (h23 : w₂ ≠ w₃) (hap : G.Adj w₁ p) (hpv : p ≠ v₀) : (∃ (q : Fin n) (l₁ : Fin n) (l₂ : Fin n) (p' : Fin n) (e' : Fin n), MShapeChair G q l₁ l₂ p' e') ∨ ∃ (q₁ : Fin n) (q₂ : Fin n) (l₁ : Fin n) (l₂ : Fin n) (m₁ : Fin n) (m₂ : Fin n), MShapeS22 G q₁ q₂ l₁ l₂ m₁ m₂

The extended-centre branch: a degree-3 claw centre whose leaf w₁ has a further M-neighbour p gives the chair or the S22.

theorem ACMax.classify_center3 (n : ℕ) (hn : 8 ≤ n) (G : SimpleGraph (Fin n)) (hT : ¬HasGoodTriangle n G) (hC4 : ¬HasGoodC4 n G) (h2k2 : ¬HasDeg3Ind2K2 n G) {v₀ w₁ w₂ w₃ : Fin n} (h0 : G.degree v₀ = 3) (h1 : G.degree w₁ = 3) (h2 : G.degree w₂ = 3) (h3 : G.degree w₃ = 3) (ha1 : G.Adj v₀ w₁) (ha2 : G.Adj v₀ w₂) (ha3 : G.Adj v₀ w₃) (h12 : w₁ ≠ w₂) (h13 : w₁ ≠ w₃) (h23 : w₂ ≠ w₃) : (∃ (z₀ : Fin n) (x₁ : Fin n) (x₂ : Fin n) (x₃ : Fin n), MShapeClaw G z₀ x₁ x₂ x₃) ∨ (∃ (q : Fin n) (l₁ : Fin n) (l₂ : Fin n) (p' : Fin n) (e' : Fin n), MShapeChair G q l₁ l₂ p' e') ∨ ∃ (q₁ : Fin n) (q₂ : Fin n) (l₁ : Fin n) (l₂ : Fin n) (m₁ : Fin n) (m₂ : Fin n), MShapeS22 G q₁ q₂ l₁ l₂ m₁ m₂

Case I of the classification: a vertex of M-degree 3 gives the claw, the chair, or the S22.

theorem ACMax.classify_path_ext (n : ℕ) (hn : 8 ≤ n) (G : SimpleGraph (Fin n)) (hT : ¬HasGoodTriangle n G) (hC4 : ¬HasGoodC4 n G) (h2k2 : ¬HasDeg3Ind2K2 n G) (hno3 : ∀ (v u₁ u₂ u₃ : Fin n), G.degree v = 3 → G.degree u₁ = 3 → G.degree u₂ = 3 → G.degree u₃ = 3 → G.Adj v u₁ → G.Adj v u₂ → G.Adj v u₃ → u₁ ≠ u₂ → u₁ ≠ u₃ → u₂ ≠ u₃ → False) {x z y a : Fin n} (hch : Cherry G x z y) (hxa : G.Adj x a) (ha3 : G.degree a = 3) (haz : a ≠ z) : (∃ (a' : Fin n) (b' : Fin n) (c' : Fin n) (d' : Fin n), MShapeP4 G a' b' c' d') ∨ ∃ (v₀ : Fin n) (v₁ : Fin n) (v₂ : Fin n) (v₃ : Fin n) (v₄ : Fin n), MShapeC5 G v₀ v₁ v₂ v₃ v₄

Case II of the classification (no M-degree-3 vertex): the cherry with an end extension gives the P4 or the C5.

theorem ACMax.third_edge_of_mIncidence (n : ℕ) (G : SimpleGraph (Fin n)) {x z y : Fin n} (hch : Cherry G x z y) (heM : 5 ≤ mIncidence G) : ∃ (u : Fin n) (v : Fin n), G.degree u = 3 ∧ G.degree v = 3 ∧ G.Adj u v ∧ v ≠ x ∧ v ≠ z ∧ v ≠ y

With mIncidence ≥ 5 some M-edge leaves the cherry.

theorem ACMax.mshape_classify (n : ℕ) (hn : 8 ≤ n) (G : SimpleGraph (Fin n)) (hT : ¬HasGoodTriangle n G) (hC4 : ¬HasGoodC4 n G) (h2k2 : ¬HasDeg3Ind2K2 n G) {x z y : Fin n} (hch : Cherry G x z y) (heM : 5 ≤ mIncidence G) : (∃ (a : Fin n) (b : Fin n) (c : Fin n) (d : Fin n), MShapeP4 G a b c d) ∨ (∃ (z₀ : Fin n) (x₁ : Fin n) (x₂ : Fin n) (x₃ : Fin n), MShapeClaw G z₀ x₁ x₂ x₃) ∨ (∃ (q : Fin n) (l₁ : Fin n) (l₂ : Fin n) (p : Fin n) (e : Fin n), MShapeChair G q l₁ l₂ p e) ∨ (∃ (q₁ : Fin n) (q₂ : Fin n) (l₁ : Fin n) (l₂ : Fin n) (m₁ : Fin n) (m₂ : Fin n), MShapeS22 G q₁ q₂ l₁ l₂ m₁ m₂) ∨ ∃ (v₀ : Fin n) (v₁ : Fin n) (v₂ : Fin n) (v₃ : Fin n) (v₄ : Fin n), MShapeC5 G v₀ v₁ v₂ v₃ v₄

THE M-SHAPE CLASSIFICATION: under the residual exclusions, a cherry and mIncidence ≥ 5 force the degree-3 graph to be exactly one of the five shapes (each with all other degree-3 vertices iso).

The assembly: the e(M) ≥ 3 corner closure and the full Δ ≤ 4 C0

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

THE BLOCKED CHERRY CORNER CLOSES for e(M) ≥ 3 (mIncidence ≥ 5), in the sea regime, for every n ≥ 18: classify the M-shape and run the per-shape kill.

theorem ACMax.caseCherry_algConn_le_two_of_sea (n : ℕ) [Nonempty (Fin n)] (hn : 18 ≤ n) (G : SimpleGraph (Fin n)) (h : ResidualCore n G) (hsea : ∀ (v : Fin n), G.degree v ≤ 4) (hcc : CaseCherry G) : algConn G ≤ 2

THE COMPLETE Δ ≤ 4 C0 CLOSURE: a ResidualCore graph with Δ ≤ 4 in the cherry world (CaseCherry, i.e. e(M) ≥ 2) has algConn G ≤ 2, unconditionally, for every n ≥ 18 — combining the e(M) = 2 closure caseCherry_algConn_le_two_of_sea_eM_four with the e(M) ≥ 3 shape closure above.

The complete Δ ≤ 4 sea closure

Assembles the Δ ≤ 4 sub-cases of ResidualCore into residual_sea_algConn_le_two, dispatched by eM_trichotomy on mIncidence G (= 2·e(M)): e(M) ≤ 1 (the poor corner) via x0_corner_close, and CaseCherry (e(M) ≥ 2) via caseCherry_algConn_le_two_of_sea.

theorem ACMax.residual_sea_algConn_le_two (n : ℕ) [Nonempty (Fin n)] (hn : 23 ≤ n) (G : SimpleGraph (Fin n)) (h : ResidualCore n G) (hsea : ∀ (v : Fin n), G.degree v ≤ 4) : algConn G ≤ 2

The complete Δ ≤ 4 closure of the general ACMAX residual. For every n ≥ 23, a ResidualCore graph on Fin n whose maximum degree is at most 4 has algConn G ≤ 2. Assembled from the poor-corner service bound (x0_corner_close) and the complete cherry closure (caseCherry_algConn_le_two_of_sea) via eM_trichotomy.