The sparse-core M-edge moat #
For an adjacent pair of degree-three vertices, the ordinary moat has at most
four vertices. If the remote bulk did not contain a sparse-boundary core, its
internal ordered-pair count would be at most twice its degree excess. The moat
and bulk incidence ledgers would then force 2 * n + 2 ≤ 5 * |F|, which is
impossible from order ten onward.
theorem
ACMax.medge_sparse_core_fires
{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)
(u p : Fin n)
(hM : G.Adj u p)
(hu : G.degree u = 3)
(hp : G.degree p = 3)
:
An edge joining two degree-three vertices produces a sparse-core cut at
every order n ≥ 10.