Transmission with both marks on one side of a vertex wedge

TransmissionWedge treats the case in which the two transmission marks lie on opposite factors. This file gives the complementary exact criteria: both marks may lie on the left factor, with the right factor attached at an unmarked cut vertex, or symmetrically both may lie on the right factor.

The first result removes the nonnegative-threshold hypothesis from the exact vertex-wedge rank formula. This is useful for arbitrary ASP transmission, whose required rank tau.s (a + 1) b - 1 can equal -1.

theorem Utilities.vertexWedge_rank_ge_iff_profile_inequalities_all_int (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (E : CFDiv H) (k : ℤ) : rank (vertexWedge G H x y) (wedgeAddDivisor G H x y D E) ≥ k ↔ ∀ (ell : ℤ), rank G (D - (ell + 1) • oneChip x) + rank H (E + ell • oneChip y) + 1 ≥ k

The exact vertex-wedge rank-profile criterion at every integer threshold. For negative thresholds both sides hold automatically, since graph rank is at least -1 and the sum of two factor ranks plus one is also at least -1.

Both marks on the left factor

theorem Utilities.wedgeAddDivisor_transmissionTwist_sameLeft (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (E : CFDiv H) (p q : G.V) (a b : ℤ) : wedgeAddDivisor G H x y D E + a • oneChip (Sum.inl p) - b • oneChip (Sum.inl q) = wedgeAddDivisor G H x y (D + a • oneChip p - b • oneChip q) E

Twisting at two left-factor vertices commutes literally with wedge addition. This remains true when either marked vertex is the gluing vertex.

def Utilities.WedgeSameLeftTransmissionRowProfile (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (E : CFDiv H) (p q : G.V) (tau : AspPerm) (a b ell : ℤ) : Prop

The factor-rank inequality for one transmission row when both marks lie on the left factor. ell records chip transfer across the gluing vertex.

Equations

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

theorem Utilities.transmissionInequality_wedgeAddDivisor_sameLeft_iff_rowProfile (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (E : CFDiv H) (p q : G.V) (tau : AspPerm) (a b : ℤ) : TransmissionInequality (vertexWedge G H x y) (Sum.inl p) (Sum.inl q) tau (wedgeAddDivisor G H x y D E) a b ↔ ∀ (ell : ℤ), WedgeSameLeftTransmissionRowProfile G H x y D E p q tau a b ell

Exact row criterion when both transmission marks lie on the left factor.

def Utilities.WedgeSameLeftTransmissionProfile (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (E : CFDiv H) (p q : G.V) (tau : AspPerm) : Prop

The full arbitrary-ASP profile with both marks on the left factor.

Equations

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

theorem Utilities.satisfiesTransmission_wedgeAddDivisor_sameLeft_iff_profile (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (E : CFDiv H) (p q : G.V) (tau : AspPerm) : SatisfiesTransmission (vertexWedge G H x y) (Sum.inl p) (Sum.inl q) tau (wedgeAddDivisor G H x y D E) ↔ WedgeSameLeftTransmissionProfile G H x y D E p q tau

Exact same-left-side wedge criterion for a fixed wedge-additive divisor.

theorem Utilities.transmissionExists_vertexWedge_sameLeft_of_profile (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (p q : G.V) (tau : AspPerm) (D : CFDiv G) (E : CFDiv H) (h : WedgeSameLeftTransmissionProfile G H x y D E p q tau) : TransmissionExists (vertexWedge G H x y) (Sum.inl p) (Sum.inl q) tau

A same-left factor profile constructs a transmission witness on the wedge.

Both marks on the right factor

theorem Utilities.wedgeAddDivisor_transmissionTwist_sameRight (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (E : CFDiv H) (p q : H.V) (a b : ℤ) : wedgeAddDivisor G H x y D E + a • oneChip (wedgeRightVertex G H x y p) - b • oneChip (wedgeRightVertex G H x y q) = wedgeAddDivisor G H x y D (E + a • oneChip p - b • oneChip q)

Twisting at two right-factor vertices commutes literally with wedge addition, including the common-vertex convention of wedgeRightVertex.

def Utilities.WedgeSameRightTransmissionRowProfile (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (E : CFDiv H) (p q : H.V) (tau : AspPerm) (a b ell : ℤ) : Prop

The factor-rank inequality for one transmission row when both marks lie on the right factor.

Equations

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

theorem Utilities.transmissionInequality_wedgeAddDivisor_sameRight_iff_rowProfile (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (E : CFDiv H) (p q : H.V) (tau : AspPerm) (a b : ℤ) : TransmissionInequality (vertexWedge G H x y) (wedgeRightVertex G H x y p) (wedgeRightVertex G H x y q) tau (wedgeAddDivisor G H x y D E) a b ↔ ∀ (ell : ℤ), WedgeSameRightTransmissionRowProfile G H x y D E p q tau a b ell

Exact row criterion when both transmission marks lie on the right factor.

def Utilities.WedgeSameRightTransmissionProfile (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (E : CFDiv H) (p q : H.V) (tau : AspPerm) : Prop

The full arbitrary-ASP profile with both marks on the right factor.

Equations

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

theorem Utilities.satisfiesTransmission_wedgeAddDivisor_sameRight_iff_profile (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (E : CFDiv H) (p q : H.V) (tau : AspPerm) : SatisfiesTransmission (vertexWedge G H x y) (wedgeRightVertex G H x y p) (wedgeRightVertex G H x y q) tau (wedgeAddDivisor G H x y D E) ↔ WedgeSameRightTransmissionProfile G H x y D E p q tau

Exact same-right-side wedge criterion for a fixed wedge-additive divisor.

theorem Utilities.transmissionExists_vertexWedge_sameRight_of_profile (G : CFGraph) (H : CFGraph) (x : G.V) (y p q : H.V) (tau : AspPerm) (D : CFDiv G) (E : CFDiv H) (h : WedgeSameRightTransmissionProfile G H x y D E p q tau) : TransmissionExists (vertexWedge G H x y) (wedgeRightVertex G H x y p) (wedgeRightVertex G H x y q) tau

A same-right factor profile constructs a transmission witness on the wedge.