The SUM (vertex-ball) Moore refutation — the band-discharge spine (B1–B3)

This file lands the SUM (vertex-ball) sharpening of the Alon–Hoory–Linial irregular Moore bound (nodes B1–B3 of the band discharge), the spine of the hStarved55 discharge on 64 ≤ n ≤ 387. It composes the landed AM–GM walk-count lower bound (nb_amgm_lambda, lambda_ge) with a new ball injectivity: at girth > 2ℓ the endpoints of all non-backtracking walks of length 1..ℓ from a fixed start are pairwise distinct and differ from the start. Writing n = Fintype.card V and D = ∑ v, G.degree v, the ball form D · Σ_{k<ℓ} (D − n)^k n^(ℓ−1−k) ≤ n^ℓ (n − 1) keeps the whole Moore ball (not just the top level), buying the extra half-level over the pair form ahl_irregular_moore.

Contents

• nb_walk_isPath_of_girth_sharp (B1) — the sharp NB-path lemma: girth > r (not 2r + 1) already forces every non-backtracking walk of length ≤ r to be a path. The landed induction only ever closes a cycle of length ≤ r, so the weaker hypothesis suffices.
• nb_ball_injectivity (B2) — the vertex-ball injectivity: at girth > 2ℓ, Σ_{k ∈ Icc 1 ℓ} nbTotalWalks G k ≤ n·(n − 1). Per start x, the endpoint map on all NB walks of length 1..ℓ is injective into univ.erase x.
• ahl_ball_moore (B3) — the SUM Moore bound D · Σ_{k<ℓ} (D − n)^k n^(ℓ−1−k) ≤ n^ℓ (n − 1); and its girth-side contrapositive ahl_ball_girth_bound (n^ℓ(n − 1) < D · Σ … ⟹ ∃ cycle ≤ 2ℓ), the form the band arithmetic instantiates at the extremal V₉/2-core.

theorem ACMax.nb_walk_isPath_of_girth_sharp {V : Type u_1} (G : SimpleGraph V) {r : ℕ} (hg : ∀ (v : V) (c : G.Walk v v), c.IsCycle → r < c.length) {x y : V} (w : G.Walk x y) : IsNonBacktracking w → w.length ≤ r → w.IsPath

B1 — the sharp non-backtracking path lemma. In a graph with no cycle of length ≤ r, every non-backtracking walk of length ≤ r is a path. This sharpens the landed nb_walk_isPath_of_girth (which demands girth > 2r + 1): peeling the first edge, the tail is a non-backtracking walk of length ≤ r, hence a path by induction; a revisit of the start supplies two distinct paths closing a cycle of length ≤ r, contradicting the hypothesis.

theorem ACMax.nb_ball_injectivity {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableEq V] [DecidableRel G.Adj] {ℓ : ℕ} (hg : ∀ (v : V) (c : G.Walk v v), c.IsCycle → 2 * ℓ < c.length) : ∑ k ∈ Finset.Icc 1 ℓ, nbTotalWalks G k ≤ Fintype.card V * (Fintype.card V - 1)

B2 — the vertex-ball injectivity. If there is no cycle of length ≤ 2ℓ, then the total number of non-backtracking walks of length 1..ℓ is at most n·(n − 1). For each start x, the endpoint map on the disjoint union of nbWalksFrom G x k (k ∈ Icc 1 ℓ) is injective into univ.erase x: two walks with a common endpoint v are paths (B1), and if distinct they close a cycle of length ≤ 2ℓ; a walk returning to x would be a positive-length closed path, impossible.

theorem ACMax.ahl_ball_moore {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {ℓ : ℕ} (hδ2 : ∀ (v : V), 2 ≤ G.degree v) [Nonempty V] (hℓ : 1 ≤ ℓ) (hg : ∀ (v : V) (c : G.Walk v v), c.IsCycle → 2 * ℓ < c.length) : (∑ v : V, G.degree v) * ∑ k ∈ Finset.range ℓ, (∑ v : V, G.degree v - Fintype.card V) ^ k * Fintype.card V ^ (ℓ - 1 - k) ≤ Fintype.card V ^ ℓ * (Fintype.card V - 1)

B3 — the SUM Moore bound. Under δ ≥ 2 (and V nonempty) with no cycle of length ≤ 2ℓ and 1 ≤ ℓ, the whole Moore ball is captured: D · Σ_{k<ℓ} (D − n)^k n^(ℓ−1−k) ≤ n^ℓ (n − 1). Per level k, the AM–GM lower bound D·((D − n)/n)^k ≤ m_{k+1} (lambda_ge, nb_amgm_lambda) is scaled by n^(ℓ−1); summing and capping Σ m_k ≤ n(n − 1) (nb_ball_injectivity) gives the ℝ inequality, cast back to ℕ via n ≤ D. This keeps the lower Moore terms the pair form ahl_irregular_moore discards.

theorem ACMax.ahl_ball_girth_bound {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {ℓ : ℕ} (hδ2 : ∀ (v : V), 2 ≤ G.degree v) [Nonempty V] (hℓ : 1 ≤ ℓ) (hbig : Fintype.card V ^ ℓ * (Fintype.card V - 1) < (∑ v : V, G.degree v) * ∑ k ∈ Finset.range ℓ, (∑ v : V, G.degree v - Fintype.card V) ^ k * Fintype.card V ^ (ℓ - 1 - k)) : ∃ (v : V) (c : G.Walk v v), c.IsCycle ∧ c.length ≤ 2 * ℓ

B3 (contrapositive) — the SUM girth bound. Under δ ≥ 2 (and V nonempty) with 1 ≤ ℓ, if n^ℓ(n − 1) < D · Σ_{k<ℓ} (D − n)^k n^(ℓ−1−k) then G contains a cycle of length ≤ 2ℓ. This is the SUM refutation the band arithmetic instantiates: a failing ball inequality forces a short cycle.