The sharpened Z1 star moat

star_moat_fires (Counting/Moats) fires a degree-d hub carrying d − 2 degree-3 twins whenever 9d ≤ n + 15, which at d = 4 gives only n ≥ 21. That threshold is not intrinsic: it bounds the outer boundary ∂₂ = e(F, S₂) from the moat side alone,

∂₂ ≤ Σ_F (deg − 1) = E_F + 2|F|,

and then charging E_F against the whole excess budget n − 8. The bulk side is never counted.

This file adds the missing bulk count. Writing E_F, E₂ for the excess carried by the moat F and the bulk S₂, the two sides say

∂₂ ≤ E_F + 2f (moat side, as before) ∂₂ + P₂ = 3|S₂| + E₂ (bulk side: every S₂-vertex sends its degree into F ⊎ S₂)

with P₂ the ordered adjacent pairs inside S₂. Under hs0 the degree-3 vertices of S₂ are pairwise non-adjacent, so every S₂-edge has an endpoint of degree at least 4 and P₂ ≤ 8·E₂. For n ≥ 16, combining this estimate with the moat ledger either fires the original cut or exposes a sparse bulk core, which supplies another cut certificate. The five remaining orders 10 ≤ n ≤ 15 have rigid excess profiles; the same ledgers, supplemented by triangle and decorated-C₄ certificates at the tight corners, close them directly.

theorem ACMax.pairs_le_eight_excess {n : ℕ} (G : SimpleGraph (Fin n)) (hs0 : ∀ (v w : Fin n), G.degree v = 3 → G.degree w = 3 → ¬G.Adj v w) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) (T : Finset (Fin n)) : {q ∈ T ×ˢ T | G.Adj q.1 q.2}.card ≤ 8 * ∑ v ∈ T, (G.degree v - 3)

The bulk-side pair bound. In a starved census (hs0: no degree-3–degree-3 edge), the ordered adjacent pairs inside any set T are at most 8·E_T, where E_T = Σ_T (deg − 3): every adjacent pair inside T has an endpoint of degree ≥ 4, there are at most E_T such vertices in T, and each has degree at most 3 + (deg − 3).

theorem ACMax.z1_star_moat_fires_core {n : ℕ} [Nonempty (Fin n)] (hn : 10 ≤ n) (G : SimpleGraph (Fin n)) (hm : G.edgeFinset.card = 2 * (n - 2)) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) (hs0 : ∀ (v w : Fin n), G.degree v = 3 → G.degree w = 3 → ¬G.Adj v w) (h t₁ t₂ : Fin n) (hdh : G.degree h = 4) (ht1 : G.Adj h t₁) (ht2 : G.Adj h t₂) (hd1 : G.degree t₁ = 3) (hd2 : G.degree t₂ = 3) (ht12 : t₁ ≠ t₂) : algConn G ≤ 2

The sparse-core Z1 star moat. A degree-4 hub with two distinct degree-3 neighbors fires at every n ≥ 10 in the starved regime. Above order fifteen an excessive bulk boundary produces a sparse core; the lower endpoints are closed by their rigid incidence censuses.

theorem ACMax.z1_star_moat_fires_sharp {n : ℕ} [Nonempty (Fin n)] (hn : 10 ≤ n) (G : SimpleGraph (Fin n)) (hm : G.edgeFinset.card = 2 * (n - 2)) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) (hs0 : ∀ (v w : Fin n), G.degree v = 3 → G.degree w = 3 → ¬G.Adj v w) (h t₁ t₂ : Fin n) (hdh : G.degree h = 4) (ht1 : G.Adj h t₁) (ht2 : G.Adj h t₂) (hd1 : G.degree t₁ = 3) (hd2 : G.degree t₂ = 3) (ht12 : t₁ ≠ t₂) : algConn G ≤ 2

Compatibility form of the sharpened shared-hub theorem.