Transmission across a vertex wedge

A wedge divisor has a marked rank profile on each factor. This module turns the vertex-wedge rank formula into an exact, arbitrary-ASP transmission criterion. It is deliberately stated for every lattice point and every integer chip-shift: no Grassmannian or rank-one specialization is used here.

For a transmission row (a,b), its marked twist on the wedge splits as (D + a[u]) ⊕ (E - b[v]). The rank condition on that row is therefore equivalent to the tropical-dot-product inequality for the two factor profiles, indexed by the extra gluing shift ell.

theorem Utilities.wedgeAddDivisor_add (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D A : CFDiv G) (E B : CFDiv H) : wedgeAddDivisor G H x y D E + wedgeAddDivisor G H x y A B = wedgeAddDivisor G H x y (D + A) (E + B)

Wedge addition is additive in its two divisor arguments.

theorem Utilities.wedgeAddDivisor_zsmul (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (E : CFDiv H) (n : ℤ) : n • wedgeAddDivisor G H x y D E = wedgeAddDivisor G H x y (n • D) (n • E)

Wedge addition commutes with integral scalar multiplication.

theorem Utilities.wedgeAddDivisor_one_chip_left (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (u : G.V) : wedgeAddDivisor G H x y (oneChip u) 0 = oneChip (Sum.inl u)

A left-factor chip is its literal wedge-additive lift.

theorem Utilities.wedgeAddDivisor_one_chip_right (G : CFGraph) (H : CFGraph) (x : G.V) (y v : H.V) : wedgeAddDivisor G H x y 0 (oneChip v) = oneChip (wedgeRightVertex G H x y v)

A right-factor chip is its wedge-additive lift, including at the common vertex when the chip is at y.

theorem Utilities.wedgeAddDivisor_transmissionTwist (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (E : CFDiv H) (u : G.V) (v : H.V) (a b : ℤ) : wedgeAddDivisor G H x y D E + a • oneChip (Sum.inl u) - b • oneChip (wedgeRightVertex G H x y v) = wedgeAddDivisor G H x y (D + a • oneChip u) (E - b • oneChip v)

The transmission twist of a wedge-additive divisor splits literally into the corresponding left and right factor twists.

def Utilities.WedgeTransmissionRowProfile (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (E : CFDiv H) (u : G.V) (v : H.V) (tau : AspPerm) (a b ell : ℤ) : Prop

The profile inequality attached to a single transmission row of a wedge. The ell coordinate is the chip transfer across the identified vertex.

Equations

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

theorem Utilities.transmissionInequality_wedgeAddDivisor_iff_rowProfile (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (E : CFDiv H) (u : G.V) (v : H.V) (tau : AspPerm) (a b : ℤ) : TransmissionInequality (vertexWedge G H x y) (Sum.inl u) (wedgeRightVertex G H x y v) tau (wedgeAddDivisor G H x y D E) a b ↔ ∀ (ell : ℤ), WedgeTransmissionRowProfile G H x y D E u v tau a b ell

A wedge-additive divisor has the required transmission ranks exactly when every row satisfies all of its factor-profile inequalities.

theorem Utilities.transmissionInequality_wedgeAddDivisor_of_rowProfile (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (E : CFDiv H) (u : G.V) (v : H.V) (tau : AspPerm) (a b : ℤ) (h : ∀ (ell : ℤ), WedgeTransmissionRowProfile G H x y D E u v tau a b ell) : TransmissionInequality (vertexWedge G H x y) (Sum.inl u) (wedgeRightVertex G H x y v) tau (wedgeAddDivisor G H x y D E) a b

The usable forward direction of the row-profile criterion.

theorem Utilities.wedgeTransmissionRowProfile_of_transmissionInequality (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (E : CFDiv H) (u : G.V) (v : H.V) (tau : AspPerm) (a b ell : ℤ) (h : TransmissionInequality (vertexWedge G H x y) (Sum.inl u) (wedgeRightVertex G H x y v) tau (wedgeAddDivisor G H x y D E) a b) : WedgeTransmissionRowProfile G H x y D E u v tau a b ell

Every wedge transmission row supplies all of its factor-profile bounds.

def Utilities.WedgeTransmissionProfile (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (E : CFDiv H) (u : G.V) (v : H.V) (tau : AspPerm) : Prop

The full factor-profile condition for a wedge divisor and an arbitrary ASP permutation.

Equations

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

theorem Utilities.satisfiesTransmission_wedgeAddDivisor_iff_profile (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (E : CFDiv H) (u : G.V) (v : H.V) (tau : AspPerm) : SatisfiesTransmission (vertexWedge G H x y) (Sum.inl u) (wedgeRightVertex G H x y v) tau (wedgeAddDivisor G H x y D E) ↔ WedgeTransmissionProfile G H x y D E u v tau

Exact wedge criterion for a fixed wedge-additive divisor. In particular, the global transmission predicate reduces to factor rank profiles with no loss at non-special or boundary rows.

theorem Utilities.satisfiesTransmission_wedgeAddDivisor_of_profile (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (E : CFDiv H) (u : G.V) (v : H.V) (tau : AspPerm) (h : WedgeTransmissionProfile G H x y D E u v tau) : SatisfiesTransmission (vertexWedge G H x y) (Sum.inl u) (wedgeRightVertex G H x y v) tau (wedgeAddDivisor G H x y D E)

A convenient one-way constructor when the factor degree and all factor row profiles have been established independently.

theorem Utilities.transmissionExists_vertexWedge_of_profile (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (u : G.V) (v : H.V) (tau : AspPerm) (D : CFDiv G) (E : CFDiv H) (h : WedgeTransmissionProfile G H x y D E u v tau) : TransmissionExists (vertexWedge G H x y) (Sum.inl u) (wedgeRightVertex G H x y v) tau

Existence on the wedge follows from one pair of factor divisors satisfying the explicit wedge transmission profile.