The tier-9 girth discharge of the starved census

Kills the never-firing starved census import-free for n ≥ 388, by a girth argument on the honest population V₉ = {v : deg v ≤ 4} (twins and sea together). On the window boundary the deg-4-only sea has excess O(1), but including the twins turns the honest excess into t₉ = n − 4 − X − 3h = Θ(n) (X = excessX, h = #heavies), which the SQRT girth bound consumes.

Main results

• v9_size_row, v9_density_row_quant — the tight size row n ≤ |V₉| + X and the honest quantitative excess v9Pairs ≥ 2|V₉| + 2·t₉.
• v9_short_cycle_fires, v9_girth — the direct deg-≤ 4 instance of master_cycle_fires (a V₉-cycle with 9k ≤ n + 8 fires), so a never-firing graph has no short V₉-cycle.
• GirthExcessBound, girth_excess_bound_holds — the census-free girth import and its unconditional proof, assembling the SQRT cluster with a component descent.
• starved_v9_kill_of_import, starved_v9_kill_sqrt — the rebased kill, with the import discharged via the self-provable SQRT Moore side condition.
• strip_cubic, moore_strip_core, moore_strip_arith, starved_dead_ge_388 — the import-free kill of the whole starved census for n ≥ 388, a single branch: the derived constraint 10X + 7h ≤ 4n − 200 (slots_p_row, p_choke_row_unconditional, heavy_full_budget) discharges the SQRT side condition at the ball radius r = ⌊(⌊(n+8)/9⌋ − 1)/2⌋. The former n ≥ 1100 threshold came from three separate losses in the girth bound (see GirthExcessBound) and a 119-fold giant credit in heavy_full_budget.

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

The honest tier-9 population V₉: the degree-≤ 4 vertices (the twins deg 3 together with the sea deg 4). Its complement is exactly the heavies {deg ≥ 5}, so V₉ is almost everything and its internal excess is Θ(n).

Equations

• ACMax.v9Set G = {v : Fin n | G.degree v ≤ 4}

theorem ACMax.mem_v9Set {n : ℕ} {G : SimpleGraph (Fin n)} {v : Fin n} : v ∈ v9Set G ↔ G.degree v ≤ 4

Membership in the tier-9 population.

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

Ordered adjacent pairs within V₉ (twice the number of internal tier-9 edges); 2·|V₉| < v9Pairs G is the density row "average tier-9 degree > 2".

Equations

• ACMax.v9Pairs G = {q ∈ ACMax.v9Set G ×ˢ ACMax.v9Set G | G.Adj q.1 q.2}.card

theorem ACMax.v9_size_row {n : ℕ} (G : SimpleGraph (Fin n)) : n ≤ (v9Set G).card + excessX n G

The tier-9 size row. n ≤ |V₉| + X (X = excessX n G): Fin n partitions as V₉ ⊔ V₉ᶜ with V₉ᶜ ⊆ {deg ≥ 5}, so |V₉ᶜ| ≤ |heavies| ≤ X (heavy_le_excess). The twins and sea are all inside V₉, so the size row is tight (|V₉| ≥ n − X, not n − 8 − 2X).

theorem ACMax.v9_density_row_quant {n : ℕ} (G : SimpleGraph (Fin n)) (hn : 2 ≤ n) (hm : G.edgeFinset.card = 2 * (n - 2)) : 2 * (v9Set G).card + 2 * n ≤ v9Pairs G + 2 * excessX n G + 6 * (v9Set G)ᶜ.card + 8

The tier-9 quantitative density row (the honest t₉ = Θ(n)). On a census graph (m = 2(n−2), n ≥ 2) the internal tier-9 pairs satisfy 2|V₉| + 2n ≤ v9Pairs + 2X + 6h + 8 (X = excessX n G, h = |V₉ᶜ|), i.e. v9Pairs ≥ 2|V₉| + 2·t₉ with the honest excess t₉ = n − 4 − X − 3h. The twins are inside V₉, so the only leakage is to V₉ᶜ ⊆ heavies: the total-degree identity ∑ deg = 4n − 8 (residual_degree_sum) and the bipartite cross_count give v9Pairs ≥ 4n − 8 − 2∑_R deg, and ∑_R deg = ∑_R(deg − 4) + 4h ≤ X + 4h.

def ACMax.GirthExcessBound (n : ℕ) (G : SimpleGraph (Fin n)) : Prop

N3 — the census-free girth import (SW5′). The single graph-generic girth surface that replaces the falsified AHLSeaTier9/AHLSeaTier18 bylines: quantified over an arbitrary nonempty subset S : Finset (Fin n) and its excess t (no seaSet, no excessX — nothing census; the S.Nonempty guard closes the vacuous S = ∅, t = 0 slot where both side conditions hold but no cycle can land), it says a subgraph on S with excess 2|S| + 2t ≤ pairs(S) (i.e. e(S) ≥ |S| + t) that also meets the strength-specific Moore side condition — here the self-provable SQRT form, stated at the ball radius r rather than at a cycle-length target, as

|S|² < |S|·(2r + 1) + t·(3r² − r)

— contains a cycle of length 3 ≤ k ≤ 2r + 1 inside S. This is the exact negation of the sqrt_double_count conclusion transported from the 2-core to S, so no strength is thrown away between the ball count and the side condition: the older shape 2|S|² ≤ (L − 5)²·t is the same inequality after discarding the |S|(2r+1) ball term, weakening the level floor |L_i| ≥ deg to ≥ 2, and rounding 2r ≥ L − 2 down to L − 5. Recovering those three losses is what moves the import-free floor from n ≥ 1071 to n ≥ 379. Threaded through intermediate bounds and discharged by girth_excess_bound_holds below. The separate AHL strength reaches further down the band.

Equations

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

The SQRT discharge of GirthExcessBound

Assembles the SQRT girth cluster into girth_excess_bound_holds : ∀ n G, GirthExcessBound n G. The one new ingredient is the component descent: after extracting a min-degree-2 core (two_core_aux), a mediant/pigeonhole selects a component C on which sqrt_double_count gives |C|·(1+2r) + 2·t_C·r² ≤ |C|², colliding with the SQRT side condition to force a short cycle that lifts back to G. starved_v9_kill_sqrt is the rebased kill with this import discharged.

theorem ACMax.induce_degree_eq_degWithin {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) (w : ↑↑S) : (SimpleGraph.induce (↑S) G).degree w = degWithin G S ↑w

Induced degree equals the within-S degree. For w ∈ S, the degree of w in the induced subgraph G.induce ↑S is exactly degWithin G S w.

theorem ACMax.degree_induce_supp_eq {V : Type u_1} [Fintype V] [DecidableEq V] (H : SimpleGraph V) [DecidableRel H.Adj] (C : H.ConnectedComponent) (u : ↑C.supp) : (SimpleGraph.induce C.supp H).degree u = H.degree ↑u

Component degree preservation. In a graph H, the degree of a vertex u in the induced graph on its connected component's support equals its degree in H, since every neighbour of u lies in the same component.

theorem ACMax.card_supp_eq_fiber {V : Type u_1} [Fintype V] [DecidableEq V] (H : SimpleGraph V) [DecidableRel H.Adj] [DecidableEq H.ConnectedComponent] (C : H.ConnectedComponent) : Fintype.card ↑C.supp = {v : V | H.connectedComponentMk v = C}.card

Component size as a fibre. The number of vertices in a connected component C equals the number of vertices mapping to C under connectedComponentMk.

theorem ACMax.sum_degree_component_eq {V : Type u_1} [Fintype V] [DecidableEq V] (H : SimpleGraph V) [DecidableRel H.Adj] [DecidableEq H.ConnectedComponent] (C : H.ConnectedComponent) : ∑ v : V with H.connectedComponentMk v = C, H.degree v = 2 * (SimpleGraph.induce C.supp H).edgeFinset.card

Component degree sum. Summing H.degree over the vertices of a connected component C equals twice the edge count of C.toSimpleGraph, via the component handshake and degree preservation.

theorem ACMax.exists_mediant_component {κ : Type u_2} [Fintype κ] (nc tc : κ → ℕ) {N t : ℕ} (hne : Finset.univ.Nonempty) (hN : ∑ C : κ, nc C = N) (ht : t ≤ ∑ C : κ, tc C) : ∃ (C : κ), nc C ^ 2 * t ≤ N ^ 2 * tc C

The mediant pigeonhole. Given nonneg fibre sizes nc and excesses tc over a nonempty finite index with total size N and total excess ≥ t, some index C satisfies nc C² · t ≤ N² · tc C. Otherwise summing the strict reverse inequalities collides with ∑ nc² ≤ (∑ nc)² = N².

theorem ACMax.girth_excess_bound_holds (n : ℕ) (G : SimpleGraph (Fin n)) : GirthExcessBound n G

The girth-excess bound holds for every graph. A nonempty vertex set S with at least 2 * S.card + 2 * t ordered adjacent pairs and S.card ^ 2 < S.card * (2 * r + 1) + t * (3 * r ^ 2 - r), for positive t and r, contains a cycle of length between 3 and 2 * r + 1. The proof extracts a minimum-degree-two core, selects an excess-carrying component, applies the short-cycle bound, and lifts the cycle through the induced-graph embeddings.

The honest heavy budget

The one counting row that lives here rather than in Counting.StarvedCensus: the heavy budget h + h₆₊ + 4·n_g ≤ X, which the MASTER′ assembly consumes. The n ≥ 388 dispatch that this section used to carry has been superseded by Counting.V9DischargeSharp (starved_dead_ge_123), which runs the same collision at the bulk-credited moat radius of Counting.MoatSharp.

theorem ACMax.heavy_full_budget {n : ℕ} (G : SimpleGraph (Fin n)) (hn : 57 ≤ n) : (v9Set G)ᶜ.card + {h ∈ hubSet G | 6 ≤ G.degree h ∧ ¬n + 15 < 9 * G.degree h}.card + 4 * {h ∈ hubSet G | n + 15 < 9 * G.degree h}.card ≤ excessX n G

The honest heavy budget (D1′). At n ≥ 57 the total excess X = excessX n G dominates h + h₆₊ + 4·n_g, where h = |V₉ᶜ| counts the heavies (deg ≥ 5), h₆₊ the non-giant deg-≥6 hubs and n_g the giants (n + 15 < 9·deg). Each deg-≥5 vertex spends deg − 4 ≥ 1 excess (that is h), each deg-≥6 non-giant an extra 1 (so 2 ≤ deg − 4), and each giant (deg ≥ 9 already at n ≥ 57) an extra 4 (so 5 ≤ deg − 4).

The giant credit is 4 — exactly what the MASTER′ assembly consumes (28·n_g ≤ 7·4·n_g). It used to be 119, which forced n ≥ 1100 on this row alone and so on the whole import-free band; 4 costs the assembly nothing and holds from n = 57.