The same-loop branch for a chain of two loops

The graph is the vertex wedge of two positive two-path cycles. This file isolates the same-left-side argument in paper Proposition 3.7.

theorem Bananas.genusOne_rank_eq_degree_sub_one {G : CFGraph} (hG : _root_.graphConnected G) (hGenus : G.genus = 1) (D : CFDiv G) (hDegree : 0 < CFDiv.degree D) : rank G D = CFDiv.degree D - 1

On a connected genus-one graph every positive-degree divisor has the Riemann--Roch rank deg D - 1.

theorem Bananas.allSubmodular_of_connected_genus_one_distinct_classes {G : CFGraph} (hG : _root_.graphConnected G) (hGenus : G.genus = 1) (u v : G.V) (hMarks : ¬linearEquiv G (oneChip u - oneChip v) 0) : AllSubmodular (mark G u v)

Distinct degree-one classes on a connected genus-one graph make every divisor submodular. This is the factor-level submodularity input for the opposite-side vertex-wedge branch of the genus-two classification.

theorem Bananas.wedge_left_difference (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (a b : G.V) : oneChip (Sum.inl a) - oneChip (Sum.inl b) = Utilities.wedgeLiftLeftDivisor G H x y (oneChip a - oneChip b)

theorem Bananas.wedge_left_pair (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (a b : G.V) : oneChip (Sum.inl a) + oneChip (Sum.inl b) = Utilities.wedgeLiftLeftDivisor G H x y (oneChip a + oneChip b)

A pair of left-factor chips is the wedge lift of the corresponding left-factor divisor.

theorem Bananas.left_mark_difference_not_principal (G : CFGraph) (H : CFGraph) (x u : G.V) (y : H.V) (hG : Utilities.PointedGenusOneRigid G x) (hu : u ≠ x) : ¬linearEquiv (Utilities.vertexWedge G H x y) (oneChip (Sum.inl x) - oneChip (Sum.inl u)) 0

theorem Bananas.rankDelta_wedgeLiftLeft_pair_neg (G H : CFGraph) (x u w : G.V) (y : H.V) (hGconn : _root_.graphConnected G) (hGgenus : G.genus = 1) (hGx : Utilities.PointedGenusOneRigid G x) (hGu : Utilities.PointedGenusOneRigid G u) (hH : Utilities.PointedGenusOneRigid H y) (hwx : w ≠ x) (hwu : w ≠ u) : rankDelta (mark (Utilities.vertexWedge G H x y) (Sum.inl x) (Sum.inl u)) (Utilities.wedgeLiftLeftDivisor G H x y (oneChip x + oneChip w)) < 0

If a genus-one left factor contains a third vertex besides the two marks, the divisor consisting of the gluing mark and that third vertex has negative marked second difference after attaching a rigid genus-one right factor.

theorem Bananas.rankDelta_wedgeLiftLeft_mark_add_glue_neg (G H : CFGraph) (x p q : G.V) (y : H.V) (hGconn : _root_.graphConnected G) (hGgenus : G.genus = 1) (hGx : Utilities.PointedGenusOneRigid G x) (hGq : Utilities.PointedGenusOneRigid G q) (hH : Utilities.PointedGenusOneRigid H y) (hpx : p ≠ x) (hqx : q ≠ x) : rankDelta (mark (Utilities.vertexWedge G H x y) (Sum.inl p) (Sum.inl q)) (Utilities.wedgeLiftLeftDivisor G H x y (oneChip p + oneChip x)) < 0

When neither mark is the gluing vertex, the gluing vertex itself supplies the auxiliary chip in the paper's negative-second-difference witness.

theorem Bananas.wedge_right_aux_pair_not_winnable (G : CFGraph) (H : CFGraph) (x u : G.V) (y : H.V) (hG : Utilities.PointedGenusOneRigid G x) (hH : Utilities.PointedGenusOneRigid H y) (hu : u ≠ x) (b : { z : H.V // z ≠ y }) : ¬winnable (Utilities.vertexWedge G H x y) (oneChip (Sum.inr b) + oneChip (Sum.inl x) - oneChip (Sum.inl u))

A chip on the unmarked part of the right rigid factor cannot repair the degree-zero left marked difference after wedging.

theorem Bananas.exists_ne_two_of_two_lt_card {X : Type} [Fintype X] (x u : X) (hCard : 2 < Fintype.card X) : ∃ (w : X), w ≠ x ∧ w ≠ u

Proposition 3.7, same-loop branch

theorem Bananas.chainTwoLoops_allSubmodular_same_left_iff (leftLength rightLength : Fin 2 → ℕ) (hLeftLength : ∀ (edge : Fin 2), 0 < leftLength edge) (hRightLength : ∀ (edge : Fin 2), 0 < rightLength edge) (leftGlue u : (Utilities.TwoPathCycle.spec leftLength hLeftLength).graph.V) (rightGlue : (Utilities.TwoPathCycle.spec rightLength hRightLength).graph.V) (hu : u ≠ leftGlue) : AllSubmodular (mark (Utilities.vertexWedge (Utilities.TwoPathCycle.spec leftLength hLeftLength).graph (Utilities.TwoPathCycle.spec rightLength hRightLength).graph leftGlue rightGlue) (Sum.inl leftGlue) (Sum.inl u)) ↔ leftLength 0 + leftLength 1 = 2

On a vertex wedge of two positive subdivided cycles, with both marks on the left cycle and one mark at the gluing vertex, every divisor is submodular exactly when the marked cycle has total combinatorial length two.

theorem Bananas.chainTwoLoops_allSubmodular_opposite (leftLength rightLength : Fin 2 → ℕ) (hLeftLength : ∀ (edge : Fin 2), 0 < leftLength edge) (hRightLength : ∀ (edge : Fin 2), 0 < rightLength edge) (leftGlue p : (Utilities.TwoPathCycle.spec leftLength hLeftLength).graph.V) (rightGlue q : (Utilities.TwoPathCycle.spec rightLength hRightLength).graph.V) (hp : p ≠ leftGlue) (hq : q ≠ rightGlue) : AllSubmodular (mark (Utilities.vertexWedge (Utilities.TwoPathCycle.spec leftLength hLeftLength).graph (Utilities.TwoPathCycle.spec rightLength hRightLength).graph leftGlue rightGlue) (Sum.inl p) (Utilities.wedgeRightVertex (Utilities.TwoPathCycle.spec leftLength hLeftLength).graph (Utilities.TwoPathCycle.spec rightLength hRightLength).graph leftGlue rightGlue q))

Distinct-loop clause of Proposition 3.7 for arbitrary non-gluing marks on the two cycle factors.

theorem Bananas.chainTwoLoops_not_allSubmodular_same_left_of_two_lt_length (leftLength rightLength : Fin 2 → ℕ) (hLeftLength : ∀ (edge : Fin 2), 0 < leftLength edge) (hRightLength : ∀ (edge : Fin 2), 0 < rightLength edge) (leftGlue p q : (Utilities.TwoPathCycle.spec leftLength hLeftLength).graph.V) (rightGlue : (Utilities.TwoPathCycle.spec rightLength hRightLength).graph.V) (hpq : p ≠ q) (hLength : 2 < leftLength 0 + leftLength 1) : ¬AllSubmodular (mark (Utilities.vertexWedge (Utilities.TwoPathCycle.spec leftLength hLeftLength).graph (Utilities.TwoPathCycle.spec rightLength hRightLength).graph leftGlue rightGlue) (Sum.inl p) (Sum.inl q))

The missing arbitrary-mark negative direction of Proposition 3.7. If a left loop has at least three vertices, every pair of distinct marks on that loop admits a negative-rankDelta divisor, whether or not either mark is the gluing vertex.

theorem Bananas.chainTwoLoops_allSubmodular_same_left_arbitrary_iff (leftLength rightLength : Fin 2 → ℕ) (hLeftLength : ∀ (edge : Fin 2), 0 < leftLength edge) (hRightLength : ∀ (edge : Fin 2), 0 < rightLength edge) (leftGlue p q : (Utilities.TwoPathCycle.spec leftLength hLeftLength).graph.V) (rightGlue : (Utilities.TwoPathCycle.spec rightLength hRightLength).graph.V) (hpq : p ≠ q) : AllSubmodular (mark (Utilities.vertexWedge (Utilities.TwoPathCycle.spec leftLength hLeftLength).graph (Utilities.TwoPathCycle.spec rightLength hRightLength).graph leftGlue rightGlue) (Sum.inl p) (Sum.inl q)) ↔ leftLength 0 + leftLength 1 = 2

Full same-loop clause of Proposition 3.7 for arbitrary distinct marks on the left loop. When the loop has length two, distinctness forces its two vertices to be precisely the marks; at every larger length the preceding explicit witness gives non-submodularity.