Normalized coordinates for the far-mark construction

SameStrand and GenericRankWitness deliberately state their Dhar lemmas in the stored pathVertex coordinates. The paper, and the far-mark statements, use the normalized strandVertex coordinates instead. This file is the small adapter between those two interfaces. In particular, it does not attempt the far-mark case split itself: it exposes the rank-zero and rank-minus-one three-chip facts that each case consumes.

The normalized/raw coordinate adapter (normalizedPathPosition, strandVertex_eq_pathVertex_normalized, normalizedPathPosition_isInterior) now lives in BananaBasics.lean, since several files need it.

theorem Bananas.normalizedPathPosition_far {g : ℕ} (B : Banana g) (α : Fin (g + 1)) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (hi : 2 ≤ ↑i ∧ ↑i + 2 ≤ B.length α) : 2 ≤ ↑(normalizedPathPosition B α i) ∧ ↑(normalizedPathPosition B α i) + 2 ≤ B.length α

Far normalized positions remain far after changing the stored path orientation. This is the arithmetic part of the paper's far-mark construction; it is independent of the choice of auxiliary chips.

theorem Bananas.far_mark_to_raw {g : ℕ} (B : Banana g) (α : Fin (g + 1)) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (x : (Utilities.Certificate.SubdivisionGraph.Spec.graph B).V) (hx : strandVertex B α i = x) (hi : 2 ≤ ↑i ∧ ↑i + 2 ≤ B.length α) : ∃ (p : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α), Utilities.Certificate.SubdivisionGraph.Spec.pathVertex B α p = x ∧ 2 ≤ ↑p ∧ ↑p + 2 ≤ B.length α

Package a normalized far mark as the raw path vertex and coordinate facts consumed by the path-firing lemmas.

theorem Bananas.rank_strand_pair_sub_of_distinct_interior {g : ℕ} (hg : 2 ≤ g) (B : Banana g) (α β γ : Fin (g + 1)) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B β) (q : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B γ) (hi : 0 < ↑i ∧ ↑i < B.length α) (hj : 0 < ↑j ∧ ↑j < B.length β) (hq : 0 < ↑q ∧ ↑q < B.length γ) (hαβ : α ≠ β) (hqx : strandVertex B γ q ≠ strandVertex B α i) (hqy : strandVertex B γ q ≠ strandVertex B β j) : rank (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (oneChip (strandVertex B α i) + oneChip (strandVertex B β j) - oneChip (strandVertex B γ q)) = -1

Three interior chips on two distinct normalized strands leave rank -1 after deleting a distinct third interior chip. The third chip may be on either of the two marked strands; this is the form used by the far-mark construction after a path slide.

theorem Bananas.rank_strand_pair_zero_of_distinct_interior {g : ℕ} (hg : 2 ≤ g) (B : Banana g) (α β γ : Fin (g + 1)) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B β) (q : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B γ) (hi : 0 < ↑i ∧ ↑i < B.length α) (hj : 0 < ↑j ∧ ↑j < B.length β) (hq : 0 < ↑q ∧ ↑q < B.length γ) (hαβ : α ≠ β) (hqx : strandVertex B γ q ≠ strandVertex B α i) (hqy : strandVertex B γ q ≠ strandVertex B β j) : rank (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (oneChip (strandVertex B α i) + oneChip (strandVertex B β j)) = 0

The positive two-chip companion of rank_strand_pair_sub_of_distinct_interior.