Reducing bridgeless genus-two general transmission to core normal forms

This is the marked, transmission-theoretic form of the pseudocore reduction. It keeps the remaining work in Theorem 4.13 genuinely algebraic: after this theorem, there is no bivalent-path suppression or graph-isomorphism transport left to prove.

theorem Bananas.kGeneralTransmission_bridgelessGenusTwo_coreNormalForm (G : CFGraph) (u v : G.V) (k : ℕ) (hConnected : _root_.graphConnected G) (hCut : Utilities.TwoEdgeCutCondition G) (hNontrivial : ∃ (p : G.V) (q : G.V), p ≠ q) (hGenus : G.genus = 2) (hKGT : KGeneralTransmission (mark G u v) k) : (∃ (B : Banana 2) (u' : (Utilities.Certificate.SubdivisionGraph.Spec.graph B).V) (v' : (Utilities.Certificate.SubdivisionGraph.Spec.graph B).V), KGeneralTransmission (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) u' v') k) ∨ ∃ (base : CFGraph) (factor : CFGraph) (attachment : base.V) (root : factor.V) (u' : (Utilities.vertexWedge base factor attachment root).V) (v' : (Utilities.vertexWedge base factor attachment root).V), Utilities.PointedGenusOneRigid base attachment ∧ Utilities.PointedGenusOneRigid factor root ∧ Utilities.TwoEdgeCutCondition base ∧ Utilities.TwoEdgeCutCondition factor ∧ Utilities.TwoEdgeCutCondition (Utilities.vertexWedge base factor attachment root) ∧ KGeneralTransmission (mark (Utilities.vertexWedge base factor attachment root) u' v') k

A k-general transmission instance on a nontrivial bridgeless genus-two graph has a theta or a two pointed-rigid-genus-one-factor wedge presentation, with the ordered marks and the k-general-transmission assertion transported to that presentation.