Corrected Theorem 1.16

The published thm:bananaSimple claims that a banana marking has a non-submodular divisor whenever one mark is at distance at least two from both multivalent vertices. The corrected Theorem 3.9 shows that this is false: the other mark may be the midpoint of a distinct length-two strand. In that case every divisor is submodular, no matter where the first interior mark lies.

This module records the sharp corrected statement. A normalized coordinate p is far from both endpoints when 2 ≤ p.val and p.val + 2 ≤ B.length alpha. If either mark is far, then either the other mark is the midpoint of a distinct length-two strand, or an explicit divisor has negative marked rank difference.

def Bananas.FarFromBananaEndpoints {g : ℕ} (B : Banana g) (alpha : Fin (g + 1)) (p : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B alpha) : Prop

A normalized banana-strand position lies at graph distance at least two from each of the two multivalent vertices.

Equations

• Bananas.FarFromBananaEndpoints B alpha p = (2 ≤ ↑p ∧ ↑p + 2 ≤ B.length alpha)

def Bananas.CorrectedBananaSimpleException {g : ℕ} (B : Banana g) (alpha beta : Fin (g + 1)) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B alpha) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B beta) : Prop

The extra exceptional family missing from the published Theorem 1.16: one of the marks is the midpoint of a length-two strand distinct from the strand containing the other mark.

Equations

• Bananas.CorrectedBananaSimpleException B alpha beta i j = (alpha ≠ beta ∧ B.length beta = 2 ∧ ↑j = 1 ∨ alpha ≠ beta ∧ B.length alpha = 2 ∧ ↑i = 1)

theorem Bananas.corrected_bananaSimple_of_first_far {g : ℕ} (hg : 3 ≤ g) (B : Banana g) (alpha beta : Fin (g + 1)) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B alpha) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B beta) (hiFar : FarFromBananaEndpoints B alpha i) : alpha ≠ beta ∧ B.length beta = 2 ∧ ↑j = 1 ∨ ∃ (D : CFDiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B)), rankDelta (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B alpha i) (strandVertex B beta j)) D < 0

One-sided sharp form of corrected Theorem 1.16.

If the first mark is far from both endpoints, the only exceptional case is that the second mark is the midpoint of a distinct length-two strand.

theorem Bananas.corrected_bananaSimple {g : ℕ} (hg : 3 ≤ g) (B : Banana g) (alpha beta : Fin (g + 1)) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B alpha) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B beta) (hFar : FarFromBananaEndpoints B alpha i ∨ FarFromBananaEndpoints B beta j) : CorrectedBananaSimpleException B alpha beta i j ∨ ∃ (D : CFDiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B)), rankDelta (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B alpha i) (strandVertex B beta j)) D < 0

Sharp corrected Theorem 1.16 (thm:bananaSimple).

If at least one marked coordinate is at distance at least two from both multivalent vertices, then either the other mark is the midpoint of a distinct length-two strand, or there is an explicit divisor with negative marked rank difference.