Documentation

LeanPool.BrillNoetherGraphs.Utilities.Subdivision.CoreBridgeRankOne

Rank one across a checked genus-two/genus-two core bridge #

A separating core slot remains a separating unit edge in every positive subdivision. When its two induced factors have genus two, elementary Brill--Noether existence supplies degree-two pencils on the factors and the bridge gluing theorem removes one chip. The result is a degree-three pencil on the original subdivision, uniformly in all positive slot lengths.

This is the structural shortcut used by the first Draisma--Vargas genus-four type. It is independent of that application and of any finite cone cover.

theorem MarkedGraphs.Certificate.CoreBridgeCut.Data.bnExists_one_three_of_two_two {n p : ℕ} {spec : Utilities.Certificate.SubdivisionGraph.Spec n p} (cutData : Data spec.core) (hValid : cutData.Valid) (hConnected : graphConnected spec.graph) (hLeft : cutData.toCoreVertexCut.leftGenus = 2) (hRight : cutData.toCoreVertexCut.rightGenus = 2) :

A valid separating core edge with two genus-two sides gives a degree-three rank-one divisor on every positive subdivision of that core.