Rank-one existence from reaching the core of a subdivision #
The embedded core vertices are a strong separator in every positive subdivision. Consequently, on a connected subdivision, it is enough for a divisor to reach every core vertex in order to have rank at least one. This is the common final step shared by explicit-potential, loop-split, and local configuration certificates.
theorem
Utilities.Certificate.CoreVertexReachability.bnExists_of_reaches_coreVertices
{n p : ℕ}
(spec : SubdivisionGraph.Spec n p)
(hConnected : graphConnected spec.graph)
(D : CFDiv spec.graph)
(degree : ℤ)
(hDegree : CFDiv.degree D = degree)
(hReaches : ∀ (vertex : Fin n), StrongSeparator.Reaches spec.graph D (spec.coreVertex vertex))
:
On a connected positive subdivision, a divisor which reaches every embedded core vertex has rank at least one.