The support of a cross-strand two-chip divisor

Paper source: cor:suppUV (Corollary 3.8). Two chips at interior points of distinct strands of a banana have rank support exactly at those two points.

ThetaNonrecurrence proves this for Banana 2, as the geometric input to the non-recurrence argument. This file gives the general-genus statement. The interior half is FarMarkAPI.rank_strand_pair_sub_of_distinct_interior; what had to be added is the two multivalent vertices, which the banana normal form handles directly: deleting an endpoint from a semibreak divisor puts a -1 endpoint coefficient into the normal form, and such a divisor has rank -1.

theorem Bananas.exists_interior_strandVertex {g : ℕ} (B : Banana g) (γ : Fin (g + 1)) (o : Fin (B.length γ - 1)) : ∃ (q : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B γ), Utilities.Certificate.SubdivisionGraph.Spec.IsInteriorPosition B γ q ∧ strandVertex B γ q = Utilities.Certificate.SubdivisionGraph.Spec.interiorVertex B γ o

Every interior vertex is a normalized strand position.

strandVertex stores a strand in either orientation, so the position realizing a given interior offset depends on B.core.tail.

theorem Bananas.rankSupport_two_interior_distinct_strands {g : ℕ} (hg : 2 ≤ g) (B : Banana g) (α β : Fin (g + 1)) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B β) (hi : Utilities.Certificate.SubdivisionGraph.Spec.IsInteriorPosition B α i) (hj : Utilities.Certificate.SubdivisionGraph.Spec.IsInteriorPosition B β j) (hαβ : α ≠ β) : rankSupport (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (oneChip (strandVertex B α i) + oneChip (strandVertex B β j)) = {strandVertex B α i, strandVertex B β j}

TeX label: cor:suppUV (Corollary 3.8), general genus.

Two chips at interior points of distinct strands have rank support exactly at those two points.

theorem Bananas.suppUV {g : ℕ} (hg : 2 ≤ g) (B : Banana g) (α β : Fin (g + 1)) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B β) (hi : Utilities.Certificate.SubdivisionGraph.Spec.IsInteriorPosition B α i) (hj : Utilities.Certificate.SubdivisionGraph.Spec.IsInteriorPosition B β j) (hαβ : α ≠ β) : rankSupport (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (oneChip (strandVertex B α i) + oneChip (strandVertex B β j)) = {strandVertex B α i, strandVertex B β j}

TeX label: cor:suppUV (Corollary 3.8), general genus.

Two chips at interior points of distinct strands of a banana of genus at least two have rank support exactly at those two points.

FarMarkAPI already supplied r(u + v - w) = -1 for every interior w distinct from both marks; what completes the statement is the two multivalent vertices, which the banana normal form handles directly: u + v is a semibreak, so deleting an endpoint from it is a normal form with a negative endpoint coefficient, and those have rank -1.