The SUM band-discharge subset wrapper (B5)

This file lands the census-free subset/2-core wrapper for the SUM (vertex-ball) Moore refutation (node B5 of the band discharge): it instantiates the abstract girth bound ahl_ball_girth_bound (Band.Sum) at the induced graph on the 2-core of a subset S, producing a short cycle inside S in the exact ZMod k cyclic-map form demanded by GirthExcessBound. It mirrors the SQRT discharge plumbing (Counting.SqrtDischarge) minus the component descent — the Alon–Hoory–Linial AM–GM walk count and the ball injectivity are global sums, so no connectivity is needed and the 2-core alone suffices.

The v-transport

The SUM side condition is verified at v = S.card, but the 2-core shrinks to v' = S'.card ≤ v. The single genuinely-new arithmetic step is the v-transport ball_side_transport: the per-cell SUM inequality (in vertex-ball sum form) is monotone the right way, so it descends from v to any v' ≤ v. The proof is term-by-term over the geometric sum, each summand comparison reducing to the three base facts v' - 1 ≤ v - 1, (v + t)·v' ≤ (v' + t)·v, (v + 2t)·v' ≤ (v' + 2t)·v (all ↔ v' ≤ v) plus Nat.pow_le_pow_left — no nlinarith, matching the doc's 0/9000-violation verification.

Contents

• ball_side_transport — the v-transport of the SUM side condition (sum form) from v to v' ≤ v.
• ahl_ball_girth_subset — the subset wrapper: a nonempty S with edge excess 2|S| + 2t ≤ pairs(S) meeting the SUM side condition t(|S| − 1)|S|^(L/2) < (|S| + t)((|S| + 2t)^(L/2) − |S|^(L/2)) (6 ≤ L) carries a cycle of length 3 ≤ k ≤ L inside S, in the ZMod k cyclic-map form.

theorem ACMax.ball_side_transport {t ℓ v v' : ℕ} (ht : 1 ≤ t) (hℓ : 1 ≤ ℓ) (hvv' : v' ≤ v) (hQ : (v - 1) * v ^ ℓ < 2 * (v + t) * ∑ k ∈ Finset.range ℓ, (v + 2 * t) ^ k * v ^ (ℓ - 1 - k)) : (v' - 1) * v' ^ ℓ < 2 * (v' + t) * ∑ k ∈ Finset.range ℓ, (v' + 2 * t) ^ k * v' ^ (ℓ - 1 - k)

The v-transport of the SUM side condition. In vertex-ball sum form (v − 1)·v^ℓ < 2(v + t)·Σ_{k<ℓ}(v + 2t)^k v^(ℓ−1−k), the condition descends from v to any v' ≤ v. The proof is term-by-term over the geometric sum: each summand comparison, after peeling a common v'^(ℓ−1−k)·v^(ℓ−1−k) factor, reduces to v' − 1 ≤ v − 1, (v + t)v' ≤ (v' + t)v and ((v + 2t)v')^k ≤ ((v' + 2t)v)^k (all consequences of v' ≤ v); a cross-multiplied cancellation finishes.

theorem ACMax.ahl_ball_girth_subset {n : ℕ} (G : SimpleGraph (Fin n)) (S : Finset (Fin n)) (t L : ℕ) (_hSne : S.Nonempty) (hL6 : 6 ≤ L) (hexc : 2 * S.card + 2 * t ≤ {q ∈ S ×ˢ S | G.Adj q.1 q.2}.card) (hside : t * (S.card - 1) * S.card ^ (L / 2) < (S.card + t) * ((S.card + 2 * t) ^ (L / 2) - S.card ^ (L / 2))) : ∃ (k : ℕ), 3 ≤ k ∧ k ≤ L ∧ ∃ (c : ZMod k → Fin n), Function.Injective c ∧ (∀ (i : ZMod k), G.Adj (c i) (c (i + 1))) ∧ ∀ (i : ZMod k), c i ∈ S

The SUM band-discharge subset wrapper. For a nonempty S : Finset (Fin n) with edge excess 2|S| + 2t ≤ pairs(S) (i.e. the induced graph on S has ≥ |S| + t edges) meeting the SUM Moore side condition t(|S| − 1)|S|^(L/2) < (|S| + t)((|S| + 2t)^(L/2) − |S|^(L/2)) with 6 ≤ L, there is a cycle of length 3 ≤ k ≤ L inside S, given as an injective cyclic map c : ZMod k → Fin n. Assembly (mirrors girth_excess_bound_holds minus the component descent): extract the minimum-degree-2 2-core S' (two_core_aux), instantiate ahl_ball_girth_bound at the induced graph on S' — the side condition transports from |S| to |S'| (ball_side_transport) and the degree bound D ≥ 2(|S'| + t) supplies the remaining term-wise monotonicity — then lift the short 2-core cycle to G (Embedding.induce, Walk.map) and convert with cycle_walk_to_zmod.