Rank one across a positive-genus articulation in genus five

The unmarked genus-five structural exit is considerably simpler than its once-marked ancestor. The two factors have genera (1,4) or (2,3), up to order. The genus-at-most-three factor carries its elementary critical pencil, the genus-four factor uses the supplied genus-four theorem, and bridge gluing followed by contraction of the artificial bridge loses exactly one degree.

theorem Utilities.BNExists_vertexWedge_rank_one_bridge_corrected (G H : CFGraph) (x : G.V) (y : H.V) {dG dH : ℤ} (hG : BNExists G 1 dG) (hH : BNExists H 1 dH) : BNExists (vertexWedge G H x y) 1 (dG + dH - 1)

Rank-one pencils on two factors glue on their vertex wedge with the bridge correction: the resulting degree is one less than the sum.

theorem Utilities.BNExists_vertexWedge_one_four_of_genus_four (genusFour : ∀ (G : CFGraph), graphConnected G → G.genus = 4 → BNExists G 1 3) (G H : CFGraph) (x : G.V) (y : H.V) (hGConnected : graphConnected G) (hGGenus : G.genus = 4) (hHRigid : PointedGenusOneRigid H y) : BNExists (vertexWedge G H x y) 1 4

Attaching a pointed rigid genus-one factor to a genus-four graph raises the critical pencil degree from three to four.

theorem Utilities.BNExists_one_four_of_positiveGenus_oneVertexCut (genusFour : ∀ (G : CFGraph), graphConnected G → G.genus = 4 → BNExists G 1 3) (K : CFGraph) (hConnected : graphConnected K) (hGenus : K.genus = 5) (cut : OneVertexCut K) (hLeftPos : 0 < cut.leftGraph.genus) (hRightPos : 0 < cut.rightGraph.genus) : BNExists K 1 4

Any positive-genus one-vertex decomposition of a connected genus-five graph supplies a degree-four rank-one divisor, assuming only the genus-four critical pencil theorem in the same universe.