Theorem 4.13, bundled

The structural seam marked_bridgelessGenusTwo_coreNormalForm (Bananas/BridgelessGenusTwoPseudocore.lean) reduces any nontrivial bridgeless genus-two twice-marked graph, up to a certified graph isomorphism carrying the two marks, to either a Banana 2 theta presentation or a vertex wedge of two PointedGenusOneRigid factors. The two branch classifiers theta_kGeneral_iff_coordinates_nonRecurrent (ThetaKGeneralClassification.lean) and kGeneral_iff_wedge_placement (WedgeKGeneralClassification.lean) then pin down k-general transmission on each normal form exactly.

This file bundles the three into one biconditional: KGeneralTransmission on the original marked graph holds iff some certified isomorphism exhibits it as a theta graph with non-recurrent coordinates in one of the three admissible families, or as a rigid wedge with an admissible placement. The graph isomorphism has to be retained explicitly in the right-hand side (rather than existentially discarding it, as the raw coreNormalForm seam does) so that the statement is actually about (G, u, v) and not vacuously true of every graph. Transport of KGeneralTransmission, IsTorsionOrder, and TwoEdgeCutCondition along a CFGraphIso is already available (kGeneralTransmission_map_of_marks_iff, isTorsionOrder_map_of_marks_iff in Bananas/MarkedIso.lean; twoEdgeCutCondition_map_iff in Bananas/GraphIsoCuts.lean), so no new transport lemma is needed here.

def Bananas.BridgelessGenusTwoKGeneralCharacterization (G : CFGraph) (u v : G.V) (k : ℕ) : Prop

Theorem 4.13 (thm:g2general), bundled single-theorem form.

The right-hand side packages the paper's three cases (theta with non-recurrent coordinates in one of three families; vertex gluing of two equal-torsion-order cycles; vertex gluing of a length-two cycle at both its vertices) as an isomorphism-transported disjunction between the theta and wedge normal forms.

Equations

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

theorem Bananas.kGeneralTransmission_bridgelessGenusTwo_iff (G : CFGraph) (u v : G.V) (k : ℕ) (hConnected : _root_.graphConnected G) (hCut : Utilities.TwoEdgeCutCondition G) (huv : u ≠ v) (hGenus : G.genus = 2) (hTO : IsTorsionOrder (mark G u v) k) : KGeneralTransmission (mark G u v) k ↔ BridgelessGenusTwoKGeneralCharacterization G u v k

Theorem 4.13 (thm:g2general), bundled. Section 4.

For a connected bridgeless twice-marked genus-two graph with distinct marks and torsion order k, k-general transmission is equivalent to the paper's structural characterization.