Endpoint-aware classification for Theorem 3.9

The two core vertices of a banana have one coordinate presentation on every strand. The paper's phrase α = β is therefore not an invariant condition when a mark is an endpoint. This file states the corrected theorem directly for the two marked vertices. The exceptional alternatives retain their coordinate descriptions only for genuinely interior marks.

def Bananas.NSMForBananaException {g : ℕ} (B : Banana g) (u v : (Utilities.Certificate.SubdivisionGraph.Spec.graph B).V) : Prop

The endpoint-aware exceptional alternatives in corrected Theorem 3.9. The first three clauses are the same-strand endpoint cases, stated as vertex equalities. The final clause is the corrected interior classification.

Equations

• One or more equations did not get rendered due to their size.

theorem Bananas.nsmForBanana_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 β) : NSMForBananaException B (strandVertex B α i) (strandVertex B β 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), fully endpoint-aware and corrected.

For any two banana vertices, either they are in one of the invariant exceptional families above, or an explicit divisor has negative marked rank difference. In particular this incorporates the missing length-two midpoint exception discovered during formalization.