The theta-coordinate branch of Theorem 4.13

Each non-endpoint coordinate family from the all-submodularity classification is rigid, so the general genus-two nonrecurrence criterion applies without any residual graph-theoretic hypothesis.

theorem Bananas.theta_distinctInterior_kGeneral_iff_nonRecurrent {k : ℕ} (B : Banana 2) (alpha beta : Fin 3) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B alpha) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B beta) (hi : Utilities.Certificate.SubdivisionGraph.Spec.IsInteriorPosition B alpha i) (hj : Utilities.Certificate.SubdivisionGraph.Spec.IsInteriorPosition B beta j) (hab : alpha ≠ beta) (hTO : IsTorsionOrder (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B alpha i) (strandVertex B beta j)) k) : KGeneralTransmission (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B alpha i) (strandVertex B beta j)) k ↔ NonRecurrent (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B alpha i) (strandVertex B beta j)) k

Distinct interior theta strands: exact torsion plus nonrecurrence is equivalent to general transmission.

theorem Bananas.theta_zeroPenultimate_kGeneral_iff_nonRecurrent {k : ℕ} (B : Banana 2) (alpha : Fin 3) (hlen : 2 ≤ B.length alpha) (hTO : IsTorsionOrder (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B alpha ⟨0, ⋯⟩) (strandVertex B alpha ⟨B.length alpha - 1, ⋯⟩)) k) : KGeneralTransmission (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B alpha ⟨0, ⋯⟩) (strandVertex B alpha ⟨B.length alpha - 1, ⋯⟩)) k ↔ NonRecurrent (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B alpha ⟨0, ⋯⟩) (strandVertex B alpha ⟨B.length alpha - 1, ⋯⟩)) k

The normalized (0,n-1) theta boundary family is rigid and hence obeys the same exact nonrecurrence criterion.

theorem Bananas.theta_oneLength_kGeneral_iff_nonRecurrent {k : ℕ} (B : Banana 2) (alpha : Fin 3) (hlen : 2 ≤ B.length alpha) (hTO : IsTorsionOrder (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B alpha ⟨1, ⋯⟩) (strandVertex B alpha ⟨B.length alpha, ⋯⟩)) k) : KGeneralTransmission (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B alpha ⟨1, ⋯⟩) (strandVertex B alpha ⟨B.length alpha, ⋯⟩)) k ↔ NonRecurrent (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B alpha ⟨1, ⋯⟩) (strandVertex B alpha ⟨B.length alpha, ⋯⟩)) k

The normalized (1,n) theta boundary family is rigid and hence obeys the same exact nonrecurrence criterion.