The right-loop branch of Proposition 3.7

ChainTwoLoopsSameLeft.lean proves the complete arbitrary-mark classification when both marks lie on the left cycle of a vertex wedge. This file transports that theorem across commutativity of vertex wedges, supplying the symmetric right-cycle statement required by the paper's Proposition 3.7.

theorem Bananas.chainTwoLoops_allSubmodular_same_right_arbitrary_iff (leftLength rightLength : Fin 2 → ℕ) (hLeftLength : ∀ (edge : Fin 2), 0 < leftLength edge) (hRightLength : ∀ (edge : Fin 2), 0 < rightLength edge) (leftGlue : (Utilities.TwoPathCycle.spec leftLength hLeftLength).graph.V) (rightGlue p q : (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) (Utilities.wedgeRightVertex (Utilities.TwoPathCycle.spec leftLength hLeftLength).graph (Utilities.TwoPathCycle.spec rightLength hRightLength).graph leftGlue rightGlue p) (Utilities.wedgeRightVertex (Utilities.TwoPathCycle.spec leftLength hLeftLength).graph (Utilities.TwoPathCycle.spec rightLength hRightLength).graph leftGlue rightGlue q)) ↔ rightLength 0 + rightLength 1 = 2

Full same-loop clause of Proposition 3.7 for arbitrary distinct marks on the right cycle. Every divisor is submodular exactly when that cycle has two vertices.