The σ-weighted firing laws, the σ-transfer, and the W₅ᵇ cloud bound

The σ-weighted supply machinery for the mid-range boundedness program: two σ-shaped firing laws, the unified σ-transfer inequality behind β = 105/128, and the bound on the one cloud class (W₅ᵇ) that obstructs it. All certificates use the σ-weights p_w = c/(deg w − 2) and the per-slot cost identity (c − c/(d−2))² + (d−3)·(c/(d−2))² = c²·σ(d).

Main results

• algConn_le_two_of_sigma_apex_pair (LAW A) — an apex pair (u, v share one neighbour g of weight 0, no cross edges, each side's non-apex σ-sum ≤ 1) closes with slack cB²(Σ_A σ − 1) + cA²(Σ_B σ − 1) ≤ 0.
• algConn_le_two_of_sigma_cross_pair (LAW B) — a far pair with one heavy cross (h, h′) and sigS + 1/(deg h − 2) ≤ 2 on each side closes (the master's leak set discounts the cross at h).
• The unified σ-transfer σ(d)·(a₃ + j) ≤ (5/4)(d − 4) + S_w: summed over heavy vertices the transfer terms cancel identically, giving Σ σ(d)·a₃ ≤ (5/4)·X + exceptions, the two exceptions being the W₅ overflow sigma_transfer_w5 (1/12) and the SFB-capped classes.
• The W₅ᵇ cloud bound: w5big_structure, w5big_pair_mechanism, w5big_cloud_le (each big hub carries ≤ 269 members) and w5big_card_le (|W₅ᵇ| ≤ 5441) — unless a σ-law fires, via W5LawConfig / w5LawConfig_closes.
• suppressed_ledger_beta — the assembled supply bound β = 105/128 < 7/8 for n ≥ 512.

theorem ACMax.sigma_slot_identity (c : ℝ) {d : ℕ} (hd : 3 ≤ d) : (c - c / (↑d - 2)) ^ 2 + (↑d - 3) * (c / (↑d - 2)) ^ 2 = c ^ 2 * sigma d

The σ-slot cost identity: with weight c/(d−2), (c − c/(d−2))² + (d−3)(c/(d−2))² = c²·σ(d).

theorem ACMax.algConn_le_two_of_sigma_apex_pair {V : Type u_1} [Fintype V] [Nonempty V] (G : SimpleGraph V) (u v g : V) (h3 : ∀ (w : V), 3 ≤ G.degree w) (hne : u ≠ v) (huv : ¬G.Adj u v) (hgu : G.Adj u g) (hgv : G.Adj v g) (hcap : ∀ (w : V), w ≠ g → ¬(G.Adj u w ∧ G.Adj v w)) (hnc : ∀ w ∈ (G.neighborFinset u).erase g, ∀ w' ∈ (G.neighborFinset v).erase g, ¬G.Adj w w') (hsu : ∑ w ∈ (G.neighborFinset u).erase g, sigma (G.degree w) ≤ 1) (hsv : ∑ w ∈ (G.neighborFinset v).erase g, sigma (G.degree w) ≤ 1) : algConn G ≤ 2

LAW A — the σ-apex law. Two non-adjacent vertices sharing exactly one common neighbour g, with no cross edges between the punctured neighbourhoods and per-side punctured σ-sum at most 1, certify algConn ≤ 2. (Weights p_w = cB/(deg w − 2) on N(u) \ {g}, q_w = cA/(deg w − 2) on N(v) \ {g}, apex at 0; the cross-scaled magnitudes au = cB, av = cA balance the sides exactly.)

theorem ACMax.sigma_slot_le {V : Type u_1} [Fintype V] (G : SimpleGraph V) (h3 : ∀ (w : V), 3 ≤ G.degree w) (c : ℝ) (z : V) (Z : Finset V) (w : V) (hzw : G.Adj z w) : (c - c / (↑(G.degree w) - 2)) ^ 2 + ↑(G.neighborFinset w \ insert z Z).card * (c / (↑(G.degree w) - 2)) ^ 2 ≤ c ^ 2 * sigma (G.degree w) + 2 * (c / (↑(G.degree w) - 2)) ^ 2

Generic σ-slot bound: for any adjacent anchor z and slot w, with weight p = c/(deg w − 2) and master leak set N(w) ∖ insert z Z,

(c − p)² + L·p² ≤ c²·σ(deg w) + 2p².

theorem ACMax.sigma_slot_le_sharp {V : Type u_1} [Fintype V] (G : SimpleGraph V) (h3 : ∀ (w : V), 3 ≤ G.degree w) (c : ℝ) (z : V) (Z : Finset V) (w y : V) (hzw : G.Adj z w) (hwy : G.Adj w y) (hyZ : y ∈ Z) (hyz : y ≠ z) : (c - c / (↑(G.degree w) - 2)) ^ 2 + ↑(G.neighborFinset w \ insert z Z).card * (c / (↑(G.degree w) - 2)) ^ 2 ≤ c ^ 2 * sigma (G.degree w) + (c / (↑(G.degree w) - 2)) ^ 2

Sharp σ-slot bound at a crossing slot: if additionally w has a neighbour y ∈ Z distinct from z, the leak drops by one more:

(c − p)² + L·p² ≤ c²·σ(deg w) + p².

theorem ACMax.algConn_le_two_of_sigma_cross_pair {V : Type u_1} [Fintype V] [Nonempty V] (G : SimpleGraph V) (u v h h' : V) (h3 : ∀ (w : V), 3 ≤ G.degree w) (hne : u ≠ v) (huv : ¬G.Adj u v) (hcap : ∀ (w : V), ¬(G.Adj u w ∧ G.Adj v w)) (hh : G.Adj u h) (hh' : G.Adj v h') (hcross1 : ∀ w ∈ G.neighborFinset u, ∀ w' ∈ G.neighborFinset v, G.Adj w w' → w = h ∧ w' = h') (hsu : sigS G u + 1 / (↑(G.degree h) - 2) ≤ 2) (hsv : sigS G v + 1 / (↑(G.degree h') - 2) ≤ 2) : algConn G ≤ 2

LAW B — the σ-cross law. Two non-adjacent vertices with no common neighbour whose only cross edge can be (h, h′) (h ∈ N(u), h′ ∈ N(v)), with the σ-slack conditions sigS u + 1/(deg h − 2) ≤ 2 and sigS v + 1/(deg h′ − 2) ≤ 2, certify algConn ≤ 2. The master's leak set discounts the cross edge at h and h′, leaving exactly the cross cost 2·p_h·q_{h′} ≤ cB²s_h + cA²s_{h′}, which the slack absorbs.

The unified σ-transfer (c = 5/4)

The supply bound behind β = 105/128. Partition each heavy vertex w (degree d ≥ 5) into a₃ degree-3 twins, f degree-4 and j heavy neighbours (σ-mass S_w), so sigS w = f/2 + S_w. The transfer inequality σ(d)·(a₃ + j) ≤ (5/4)(d − 4) + S_w charges σ(d) per heavy neighbour and refunds the σ-mass received; summed over heavies the transfer terms cancel identically, leaving Σ σ(d)·a₃ ≤ (5/4)·X + exceptions. It holds for every heavy vertex except the W₅ overflow (1/12, sigma_transfer_w5) and the SFB-capped usable classes (a₃ ≥ d − 2, 5 ≤ d ≤ 15). The per-degree certificates are (d−4)(d−6+2f) ≥ 0 (non-usable), a triple-gap tie at d = 5, f = 0, and (d−16)(d−2) ≥ 0 (saturated d ≥ 16).

σ set-sum bounds

theorem ACMax.sigma_setsum_ge_free {n : ℕ} (G : SimpleGraph (Fin n)) (K : Finset (Fin n)) (hK : ∀ x ∈ K, 5 ≤ G.degree x) : 2 / 3 * ↑K.card ≤ ∑ x ∈ K, sigma (G.degree x)

Any set of heavy σ-values has sum at least (2/3)·card.

theorem ACMax.sigma_setsum_le_card {n : ℕ} (G : SimpleGraph (Fin n)) (K : Finset (Fin n)) (hK : ∀ x ∈ K, 3 ≤ G.degree x) : ∑ x ∈ K, sigma (G.degree x) ≤ ↑K.card

Any set of σ-values (degrees ≥ 3) has sum at most card.

theorem ACMax.sigma_setsum_triple_gap {n : ℕ} (G : SimpleGraph (Fin n)) (K : Finset (Fin n)) (hK : ∀ x ∈ K, 5 ≤ G.degree x) (h2 : 2 < ∑ x ∈ K, sigma (G.degree x)) : 25 / 12 ≤ ∑ x ∈ K, sigma (G.degree x)

The set triple gap: a set of heavy σ-values summing strictly above 2 sums to at least 25/12. Either every member has degree 5 — then the sum is (2/3)·card > 2, forcing card ≥ 4 and sum ≥ 8/3 — or some member has degree ≥ 6, contributing ≥ 3/4 on top of ≥ 2/3 from each of the ≥ 2 others.

The neighbourhood profile of a heavy vertex

theorem ACMax.nbr_profile_partition {n : ℕ} (G : SimpleGraph (Fin n)) (w : Fin n) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) : (hubTwins G w).card + {u ∈ G.neighborFinset w | G.degree u = 4}.card + {u ∈ G.neighborFinset w | 5 ≤ G.degree u}.card = G.degree w

The degree-partition of a neighbourhood: with minimum degree 3, the twins, the degree-4 neighbours, and the heavy neighbours partition N(w).

theorem ACMax.sigS_decomp {n : ℕ} (G : SimpleGraph (Fin n)) (w : Fin n) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) : sigS G w = 1 / 2 * ↑{u ∈ G.neighborFinset w | G.degree u = 4}.card + ∑ u ∈ G.neighborFinset w with 5 ≤ G.degree u, sigma (G.degree u)

The σ-sum decomposition: sigS w = f/2 + S_w (twins contribute σ(3) = 0, degree-4 neighbours 1/2 each).

The pointwise transfer inequalities

theorem ACMax.sigma_transfer_sat {d : ℕ} (hd : 16 ≤ d) : sigma d * ↑d ≤ 5 / 4 * (↑d - 4)

Saturated cap (d ≥ 16): σ(d)·d ≤ (5/4)(d−4) — certificate (d−16)(d−2) ≥ 0.

theorem ACMax.sigma_transfer_nonusable {n : ℕ} (G : SimpleGraph (Fin n)) (w : Fin n) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) (hd : 5 ≤ G.degree w) (hs : 2 < sigS G w) : sigma (G.degree w) * (↑(hubTwins G w).card + ↑{u ∈ G.neighborFinset w | 5 ≤ G.degree u}.card) ≤ 5 / 4 * (↑(G.degree w) - 4) + ∑ u ∈ G.neighborFinset w with 5 ≤ G.degree u, sigma (G.degree u)

The non-usable transfer (suppressed heavy vertices): if deg w = d ≥ 5 and sigS w > 2, then σ(d)(a₃ + j) ≤ (5/4)(d−4) + S_w. The real relaxation S_w > 2 − f/2 gives the certificate (d−4)(d−6+2f) ≥ 0 except at d = 5, f = 0, where the triple gap S_w ≥ 25/12 makes the exact tie 10/3 = 5/4 + 25/12.

theorem ACMax.sigma_transfer_usable {n : ℕ} (G : SimpleGraph (Fin n)) (w : Fin n) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) (hd : 5 ≤ G.degree w) (hs : sigS G w ≤ 2) (ha : (hubTwins G w).card + 3 ≤ G.degree w) (hW5 : ¬(G.degree w = 5 ∧ (hubTwins G w).card = 2)) : sigma (G.degree w) * (↑(hubTwins G w).card + ↑{u ∈ G.neighborFinset w | 5 ≤ G.degree u}.card) ≤ 5 / 4 * (↑(G.degree w) - 4) + ∑ u ∈ G.neighborFinset w with 5 ≤ G.degree u, sigma (G.degree u)

The usable transfer (uncapped, non-W₅): if deg w = d ≥ 5, sigS w ≤ 2, a₃ ≤ d − 3, and not (d = 5 and a₃ = 2), then σ(d)(a₃ + j) ≤ (5/4)(d−4) + S_w. Uses S_w ≥ (2/3)j and f + j ≥ 3; certificate 3(d−4)(d−6) + 4f(d−5) + 8j(d−5) ≥ 0 for d ≥ 6, while d = 5 degenerates to j = 0, f ≥ 4 via 3f + 4j ≤ 12.

theorem ACMax.sigma_transfer_w5 {n : ℕ} (G : SimpleGraph (Fin n)) (w : Fin n) (hd : G.degree w = 5) (ha : (hubTwins G w).card = 2) : sigma (G.degree w) * (↑(hubTwins G w).card + ↑{u ∈ G.neighborFinset w | 5 ≤ G.degree u}.card) ≤ 5 / 4 * (↑(G.degree w) - 4) + ∑ u ∈ G.neighborFinset w with 5 ≤ G.degree u, sigma (G.degree u) + 1 / 12

The W₅ transfer with overflow 1/12: a usable degree-5 vertex with exactly 2 twins satisfies the transfer inequality with an extra 1/12 — exactly, in all four sub-profiles.

The extended capped-class count (d ≤ 15)

theorem ACMax.capped_overflow_nonneg {d : ℕ} (hd5 : 5 ≤ d) (hd15 : d ≤ 15) : 0 ≤ sigma d * ↑d - 5 / 4 * (↑d - 4)

The capped overflow is nonnegative for d ≤ 15.

theorem ACMax.capped_overflow_le_max {d : ℕ} (hd5 : 5 ≤ d) (_hd15 : d ≤ 15) : sigma d * ↑d - 5 / 4 * (↑d - 4) ≤ 25 / 12

The per-hub capped overflow is at most 25/12 (attained at d = 5).

theorem ACMax.capped_overflow_grid_collapsed : ∑ d ∈ Finset.Icc 5 15, ↑(2 * d - 1) * (sigma d * ↑d - 5 / 4 * (↑d - 4)) ≤ 205

The collapsed capped-overflow grid: with the block law pinning every capped class to a = d − 2 exactly, Σ_{d=5}^{15} (2d−1)·(σ(d)·d − (5/4)(d−4)) ≤ 205.

theorem ACMax.capped_overflow_le (n : ℕ) (G : SimpleGraph (Fin n)) (h : ResidualCore n G) (hb : SeaFatBoundary G) (C : Finset (Fin n)) (hC : ∀ w ∈ C, 5 ≤ G.degree w ∧ G.degree w ≤ 15 ∧ G.degree w ≤ (hubTwins G w).card + 2) (hblk : ∀ w ∈ C, (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₄}) : ∑ w ∈ C, (sigma (G.degree w) * ↑(G.degree w) - 5 / 4 * (↑(G.degree w) - 4)) ≤ 214

The capped overflow bound: the capped classes overflow the (5/4)-rate by total σ-mass at most 214 = 4·(25/12) + Σ (2d−1)·overflow(d).

The exchange identity and the summed transfer

theorem ACMax.sigma_exchange {n : ℕ} (G : SimpleGraph (Fin n)) : ∑ w : Fin n with 5 ≤ G.degree w, sigma (G.degree w) * ↑{u ∈ G.neighborFinset w | 5 ≤ G.degree u}.card = ∑ w : Fin n with 5 ≤ G.degree w, ∑ u ∈ G.neighborFinset w with 5 ≤ G.degree u, sigma (G.degree u)

The σ-exchange identity: over the heavy set, paying σ(d_w) per heavy neighbour equals receiving the neighbours' σ-mass — both sides count ordered heavy-heavy adjacencies.

theorem ACMax.sigma_transfer_sum (n : ℕ) (G : SimpleGraph (Fin n)) (h : ResidualCore n G) (hb : SeaFatBoundary G) (hblk : ∀ (w : Fin n), 5 ≤ G.degree w → G.degree w ≤ 15 → (hubTwins G w).card + 2 ≤ G.degree w) (_hml : ∀ (z : Fin n), G.degree z ≤ 4 → {t ∈ G.neighborFinset z | G.degree t = 3}.card ≤ G.degree z - 2) (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₄}) : ∑ w : Fin n with 5 ≤ G.degree w, sigma (G.degree w) * ↑(hubTwins G w).card ≤ 5 / 4 * ↑(excessX n G) + 1 / 12 * ↑{w : Fin n | G.degree w = 5 ∧ sigS G w ≤ 2 ∧ (hubTwins G w).card = 2}.card + 214

The summed σ-transfer (c = 5/4): on the boundary of the compact cell,

Σ_{deg w ≥ 5} σ(deg w)·|hubTwins w| ≤ (5/4)·X + (1/12)·N₅ + 214,

where N₅ counts the usable degree-5 hubs with exactly two twins (W₅) and 862 charges the capped classes only their OVERFLOW beyond the (5/4)-rate (capped_overflow_le) — their base (5/4)(d−4) share rides in the X-term. The transfer terms cancel exactly via sigma_exchange.

The W₅ᵇ cloud bound

W₅ᵇ — usable degree-5 hubs with two twins and a big neighbour — is the sole class obstructing β < 7/8; it is bounded by a two-round pair coverage driven by the σ-laws. Each member has neighbourhood {h, ≤4, ≤4, 3, 3} with deg h ≥ 9 the unique non-light neighbour (w5big_structure), so LAW A / LAW B fire at side-σ exactly 1 / slack 1/(deg h − 2). Unless a σ-law fires, every member pair has a light-endpoint common neighbour or cross (w5big_pair_mechanism), each big hub carrying ≤ 269 members (w5big_cloud_le), giving |W₅ᵇ| ≤ 5441 (w5big_card_le).

noncomputable def ACMax.w5big {n : ℕ} (G : SimpleGraph (Fin n)) : Finset (Fin n)

The W₅ᵇ class: usable degree-5 hubs with exactly two twins and a big neighbour.

Equations

• ACMax.w5big G = {w : Fin n | G.degree w = 5 ∧ ACMax.sigS G w ≤ 2 ∧ (ACMax.hubTwins G w).card = 2 ∧ ∃ x ∈ G.neighborFinset w, 9 ≤ G.degree x}

theorem ACMax.w5big_structure {n : ℕ} (G : SimpleGraph (Fin n)) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) (u : Fin n) (hu : u ∈ w5big G) : ∃ (h : Fin n), G.Adj u h ∧ 9 ≤ G.degree h ∧ (∀ x ∈ G.neighborFinset u, x ≠ h → G.degree x ≤ 4) ∧ sigS G u = 1 + sigma (G.degree h)

Structure of a W₅ᵇ member: a unique big neighbour h, every other neighbour light, and sigS = 1 + σ(deg h) exactly.

theorem ACMax.w5big_no_mid_inc {n : ℕ} (G : SimpleGraph (Fin n)) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) (w : Fin n) (h5 : 5 ≤ G.degree w) (h8 : G.degree w ≤ 8) : G.neighborFinset w ∩ w5big G = ∅

Mid-degree vertices (degree 5–8) carry no W₅ᵇ members.

theorem ACMax.w5big_inc_le {n : ℕ} (G : SimpleGraph (Fin n)) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) (K : ℕ) (hK : ∀ (w : Fin n), 9 ≤ G.degree w → (G.neighborFinset w ∩ w5big G).card ≤ K) (y : Fin n) : (G.neighborFinset y ∩ w5big G).card ≤ K + 4

Every vertex carries at most K + 4 members, given the big-hub cap K.

theorem ACMax.w5big_light_nbrs_le {n : ℕ} (G : SimpleGraph (Fin n)) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) (u : Fin n) (hu : u ∈ w5big G) : {w ∈ G.neighborFinset u | G.degree w ≤ 4}.card ≤ 4

Per-member light-neighbour count: at most 4.

theorem ACMax.w5big_big_nbrs_le_one {n : ℕ} (G : SimpleGraph (Fin n)) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) (u : Fin n) (hu : u ∈ w5big G) : {w ∈ G.neighborFinset u | 9 ≤ G.degree w}.card ≤ 1

Per-member big-neighbour count: exactly one, so at most 1.

theorem ACMax.w5big_light_slots_le' {n : ℕ} (G : SimpleGraph (Fin n)) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) (T : Finset (Fin n)) (hT : T ⊆ w5big G) (S : Finset (Fin n)) (hS : ∀ w ∈ S, G.degree w ≤ 8) : ∑ w ∈ S, (G.neighborFinset w ∩ T).card ≤ 4 * T.card

Subset light-slot exchange: for T ⊆ W₅ᵇ and any class S of degree-≤8 vertices, Σ_{w ∈ S} |N(w) ∩ T| ≤ 4·|T|.

theorem ACMax.w5big_law_hypotheses {n : ℕ} (G : SimpleGraph (Fin n)) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) (u h : Fin n) (hu : u ∈ w5big G) (hadj : G.Adj u h) (hbig : 9 ≤ G.degree h) : sigS G u ≤ 1 + sigma (G.degree h) ∧ sigS G u + 1 / (↑(G.degree h) - 2) ≤ 2

The law hypotheses of a member at its big hub: sigS ≤ 1 + σ(deg h) (the erase-free LAW A side condition) and the LAW B slack sigS + 1/(deg h − 2) ≤ 2.

def ACMax.W5LawConfig {V : Type u_1} [Fintype V] (G : SimpleGraph V) : Prop

The σ-law firing configuration: either a LAW A apex configuration or a LAW B cross configuration exists (stated erase-free: the LAW A side condition is sigS ≤ 1 + σ(deg g) and the no-cross condition is pure adjacency).

Equations

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

theorem ACMax.w5LawConfig_closes {V : Type u_1} [Fintype V] [Nonempty V] (G : SimpleGraph V) (h3 : ∀ (v : V), 3 ≤ G.degree v) (hcfg : W5LawConfig G) : algConn G ≤ 2

A firing configuration closes the conjecture.

theorem ACMax.w5big_not_adj {n : ℕ} (G : SimpleGraph (Fin n)) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) (u v : Fin n) (hu : u ∈ w5big G) (hv : v ∈ w5big G) : ¬G.Adj u v

Members are pairwise non-adjacent.

theorem ACMax.w5big_pair_mechanism {n : ℕ} (G : SimpleGraph (Fin n)) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) (hnofire : ¬W5LawConfig G) (u v : Fin n) (hu : u ∈ w5big G) (hv : v ∈ w5big G) (hne : 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 global pair mechanism: unless a σ-law fires, every member pair has a common neighbour or a cross edge with a light endpoint.

theorem ACMax.w5big_cloud_pair_mechanism {n : ℕ} (G : SimpleGraph (Fin n)) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) (hnofire : ¬W5LawConfig G) (h : Fin n) (hbig : 9 ≤ G.degree h) (u v : Fin n) (hu : u ∈ G.neighborFinset h ∩ w5big G) (hv : v ∈ G.neighborFinset h ∩ w5big G) (hne : u ≠ v) : (∃ (w : Fin n), G.Adj u w ∧ G.Adj v w ∧ G.degree w ≤ 4) ∨ ∃ (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 same-cloud pair mechanism: unless a σ-law fires, every pair sharing the big hub h has a light common neighbour or a cross edge with both endpoints light.

theorem ACMax.w5big_deg4_nbrs_le {n : ℕ} (G : SimpleGraph (Fin n)) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) (u : Fin n) (hu : u ∈ w5big G) : {w ∈ G.neighborFinset u | G.degree w = 4}.card ≤ 2

A W₅ᵇ member has at most 2 degree-4 neighbours: its five slots are one big vertex, exactly two degree-3 twins, and the rest.

theorem ACMax.light_weighted_slots_le {n : ℕ} (G : SimpleGraph (Fin n)) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) (T : Finset (Fin n)) (hT : T ⊆ w5big G) : ∑ w : Fin n with G.degree w ≤ 4, (G.degree w - 1) * (G.neighborFinset w ∩ T).card ≤ 10 * T.card

The weighted light-slot exchange: summing (deg−1)·|N(w) ∩ T| over light vertices costs 2 per twin-slot and 3 per degree-4 slot — total 10|T|.

theorem ACMax.w5big_nbr_inter_self_empty {n : ℕ} (G : SimpleGraph (Fin n)) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) (u : Fin n) (hu : u ∈ w5big G) : G.neighborFinset u ∩ w5big G = ∅

A W₅ᵇ member has no w5big neighbours: its neighbourhood is one big vertex and four light ones, none of degree 5.

theorem ACMax.w5_quad {c b : ℕ} (h : c * (c - 1) ≤ b * c) : c ≤ b + 1

Quadratic escape: c(c−1) ≤ b·c forces c ≤ b + 1.

theorem ACMax.w5big_cloud_le {n : ℕ} (G : SimpleGraph (Fin n)) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) (hnofire : ¬W5LawConfig G) (h : Fin n) (hbig : 9 ≤ G.degree h) : (G.neighborFinset h ∩ w5big G).card ≤ 89

The per-cloud cap: unless a σ-law fires, each big hub carries at most 89 members: same-cloud pairs mediate through light-only channels (per-degree refined cells: (deg−1)²·3-weights).

theorem ACMax.w5big_card_le {n : ℕ} (G : SimpleGraph (Fin n)) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) (hnofire : ¬W5LawConfig G) : (w5big G).card ≤ 2301

The global W₅ᵇ bound: unless a σ-law fires, |W₅ᵇ| ≤ 100 + 2200 + 1 = 2301. The P3 slot trade-off: a light x that mediates b big neighbours spends b of its degree slots on them, so it keeps at most deg x − b T-neighbours; balancing the b big cells (≤ 2·89 each) against the deg x − 1 − b small cells (≤ 2·4 each) caps the per-x P3 contribution at 728 (deg 4) / 372 (deg 3).

theorem ACMax.hub_saturated_fires (n : ℕ) [Nonempty (Fin n)] (hn : 512 ≤ n) (G : SimpleGraph (Fin n)) (w : Fin n) (h15 : G.degree w ≤ 15) (ha : G.degree w ≤ (hubTwins G w).card + 1) : algConn G ≤ 2

A saturated small vertex fires the block cut. ANY vertex of degree d ≤ 15 with at least d − 1 degree-3 twins fires algConn_le_two_of_hub_block as soon as n ≥ 512 ≥ 2(k+1)² — in particular a degree-3 vertex with 2 degree-3 neighbours and a degree-4 vertex with 3.

theorem ACMax.blocks_or_smallcap (n : ℕ) [Nonempty (Fin n)] (hn : 512 ≤ n) (G : SimpleGraph (Fin n)) : algConn G ≤ 2 ∨ ∀ (w : Fin n), G.degree w ≤ 15 → (hubTwins G w).card + 2 ≤ G.degree w

The block dichotomy: either some degree-≤ 15 vertex is twin-saturated (and the graph fires), or EVERY vertex of degree d ≤ 15 has at most d − 2 degree-3 neighbours — degree-3 vertices at most one (M is a matching), degree-4 vertices at most two.

theorem ACMax.suppressed_ledger_beta (n : ℕ) [Nonempty (Fin n)] (hn : 512 ≤ n) (G : SimpleGraph (Fin n)) (h : ResidualCore n G) (hb : SeaFatBoundary G) (hcpt : ¬HasUsableFarPair G) : algConn G ≤ 2 ∨ 32 / 21 * ↑{v : Fin n | G.degree v = 3 ∧ 2 < sigS G v}.card ≤ 5 / 4 * ↑(excessX n G) + 423

The β-ledger (β = 105/128 < 7/8): on the boundary of the compact cell, either a σ-law fires (closing the conjecture outright), or the suppressed count obeys the sharpened supply bound

(32/21)·s ≤ (5/4)·X + 423

— i.e. s ≤ (105/128)·X + C, breaking the β = 7/8 ledger wall. The constant is 214 (capped overflow) plus (206 + 2301)/12 (the W₅ overflow through the Moore bound and the refined cloud bound).