Transmission through a presented vertex wedge

This file joins the abstract factor-profile theorem for a vertex wedge to the presentation interface for an ambient graph. It is deliberately valid for an arbitrary ASP permutation and arbitrary factor divisors.

@[simp]

theorem Utilities.VertexWedgePresentation.transmissionExists_iff {K : CFGraph} {G : CFGraph} {H : CFGraph} {x : G.V} {y : H.V} (P : VertexWedgePresentation K G H x y) (u : G.V) (v : H.V) (tau : AspPerm) : TransmissionExists K (P.leftMap u) (P.rightMap v) tau ↔ TransmissionExists (vertexWedge G H x y) (Sum.inl u) (wedgeRightVertex G H x y v) tau

Transmission existence on a presented graph is exactly transmission existence on its concrete vertex-wedge model.

theorem Utilities.VertexWedgePresentation.transmissionExists_of_profile {K : CFGraph} {G : CFGraph} {H : CFGraph} {x : G.V} {y : H.V} (P : VertexWedgePresentation K G H x y) (u : G.V) (v : H.V) (tau : AspPerm) (D : CFDiv G) (E : CFDiv H) (hProfile : WedgeTransmissionProfile G H x y D E u v tau) : TransmissionExists K (P.leftMap u) (P.rightMap v) tau

A pair of factor divisors satisfying the exact wedge rank profile gives a transmission witness on any graph carrying the corresponding wedge presentation.

theorem Utilities.VertexWedgePresentation.satisfiesTransmission_map_wedgeAddDivisor_of_profile {K : CFGraph} {G : CFGraph} {H : CFGraph} {x : G.V} {y : H.V} (P : VertexWedgePresentation K G H x y) (u : G.V) (v : H.V) (tau : AspPerm) (D : CFDiv G) (E : CFDiv H) (hProfile : WedgeTransmissionProfile G H x y D E u v tau) : SatisfiesTransmission K (P.leftMap u) (P.rightMap v) tau (P.graphIso.mapDiv (wedgeAddDivisor G H x y D E))

Explicit-divisor form of transmissionExists_of_profile: the witness on the ambient graph is the relabeling of the wedge-additive factor divisor.