The SQRT girth cluster

A self-contained girth development: from an edge excess t on a graph one extracts a short cycle, quantified by the SQRT bound (g − 5)² ≤ 2|S|²/t. The engine is a BFS ball-excess count in a graph with no cycle of length ≤ 2r + 1.

Main results

• exists_isCycle_of_excess, acyclic_card_edge_le, induced_pairs_eq_two_mul_edges — from |S| edges inside S, extract a cycle whose support lies in S (the induced subgraph is not acyclic).
• cycle_walk_to_zmod — the Walk.IsCycle → (c : ZMod k → Fin n) conversion into the cyclic-map form the master_cycle_fires firing surface expects.
• level_no_internal_edge, level_unique_parent, level_children_count, level_card_growth — the BFS-level growth rows exposing the tree-like ball structure up to radius r (girth-only, no min-degree hypothesis).
• ball_weighted_lower — the quadratic degree-weighted ball lower bound 1 + 2r + Σ_{i<r}(r − i)·ε_i(x) ≤ |B(x, r)| (an equality under connectivity, ε_i = level excess).
• sum_level_excess_swap and the SQRT double count |V|·(1 + 2r) + 2·t·r² ≤ |V|², together with the 2-core extraction two_core_of_excess (degWithin, edgeSumWithin).

theorem ACMax.induced_pairs_eq_two_mul_edges {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) : {q ∈ S ×ˢ S | G.Adj q.1 q.2}.card = 2 * (SimpleGraph.induce (↑S) G).edgeFinset.card

Ordered adjacent pairs count twice the induced edges. The number of ordered pairs (x, y) with x, y ∈ S and G.Adj x y equals 2 * (G.induce ↑S).edgeFinset.card.

The ZMod-cycle conversion

cycle_walk_to_zmod: from a cycle walk w whose support lies inside S, produce k = w.length ≥ 3 and an injective c : ZMod k → Fin n with cyclic adjacency c i ~ c (i+1) and c i ∈ S — the cyclic-map form the master_cycle_fires firing surface expects (c i = w.getVert i.val, injectivity via IsCycle.isPath_dropLast, cyclic adjacency via adj_getVert_succ).

theorem ACMax.cycle_walk_to_zmod {n : ℕ} {G : SimpleGraph (Fin n)} {v : Fin n} {w : G.Walk v v} (hcyc : w.IsCycle) {S : Finset (Fin n)} (hsupp : ∀ x ∈ w.support, x ∈ S) : 3 ≤ w.length ∧ ∃ (c : ZMod w.length → Fin n), Function.Injective c ∧ (∀ (i : ZMod w.length), G.Adj (c i) (c (i + 1))) ∧ ∀ (i : ZMod w.length), c i ∈ S

The Walk.IsCycle → ZMod k conversion. A cycle walk w in G of length k whose support sits inside S yields 3 ≤ k and an injective cyclic map c : ZMod k → Fin n (c i ~ c (i+1), c i ∈ S) — the existential shape demanded by GirthExcessBound. Reusable for any girth discharge that produces a bounded-length cycle walk.

BFS-level growth rows

The BFS levels L_i(x) = (Finset.univ.filter fun v => dist x v = i) in a graph with no cycle of length ≤ 2r + 1 are tree-like: no edge inside a level (level_no_internal_edge), a level-(i+1) vertex has a unique parent (level_unique_parent), a level-i vertex sends deg v − 1 edges up (level_children_count), and the levels grow by |L_{i+1}| = Σ_{v∈L_i}(deg v − 1) (level_card_growth). All four are girth-only (no min-degree hypothesis).

theorem ACMax.dist_le_of_mem_support {V : Type u_1} (G : SimpleGraph V) {x z : V} (g : G.Walk x z) {w : V} (hw : w ∈ g.support) : G.dist x w ≤ g.length

The distance from x to a vertex on a walk x → z is bounded by the walk's length.

theorem ACMax.no_short_cycle_of_paths {V : Type u_1} (G : SimpleGraph V) {r : ℕ} (hg : ∀ (v : V) (c : G.Walk v v), c.IsCycle → 2 * r + 1 < c.length) {x y : V} {P Q : G.Walk x y} (hP : P.IsPath) (hQ : Q.IsPath) (hne : P ≠ Q) (hlen : P.length + Q.length ≤ 2 * r + 1) : False

Two distinct paths with the same endpoints whose total length is ≤ 2r + 1 are impossible under the girth hypothesis: they close a cycle of length ≤ 2r + 1.

theorem ACMax.notMem_geodesic_of_dist_eq {V : Type u_1} (G : SimpleGraph V) {x y : V} (g : G.Walk x y) (hglen : g.length = G.dist x y) {z : V} (hdist : G.dist x z = G.dist x y) (hne : z ≠ y) : z ∉ g.support

On a geodesic g : x → y, a vertex z ≠ y at the same distance from x as y cannot lie on g (the geodesic reaches distance dist x y only at its endpoint).

theorem ACMax.level_no_internal_edge {V : Type u_1} (G : SimpleGraph V) {r : ℕ} (hg : ∀ (v : V) (c : G.Walk v v), c.IsCycle → 2 * r + 1 < c.length) (x : V) {i : ℕ} (hi1 : 1 ≤ i) (hir : i ≤ r) {v w : V} (hv : G.dist x v = i) (hw : G.dist x w = i) : ¬G.Adj v w

No same-level edge. Under hg (no cycle of length ≤ 2r + 1), no two vertices at the same BFS level L_i(x) with 1 ≤ i ≤ r are adjacent — the edge plus two dist-i geodesics would close a cycle of length ≤ 2i + 1 ≤ 2r + 1.

theorem ACMax.level_unique_parent {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] {r : ℕ} (hg : ∀ (v : V) (c : G.Walk v v), c.IsCycle → 2 * r + 1 < c.length) (x : V) {i : ℕ} (hir : i + 1 ≤ r) {v : V} (hv : G.dist x v = i + 1) : {w ∈ G.neighborFinset v | G.dist x w = i}.card = 1

Unique parent. Under hg, a level-(i+1) vertex v (i + 1 ≤ r) has exactly one neighbour at level i: ((N v) ∩ L_i).card = 1. Existence is the penultimate vertex of a geodesic x → v; uniqueness is a short cycle from two length-(i+1) paths to v.

theorem ACMax.level_children_count {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] {r : ℕ} (hg : ∀ (v : V) (c : G.Walk v v), c.IsCycle → 2 * r + 1 < c.length) (x : V) {i : ℕ} (hi1 : 1 ≤ i) (hir : i ≤ r) {v : V} (hv : G.dist x v = i) : {w ∈ G.neighborFinset v | G.dist x w = i + 1}.card = G.degree v - 1

Children count. Under hg, a level-i vertex v (1 ≤ i ≤ r) has exactly deg v − 1 neighbours at level i + 1. Its neighbourhood splits into the unique parent (level i − 1), no same-level neighbour, and the remaining deg v − 1 children at level i + 1.

theorem ACMax.level_card_growth {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] {r : ℕ} (hg : ∀ (v : V) (c : G.Walk v v), c.IsCycle → 2 * r + 1 < c.length) (x : V) {i : ℕ} (hi1 : 1 ≤ i) (hir : i + 1 ≤ r) : {v : V | G.dist x v = i + 1}.card = ∑ v : V with G.dist x v = i, (G.degree v - 1)

Level identity. Under hg, for 1 ≤ i and i + 1 ≤ r the BFS level L_{i+1}(x) has cardinality Σ_{v ∈ L_i}(deg v − 1). Proof: double-count the L_i–L_{i+1} edges — the parent map (level_unique_parent) counts each child once, the children map (level_children_count) sums to Σ(deg v − 1), and the two counts agree by symmetry of adjacency.

The quadratic degree-weighted ball lower bound

The engine behind (g − 5)² ≤ 2|S|²/t. For a root x in a connected graph with minimum degree ≥ 2 and no cycle of length ≤ 2r + 1, with level excess ε_i(x) = Σ_{v∈L_i}(deg v − 2), the ball satisfies

1 + 2r + Σ_{i < r}(r − i)·ε_i(x) ≤ |B(x, r)|.

Under connectivity this is an equality: the ball partitions into levels whose sizes telescope through level_card_growth, each excess ε_i surfacing in the r − i levels i+1, …, r. Connectivity is essential — SimpleGraph.dist returns 0 for unreachable pairs, so without it L_0 and the ball absorb the far part of the graph and the bound breaks (ball_weighted_lower).

theorem ACMax.sum_range_triangle (r : ℕ) (ε : ℕ → ℕ) : ∑ i ∈ Finset.range r, ∑ k ∈ Finset.range (i + 1), ε k = ∑ k ∈ Finset.range r, (r - k) * ε k

Triangular double-sum identity. Σ_{i < r} Σ_{k ≤ i} ε k = Σ_{k < r}(r − k)·ε k: reindex the lower-triangular pairs k ≤ i < r by their column k, which appears in the r − k rows k, …, r − 1.

theorem ACMax.ball_weighted_lower {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] {r : ℕ} (hmin : ∀ (v : V), 2 ≤ G.degree v) (hg : ∀ (v : V) (c : G.Walk v v), c.IsCycle → 2 * r + 1 < c.length) (hconn : G.Connected) (x : V) : 1 + 2 * r + ∑ i ∈ Finset.range r, (r - i) * ∑ v : V with G.dist x v = i, (G.degree v - 2) ≤ {v : V | G.dist x v ≤ r}.card

Quadratic degree-weighted ball bound. In a connected graph with minimum degree at least 2 and no cycle of length ≤ 2r + 1, the ball B(x, r) = (Finset.univ.filter fun v => dist x v ≤ r) satisfies 1 + 2r + Σ_{i < r}(r − i)·ε_i(x) ≤ |B(x, r)|, where ε_i(x) = Σ_{v ∈ L_i}(deg v − 2) is the excess at BFS level L_i(x) = (Finset.univ.filter fun v => dist x v = i). Under connectivity the bound is an exact equality; the levels telescope through level_card_growth.

The SQRT double count

The global double count turning the per-root ball_weighted_lower into (g − 5)² ≤ 2|S|²/t. Fix a connected graph on a finite V, minimum degree ≥ 2, edge excess t (|V| + t ≤ e(G)), and no cycle of length ≤ 2r + 1. Summing the ball bound over all roots, using the swap sum_level_excess_swap (Σ_x ε_i(x) = Σ_v (deg v − 2)·|L_i(v)| by distance symmetry), the level floor level_card_ge_two and the handshake Σ_v (deg v − 2) ≥ 2t, yields the quadratic

|V|·(1 + 2r) + 2·t·r² ≤ |V|².

The full GirthExcessBound discharge additionally needs a component descent (picking the component carrying the excess), the contrapositive arithmetic, and the exists_isCycle_of_excess / cycle_walk_to_zmod witness plumbing.

theorem ACMax.two_mul_sum_range_sub (m : ℕ) : 2 * ∑ i ∈ Finset.range m, (m - i) = m * (m + 1)

Triangular Gauss sum. 2·Σ_{i<m}(m − i) = m·(m + 1): the descending run m, m−1, …, 1 has twice-sum m(m+1).

theorem ACMax.level_card_ge_deg {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] {r : ℕ} (hmin : ∀ (v : V), 2 ≤ G.degree v) (hg : ∀ (v : V) (c : G.Walk v v), c.IsCycle → 2 * r + 1 < c.length) (x : V) {j : ℕ} (hj1 : 1 ≤ j) (hjr : j ≤ r) : G.degree x ≤ {v : V | G.dist x v = j}.card

BFS levels are at least as wide as the root degree. The sharpening of level_card_ge_two that the SQRT double count actually wants: in a graph with minimum degree at least 2 and no cycle of length ≤ 2r + 1, every BFS level L_j(x) = (Finset.univ.filter fun v => dist x v = j) with 1 ≤ j ≤ r has at least deg x vertices — the deg x branches leaving x stay separated all the way out to radius r, since two of them meeting at distance j ≤ r would close a cycle of length ≤ 2j ≤ 2r.

Formally this is the same induction as level_card_ge_two, which already produces deg x at the base level (L_1(x) is the neighbourhood) and then only ever needs deg v − 1 ≥ 1 to carry the floor outward; level_card_ge_two immediately weakens the base to 2 ≤ deg x and loses the extra deg x − 2. Keeping it multiplies the excess term of sqrt_double_count by 3/2.

theorem ACMax.sum_level_excess_swap {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (i : ℕ) : ∑ x : V, ∑ v : V with G.dist x v = i, (G.degree v - 2) = ∑ v : V, {x : V | G.dist v x = i}.card * (G.degree v - 2)

The BFS-level swap. Summing the level-i excess Σ_{v : dist x v = i}(deg v − 2) over all roots x regroups (by symmetry of distance) as Σ_v (deg v − 2)·|{x : dist v x = i}|.

theorem ACMax.sqrt_double_count {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] {r t : ℕ} (hmin : ∀ (v : V), 2 ≤ G.degree v) (hg : ∀ (v : V) (c : G.Walk v v), c.IsCycle → 2 * r + 1 < c.length) (hconn : G.Connected) (hexc : Fintype.card V + t ≤ G.edgeFinset.card) : Fintype.card V * (1 + 2 * r) + t * (3 * r ^ 2 - r) ≤ Fintype.card V ^ 2

The SQRT double count. In a connected graph G on a finite V with minimum degree at least 2, edge excess t (|V| + t ≤ e(G)), and no cycle of length ≤ 2r + 1, the ball double count gives |V|·(1 + 2r) + t·(3r² − r) ≤ |V|². Summing ball_weighted_lower over all roots, swapping (sum_level_excess_swap), and feeding the handshake Σ_v(deg v − 2) ≥ 2t together with the level floor |L_i(v)| ≥ deg v (1 ≤ i ≤ r, level_card_ge_deg) telescoped by two_mul_sum_range_sub.

The excess weight is 3r² − r, not the 2r² obtained from the weaker floor |L_i(v)| ≥ 2 (level_card_ge_two): an excess vertex v is seen at distance i by at least deg v ≥ 3 roots, not merely 2, so W i ≥ 3D for 1 ≤ i ≤ r and the triangular telescope returns rD + 3D·r(r−1)/2 ≥ t(3r² − r). Since 3r² − r ≥ 2r² for r ≥ 1, this strictly strengthens the old conclusion, and it is what pulls the import-free girth floor down.

The 2-core extraction

The entry piece: from a graph with edge excess t, extract an induced subgraph of minimum degree ≥ 2 still carrying the whole excess (two_core_of_excess). The within-S bookkeeping is degWithin G S v (neighbours of v inside S) and edgeSumWithin G S = ∑_{u∈S} degWithin G S u (twice the induced edge count), with the handshake edgeSumWithin_eq_pairs and the erase law edgeSumWithin_erase.

def ACMax.degWithin {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) (v : V) : ℕ

The number of neighbours of v lying inside the finite set S — the degree of v in the induced subgraph G.induce ↑S.

Equations

• ACMax.degWithin G S v = {w ∈ S | G.Adj v w}.card

def ACMax.edgeSumWithin {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) : ℕ

Twice the number of edges of G with both endpoints in S, written as the within-S degree sum.

Equations

• ACMax.edgeSumWithin G S = ∑ u ∈ S, ACMax.degWithin G S u

theorem ACMax.edgeSumWithin_eq_pairs {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) : edgeSumWithin G S = {q ∈ S ×ˢ S | G.Adj q.1 q.2}.card

The within-S handshake. The within-S degree sum equals the number of ordered adjacent pairs with both coordinates in S.

theorem ACMax.edgeSumWithin_erase {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {S : Finset V} {v : V} (hv : v ∈ S) : edgeSumWithin G S = edgeSumWithin G (S.erase v) + 2 * degWithin G S v

The erase law. Deleting a vertex v ∈ S drops the within-S degree sum by exactly twice the within-S degree of v.

theorem ACMax.two_core_aux {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] {t : ℕ} (ht : 1 ≤ t) (S : Finset V) : 2 * S.card + 2 * t ≤ edgeSumWithin G S → ∃ S' ⊆ S, S'.Nonempty ∧ (∀ v ∈ S', 2 ≤ degWithin G S' v) ∧ 2 * S'.card + 2 * t ≤ edgeSumWithin G S'

The 2-core induction. Starting from any S carrying the excess 2·|S| + 2t ≤ edgeSumWithin G S, one reaches a nonempty subset of minimum within-degree ≥ 2 still carrying the excess, by repeatedly deleting a within-degree ≤ 1 vertex.