Nonrecurrence on bridgeless genus-two graphs

The finite-orbit part of the proof of Theorem 4.8 does not use a theta presentation. What it needs is precisely Lemma 2.3: on a nontrivial bridgeless graph, every effective divisor of degree one has rank zero and a unique vertex representative. This module packages that argument with the library's TwoEdgeCutCondition as the no-bridge hypothesis.

theorem Bananas.rank_eq_zero_of_degree_one_rank_nonneg_of_twoEdgeCutCondition (G : CFGraph) (hConnected : _root_.graphConnected G) (hCut : Utilities.TwoEdgeCutCondition G) (hNontrivial : ∃ (p : G.V) (q : G.V), p ≠ q) (X : CFDiv G) (hDegree : CFDiv.degree X = 1) (hRank : 0 ≤ rank G X) : rank G X = 0

On a nontrivial connected graph with no one-edge cut, an effective degree-one divisor has rank zero.

theorem Bananas.effectiveDegreeOneTwistResidues_ncard_le_two_of_nonRecurrent_bridgeless (G : CFGraph) (u v : G.V) (D : CFDiv G) (k : ℕ) (hConnected : _root_.graphConnected G) (hCut : Utilities.TwoEdgeCutCondition G) (hNontrivial : ∃ (p : G.V) (q : G.V), p ≠ q) (hTO : IsTorsionOrder (mark G u v) k) (hNonrec : NonRecurrent (mark G u v) k) : (effectiveDegreeOneTwistResidues (mark G u v) D k).ncard ≤ 2

The effective degree-one members of a finite exact torsion orbit are at most two when the marked difference is nonrecurrent. This is the cardinality estimate in the proof of Theorem 4.8, stated without a theta presentation.

theorem Bananas.nonRecurrent_of_kGeneralTransmission_of_effectiveResidueFormula (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) (hFormula : ∀ (w : (mark G u v).graph.V) (τ : ℤ → ℤ), IsTransmissionPermutation (mark G u v) (oneChip w) τ → IsKAffine k τ → kInversionCount k τ = (effectiveDegreeOneTwistResidues (mark G u v) (oneChip w) k).ncard) (hKGT : KGeneralTransmission (mark G u v) k) : NonRecurrent (mark G u v) k

The converse implication in Theorem 4.8, factored from its genus-two inversion identity. The formula hypothesis is exactly the correction-free conclusion of Lemma 4.10 for the single-chip divisors used in the argument. Thus this theorem applies to any nontrivial bridgeless genus-two graph as soon as its corresponding inversion formula is supplied.