The far-pair closure of the poor corner

Closes the x = 0, e(M) ≤ 1 corner (all degrees 3 or 4, exactly 8 degree-3 vertices, no good triangle Σ ≤ 11, no good C₄ Σ ≤ 14) for every n ≥ 18, by exhibiting a far degree-3 pair on which a test-vector certificate bounds algebraic connectivity by 2.

Main results

• algConn_le_two_of_far_deg3_pair — the uniform workhorse: the integer test vector (6, 2·𝟙_{N(t)}, −6, −2·𝟙_{N(t')}) certifies algConn G ≤ 2 for any two degree-3 vertices t, t' at distance ≥ 3 with all neighbour degrees ≤ 4 and at most 3 cross edges between N(t) and N(t'). The worst-case Rayleigh numerator is Q ≤ 168 + 8c ≤ 192 = 2N, an exact tie at c = 3, shape-independent in the cross pattern.
• exists_far_deg3_pair — some two degree-3 vertices are at distance ≥ 3. If every pair were within distance 2, the twins and their hubs would form a linear space; the fibre profiles force four size-4 lines carrying all eight points, and 8 > C(4,2) = 6 yields two lines sharing two points, a contradiction.
• exists_far_deg3_pair_lowcross — some far pair has cross count ≤ 3, feeding the workhorse directly. Assuming every far pair has cross ≥ 4, the far pair from exists_far_deg3_pair has either an M-end endpoint (killed by Lemma E, service_count_end) or two iso endpoints (killed by Lemma S, service_count_iso); both are omega-impossible service-supply counts over the φ-slot budgets phi_iso / phi_end.
• x0_corner_close — the corner closure algConn G ≤ 2 for every n ≥ 23, assembled from the three results above.

theorem ACMax.algConn_le_two_of_far_deg3_pair {V : Type u_1} [Fintype V] [Nonempty V] (G : SimpleGraph V) (t t' : V) (hne : t ≠ t') (hnadj : ¬G.Adj t t') (hcap : ∀ (w : V), ¬(G.Adj t w ∧ G.Adj t' w)) (hdt : G.degree t = 3) (hdt' : G.degree t' = 3) (hnb : ∀ (w : V), G.Adj t w → G.degree w ≤ 4) (hnb' : ∀ (w : V), G.Adj t' w → G.degree w ≤ 4) (hcross : ∑ w ∈ G.neighborFinset t, (G.neighborFinset w ∩ G.neighborFinset t').card ≤ 3) : algConn G ≤ 2

The uniform far-deg-3-pair certificate (B1+B3 unified). Two degree-3 vertices at distance ≥ 3 (combinatorially: distinct, non-adjacent, no common neighbour), all of whose neighbours have degree ≤ 4, with at most 3 cross edges between their neighbourhoods, certify algConn G ≤ 2 via the integer vector (6, 2·𝟙_{N(t)}, −6, −2·𝟙_{N(t')}). Worst case Q = 168 + 8c ≤ 192 = 2N (tie at c = 3), independent of the cross-pattern shape.

Existence of a far twin pair

theorem ACMax.exists_far_deg3_pair (n : ℕ) (hn : 18 ≤ n) (G : SimpleGraph (Fin n)) (hm : G.edgeFinset.card = 2 * (n - 2)) (hdeg : ∀ (v : Fin n), G.degree v = 3 ∨ G.degree v = 4) (hT : ¬HasGoodTriangle n G) (hC4 : ¬HasGoodC4 n G) (heM : ∑ z : Fin n with G.degree z = 3, (G.neighborFinset z ∩ {v : Fin n | G.degree v = 3}).card ≤ 2) : ∃ (s : Fin n) (t : Fin n), G.degree s = 3 ∧ G.degree t = 3 ∧ s ≠ t ∧ ¬G.Adj s t ∧ ∀ (w : Fin n), ¬(G.Adj s w ∧ G.Adj t w)

Lemma B2. In the x = 0, e(M) ≤ 1 corner (n ≥ 18): all degrees 3 or 4, 2(n−2) edges (hence exactly 8 degree-3 vertices), no good triangle, no good C₄, and at most one edge inside the degree-3 set (Σ_{z∈D}|N(z)∩D| ≤ 2), some two degree-3 vertices are at distance ≥ 3: distinct, non-adjacent, with no common neighbour. Proof: otherwise twins + multi-twin hubs form a linear space; fibre partition forces per-point profiles, incidence double counts force the design (α, β, γ) = (4, 0, 4) resp. (4, 0, 3), and the Σ C(r₄,2) = 8 > C(4,2) = 6 pigeonhole gives two 4-lines sharing two twins — a forbidden induced C₄.

The service-bound counting closure (Lemmas S and E)

The service bound behind exists_far_deg3_pair_lowcross. Assuming every far pair has cross ≥ 4, the far pair from exists_far_deg3_pair has an endpoint that is either an M-end or iso. Lemma E (service_count_end) rules out the M-end via demand ≥ 3k₀ against slot budget B₀ = k₀ (phi_end) and pair budget 6x + y ≤ k₀² − k₀. Lemma S (service_count_iso) rules out the iso side via demand ≥ 4k − 1 against B = k + 2 (phi_iso) and 6x + y ≤ k² − k (service_supply); omega closes both endgames (service_endgame_end, service_endgame_iso). The section builds the vocabulary, threshold bricks, corner structure, mediator swap, service supply, deg-3 bonus and φ-identities these two lemmas consume.

Vocabulary: the far set of a degree-3 vertex

noncomputable def ACMax.farOf (n : ℕ) (G : SimpleGraph (Fin n)) (t : Fin n) : Finset (Fin n)

farOf n G t: the degree-3 vertices at combinatorial distance ≥ 3 from t (distinct, non-adjacent, no common neighbour).

Equations

• ACMax.farOf n G t = {s : Fin n | G.degree s = 3 ∧ s ≠ t ∧ ¬G.Adj t s ∧ ∀ (w : Fin n), ¬(G.Adj t w ∧ G.Adj s w)}

theorem ACMax.mem_farOf {n : ℕ} {G : SimpleGraph (Fin n)} {t s : Fin n} : s ∈ farOf n G t ↔ G.degree s = 3 ∧ s ≠ t ∧ ¬G.Adj t s ∧ ∀ (w : Fin n), ¬(G.Adj t w ∧ G.Adj s w)

Threshold bricks (tri-11 / C4-14, valid for all n ≥ 18)

theorem ACMax.tri11_false {n : ℕ} (hn : 18 ≤ n) {G : SimpleGraph (Fin n)} (hT : ¬HasGoodTriangle n G) {x y z : Fin n} (hxy : G.Adj x y) (hyz : G.Adj y z) (hxz : G.Adj x z) (hsum : G.degree x + G.degree y + G.degree z ≤ 11) : False

No good triangle: a triangle with degree sum ≤ 11 is impossible (n ≥ 18).

theorem ACMax.c4_14_false {n : ℕ} (hn : 16 ≤ n) {G : SimpleGraph (Fin n)} (hC4 : ¬HasGoodC4 n G) {a b c d : Fin n} (hcard : {a, b, c, d}.card = 4) (hab : G.Adj a b) (hbc : G.Adj b c) (hcd : G.Adj c d) (hda : G.Adj d a) (hac : ¬G.Adj a c) (hbd : ¬G.Adj b d) (hsum : G.degree a + G.degree b + G.degree c + G.degree d ≤ 14) : False

No good C₄: an induced C₄ with degree sum ≤ 14 is impossible (n ≥ 16).

theorem ACMax.twin_common_unique {n : ℕ} (hn : 18 ≤ n) {G : SimpleGraph (Fin n)} (hT : ¬HasGoodTriangle n G) (hC4 : ¬HasGoodC4 n G) (hdeg4 : ∀ (v : Fin n), G.degree v ≤ 4) {s z : Fin n} (hs : G.degree s = 3) (hz : G.degree z = 3) (hsz : s ≠ z) (w w' : Fin n) : G.Adj s w → G.Adj z w → G.Adj s w' → G.Adj z w' → w = w'

F2/F3 combined — twin-pair common-neighbour uniqueness: two distinct degree-3 vertices have at most one common neighbour (elementwise form). Adjacent pairs actually share none (good triangle at Σ ≤ 10); non-adjacent pairs share at most one (good triangle at Σ ≤ 11 / good C₄ at Σ ≤ 14).

theorem ACMax.twin_common_card_le_one {n : ℕ} (hn : 18 ≤ n) {G : SimpleGraph (Fin n)} (hT : ¬HasGoodTriangle n G) (hC4 : ¬HasGoodC4 n G) (hdeg4 : ∀ (v : Fin n), G.degree v ≤ 4) {s z : Fin n} (hs : G.degree s = 3) (hz : G.degree z = 3) (hsz : s ≠ z) : (G.neighborFinset s ∩ G.neighborFinset z).card ≤ 1

Cardinality form of twin_common_unique.

The corner degree-3 set and the unique M-edge

theorem ACMax.corner_deg3_card (n : ℕ) (hn : 18 ≤ n) (G : SimpleGraph (Fin n)) (hm : G.edgeFinset.card = 2 * (n - 2)) (hdeg : ∀ (v : Fin n), G.degree v = 3 ∨ G.degree v = 4) : {v : Fin n | G.degree v = 3}.card = 8

In the x = 0 corner (∑deg = 4n − 8, degrees ∈ {3,4}) there are exactly 8 degree-3 vertices.

theorem ACMax.three_deg3_sum_le {n : ℕ} {G : SimpleGraph (Fin n)} {D : Finset (Fin n)} (heM : ∑ z ∈ D, (G.neighborFinset z ∩ D).card ≤ 2) {a b c : Fin n} (haD : a ∈ D) (hbD : b ∈ D) (hcD : c ∈ D) (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) : (G.neighborFinset a ∩ D).card + (G.neighborFinset b ∩ D).card + (G.neighborFinset c ∩ D).card ≤ 2

Three distinct degree-3 vertices: their internal-degree sum obeys the heM budget.

theorem ACMax.m_edge_unique {n : ℕ} {G : SimpleGraph (Fin n)} {D : Finset (Fin n)} (hD : ∀ (v : Fin n), v ∈ D ↔ G.degree v = 3) (heM : ∑ z ∈ D, (G.neighborFinset z ∩ D).card ≤ 2) {a b : Fin n} (ha : G.degree a = 3) (hb : G.degree b = 3) (hab : G.Adj a b) (z u : Fin n) : G.degree z = 3 → G.degree u = 3 → G.Adj z u → z = a ∧ u = b ∨ z = b ∧ u = a

The unique M-edge: under e(M) ≤ 1 (the heM sum form), once one edge inside the degree-3 set is known, every degree-3–degree-3 edge coincides with it.

theorem ACMax.mend_nbr_inter_deg3 {n : ℕ} {G : SimpleGraph (Fin n)} {D : Finset (Fin n)} (hD : ∀ (v : Fin n), v ∈ D ↔ G.degree v = 3) (heM : ∑ z ∈ D, (G.neighborFinset z ∩ D).card ≤ 2) {e₀ e₁ : Fin n} (he₀ : G.degree e₀ = 3) (he₁ : G.degree e₁ = 3) (hadj : G.Adj e₀ e₁) : G.neighborFinset e₀ ∩ D = {e₁}

An M-end's degree-3 neighbourhood is exactly its partner.

The mediator regrouping (the anchor swap)

theorem ACMax.sum_inter_add_sum_diff' {n : ℕ} (s t : Finset (Fin n)) (f : Fin n → ℕ) : ∑ w ∈ s ∩ t, f w + ∑ w ∈ s \ t, f w = ∑ w ∈ s, f w

Splitting a sum at a cut set: ∑_{s∩t} + ∑_{s∖t} = ∑_s.

theorem ACMax.anchor_swap {n : ℕ} (G : SimpleGraph (Fin n)) (H S : Finset (Fin n)) (f : Fin n → ℕ) : ∑ h ∈ H, ∑ w ∈ G.neighborFinset h ∩ S, f w = ∑ w ∈ S, (G.neighborFinset w ∩ H).card * f w

Anchor swap: a double sum over slots (h, w ∈ N(h) ∩ S) of a mediator-only weight, regrouped by the mediator.

theorem ACMax.service_decomp {n : ℕ} (G : SimpleGraph (Fin n)) (H F D : Finset (Fin n)) : ∑ s ∈ F, ∑ h ∈ H, (G.neighborFinset h ∩ G.neighborFinset s).card = ∑ h ∈ H, ∑ w ∈ G.neighborFinset h ∩ D, (G.neighborFinset w ∩ F).card + ∑ h ∈ H, ∑ w ∈ G.neighborFinset h \ D, (G.neighborFinset w ∩ F).card

The triple double count: the total cross of F against the anchor H, regrouped by mediator and split at the degree-3 set D.

The service supply bound (shared core of Lemmas S and E)

theorem ACMax.service_supply {n : ℕ} (G : SimpleGraph (Fin n)) {D : Finset (Fin n)} (hD : ∀ (v : Fin n), v ∈ D ↔ G.degree v = 3) (hdeg : ∀ (v : Fin n), G.degree v = 3 ∨ G.degree v = 4) (H F : Finset (Fin n)) (hH4 : ∀ h ∈ H, G.degree h = 4) (hF3 : ∀ s ∈ F, G.degree s = 3) (huniq : ∀ s ∈ F, ∀ s' ∈ F, s ≠ s' → ∀ (w w' : Fin n), G.Adj s w → G.Adj s' w → G.Adj s w' → G.Adj s' w' → w = w') : ∃ (x : ℕ) (y : ℕ), x + y ≤ ∑ h ∈ H, (G.neighborFinset h \ D).card ∧ 6 * x + y ≤ F.card * F.card - F.card ∧ ∑ h ∈ H, ∑ w ∈ G.neighborFinset h \ D, (G.neighborFinset w ∩ F).card ≤ ∑ h ∈ H, (G.neighborFinset h \ D).card + 2 * x + y

The service supply bound. For an anchor set H of degree-4 vertices and a target set F of degree-3 vertices any two of which share at most one common neighbour, the deg-4-mediated service ∑_{h∈H} ∑_{w∈N(h)∖D} |N(w) ∩ F| is at most B + 2x + y for slot masses x + y ≤ B := ∑_{h∈H} |N(h)∖D| obeying the pair budget 6x + y ≤ |F|² − |F|. (x/y = slot mass on mediators serving 3/2 far partners; the coupling m(w) + v(w) ≤ 4 and the pair budget ∑ v(v−1) ≤ k(k−1) are the two nontrivial inputs.)

The degree-3 bonus bounds

theorem ACMax.bonus_le_one_iso {n : ℕ} (hn : 18 ≤ n) {G : SimpleGraph (Fin n)} (hT : ¬HasGoodTriangle n G) (hC4 : ¬HasGoodC4 n G) (hdeg4 : ∀ (v : Fin n), G.degree v ≤ 4) {D : Finset (Fin n)} (hD : ∀ (v : Fin n), v ∈ D ↔ G.degree v = 3) (heM : ∑ z ∈ D, (G.neighborFinset z ∩ D).card ≤ 2) {t : Fin n} (ht : G.degree t = 3) {F : Finset (Fin n)} (hF3 : ∀ s ∈ F, G.degree s = 3) (hFfar : ∀ s ∈ F, ∀ (w : Fin n), ¬(G.Adj t w ∧ G.Adj s w)) (hFnadj : ∀ s ∈ F, ¬G.Adj t s) : ∑ h ∈ G.neighborFinset t, ∑ w ∈ G.neighborFinset h ∩ D, (G.neighborFinset w ∩ F).card ≤ 1

The degree-3 bonus, iso side: for an iso twin t and a far family F, the deg-3-mediated service ∑_{h∈N(t)} ∑_{w∈N(h)∩D} |N(w) ∩ F| is at most 1 (the only possible contributor is the unique M-edge, once, through one hub).

theorem ACMax.bonus_zero_of_iso_partners {n : ℕ} {G : SimpleGraph (Fin n)} {D : Finset (Fin n)} (hD : ∀ (v : Fin n), v ∈ D ↔ G.degree v = 3) (H : Finset (Fin n)) {F : Finset (Fin n)} (hFiso : ∀ s ∈ F, ∀ (z : Fin n), G.Adj s z → G.degree z ≠ 3) : ∑ h ∈ H, ∑ w ∈ G.neighborFinset h ∩ D, (G.neighborFinset w ∩ F).card = 0

If every member of F is itself iso (no degree-3 neighbour), the deg-3 bonus vanishes entirely — the k = 1 clause of Lemma S.

theorem ACMax.far_deg3_inter_zero_end {n : ℕ} {G : SimpleGraph (Fin n)} {D : Finset (Fin n)} (hD : ∀ (v : Fin n), v ∈ D ↔ G.degree v = 3) (heM : ∑ z ∈ D, (G.neighborFinset z ∩ D).card ≤ 2) {e₀ e₁ : Fin n} (he₀ : G.degree e₀ = 3) (he₁ : G.degree e₁ = 3) (hadj : G.Adj e₀ e₁) (w : Fin n) : w ∈ D → (G.neighborFinset w ∩ farOf n G e₀).card = 0

The degree-3 bonus, M-end side, vanishes pointwise: no degree-3 vertex is adjacent to a far partner of the M-end e₀.

The φ-identities (slot budgets)

theorem ACMax.phi_iso {n : ℕ} (hn : 18 ≤ n) {G : SimpleGraph (Fin n)} (hm : G.edgeFinset.card = 2 * (n - 2)) (hdeg : ∀ (v : Fin n), G.degree v = 3 ∨ G.degree v = 4) (hT : ¬HasGoodTriangle n G) (hC4 : ¬HasGoodC4 n G) {D : Finset (Fin n)} (hD : ∀ (v : Fin n), v ∈ D ↔ G.degree v = 3) {t : Fin n} (ht : G.degree t = 3) (hiso : ∀ (w : Fin n), G.Adj t w → G.degree w ≠ 3) : (farOf n G t).card ≤ 7 ∧ ∑ h ∈ G.neighborFinset t, (G.neighborFinset h \ D).card = (farOf n G t).card + 2

The iso φ-identity: for an iso twin t in the corner, the slot budget is ∑_{h∈N(t)} |N(h)∖D| = k + 2 where k = |farOf t| ≤ 7.

theorem ACMax.phi_end {n : ℕ} (hn : 18 ≤ n) {G : SimpleGraph (Fin n)} (hm : G.edgeFinset.card = 2 * (n - 2)) (hdeg : ∀ (v : Fin n), G.degree v = 3 ∨ G.degree v = 4) (hT : ¬HasGoodTriangle n G) (hC4 : ¬HasGoodC4 n G) {D : Finset (Fin n)} (hD : ∀ (v : Fin n), v ∈ D ↔ G.degree v = 3) (heM : ∑ z ∈ D, (G.neighborFinset z ∩ D).card ≤ 2) {e₀ e₁ : Fin n} (he₀ : G.degree e₀ = 3) (he₁ : G.degree e₁ = 3) (hadj : G.Adj e₀ e₁) : (farOf n G e₀).card ≤ 6 ∧ ∑ γ ∈ G.neighborFinset e₀ \ D, (G.neighborFinset γ \ D).card = (farOf n G e₀).card

The end φ-identity: for the M-end e₀ (partner e₁) in the corner, the slot budget over the two hub neighbours is exactly k₀ = |farOf e₀| ≤ 6.

The omega endgames

theorem ACMax.service_endgame_iso (k bonus B X x y : ℕ) (hk1 : 1 ≤ k) (hk7 : k ≤ 7) (hB : B = k + 2) (hxy : x + y ≤ B) (h6 : 6 * x + y ≤ k * k - k) (hbonus : bonus ≤ 1) (hbz : k = 1 → bonus = 0) (hdem : 4 * k ≤ bonus + X) (hX : X ≤ B + 2 * x + y) : False

The Lemma-S endgame arithmetic: demand 4k versus supply bonus + (k+2) + 2x + y under the slot and pair budgets is infeasible for every 1 ≤ k ≤ 7 (the k = 1 tie needs bonus = 0).

theorem ACMax.service_endgame_end (k X x y : ℕ) (hk1 : 1 ≤ k) (hk6 : k ≤ 6) (hxy : x + y ≤ k) (h6 : 6 * x + y ≤ k * k - k) (hdem : 3 * k ≤ X) (hX : X ≤ k + 2 * x + y) : False

The Lemma-E endgame arithmetic: demand 3k₀ versus supply k₀ + 2x + y under x + y ≤ k₀ and the pair budget is infeasible for every 1 ≤ k₀ ≤ 6.

Lemma S and Lemma E

theorem ACMax.service_count_iso (n : ℕ) (hn : 18 ≤ n) (G : SimpleGraph (Fin n)) (hm : G.edgeFinset.card = 2 * (n - 2)) (hdeg : ∀ (v : Fin n), G.degree v = 3 ∨ G.degree v = 4) (hT : ¬HasGoodTriangle n G) (hC4 : ¬HasGoodC4 n G) (heM : ∑ z : Fin n with G.degree z = 3, (G.neighborFinset z ∩ {v : Fin n | G.degree v = 3}).card ≤ 2) (t : Fin n) (ht : G.degree t = 3) (hiso : ∀ (w : Fin n), G.Adj t w → G.degree w ≠ 3) (hne : (farOf n G t).Nonempty) (hone : (farOf n G t).card = 1 → ∀ s ∈ farOf n G t, ∀ (z : Fin n), G.Adj s z → G.degree z ≠ 3) (hdemand : ∀ s ∈ farOf n G t, 4 ≤ ∑ h ∈ G.neighborFinset t, (G.neighborFinset h ∩ G.neighborFinset s).card) : False

Lemma S — the iso-twin service bound. In the corner, an iso twin t with at least one far partner cannot have ALL far partners at cross ≥ 4 (given the k = 1 far partner iso — the excluded case is exactly the one routed to Lemma E).

theorem ACMax.service_count_end (n : ℕ) (hn : 18 ≤ n) (G : SimpleGraph (Fin n)) (hm : G.edgeFinset.card = 2 * (n - 2)) (hdeg : ∀ (v : Fin n), G.degree v = 3 ∨ G.degree v = 4) (hT : ¬HasGoodTriangle n G) (hC4 : ¬HasGoodC4 n G) (heM : ∑ z : Fin n with G.degree z = 3, (G.neighborFinset z ∩ {v : Fin n | G.degree v = 3}).card ≤ 2) (e₀ e₁ : Fin n) (he₀ : G.degree e₀ = 3) (he₁ : G.degree e₁ = 3) (hadj : G.Adj e₀ e₁) (hne : (farOf n G e₀).Nonempty) (hdemand : ∀ s ∈ farOf n G e₀, 4 ≤ ∑ γ ∈ G.neighborFinset e₀, (G.neighborFinset γ ∩ G.neighborFinset s).card) : False

Lemma E — the M-end service bound. In the corner, the M-end e₀ (partner e₁) with at least one far partner cannot have ALL far partners at cross ≥ 4.

B2⁺ — the low-cross far pair

theorem ACMax.exists_far_deg3_pair_lowcross (n : ℕ) (hn : 18 ≤ n) (G : SimpleGraph (Fin n)) (hm : G.edgeFinset.card = 2 * (n - 2)) (hdeg : ∀ (v : Fin n), G.degree v = 3 ∨ G.degree v = 4) (hT : ¬HasGoodTriangle n G) (hC4 : ¬HasGoodC4 n G) (heM : ∑ z : Fin n with G.degree z = 3, (G.neighborFinset z ∩ {v : Fin n | G.degree v = 3}).card ≤ 2) : ∃ (s : Fin n) (t : Fin n), G.degree s = 3 ∧ G.degree t = 3 ∧ s ≠ t ∧ ¬G.Adj s t ∧ (∀ (w : Fin n), ¬(G.Adj s w ∧ G.Adj t w)) ∧ ∑ w ∈ G.neighborFinset s, (G.neighborFinset w ∩ G.neighborFinset t).card ≤ 3

B2⁺ (exists_far_deg3_pair_lowcross). In the x = 0, e(M) ≤ 1 corner (n ≥ 18): all degrees 3 or 4, 2(n−2) edges, no good triangle, no good C₄, at most one edge inside the degree-3 set — some far degree-3 pair has cross count ≤ 3, in the exact hcross form of the workhorse algConn_le_two_of_far_deg3_pair. Proof: B2 (exists_far_deg3_pair) gives a far pair; if all far pairs had cross ≥ 4, an M-end endpoint is killed by Lemma E and an iso pair by Lemma S.

The band dispatch and the corner closure

theorem ACMax.farpair_dispatch_band (n : ℕ) (hn : 18 ≤ n) [Nonempty (Fin n)] (G : SimpleGraph (Fin n)) (hm : G.edgeFinset.card = 2 * (n - 2)) (hdeg : ∀ (v : Fin n), G.degree v = 3 ∨ G.degree v = 4) (hT : ¬HasGoodTriangle n G) (hC4 : ¬HasGoodC4 n G) (heM : ∑ z : Fin n with G.degree z = 3, (G.neighborFinset z ∩ {v : Fin n | G.degree v = 3}).card ≤ 2) : algConn G ≤ 2

The band far-pair dispatch (B1 + B2 + B2⁺): the x = 0, e(M) ≤ 1 corner is closed for EVERY n ≥ 18. B2⁺ produces a far degree-3 pair with cross ≤ 3; the uniform workhorse vector then certifies algConn G ≤ 2.

theorem ACMax.x0_corner_farpair_general (n : ℕ) (hn : 18 ≤ n) [Nonempty (Fin n)] (G : SimpleGraph (Fin n)) (h : ResidualCore n G) (hdeg4 : ∀ (v : Fin n), G.degree v ≤ 4) (heM : ∑ z : Fin n with G.degree z = 3, (G.neighborFinset z ∩ {v : Fin n | G.degree v = 3}).card ≤ 2) : algConn G ≤ 2

The x = 0 corner of ResidualCore, closed for every n ≥ 18 — the band extension of x0_corner_farpair (which required n ≥ 32): a ResidualCore graph with all degrees ≤ 4 whose degree-3 set spans at most one edge satisfies algConn G ≤ 2.

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

x0_corner_farpair_general in the mIncidence vocabulary of the C-case tree, at the honest n ≥ 18 threshold.

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

The band corner closure (the combined corollary, n ≥ 23). The x = 0, e(M) ≤ 1 poor corner of ResidualCore is closed for all n ≥ 23 — this single theorem covers both the band 23 ≤ n ≤ 31 (new, via B2⁺) and re-proves the n ≥ 32 range of x0_corner_farpair/x0_corner_farpair_mIncidence (which remain valid; the counting here is in fact valid from n ≥ 18, see x0_corner_farpair_general_mIncidence). This is the corner node the C-tree dispatcher should route through, replacing its n ≥ 32 guard.