Gluing a general marked graph to a graph with general transmission

This file proves Theorem 6.6 (thm:glueBNGtoKGT) of the paper. The exact transmission permutation of a wedge divisor is the Demazure product of the factor permutations (WedgeSubmodularity); Proposition 6.13 bounds its sign-changing inversions, and Proposition 6.10 identifies those inversions with the size of the Weierstrass partition at the surviving mark.

theorem Bananas.weierstrassSize_le_genus_of_sci_le {G : CFGraph} (u v : G.V) (hG : _root_.graphConnected G) (D : CFDiv G) (tau : ℤ → ℤ) (hTau : IsTransmissionPermutation (mark G u v) D tau) (hSci : ↑(sci tau) ≤ G.genus) : ↑(weierstrassSize hG v D) ≤ G.genus

Convert the sign-changing-inversion bound furnished by Proposition 6.13 into the corresponding Weierstrass-size bound. Keeping this divisor algebra at an abstract graph prevents concrete wedge vertex types from unfolding during elaboration.

theorem Bananas.onceMarkedBrillNoetherGeneral_vertexWedge_of_kGeneralTransmission (G H : CFGraph) (u x : G.V) (y v : H.V) (hGconn : _root_.graphConnected G) (hHconn : _root_.graphConnected H) (hGsub : AllSubmodular (mark G u x)) (hGgeneral : OnceMarkedBrillNoetherGeneral G x) {k : ℕ} (hK : KGeneralTransmission (mark H y v) k) (hbudget : G.genus + H.genus < ↑k) : OnceMarkedBrillNoetherGeneral (Utilities.vertexWedge G H x y) (Utilities.wedgeRightVertex G H x y v)

Paper Theorem 6.6 (thm:glueBNGtoKGT).

The first twice-marking is used only to supply a submodular transmission permutation for each divisor on G, as in the paper. The marked Brill--Noether hypothesis itself concerns only the gluing vertex x.

theorem Bananas.onceMarkedBrillNoetherGeneral_of_kGeneralTransmission {G : CFGraph} (u v : G.V) (hGconn : _root_.graphConnected G) {k : ℕ} (hK : KGeneralTransmission (mark G u v) k) (hbudget : G.genus < ↑k) : OnceMarkedBrillNoetherGeneral G v

The once-marked corollary immediately following Theorem 6.6: if the period is larger than the genus, forgetting the first mark of a graph with k-general transmission leaves a Brill--Noether general marked graph.

We prove this directly by taking the identity as the left Demazure factor; this is equivalent to the paper's specialization of Theorem 6.6 to a one-vertex first graph, without choosing a separate model of that graph.