Shared definitions for Section 5

The structures and finite rank-drop sum used by the formal statements of the marked-point symmetry section.

structure Bananas.MarkedPointAutomorphism (M : TwiceMarked) : Type

A graph automorphism which preserves the set of two marked vertices. The definition permits either fixing the marks or interchanging them.

• iso : Utilities.CFGraphIso M.graph M.graph

  The graph automorphism preserving the set of marked vertices.

• preserves_marked_set (x : M.graph.V) : x = M.u ∨ x = M.v ↔ self.iso.vertexEquiv x = M.u ∨ self.iso.vertexEquiv x = M.v

structure Bananas.MarkedPointSwap (M : TwiceMarked) extends Bananas.MarkedPointAutomorphism M : Type

A marked-point automorphism which interchanges the ordered marks.

• iso : Utilities.CFGraphIso M.graph M.graph
• preserves_marked_set (x : M.graph.V) : x = M.u ∨ x = M.v ↔ self.iso.vertexEquiv x = M.u ∨ self.iso.vertexEquiv x = M.v
• map_u : self.iso.vertexEquiv M.u = M.v
• map_v : self.iso.vertexEquiv M.v = M.u

noncomputable def Bananas.sectionFiveRankDropSum (M : TwiceMarked) (D : CFDiv M.graph) (k : ℕ) : ℤ

The finite rank-drop sum in the final, unlabelled proposition of Section 5. This is the paper's sum over a fundamental domain [k], encoded by Fin k.

Equations

• Bananas.sectionFiveRankDropSum M D k = ∑ m : Fin k, (rank M.graph (D + (↑↑m - 1) • oneChip M.u - ↑↑m • oneChip M.v) - rank M.graph (D + (↑↑m - 2) • oneChip M.u - ↑↑m • oneChip M.v))