Torsion order under graph isomorphism

The paper's torsion order is intrinsic to a marked graph. This file supplies the raw-divisor transport needed to use certified subdivision relabelings.

theorem Bananas.torsionWitness_map {G H : CFGraph} (φ : Utilities.CFGraphIso G H) (u v : G.V) (k : ℕ) (h : TorsionWitness (mark G u v) k) : TorsionWitness (mark H (φ.vertexEquiv u) (φ.vertexEquiv v)) k

theorem Bananas.torsionWitness_map_iff {G H : CFGraph} (φ : Utilities.CFGraphIso G H) (u v : G.V) (k : ℕ) : TorsionWitness (mark H (φ.vertexEquiv u) (φ.vertexEquiv v)) k ↔ TorsionWitness (mark G u v) k

theorem Bananas.isTorsionOrder_map_iff {G H : CFGraph} (φ : Utilities.CFGraphIso G H) (u v : G.V) (k : ℕ) : IsTorsionOrder (mark H (φ.vertexEquiv u) (φ.vertexEquiv v)) k ↔ IsTorsionOrder (mark G u v) k