The bulk-credited master-cycle moat (master_cycle_fires_sharp)

master_cycle_fires (Counting/Moats.lean) bounds the outer boundary ∂₂ ≤ Σ_F(deg − 1) and then caps Σ_F(deg − 3) by the whole excess budget n − 8, via F ∪ S₁ ⊆ univ. That step throws away Σ_{S₂}(deg − 3), the excess sitting in the bulk — which, on the starved census, is the bulk of the excess: only n₃ = X + 8 vertices have degree 3, so every one of the other |S₂| − n₃ bulk vertices spends at least 1.

Keeping that term turns the ledger into an identity over the partition S₁ ⊔ F ⊔ S₂ = univ and replaces the firing threshold

3·Σ_{S₁}(deg − 1) ≤ n + 8 (i.e. 9k ≤ n + 8 on a degree-≤ 4 cycle)

by the strictly weaker

4·Σ_{S₁} deg + n₃ ≤ 2n + 8 + 4k (i.e. 12k + n₃ ≤ 2n + 8, i.e. 12k + X ≤ 2n).

Since the hoarding law gives 3X + 26 ≤ n, the new threshold dominates the old at every cell: the forbidden cycle length rises from (n+8)/9 to (2n − X)/12, a factor 1.2–1.5.

Everything else — the slice bound, the moat cap |F| ≤ Σ_{S₁}(deg − 2), the two-cluster tie — is verbatim master_cycle_fires; only the ledger and the threshold change.

theorem ACMax.master_cycle_fires_sharp {n : ℕ} [Nonempty (Fin n)] {k n₃ : ℕ} [NeZero k] (hk : 3 ≤ k) (G : SimpleGraph (Fin n)) (hm : G.edgeFinset.card = 2 * (n - 2)) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) (c : ZMod k → Fin n) (hcinj : Function.Injective c) (hadj : ∀ (i : ZMod k), G.Adj (c i) (c (i + 1))) (hsum : ∑ i : ZMod k, G.degree (c i) ≤ 4 * k) (hn3 : {v : Fin n | G.degree v = 3}.card ≤ n₃) (hn : 4 * ∑ i : ZMod k, G.degree (c i) + n₃ ≤ 2 * n + 8 + 4 * k) : algConn G ≤ 2

theorem ACMax.n3_eq_excess_add_eight {n : ℕ} (hn : 8 ≤ n) (G : SimpleGraph (Fin n)) (hm : G.edgeFinset.card = 2 * (n - 2)) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) : {v : Fin n | G.degree v = 3}.card = excessX n G + 8

The degree-3 census identity n₃ = X + 8. From the excess ledger Σ_v (deg v − 3) = n − 8: a degree-3 vertex spends 0, and every other vertex spends (deg − 4) + 1, so n − 8 = X + (n − n₃).

theorem ACMax.v9_short_cycle_fires_sharp {n : ℕ} [Nonempty (Fin n)] {k : ℕ} [NeZero k] (hk : 3 ≤ k) (G : SimpleGraph (Fin n)) (hm : G.edgeFinset.card = 2 * (n - 2)) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) (c : ZMod k → Fin n) (hcinj : Function.Injective c) (hadj : ∀ (i : ZMod k), G.Adj (c i) (c (i + 1))) (hdeg : ∀ (i : ZMod k), G.degree (c i) ≤ 4) (hn8 : 8 ≤ n) (hn : 12 * k + excessX n G ≤ 2 * n) : algConn G ≤ 2

The sharpened tier-9 short-cycle kill. A cycle of degree-≤ 4 vertices fires the two-cluster moat whenever 12·k + X ≤ 2n — against 9·k ≤ n + 8 for v9_short_cycle_fires. Since the hoarding law gives 3X + 26 ≤ n, the new threshold is strictly weaker at every cell: the forbidden length rises from (n+8)/9 to (2n − X)/12.