The master X-bound assembly

Combines the D1 suppressed-mass bound suppressed_card_le with the degree handshake to bound the total excess X = excessX n G on the SeaFatBoundary linearly in the number of usable (unsuppressed, sigS ≤ 2) degree-3 vertices.

1. deg3_card_eq_eight_add_excess — handshake: |D₃| = 8 + X.
2. deg3_usable_suppressed_split — |D₃| = m + s (usable + suppressed).
3. sfb_excess_bound_beta — the sharpened excess bound on the boundary (n ≥ 512), dispatched through the slope-11/2 light-anchor cover (compact_covering_eleven_halves).

theorem ACMax.deg3_card_eq_eight_add_excess (n : ℕ) (G : SimpleGraph (Fin n)) (hn : 2 ≤ n) (hm : G.edgeFinset.card = 2 * (n - 2)) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) : (deg3Set G).card = 8 + excessX n G

Handshake: with 2(n−2) edges and minimum degree 3, the degree-3 set has exactly 8 + X members, where X = excessX n G is the total degree excess.

theorem ACMax.deg3_usable_suppressed_split (n : ℕ) (G : SimpleGraph (Fin n)) : (deg3Set G).card = {v : Fin n | G.degree v = 3 ∧ sigS G v ≤ 2}.card + {v : Fin n | G.degree v = 3 ∧ 2 < sigS G v}.card

Partition of the degree-3 set into usable (sigS ≤ 2) and suppressed (2 < sigS) vertices.

theorem ACMax.all_heavy_corner_count (n : ℕ) (hn : 2 ≤ n) (G : SimpleGraph (Fin n)) (h : ResidualCore n G) (hnolight : ∀ (u : Fin n), sigS G u ≤ 2 → 5 ≤ G.degree u) : n + 8 ≤ 5 * excessX n G

The all-usable-heavy corner count: if no light usable vertex exists, every degree-3 vertex is suppressed (needing ≥ 2 heavy neighbours) and every degree-4 vertex is suppressed (needing ≥ 1), so heavy-slot counting alone gives 2n₃ + n₄ ≤ X + 4|H| and hence

n + 8 ≤ 5·X

— no ball or covering required.

theorem ACMax.compact_covering_eleven_halves (n : ℕ) (G : SimpleGraph (Fin n)) (hm : G.edgeFinset.card = 2 * (n - 2)) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) (hcpt : ¬HasUsableFarPair G) (hlight : ∃ (u : Fin n), sigS G u ≤ 2 ∧ G.degree u ≤ 4) : 2 * n ≤ 151 + 11 * excessX n G

The slope-11/2 light-cell covering — a sharpening of compact_covering_nine (slope 6 → 11/2). Two extra levers over the crude covering: (1) the degree-3 handshake |D₃| = 8 + X, and (2) the far-heavy multiplicity of a suppressed degree-3 halo vertex — it has two heavy neighbours (nonusable_deg3_structure), and every heavy neighbour of a vertex outside the ball lies outside the 2-ball (hfarnbr), so it draws two far heavy slots, not one. A suppressed degree-4 halo vertex still draws only one (v with three degree-4 and one degree-5 neighbour has sigS = 2/3 + 3·(1/2) > 2 yet a single heavy neighbour), so the naive ≥ 2-far bound is false; but the handshake forces |Bh₃| large whenever the far excess outgrows the ball, and balancing |Bh₃| ≥ 0 against |closeSet| + |Bh₃| ≥ 8 + X yields, on a non-double-counting four-piece cover,

2·n ≤ 151 + 11·X

i.e. n ≤ 75.5 + 5.5·X. The slope 11/2 is tight (achieved at X_far = 3·X_near).

theorem ACMax.sfb_excess_bound_beta (n : ℕ) [Nonempty (Fin n)] (hn : 512 ≤ n) (G : SimpleGraph (Fin n)) (h : ResidualCore n G) (hb : SeaFatBoundary G) (hcpt : ¬HasUsableFarPair G) (C_m : ℕ) (hmb : {v : Fin n | G.degree v = 3 ∧ sigS G v ≤ 2}.card ≤ C_m) : algConn G ≤ 2 ∨ 23 * excessX n G ≤ 128 * C_m + 34508

The β excess bound (β = 105/128): on the boundary of the compact cell, either a σ-law fires or 23·X ≤ 128·C_m + 34508 — the sharpened X ≤ (128/23)·m + const from suppressed_ledger_beta ((32/21)s ≤ (5/4)X + 685 with 8 + X = m + s).