The large-n assembly and the cloud bound

Assembles the compact-cell machinery into the unconditional ACMAX theorem for large n, reducing the general conjecture to a finite range 19 ≤ n ≤ 17692. The chain: kill the hoarding regime, reduce the m-bound to a max-cloud bound via the hub-cross law, bound the cloud by the apex-tie law, and sharpen the constants.

Main results

• hoarding_impossible, hunblocked_large — on the compact cell (n ≥ 520) a DS-unblocked hub pair cannot hoard the degree-3 supply, so off the SeaFatBoundary some pair fires as a W1Config.
• acmax_general_final, acmax_general_final_threeconn — the general dispatch (sea / usable far pair / boundary-with-m-bound / W1), with the 3-connectivity reduction HasTwoCut / algConn_le_two_of_hasTwoCut discharging the two-cut case directly.
• acmax_general_final_cloud, usable_deg3_card_le_of_cloud — the hub-cross coverage m ≤ 13·A + 172 reducing the m-bound to the max-cloud bound A.
• cloud_usable_card_le, acmax_general_residual_large — the apex-tie cloud bound (A ≤ 61, hence m ≤ 151), giving unconditional ACMAX for large n.
• cloud_card_le_sharp (A ≤ 13), usable_deg3_card_le_sharp and the mid-leaf sharpening — the constant chain pushing the wall down to boundLin 3203 = 17692 (acmax_conjecture_large_n_sharp).

Hoarding basics for the two-mega pair

unblocked_gap_pos_nonadj: a DS-unblocked pair (dsValue ≤ 4) of degree-≥ 4 hubs with a positive private-twin gap is non-adjacent (adjacency already costs 1 + 1 + 1 + 2 = 5 > 4).

theorem ACMax.unblocked_gap_pos_nonadj {V : Type u_1} [Fintype V] (G : SimpleGraph V) (g h : V) (hg4 : 4 ≤ G.degree g) (hh4 : 4 ≤ G.degree h) (hds : dsValue G g h ≤ 4) (hgap : (privTwins G h g).card < (privTwins G g h).card) : ¬G.Adj g h

Unblocked positive-gap pairs are non-adjacent. If dsValue G g h ≤ 4, both hubs have degree ≥ 4, and the private-twin gap is positive, then g and h cannot be adjacent: adjacency puts each hub in the other's internal degree (they are not degree-3) and switches on the adjacency indicator, forcing dsValue ≥ 5.

theorem ACMax.ds_unblocked_fires (n : ℕ) [Nonempty (Fin n)] (G : SimpleGraph (Fin n)) (g h' : Fin n) (hg4 : 4 ≤ G.degree g) (hh4 : 4 ≤ G.degree h') (hne : g ≠ h') (hds : dsValue G g h' ≤ 4) (hgap : (privTwins G h' g).card ≤ (privTwins G g h').card) : algConn G ≤ 2 ∨ W1Config G

The DS-unblocked double-star fire (the v66 tie-breaker, n-free). A DS-unblocked pair (dsValue ≤ 4) of degree-≥4 hubs with non-negative private gap either fires the double-star two-cluster cut outright or is a gap-0 W1 configuration. The dsValue budget does all the work: mCross ≥ 1 or adjacency force gap 0; otherwise the intDeg/shared patterns satisfy the exact double-star condition — the (0,3)-corner dies on deg g ≥ 4. No largeness of n is required.

Killing the hoarding regime and the final assembly

dsValue_comm (the DS value is symmetric); hoarding_impossible (for n ≥ 520 on the compact cell a DS-unblocked pair with a positive gap cannot hoard the degree-3 supply — the cross-pack bound |Pg|·|Ph| ≤ |D|·(76 + 14S) contradicts a quadratic lower bound); hunblocked_large (off the SeaFatBoundary some pair fires as a W1Config); and the dispatch acmax_general_final.

theorem ACMax.adjInd_comm {V : Type u_1} (G : SimpleGraph V) (g h : V) : adjInd G g h = adjInd G h g

The adjacency indicator is symmetric.

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

The M-cross count is symmetric: both directions count the edges between the two private sides (indicator double count).

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

The DS value is symmetric: the two ℕ-gap terms swap, the internal degrees commute, and the shared-twin, adjacency and M-cross terms are symmetric.

theorem ACMax.hunblocked_all (n : ℕ) [Nonempty (Fin n)] (G : SimpleGraph (Fin n)) (hb : ¬SeaFatBoundary G) : algConn G ≤ 2 ∨ W1Config G

Off the boundary, every graph fires — at every n (the v66 routing). ¬SeaFatBoundary produces a DS-unblocked pair; WLOG the gap is non-negative and ds_unblocked_fires closes it via the double-star cut or the gap-0 W1 route. No largeness of n, compactness, or M-matching hypothesis is used.

theorem ACMax.acmax_general_final (C_m n : ℕ) [Nonempty (Fin n)] (G : SimpleGraph (Fin n)) (h : ResidualCore n G) (hn : boundLin ((128 * C_m + 34508) / 23) < n) (hnBig : 520 ≤ n) (hmb : SeaFatBoundary G → ¬HasUsableFarPair G → {v : Fin n | G.degree v = 3 ∧ sigS G v ≤ 2}.card ≤ C_m) : algConn G ≤ 2

The final general assembly. For n beyond boundLin ((128·C_m + 34508)/23) (and the trivial floor 520), a single hypothesis — the usable degree-3 count is at most C_m on the boundary of the compact cell — gives algConn G ≤ 2 for every ResidualCore graph: sea → residual_sea_algConn_le_two; usable far pair → direct; boundary → the m-bound excess route contradicts compactness; otherwise → hunblocked_large fires a W1.

The 3-connectivity reduction

HasTwoCut (a two-vertex cut {a, b} separating nonempty disjoint sets with no cross edges, the hypothesis bundle of algConn_le_two_of_two_vertex_cut), algConn_le_two_of_hasTwoCut (any two-cut gives algConn G ≤ 2), and acmax_general_final_threeconn (the dispatch with the boundary m-bound hypothesis weakened by also assuming ¬HasTwoCut G).

def ACMax.HasTwoCut {n : ℕ} (G : SimpleGraph (Fin n)) : Prop

A two-vertex cut: a ≠ b together with nonempty disjoint A, B covering all remaining vertices and with no A–B edges.

Equations

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

theorem ACMax.algConn_le_two_of_hasTwoCut {n : ℕ} [Nonempty (Fin n)] (G : SimpleGraph (Fin n)) (h : HasTwoCut G) : algConn G ≤ 2

Any graph with a two-vertex cut has algConn G ≤ 2.

theorem ACMax.acmax_general_final_threeconn (C_m n : ℕ) [Nonempty (Fin n)] (G : SimpleGraph (Fin n)) (h : ResidualCore n G) (hn : boundLin ((128 * C_m + 34508) / 23) < n) (hnBig : 520 ≤ n) (hmb : SeaFatBoundary G → ¬HasUsableFarPair G → ¬HasTwoCut G → {v : Fin n | G.degree v = 3 ∧ sigS G v ≤ 2}.card ≤ C_m) : algConn G ≤ 2

The final general assembly, 3-connected form. Same as acmax_general_final, but the boundary m-bound hypothesis may additionally assume there is no two-vertex cut: if a two-cut exists, the cut certificate gives algConn G ≤ 2 outright.

Hub-cross pair coverage: m-bound to max-cloud bound

The payoff of the hub-cross firing law: on the compact boundary cell the usable degree-3 count m is linearly controlled by the max-cloud bound A = max_{deg w ≥ 9} #(usable degree-3 neighbours of w). By usable_deg3_split_mid, m ≤ 268 + |T'| with T' = bigCleanTwins G; unless a FiringConfig exists, every ordered pair of T' is covered by a common neighbour or a partner-involving cross (the pure hub–hub cross being excluded by the law), and charging every cross to the degree-4 partner set gives |T'|·(|T'|−1) ≤ (13A + 26)·|T'|, hence m ≤ 13·A + 172 (usable_deg3_card_le_of_cloud). acmax_general_final_cloud replaces the m-bound hypothesis of acmax_general_final_threeconn by this max-cloud bound.

The firing configuration

def ACMax.FiringConfig (n : ℕ) (G : SimpleGraph (Fin n)) (u v g g' : Fin n) : Prop

A firing configuration for the hub-cross law: the full hypothesis set of algConn_le_two_of_hub_cross_pair.

Equations

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

theorem ACMax.firingConfig_closes {n : ℕ} [Nonempty (Fin n)] (G : SimpleGraph (Fin n)) {u v g g' : Fin n} (hf : FiringConfig n G u v g g') : algConn G ≤ 2

A firing configuration closes the graph, via the hub-cross law.

theorem ACMax.bigclean_mechanism_of_no_firing (n : ℕ) (G : SimpleGraph (Fin n)) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) (hnf : ¬∃ (u : Fin n) (v : Fin n) (g : Fin n) (g' : Fin n), FiringConfig n G u v g g') (u v : Fin n) : u ∈ bigCleanTwins G → v ∈ bigCleanTwins G → u ≠ v → (∃ (w : Fin n), G.Adj u w ∧ G.Adj v w) ∨ ∃ (w : Fin n) (w' : Fin n), G.Adj u w ∧ G.Adj v w' ∧ G.Adj w w' ∧ (G.degree w ≤ 4 ∨ G.degree w' ≤ 4)

The mechanism, given no firing configuration. If no firing configuration exists, then any two distinct big clean twins share a common neighbour or carry a partner-involving cross edge (one end of degree ≤ 4). The pure hub–hub cross is impossible: it would complete a firing configuration.

Auxiliary caps

theorem ACMax.aT_zero_of_mid {n : ℕ} (G : SimpleGraph (Fin n)) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) {w : Fin n} (hw5 : 5 ≤ G.degree w) (hw8 : G.degree w ≤ 8) : (G.neighborFinset w ∩ bigCleanTwins G).card = 0

A mid-degree (5 ≤ deg ≤ 8) vertex has no big-clean-twin neighbours.

The pair-coverage master count

theorem ACMax.bigclean_pair_coverage (n : ℕ) (G : SimpleGraph (Fin n)) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) (hmech : ∀ (u v : Fin n), u ∈ bigCleanTwins G → v ∈ bigCleanTwins G → u ≠ v → (∃ (w : Fin n), G.Adj u w ∧ G.Adj v w) ∨ ∃ (w : Fin n) (w' : Fin n), G.Adj u w ∧ G.Adj v w' ∧ G.Adj w w' ∧ (G.degree w ≤ 4 ∨ G.degree w' ≤ 4)) (A : ℕ) (hA : ∀ (w : Fin n), 9 ≤ G.degree w → (G.neighborFinset w ∩ bigCleanTwins G).card ≤ A) (hml : ∀ (z : Fin n), G.degree z ≤ 4 → {t ∈ G.neighborFinset z | G.degree t = 3}.card ≤ G.degree z - 2) : (bigCleanTwins G).card ≤ 13 * A + 27

Hub-cross pair coverage. Given the mechanism (no firing configuration) and the big-cloud cap A, the ordered distinct pairs of big clean twins are covered by common neighbours (P2 ≤ (A+2)|T|) and partner-involving crosses, every cross edge charged to the partner set P = ⋃_{t∈T} {deg-≤4 neighbours of t} (|P| ≤ 2|T|, all degree 4). In the cross channel, factoring the twin count c_x = |N(x)∩T| ≤ 2 out of each per-x sum, using that the mediator at x's own twin vanishes (a big clean twin has no degree-3 neighbour) and that every mediator carries ≤ A + 2 twins, gives per-x ≤ 6·c_x·(A+2); the exact double count Σ_{x∈P} c_x = 2|T| then yields P3 ≤ (12A + 24)|T|. Hence

|T|·(|T|−1) ≤ (13A + 26)·|T|, i.e. |T| ≤ 13A + 27 —

with no dependence on n or on the excess.

Quadratic root + the m-bound assembly

theorem ACMax.nat_quad_bound (x b c : ℕ) (h : x * (x - 1) ≤ b * x + c) : x ≤ b + c + 1

Crude quadratic-root bound over ℕ: x(x−1) ≤ bx + c → x ≤ b + c + 1.

The cloud bound and unconditional large-n ACMAX

The payoff of the apex-tie law: the A-bound is a theorem. Fix a hub g of degree ≥ 9 with clean twin cloud C = N(g) ∩ bigCleanTwins G, A = |C|. Unless an apex configuration exists, every ordered pair of C is covered by a shared degree-4 partner (≤ 6A) or a partner–partner cross (≤ 128A), so A(A−1) ≤ 102A, i.e. A ≤ 61, and the usable cloud of any degree-≥ 9 vertex has ≤ 151 members (cloud_usable_card_le). acmax_general_residual_large then proves algConn ≤ 2 for large n with no cell hypotheses, reducing the general conjecture to a finite range.

The apex firing configuration

def ACMax.ApexConfig (n : ℕ) (G : SimpleGraph (Fin n)) (u v g : Fin n) : Prop

An apex configuration: the full hypothesis set of the apex-tie law algConn_le_two_of_apex_twin_pair.

Equations

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

theorem ACMax.apexConfig_closes {n : ℕ} [Nonempty (Fin n)] (G : SimpleGraph (Fin n)) {u v g : Fin n} (hf : ApexConfig n G u v g) : algConn G ≤ 2

An apex configuration closes the graph, via the apex-tie law.

Cloud structure helpers

theorem ACMax.cloud_partner_deg {n : ℕ} (G : SimpleGraph (Fin n)) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) {g u : Fin n} (hg : 9 ≤ G.degree g) (hu : u ∈ bigCleanTwins G) (hug : G.Adj u g) (w : Fin n) : G.Adj u w → w ≠ g → G.degree w = 4

The unique big neighbour of a big clean twin u ∈ N(g) with deg g ≥ 9 is g itself: every other neighbour has degree 4.

theorem ACMax.cloud_inter_card_le_two {n : ℕ} (G : SimpleGraph (Fin n)) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) (hblk4 : ∀ (x : Fin n), G.degree x = 4 → (hubTwins G x).card ≤ 2) {g : Fin n} (hg : 9 ≤ G.degree g) {w : Fin n} (hwg : w ≠ g) : (G.neighborFinset w ∩ (G.neighborFinset g ∩ bigCleanTwins G)).card ≤ 2

With the block law (every degree-4 vertex has at most 2 degree-3 neighbours), a non-apex vertex meets the cloud in at most 2 members.

The same-cloud mechanism

theorem ACMax.cloud_pair_mechanism {n : ℕ} (G : SimpleGraph (Fin n)) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) (hnf : ¬∃ (u : Fin n) (v : Fin n) (g : Fin n), ApexConfig n G u v g) {g : Fin n} (hg : 9 ≤ G.degree g) (u v : Fin n) : u ∈ G.neighborFinset g ∩ bigCleanTwins G → v ∈ G.neighborFinset g ∩ bigCleanTwins G → u ≠ v → (∃ (w : Fin n), w ≠ g ∧ G.Adj u w ∧ G.Adj v w) ∨ ∃ (w : Fin n) (w' : Fin n), G.Adj u w ∧ w ≠ g ∧ G.Adj v w' ∧ w' ≠ g ∧ G.Adj w w'

The same-cloud mechanism, given no apex configuration. Two distinct members of a degree-≥ 9 cloud share a non-apex (degree-4) neighbour or carry a partner–partner cross edge.

Sharpening the usable-count cap chain

Sharpens the concrete m-bound by two improvements. cloud_card_le_sharp tightens the cloud cap to A ≤ 13: charging both the shared-partner and partner-cross channels to the same degree-4 partner set gives offDiag + cross ≤ 6·c_x pointwise, so A(A−1) ≤ 12A. usable_deg3_card_le_sharp then gives m ≤ 341 via usable_deg3_card_le_of_cloud, and acmax_general_residual_large_sharp / acmax_conjecture_large_n_sharp rethread the argument with C_m' = 341, reducing the wall to boundLin ((128·341 + 34508)/23) = 18764. The standalone lever iso_twin_le_one_double_hub (every degree-3 vertex has at most one degree-4 neighbour carrying a second degree-3 neighbour) is proved here but not consumed by the sharpened bound.

The sharpened cloud bound A ≤ 13

theorem ACMax.cloud_card_le_sharp {n : ℕ} (G : SimpleGraph (Fin n)) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) (hblk4 : ∀ (x : Fin n), G.degree x = 4 → (hubTwins G x).card ≤ 2) (hnf : ¬∃ (u : Fin n) (v : Fin n) (g : Fin n), ApexConfig n G u v g) {g : Fin n} (hg : 9 ≤ G.degree g) : (G.neighborFinset g ∩ bigCleanTwins G).card ≤ 13

The sharpened cloud bound. If no apex configuration exists, every degree-≥ 9 vertex has at most 13 big-clean-twin neighbours. The shared-partner channel P2 and the partner-cross channel P3 are both charged to the same degree-4 partner set P; combining the two per-mediator bounds pointwise gives offDiag(x) + cross(x) ≤ 6·c_x for every x ∈ P (c_x = |N(x)∩C| ≤ 2), so P2 + P3 ≤ 6·Σ_x c_x = 12A and A(A−1) ≤ 12A ⟹ A ≤ 13 (vs. the loose 14A of cloud_card_le, which bounds the two channels separately).

Threading the sharpened mid-leaf bound into the wall chain

Threads the sharpened mid-leaves bound (143 → 108, from spending the base mid leaf's own σ-budget Σσ ≤ 2 ⟹ Σdeg ≤ 19) through the usable-count chain: the coverage improves to 13A + 137, the usable cap to C_m = 306, and the wall to boundLin 3203 = 17692. The three theorems mirror usable_deg3_card_le_of_cloud, usable_deg3_card_le_sharp and acmax_conjecture_large_n_sharp with the sharpened constants; the original chain is left untouched.

theorem ACMax.usable_deg3_card_le_of_cloud_sharp (n : ℕ) (G : SimpleGraph (Fin n)) (h : ResidualCore n G) (hcpt : ¬HasUsableFarPair G) (hmech : ∀ (u v : Fin n), u ∈ bigCleanTwins G → v ∈ bigCleanTwins G → u ≠ v → (∃ (w : Fin n), G.Adj u w ∧ G.Adj v w) ∨ ∃ (w : Fin n) (w' : Fin n), G.Adj u w ∧ G.Adj v w' ∧ G.Adj w w' ∧ (G.degree w ≤ 4 ∨ G.degree w' ≤ 4)) (A : ℕ) (hA : ∀ (w : Fin n), 9 ≤ G.degree w → (G.neighborFinset w ∩ bigCleanTwins G).card ≤ A) (hblk : ∀ (w : Fin n), G.degree w ≤ 15 → (hubTwins G w).card + 2 ≤ G.degree w) (huniq : ∀ (t₁ t₂ t₃ t₄ : Fin n), G.Adj t₁ t₂ → G.Adj t₃ t₄ → G.degree t₁ = 3 → G.degree t₂ = 3 → G.degree t₃ = 3 → G.degree t₄ = 3 → {t₁, t₂} = {t₃, t₄}) : {v : Fin n | G.degree v = 3 ∧ sigS G v ≤ 2}.card ≤ 13 * A + 137

The sharpened m-bound from the max-cloud bound (no firing configuration). Mirror of usable_deg3_card_le_of_cloud with the sharpened mid split (usable_deg3_split_mid_sharp, 108) in place of usable_deg3_split_mid (143); the coverage constant drops accordingly to

m ≤ 13·A + 137

(108 mid split + 2 M-bridge + the coverage bound 13A + 27). Needs the extra min degree ≥ 3 hypothesis, which is available here as h.min_degree.

theorem ACMax.usable_deg3_card_le_sharp2 (n : ℕ) (G : SimpleGraph (Fin n)) (h : ResidualCore n G) (hcpt : ¬HasUsableFarPair G) (hnofire : ¬∃ (u : Fin n) (v : Fin n) (g : Fin n) (g' : Fin n), FiringConfig n G u v g g') (hnapex : ¬∃ (u : Fin n) (v : Fin n) (g : Fin n), ApexConfig n G u v g) (hblk : ∀ (w : Fin n), G.degree w ≤ 15 → (hubTwins G w).card + 2 ≤ G.degree w) (huniq : ∀ (t₁ t₂ t₃ t₄ : Fin n), G.Adj t₁ t₂ → G.Adj t₃ t₄ → G.degree t₁ = 3 → G.degree t₂ = 3 → G.degree t₃ = 3 → G.degree t₄ = 3 → {t₁, t₂} = {t₃, t₄}) : {v : Fin n | G.degree v = 3 ∧ sigS G v ≤ 2}.card ≤ 306

The sharpened concrete m-bound m ≤ 306 = 13·13 + 137. Mirror of usable_deg3_card_le_sharp (GeneralCloudSharp) feeding the sharpened cloud cap A = 13 (cloud_card_le_sharp) through the sharpened coverage assembly usable_deg3_card_le_of_cloud_sharp (m ≤ 13A + 137). Down from 341.

theorem ACMax.boundLin_sharp2_eq : boundLin ((128 * 306 + 34508) / 23) = 17692

The doubly-sharpened residual threshold boundLin ((128·306 + 34508)/23) = boundLin 3203 = 17692.

theorem ACMax.acmax_general_residual_large_sharp2 (n : ℕ) [Nonempty (Fin n)] (G : SimpleGraph (Fin n)) (h : ResidualCore n G) (hn : boundLin ((128 * 306 + 34508) / 23) < n) : algConn G ≤ 2

General ACMAX for large n, doubly-sharpened form. Every ResidualCore graph with n > 17692 has algConn ≤ 2 — no open hypotheses. Same dispatch as acmax_general_residual_large_sharp, but with the doubly-sharpened concrete m-bound m ≤ 306 (mid split 108, cloud cap A = 13), lowering the threshold from 18764 to 17692.

theorem ACMax.acmax_conjecture_large_n_sharp2 (n : ℕ) [Nonempty (Fin n)] (G : SimpleGraph (Fin n)) (hm : G.edgeFinset.card = 2 * (n - 2)) (hn : boundLin ((128 * 306 + 34508) / 23) < n) : algConn G ≤ 2

Kolokolnikov Conjecture 1.5 for large n, doubly-sharpened. Every simple graph on Fin n with exactly 2(n−2) edges and n > 17692 has algebraic connectivity at most 2 — the finite residual range shrinks to 19 ≤ n ≤ 17692 (from 19 ≤ n ≤ 18764).