Corrected interior classification for Theorem 3.9

This is the interior-coordinate portion of thm-NSMForBanana. Endpoint markings require a separate statement because a multivalent vertex has several strand-coordinate presentations. Keeping this statement in coordinates makes the two genuine cross-strand exceptions visible:

• the published near-opposite-endpoint cases; and
• the corrected length-two-midpoint case, in which the other mark may be any interior point on another strand.

The proof is intentionally left as a named, documented obligation while the remaining far-mark rank calculations are assembled. In particular, it must not be replaced by the weaker nonSubmodular_of_rank_pattern API, whose rank pattern is itself a hypothesis.

def Bananas.NSMForBananaInteriorException {g : ℕ} (B : Banana g) (α β : Fin (g + 1)) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B β) : Prop

The interior-coordinate exceptional alternatives in the corrected form of Theorem 3.9. The first two clauses are exchanged by globally swapping the two multivalent vertices. The latter two clauses are the correction: a midpoint on a length-two strand is exceptional against every interior mark on a distinct strand, not only a near-endpoint mark.

Equations

• Bananas.NSMForBananaInteriorException B α β i j = (α ≠ β ∧ (↑i = 1 ∧ ↑j + 1 = B.length β ∨ ↑i + 1 = B.length α ∧ ↑j = 1 ∨ B.length α = 2 ∧ ↑i = 1 ∨ B.length β = 2 ∧ ↑j = 1))

theorem Bananas.nsmForBanana_interior_classification {g : ℕ} (hg : 3 ≤ 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) : NSMForBananaInteriorException B α β i j ∨ ∃ (D : CFDiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B)), rankDelta (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B α i) (strandVertex B β j)) D < 0

TeX label: thm-NSMForBanana (Theorem 3.9), corrected interior-mark case.

For two strictly interior marked points, either the coordinate pair belongs to the corrected cross-strand exceptional family, or there is a divisor with negative marked rank difference. The two nonexceptional distinct-strand branches use the paper's explicit three-chip witnesses; the same-strand branch uses the genus-independent witness in SameStrandInteriorNegative.lean.