The compact-cell reduction of the Δ ≥ 5 fat side

Develops the fat frontier (ResidualCore n G with a vertex of degree ≥ 5) and reduces it to a bounded compact cell. The σ-ecology of a min-degree-3 world (σ(d) = (d−3)/(d−2), cW, sigS) drives a family of test-vector certificates; when none fires the graph is a compact cell whose size is bounded by the total degree excess.

Main results

• algConn_le_two_of_slot_far_pair — the slot far-pair certificate: a far pair u, v with slot value c_v²·(Σσ_u − 2) + c_u²·(Σσ_v − 2) + Σ_{cross} (p_w + q_{w'})² ≤ 0 certifies algConn G ≤ 2, a σ-arithmetic instance of the weighted double-star master (per-slot identity (c_v − p_w)² + (deg w − 1)·p_w² = 2·p_w² + c_v²·σ(deg w)).
• algConn_le_two_of_usable_far_pair, HasUsableFarPair — the cross-free usable far-pair law: two σ-usable vertices (sigS ≤ 2) at distance ≥ 4 close; HasUsableFarPair is the spread/compact discriminator.
• usable_deg3_of_light, nonusable_deg3_structure — the σ-profile suppression: a degree-3 vertex with neighbour degrees ≤ 5 is usable, and a non-usable one has a heavy neighbourhood.
• card_closeSet_le_light_twoball bounds the size of a three-step neighborhood in terms of nearby degree excess. Together with card_heavy_le and card_nonusable_light_le, it supplies the counting vocabulary used downstream.
• boundLin packages the numerical bound max ((151 + 11·C₀) / 2) 520 used by the large-order reduction. The full theorem is assembled in Band.Final.

The σ ecology quantities

noncomputable def ACMax.sigma (d : ℕ) : ℝ

The slot value function σ(d) = (d−3)/(d−2): the per-slot worst-case surplus of a degree-d neighbour used as a leak carrier. σ(3) = 0, σ(4) = 1/2, σ(5) = 2/3, σ(6) = 3/4, σ → 1.

Equations

• ACMax.sigma d = (↑d - 3) / (↑d - 2)

noncomputable def ACMax.cW {V : Type u_1} [Fintype V] (G : SimpleGraph V) (u : V) : ℝ

The mass factor c_u = 1 + Σ_{w∈N(u)} 1/(deg w − 2).

Equations

• ACMax.cW G u = 1 + ∑ w ∈ G.neighborFinset u, 1 / (↑(G.degree w) - 2)

noncomputable def ACMax.sigS {V : Type u_1} [Fintype V] (G : SimpleGraph V) (u : V) : ℝ

The σ-sum Σσ_u = Σ_{w∈N(u)} σ(deg w).

Equations

• ACMax.sigS G u = ∑ w ∈ G.neighborFinset u, ACMax.sigma (G.degree w)

σ arithmetic (L-FB-2 real-valued facts)

theorem ACMax.sigma_three : sigma 3 = 0

theorem ACMax.sigma_four : sigma 4 = 1 / 2

theorem ACMax.sigma_five : sigma 5 = 2 / 3

theorem ACMax.sigma_six : sigma 6 = 3 / 4

theorem ACMax.sigma_nonneg {d : ℕ} (hd : 3 ≤ d) : 0 ≤ sigma d

σ(d) ≥ 0 for d ≥ 3.

theorem ACMax.sigma_lt_one {d : ℕ} (hd : 3 ≤ d) : sigma d < 1

σ(d) < 1 for d ≥ 3.

theorem ACMax.sigma_le_of_le {c d : ℕ} (hc : 3 ≤ c) (hcd : c ≤ d) : sigma c ≤ sigma d

σ is monotone on d ≥ 3: σ(d) = 1 − 1/(d−2).

theorem ACMax.sigSum_le_two_of_three_nbrs_deg_le_five {V : Type u_1} [Fintype V] (G : SimpleGraph V) (u : V) (hmin : ∀ (w : V), 3 ≤ G.degree w) (hdeg : G.degree u = 3) (hnbr : ∀ w ∈ G.neighborFinset u, G.degree w ≤ 5) : sigS G u ≤ 2

σ-usability at Δ = 5: three neighbours of degree ≤ 5 give σ-sum ≤ 2 (the (5,5,5) tie). This is the exact fact that makes every degree-3 vertex a usable slot far-pair end in a Δ ≤ 5 world.

cW positivity

theorem ACMax.one_le_cW {V : Type u_1} [Fintype V] (G : SimpleGraph V) (u : V) (hmin : ∀ (w : V), 3 ≤ G.degree w) : 1 ≤ cW G u

The mass factor is at least 1 on a graph of minimum degree ≥ 3.

theorem ACMax.cW_pos {V : Type u_1} [Fintype V] (G : SimpleGraph V) (u : V) (hmin : ∀ (w : V), 3 ≤ G.degree w) : 0 < cW G u

L-FB-1: the slot far-pair certificate

theorem ACMax.slot_pointwise (au : ℝ) (d : ℕ) (hd : 3 ≤ d) : (au - au / (↑d - 2)) ^ 2 + (↑d - 1) * (au / (↑d - 2)) ^ 2 = 2 * (au / (↑d - 2)) ^ 2 + au ^ 2 * sigma d

The per-slot identity. With slot weight p = au/(d−2) and worst-case leak d − 1, the slot cost equals 2·p² + au²·σ(d).

theorem ACMax.algConn_le_two_of_slot_far_pair {V : Type u_1} [Fintype V] [Nonempty V] (G : SimpleGraph V) (u v : V) (hne : u ≠ v) (huv : ¬G.Adj u v) (hcap : ∀ (w : V), ¬(G.Adj u w ∧ G.Adj v w)) (hmin : ∀ (w : V), 3 ≤ G.degree w) (hslot : (cW G v ^ 2 * (sigS G u - 2) + cW G u ^ 2 * (sigS G v - 2) + ∑ w ∈ G.neighborFinset u, ∑ w' ∈ G.neighborFinset v, if G.Adj w w' then (cW G v / (↑(G.degree w) - 2) + cW G u / (↑(G.degree w') - 2)) ^ 2 else 0) ≤ 0) : algConn G ≤ 2

L-FB-1 — the slot far-pair certificate (general cross form). A far pair u ≠ v (not adjacent, no common neighbour) in a graph of minimum degree ≥ 3 whose slot value

c_v²·(Σσ_u − 2) + c_u²·(Σσ_v − 2) + Σ_{w∈N(u),w'∈N(v)} [w ~ w']·(p_w + q_{w'})² ≤ 0

certifies algConn G ≤ 2. Instance of algConn_le_two_of_weighted_double_star with slot weights p_w = c_v/(deg w − 2), q_{w'} = c_u/(deg w' − 2).

theorem ACMax.algConn_le_two_of_slot_far_pair_far {V : Type u_1} [Fintype V] [Nonempty V] (G : SimpleGraph V) (u v : V) (hne : u ≠ v) (huv : ¬G.Adj u v) (hcap : ∀ (w : V), ¬(G.Adj u w ∧ G.Adj v w)) (hmin : ∀ (w : V), 3 ≤ G.degree w) (hfar : ∀ (w w' : V), G.Adj u w → G.Adj v w' → ¬G.Adj w w') (hslot0 : cW G v ^ 2 * (sigS G u - 2) + cW G u ^ 2 * (sigS G v - 2) ≤ 0) : algConn G ≤ 2

L-FB-1 — cross-free (distance-≥ 4) corollary. When there is no edge between N(u) and N(v) the cross term vanishes, and the criterion reduces to c_v²·(Σσ_u − 2) + c_u²·(Σσ_v − 2) ≤ 0.

theorem ACMax.algConn_le_two_of_slot_far_pair_both {V : Type u_1} [Fintype V] [Nonempty V] (G : SimpleGraph V) (u v : V) (hne : u ≠ v) (huv : ¬G.Adj u v) (hcap : ∀ (w : V), ¬(G.Adj u w ∧ G.Adj v w)) (hmin : ∀ (w : V), 3 ≤ G.degree w) (hfar : ∀ (w w' : V), G.Adj u w → G.Adj v w' → ¬G.Adj w w') (hu : sigS G u ≤ 2) (hv : sigS G v ≤ 2) : algConn G ≤ 2

L-FB-1 — the hslot_both workhorse form. A cross-free far pair each of whose ends is σ-usable (Σσ ≤ 2) fires. This is the exact form that makes every clean carrier / Δ ≤ 5 degree-3 end usable.

The slot-far-pair packaging and the fat-side assembly

The spread half: the usable-far-pair firing law

The spread (large-diameter) half of the fat side. The workhorse algConn_le_two_of_usable_far_pair is the cross-free instance of the slot far-pair certificate: two σ-usable vertices (sigS ≤ 2) at distance ≥ 4 close, the slot value collapsing to c_v²·(Σσ_u − 2) + c_u²·(Σσ_v − 2) ≤ 0. This strengthens the all-degree-≤ 4 far-pair law to every usable profile. spread_fat_close discharges any fat ResidualCore graph carrying such a pair, so HasUsableFarPair reduces the open input to the compact boundary only.

theorem ACMax.algConn_le_two_of_usable_far_pair {V : Type u_1} [Fintype V] [Nonempty V] (G : SimpleGraph V) (u v : V) (hne : u ≠ v) (huv : ¬G.Adj u v) (hcap : ∀ (w : V), ¬(G.Adj u w ∧ G.Adj v w)) (hfar : ∀ (w w' : V), G.Adj u w → G.Adj v w' → ¬G.Adj w w') (hmin : ∀ (w : V), 3 ≤ G.degree w) (hu : sigS G u ≤ 2) (hv : sigS G v ≤ 2) : algConn G ≤ 2

L-USABLE-FAR — usable clean far pair fires. Two vertices u ≠ v at distance ≥ 4 (not adjacent, no common neighbour hcap, and no N(u)–N(v) edge hfar) in a graph of minimum degree ≥ 3, both of whose σ-sums are usable (sigS ≤ 2), certify algConn G ≤ 2.

Instance of the cross-free slot certificate algConn_le_two_of_slot_far_pair_both (GeneralFatSide): with no cross edges the slot value is c_v²·(Σσ_u − 2) + c_u²·(Σσ_v − 2), which is ≤ 0 precisely when both ends are usable. Strengthens algConn_le_two_of_far_pair_deg4 from the Δ ≤ 4 ball to every usable degree profile; tight at the (5,5,5) σ-tie (value = 2).

The HasUsableFarPair packaging + spread closer

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

A usable clean far pair exists. G has two vertices at distance ≥ 4 (combinatorially: u ≠ v, ¬Adj u v, no common neighbour, no N(u)–N(v) edge) each of which is σ-usable. This is the exact spread witness: present on every diameter-≥ 4 "buried" world and absent on every diameter-3 compact cell inhabitant.

Equations

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

theorem ACMax.hasUsableFarPair_algConn_le_two {V : Type u_1} [Fintype V] [Nonempty V] (G : SimpleGraph V) (hmin : ∀ (w : V), 3 ≤ G.degree w) (h : HasUsableFarPair G) : algConn G ≤ 2

A usable clean far pair closes the graph (given δ ≥ 3).

σ-profile suppression lemmas

Sharp bounds on the σ-sum sigS G u = Σ_{w∈N(u)} σ(deg w) in a min-degree-3 world: usable_deg3_of_light (a degree-3 vertex with all neighbours of degree ≤ 5 is usable) and nonusable_deg3_structure (a non-usable degree-3 vertex has all three neighbours of degree ≥ 4, one of degree ≥ 6, and two of degree ≥ 5).

σ arithmetic on the profile intervals

theorem ACMax.sigma_mono {d e : ℕ} (hd : 3 ≤ d) (hde : d ≤ e) : sigma d ≤ sigma e

σ is monotone on d ≥ 3 (restatement of sigma_le_of_le in the frontier-facing name).

σ-sum versus the heavy-neighbour count

theorem ACMax.usable_deg3_of_light {V : Type u_1} [Fintype V] (G : SimpleGraph V) (u : V) (hd : G.degree u = 3) (h3 : ∀ (w : V), 3 ≤ G.degree w) (hlight : ∀ w ∈ G.neighborFinset u, G.degree w ≤ 5) : sigS G u ≤ 2

Usability of light degree-3 vertices: a degree-3 vertex all of whose neighbours have degree ≤ 5 has sigS ≤ 3 · σ(5) = 2.

The non-usable degree-3 frontier

theorem ACMax.nonusable_deg3_structure {V : Type u_1} [Fintype V] (G : SimpleGraph V) (u : V) (hd : G.degree u = 3) (h3 : ∀ (w : V), 3 ≤ G.degree w) (h : 2 < sigS G u) : (∀ w ∈ G.neighborFinset u, 4 ≤ G.degree w) ∧ (∃ w ∈ G.neighborFinset u, 6 ≤ G.degree w) ∧ {w ∈ G.neighborFinset u | 5 ≤ G.degree w}.card ≥ 2

Structure of a non-usable degree-3 vertex: if deg u = 3 and sigS G u > 2, then all three neighbours are heavy (degree ≥ 4), at least one has degree ≥ 6, and at least two have degree ≥ 5.

The parametric compact-covering theorem

On the compact cell (¬HasUsableFarPair G), every vertex outside the radius-3 ball around a usable vertex u₀ is non-usable. Non-usable light (degree ≤ 4) vertices each have a heavy neighbour, so number at most 5·X, and the heavy vertices number at most X, where X = ∑_{deg v ≥ 5} (deg v − 4) is the total degree excess. Since every degree is at most 4 + X, the radius-3 ball gives the covering bound n ≤ 1 + (4+X) + (4+X)² + (4+X)³ + 6·X (compact_covering): a compact ResidualCore world is finite in n for each fixed excess X.

noncomputable def ACMax.excessX (n : ℕ) (G : SimpleGraph (Fin n)) : ℕ

The total degree excess X = ∑_{deg v ≥ 5} (deg v − 4) (ℕ-valued; the truncated subtraction is exact since every summand has degree ≥ 5).

Equations

• ACMax.excessX n G = ∑ v : Fin n with 5 ≤ G.degree v, (G.degree v - 4)

noncomputable def ACMax.closeSet {n : ℕ} (G : SimpleGraph (Fin n)) (u₀ : Fin n) : Finset (Fin n)

The radius-3 combinatorial ball around u₀: u₀ together with its neighbours, second neighbours, and third neighbours.

Equations

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

theorem ACMax.mem_closeSet_self {n : ℕ} (G : SimpleGraph (Fin n)) (u₀ : Fin n) : u₀ ∈ closeSet G u₀

The centre is in the ball.

theorem ACMax.mem_closeSet_of_adj {n : ℕ} (G : SimpleGraph (Fin n)) {u₀ v : Fin n} (h : G.Adj u₀ v) : v ∈ closeSet G u₀

A neighbour of u₀ is in the ball.

theorem ACMax.mem_closeSet_of_adj_adj {n : ℕ} (G : SimpleGraph (Fin n)) {u₀ w v : Fin n} (h1 : G.Adj u₀ w) (h2 : G.Adj w v) : v ∈ closeSet G u₀

A second neighbour of u₀ is in the ball.

theorem ACMax.mem_closeSet_of_adj_adj_adj {n : ℕ} (G : SimpleGraph (Fin n)) {u₀ w x v : Fin n} (h1 : G.Adj u₀ w) (h2 : G.Adj w x) (h3 : G.Adj x v) : v ∈ closeSet G u₀

A third neighbour of u₀ is in the ball.

theorem ACMax.far_of_not_mem_closeSet {n : ℕ} (G : SimpleGraph (Fin n)) (u₀ v : Fin n) (hv : v ∉ closeSet G u₀) : v ≠ u₀ ∧ ¬G.Adj u₀ v ∧ (∀ (w : Fin n), ¬(G.Adj u₀ w ∧ G.Adj v w)) ∧ ∀ (w w' : Fin n), G.Adj u₀ w → G.Adj v w' → ¬G.Adj w w'

Vertices outside the ball are far: v ∉ closeSet G u₀ yields the four combinatorial distance-≥ 4 conditions of a clean far pair.

theorem ACMax.nonusable_of_far {n : ℕ} (G : SimpleGraph (Fin n)) (hcpt : ¬HasUsableFarPair G) (u₀ : Fin n) (hu₀ : sigS G u₀ ≤ 2) (v : Fin n) (hv : v ∉ closeSet G u₀) : 2 < sigS G v

On the compact cell, far vertices are non-usable: with no usable far pair and u₀ usable, every vertex outside the ball has sigS > 2.

theorem ACMax.nonusable_light_has_heavy_nbr {n : ℕ} (G : SimpleGraph (Fin n)) (h3 : ∀ (w : Fin n), 3 ≤ G.degree w) (v : Fin n) (hd : G.degree v ≤ 4) (h : 2 < sigS G v) : ∃ w ∈ G.neighborFinset v, 5 ≤ G.degree w

Non-usable light vertices see a heavy vertex: if deg v ≤ 4 and sigS v > 2, some neighbour has degree ≥ 5 (else all σ-terms are ≤ 1/2 and the sum is ≤ 4·(1/2) = 2).

theorem ACMax.card_nonusable_light_le {n : ℕ} (G : SimpleGraph (Fin n)) (h3 : ∀ (w : Fin n), 3 ≤ G.degree w) : {v : Fin n | G.degree v ≤ 4 ∧ 2 < sigS G v}.card ≤ 5 * excessX n G

The non-usable light population is at most 5·X: each such vertex is a neighbour of a heavy vertex, and ∑_{heavy w} deg w ≤ 5·∑_{heavy w} (deg w − 4).

theorem ACMax.card_heavy_le {n : ℕ} (G : SimpleGraph (Fin n)) : {v : Fin n | 5 ≤ G.degree v}.card ≤ excessX n G

The heavy population is at most X: each heavy vertex contributes at least 1 to the excess.

The linear compact-covering theorem

Sharpens the cubic compact_covering bound to a linear one. With minimum degree 3 each breadth-first layer satisfies |Lₖ₊₁| ≤ 4·|Lₖ| + X, so |B₃(u₀)| ≤ 85 + 27·X; combined with the far-vertex partition (non-usable light ≤ 5X, heavy ≤ X) this gives n ≤ 53 + 19·X. The assembly acmax_general_of_xbound_linear uses the linear bound boundLin in place of the cubic one.

theorem ACMax.sum_degree_sub_one_le_local {n : ℕ} (G : SimpleGraph (Fin n)) (S : Finset (Fin n)) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) : ∑ w ∈ S, (G.degree w - 1) ≤ 3 * S.card + ∑ w ∈ S with 5 ≤ G.degree w, (G.degree w - 4)

Local pointwise-summed degree bound: with minimum degree 3, ∑_{w ∈ S} (deg w − 1) ≤ 3·|S| + ∑_{w ∈ S, deg ≥ 5} (deg w − 4) — the excess part charged only to S itself.

theorem ACMax.card_closeSet_le_light_twoball {n : ℕ} (G : SimpleGraph (Fin n)) (u₀ : Fin n) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) (h4 : G.degree u₀ ≤ 4) : (closeSet G u₀).card ≤ 53 + 4 * ∑ w ∈ insert u₀ (G.neighborFinset u₀ ∪ (G.neighborFinset u₀).biUnion fun (w : Fin n) => G.neighborFinset w) with 5 ≤ G.degree w, (G.degree w - 4)

def ACMax.boundLin (C₀ : ℕ) : ℕ

The linear covering bound evaluated at an excess bound C₀: the light-anchor cover 53 + 6·C₀ (the disjoint-slot 6X covering: heavy counts are dominated by their own excess pools) when a light usable vertex exists; the second arm 199990 dominates both the all-usable-heavy case (n + 8 ≤ 5·29877) and the hoarding wall (199985 = 6·33322 + 53).

Equations

• ACMax.boundLin C₀ = max ((151 + 11 * C₀) / 2) 520