Orders below fifty

One continuous structural argument handles orders through 31, and the owner-slot census handles 32 ≤ n ≤ 49.

Main results

• z1_fires_sharp, z1_forced_of_le_31 — the Z1 star-moat (a degree-4 hub with two degree-3 neighbors) and its forcing count on 8 ≤ n ≤ 31.
• upperBound_moat — the upper bound on the complete window 4 ≤ n ≤ 31, including the low-order degree-three core and the sparse-core endpoints.
• starved_band_kill_32_49, acmax_conjecture_range_49 — the widened starved band and the continuous verdict on 4 ≤ n ≤ 49.

The window-34 discharge

For a graph of minimum degree three, split on the presence of an M-edge: present ⟹ the sparse-core moat fires; absent ⟹ the shared-hub stars are forced. On 10 ≤ n ≤ 31 the E1 count z1_forced_of_le_31 forces Z1 with no heavy hypothesis (negating Z1 starves the degree-4 hubs and the incidence total forces n ≥ 32). The same star moat fires throughout this range by z1_fires_sharp.

theorem ACMax.z1_fires_sharp {n : ℕ} [Nonempty (Fin n)] (hn : 10 ≤ n) (G : SimpleGraph (Fin n)) (hm : G.edgeFinset.card = 2 * (n - 2)) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) (hs0 : ∀ (v w : Fin n), G.degree v = 3 → G.degree w = 3 → ¬G.Adj v w) (hZ1 : ∃ (h : Fin n), G.degree h = 4 ∧ 2 ≤ (G.neighborFinset h ∩ deg3Set G).card) : algConn G ≤ 2

Z1 fires via a sparse bulk core. A degree-4 hub owning at least two degree-3 neighbors closes the graph at every n ≥ 10.

The finite window 4 ≤ n ≤ 31

Closes the complete finite window 4 ≤ n ≤ 31. The low-degree test vector handles all orders below eight. At orders eight and nine, the degree-three core supplies a triangle or an induced 2K₂. From order ten onward, an M-edge fires via medge_sparse_core_fires; with no M-edge, the Z1-only forcing count z1_forced_of_le_31 is killed by z1_fires_sharp. The λ₂(K_{2,n-2}) = 2 half reuses algConn_completeBipartite_two.

theorem ACMax.upperBound_moat {n : ℕ} [Nonempty (Fin n)] (hn4 : 4 ≤ n) (hn31 : n ≤ 31) (G : SimpleGraph (Fin n)) (hm : G.edgeFinset.card = 2 * (n - 2)) : algConn G ≤ 2

The finite-window upper bound on 4 ≤ n ≤ 31. Every G on Fin n with 2(n−2) edges has algConn G ≤ 2.

The continuous range 4 ≤ n ≤ 49

Assembles the moat window upperBound_moat with the starved band 32 ≤ n ≤ 49 into a single verdict. The starved band kill is widened from 35 ≤ n ≤ 49 to 32 ≤ n ≤ 49 — every owner-choke ingredient is n-generic well below 35, and the closing interval_cases count still closes at n ∈ {32,33,34} (where the hoarding and giant-census rows force n_g = X = 0 and the choke caps 7·t₄ < 7·24), giving starved_band_kill_32_49. The verdict acmax_conjecture_range_49 dispatches on δ ≤ 2 / M-edge / starved band.

theorem ACMax.starved_owner_choke_32_49 {n : ℕ} [Nonempty (Fin n)] (G : SimpleGraph (Fin n)) (hn32 : 32 ≤ n) (hn49 : n ≤ 49) (hm : G.edgeFinset.card = 2 * (n - 2)) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) (hs0 : ∀ (v w : Fin n), G.degree v = 3 → G.degree w = 3 → ¬G.Adj v w) (hchoke : 7 * ∑ h ∈ hubSet G with G.degree h = 4, (G.neighborFinset h ∩ isoTwins G).card + 3 * excessX n G + 32 ≤ 4 * n) : algConn G ≤ 2

The starved owner-choke, widened to 32 ≤ n ≤ 49. Identical to starved_owner_choke_35_49 but with the closing interval_cases n <;> omega run over the wider window; the extra rows n ∈ {32, 33, 34} close because hoarding forces X ≤ n_g, the giant census forces (n − 20)·n_g ≤ 9X, together pinning n_g = X = 0, which collides the slots row (t₄ ≥ 24) with the choke (7·t₄ ≤ 4n − 32).

theorem ACMax.starved_band_kill_32_49 {n : ℕ} [Nonempty (Fin n)] (G : SimpleGraph (Fin n)) (hn32 : 32 ≤ n) (hn49 : n ≤ 49) (hm : G.edgeFinset.card = 2 * (n - 2)) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) (hs0 : ∀ (v w : Fin n), G.degree v = 3 → G.degree w = 3 → ¬G.Adj v w) : algConn G ≤ 2

The starved band kill, widened to 32 ≤ n ≤ 49. Identical to starved_band_kill_35_49 but routed through starved_owner_choke_32_49; a never-firing starved census on 32 ≤ n ≤ 49 cannot exist, so the graph fires: algConn G ≤ 2.

theorem ACMax.upperBound_range_49 {n : ℕ} [Nonempty (Fin n)] (hn4 : 4 ≤ n) (hn49 : n ≤ 49) (G : SimpleGraph (Fin n)) (hm : G.edgeFinset.card = 2 * (n - 2)) : algConn G ≤ 2

The moat/choke upper bound on the continuous range 4 ≤ n ≤ 49. Every G on Fin n with 2(n−2) edges has algConn G ≤ 2: below 32 this is upperBound_moat; on 32 ≤ n ≤ 49 the graph is dispatched by minimum degree — low-degree test vector, sparse-core certificate, or the widened starved band kill.

theorem ACMax.acmax_conjecture_range_49 {n : ℕ} [Nonempty (Fin n)] (hn4 : 4 ≤ n) (hn49 : n ≤ 49) : algConn (completeBipartiteGraph (Fin 2) (Fin (n - 2))) = 2 ∧ ∀ (G : SimpleGraph (Fin n)), G.edgeFinset.card = 2 * (n - 2) → algConn G ≤ 2

The ACMAX conjecture on the continuous range 4 ≤ n ≤ 49. K_{2,n-2} is the maximizer (λ₂ = 2) and every G with 2(n−2) edges has algConn G ≤ 2.