Final two-range assembly

The conjecture is assembled from the same ranges used in the mathematical paper:

• 4 ≤ n ≤ 31;
• n ≥ 32.

The second range combines the direct incidence-capacity proof on 32 ≤ n ≤ 49 with the exact Moore closure for n ≥ 48; their overlap at orders 48 and 49 is harmless.

theorem ACMax.upperBound_ge_32_exact {n : ℕ} [Nonempty (Fin n)] (hn32 : 32 ≤ n) (G : SimpleGraph (Fin n)) (hm : G.edgeFinset.card = 2 * (n - 2)) : algConn G ≤ 2

Every graph of order at least 32 with exactly 2(n-2) edges has algebraic connectivity at most 2.

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

The ACMAX conjecture for every order n ≥ 4, assembled at the paper's 31/32 boundary.

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

Canonical hypothesis-free formulation of the ACMAX conjecture.

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

Every residual graph has algebraic connectivity at most 2, as an immediate corollary of the full theorem.

theorem ACMax.algConn_le_two_of_card_general (n : ℕ) (hn : 12 ≤ n) [Nonempty (Fin n)] (G : SimpleGraph (Fin n)) (hm : G.edgeFinset.card = 2 * (n - 2)) : algConn G ≤ 2

Every graph on Fin n, n ≥ 12, with exactly 2(n-2) edges has algebraic connectivity at most 2.