Section 5: transmission transports

The three exact transport calculations used in Section 5 of the twice-marked banana paper. They are kept apart from the statement ledger so that the latter can expose the paper-facing names without becoming an implementation dependency for later symmetry arguments.

theorem Bananas.sectionFive_swap_value_iff_proof {M : TwiceMarked} {D : CFDiv M.graph} {tau : ℤ → ℤ} (hTau : IsTransmissionPermutation M D tau) (a b : ℤ) : tau b = a ↔ swapTransmissionPermutation tau (-a) = -b

The reflected inverse used after exchanging marks has the expected value relation. This is the raw-function form of the first calculation in Lemma 5.2.

theorem Bananas.sectionFive_dual_transmission_proof {G : CFGraph} (hconn : _root_.graphConnected G) (u v : G.V) {D : CFDiv G} {tau : ℤ → ℤ} (hTau : IsTransmissionPermutation (mark G u v) D tau) : IsTransmissionPermutation (mark G v u) (Utilities.transmissionDualDivisor u v D) (rawInverse tau)

Canonical duality gives the raw inverse transmission permutation at the exchanged marks. Riemann--Roch supplies the only non-formal ingredient: it identifies the marked second differences of a divisor and its normalized canonical complement.

theorem Bananas.sectionFive_map_transmission_proof {G H : CFGraph} (phi : Utilities.CFGraphIso G H) (u v : G.V) {D : CFDiv G} {tau : ℤ → ℤ} (hTau : IsTransmissionPermutation (mark G u v) D tau) : IsTransmissionPermutation (mark H (phi.vertexEquiv u) (phi.vertexEquiv v)) (phi.mapDiv D) tau

Relabeling a graph transports a raw transmission permutation unchanged. This is the raw counterpart of CFGraphIso.satisfiesTransmission_mapDiv.