Exact transmission and submodularity across a vertex wedge

Utilities.satisfiesTransmission_wedgeAddDivisor_star supplies the lower rank inequalities for the Demazure product of two transmission witnesses. For the paper's gluing formula, one needs the stronger statement that the raw transmission permutation of the wedge divisor is equal to that Demazure product. This file proves that equality from the attained vertex-wedge rank formula.

The divisor algebra which turns an exact rank surface into a raw transmission permutation is kept abstract. This avoids unfolding oneChip on a concrete wedge vertex type.

theorem Bananas.isTransmissionPermutation_of_rank_eq_slipface {M : TwiceMarked} (D : CFDiv M.graph) (tau : AspPerm) (hRank : ∀ (a b : ℤ), rank M.graph (D + a • oneChip M.u - b • oneChip M.v) = tau.s.func (a + 1) b - 1) : IsTransmissionPermutation M D tau.func

An ASP permutation whose slipface is the exact marked rank surface is the raw transmission permutation.

theorem Bananas.rank_wedgeAddDivisor_transmissionTwist_eq_star (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (E : CFDiv H) (u : G.V) (v : H.V) (alpha beta : AspPerm) (hD : ∀ (a b : ℤ), rank G (D + a • oneChip u - b • oneChip x) = alpha.s.func (a + 1) b - 1) (hE : ∀ (a b : ℤ), rank H (E + a • oneChip y - b • oneChip v) = beta.s.func (a + 1) b - 1) (a b : ℤ) : rank (Utilities.vertexWedge G H x y) (Utilities.wedgeAddDivisor G H x y D E + a • oneChip (Sum.inl u) - b • oneChip (Utilities.wedgeRightVertex G H x y v)) = (alpha ⋆ beta).s.func (a + 1) b - 1

Exact min-plus rank formula for an opposite-side wedge twist when the two factor rank surfaces are represented by ASP permutations.

theorem Bananas.exists_isTransmissionPermutation_wedgeAddDivisor_star (G H : CFGraph) (x : G.V) (y : H.V) (hG : _root_.graphConnected G) (hH : _root_.graphConnected H) (D : CFDiv G) (E : CFDiv H) (u : G.V) (v : H.V) (tau sigma : ℤ → ℤ) (hTau : IsTransmissionPermutation (mark G u x) D tau) (hSigma : IsTransmissionPermutation (mark H y v) E sigma) : ∃ (alpha : AspPerm) (beta : AspPerm), alpha.func = tau ∧ beta.func = sigma ∧ IsTransmissionPermutation (mark (Utilities.vertexWedge G H x y) (Sum.inl u) (Utilities.wedgeRightVertex G H x y v)) (Utilities.wedgeAddDivisor G H x y D E) (alpha ⋆ beta).func

The exact raw transmission permutation of a wedge-additive divisor is the Demazure product of the exact raw transmission permutations of its factors.

theorem Bananas.allSubmodular_vertexWedge_opposite (G H : CFGraph) (x : G.V) (y : H.V) (hGconn : _root_.graphConnected G) (hHconn : _root_.graphConnected H) (u : G.V) (v : H.V) (hG : AllSubmodular (mark G u x)) (hH : AllSubmodular (mark H y v)) : AllSubmodular (mark (Utilities.vertexWedge G H x y) (Sum.inl u) (Utilities.wedgeRightVertex G H x y v))

All-divisor submodularity is closed under opposite-side vertex gluing.