Elementary geometry of normalized banana coordinates

The reusable subdivision representation stores each parallel core edge with an arbitrary orientation. These lemmas certify that strandVertex repairs that choice and agrees with the paper's common two-endpoint coordinates.

theorem Bananas.fin_two_eq_zero_or_one (x : Fin 2) : x = 0 ∨ x = 1

theorem Bananas.head_eq_other_of_tail {g : ℕ} (B : Banana g) (α : Fin (g + 1)) (hTail : B.core.tail α = 0) : B.core.head α = 1

A loopless slot in a two-vertex core has the other vertex as its head.

theorem Bananas.tail_eq_other_of_head {g : ℕ} (B : Banana g) (α : Fin (g + 1)) (hHead : B.core.head α = 0) : B.core.tail α = 1

A loopless slot in a two-vertex core has the other vertex as its tail.

theorem Bananas.strandVertex_zero {g : ℕ} (B : Banana g) (α : Fin (g + 1)) : strandVertex B α ⟨0, ⋯⟩ = leftEndpoint B

Coordinate zero on every strand is the common left endpoint.

theorem Bananas.strandVertex_length {g : ℕ} (B : Banana g) (α : Fin (g + 1)) : strandVertex B α ⟨B.length α, ⋯⟩ = rightEndpoint B

Coordinate length α on every strand is the common right endpoint.

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

The stored path position corresponding to a normalized strand position. SubdivisionGraph.Spec allows a slot to be stored in either orientation; this picks out whichever raw path position strandVertex actually reads from.

Equations

• Bananas.normalizedPathPosition B α i = if B.core.tail α = 0 then i else ⟨B.length α - ↑i, ⋯⟩

theorem Bananas.strandVertex_eq_pathVertex_normalized {g : ℕ} (B : Banana g) (α : Fin (g + 1)) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) : strandVertex B α i = Utilities.Certificate.SubdivisionGraph.Spec.pathVertex B α (normalizedPathPosition B α i)

strandVertex is pathVertex at the corresponding stored position.

theorem Bananas.normalizedPathPosition_isInterior {g : ℕ} (B : Banana g) (α : Fin (g + 1)) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (hi : 0 < ↑i ∧ ↑i < B.length α) : Utilities.Certificate.SubdivisionGraph.Spec.IsInteriorPosition B α (normalizedPathPosition B α i)

Interior normalized positions remain interior after changing storage orientation.

theorem Bananas.exists_normalized_pathPosition {g : ℕ} (B : Banana g) (α : Fin (g + 1)) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) : ∃ (p : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α), strandVertex B α i = Utilities.Certificate.SubdivisionGraph.Spec.pathVertex B α p ∧ (Utilities.Certificate.SubdivisionGraph.Spec.IsInteriorPosition B α i → Utilities.Certificate.SubdivisionGraph.Spec.IsInteriorPosition B α p)

Bundled form of normalizedPathPosition: a normalized strand position always has a raw path-position witness that agrees with strandVertex and transports interiority.

theorem Bananas.strandVertex_injective {g : ℕ} (B : Banana g) (α : Fin (g + 1)) : Function.Injective (strandVertex B α)

On a fixed strand, normalized positions name distinct vertices.

theorem Bananas.strandVertex_ne_leftEndpoint {g : ℕ} (B : Banana g) (α : Fin (g + 1)) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (hi : 0 < ↑i) : strandVertex B α i ≠ leftEndpoint B

A strictly positive normalized position is not the left endpoint.

theorem Bananas.strandVertex_ne_rightEndpoint {g : ℕ} (B : Banana g) (α : Fin (g + 1)) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (hi : ↑i < B.length α) : strandVertex B α i ≠ rightEndpoint B

A position strictly before the end is not the right endpoint.

theorem Bananas.leftEndpoint_ne_rightEndpoint {g : ℕ} (B : Banana g) : leftEndpoint B ≠ rightEndpoint B

The two multivalent vertices of a banana are distinct. (coreVertex is Sum.inl on the nose, so this is (0 : Fin 2) ≠ 1.)

theorem Bananas.endpoint_sum_linearEquiv_strand_reflection {g : ℕ} (B : Banana g) (α : Fin (g + 1)) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) : linearEquiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (oneChip (leftEndpoint B) + oneChip (rightEndpoint B)) (oneChip (strandVertex B α i) + oneChip (strandVertex B α (strandMirror B α i)))

On every strand, the sum of the two endpoints is linearly equivalent to the sum of a normalized position and its reflected position.

theorem Bananas.strandVertex_surjective {g : ℕ} (B : Banana g) (x : (Utilities.Certificate.SubdivisionGraph.Spec.graph B).V) : ∃ (alpha : Fin (g + 1)) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B alpha), strandVertex B alpha i = x

Every physical vertex of a banana graph lies at some normalized position on some strand: strandVertex is (jointly, over all strands) surjective.