Demazure composition across a vertex wedge

For opposite marked vertices, the vertex-wedge rank formula composes transmission witnesses by the Demazure product. At gluing shift ell, the left and right transmission rows are respectively (a, ell + 1) and (ell, b). Thus the min-plus formula for AspPerm.star is exactly the factor-rank profile required by TransmissionWedge.

The final existence theorem is conditional only on the finite-length factorization of an ASP permutation into two factors within prescribed genus budgets. The imported Demazure library supplies the min-plus product formula but currently no theorem producing this bounded finite factorization.

theorem Utilities.satisfiesTransmission_wedgeAddDivisor_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 : SatisfiesTransmission G u x alpha D) (hE : SatisfiesTransmission H y v beta E) : SatisfiesTransmission (vertexWedge G H x y) (Sum.inl u) (wedgeRightVertex G H x y v) (alpha ⋆ beta) (wedgeAddDivisor G H x y D E)

Opposite-side wedge addition composes two transmission witnesses by the Demazure product.

theorem Utilities.transmissionExists_vertexWedge_opposite_star (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (u : G.V) (v : H.V) (alpha beta : AspPerm) (hG : TransmissionExists G u x alpha) (hH : TransmissionExists H y v beta) : TransmissionExists (vertexWedge G H x y) (Sum.inl u) (wedgeRightVertex G H x y v) (alpha ⋆ beta)

The existential form of opposite-side Demazure composition.

def Utilities.BoundedDemazureFactorization (tau : AspPerm) (gG gH : ℤ) : Prop

A finite Demazure factorization whose two factors fit the two genus budgets. This is the precise combinatorial input needed to glue full TransmissionExistence statements.

Equations

• One or more equations did not get rendered due to their size.

def Utilities.HasBoundedDemazureFactorizations (gG gH : ℤ) : Prop

The bounded finite Demazure-factorization assertion needed for vertex wedge gluing. It is isolated here because Demazure.Submodular proves the min-plus product formula but does not provide this length-budgeted factorization theorem.

Equations

• One or more equations did not get rendered due to their size.

theorem Utilities.transmissionExistence_vertexWedge_opposite_of_factorizations (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (u : G.V) (v : H.V) (hG : TransmissionExistence G u x) (hH : TransmissionExistence H y v) (hFactor : HasBoundedDemazureFactorizations G.genus H.genus) : TransmissionExistence (vertexWedge G H x y) (Sum.inl u) (wedgeRightVertex G H x y v)

Conditional gluing for the full finite-length transmission-existence predicate. The sole additional input is the named bounded Demazure factorization property above.