The tricycle core

The counterexample of van Dobben de Bruyn, Smit and van der Wegen, Discrete and metric divisorial gonality can be different, JCTA 189 (2022) 105619 (arXiv:2106.12568), in the vocabulary of this repository.

Tricycle characterization. The formalization uses the characterization stated in the source text and depicted in Figures 1(b), 1(c), and 3:

a multigraph is a tricycle if and only if it is a subdivision of the minimal tricycle T_m in which the transition edges are not subdivided.

That is the definition formalized here. The theorems in this library prove dgon(T_m) = 6 and dgon(σ₂(T_m)) = 5.

The slot dictionary

tricycleCore : Core 7 15 has vertices v₀ = 0 and v₁⁻ = 1, v₁⁺ = 2, v₂⁻ = 3, v₂⁺ = 4, v₃⁻ = 5, v₃⁺ = 6, and slots

slots	role	source's name
0–5	v₀ — vᵢ^±	the six spokes
6,7 / 8,9 / 10,11	parallel pairs vᵢ⁻ — vᵢ⁺	the three cycles C₁,C₂,C₃
12,13,14	v₁⁺—v₂⁻, v₂⁺—v₃⁻, v₃⁺—v₁⁻	the three transition slots

A subdivision H of T_m is tricycleSpec length hpos for an arbitrary positive length vector; σ_k(T_m) is length ≡ k; and a tricycle graph is one with IsTricycle length, i.e. the three transition slots have length one.

The core

def Utilities.Tricycle.tricycleCore : Certificate.ExplicitPotential.Core 7 15

The minimal tricycle T_m as an ordered core: six spokes, three bananas, three transition slots.

Equations

• Utilities.Tricycle.tricycleCore = { tail := ![0, 0, 0, 0, 0, 0, 1, 1, 3, 3, 5, 5, 2, 4, 6], head := ![1, 2, 3, 4, 5, 6, 2, 2, 4, 4, 6, 6, 3, 5, 1] }

theorem Utilities.Tricycle.tricycleCore_loopless (edge : Fin 15) : tricycleCore.tail edge ≠ tricycleCore.head edge

theorem Utilities.Tricycle.tricycleCore_connected : tricycleCore.Connected

Named vertices and slots

def Utilities.Tricycle.centre : Fin 7

The central vertex v₀.

Equations

• Utilities.Tricycle.centre = 0

def Utilities.Tricycle.vMinus : Fin 3 → Fin 7

The transition vertices vᵢ⁻.

Equations

• Utilities.Tricycle.vMinus = ![1, 3, 5]

def Utilities.Tricycle.vPlus : Fin 3 → Fin 7

The transition vertices vᵢ⁺.

Equations

• Utilities.Tricycle.vPlus = ![2, 4, 6]

def Utilities.Tricycle.spokeMinus : Fin 3 → Fin 15

The spoke slot v₀ — vᵢ⁻.

Equations

• Utilities.Tricycle.spokeMinus = ![0, 2, 4]

def Utilities.Tricycle.spokePlus : Fin 3 → Fin 15

The spoke slot v₀ — vᵢ⁺.

Equations

• Utilities.Tricycle.spokePlus = ![1, 3, 5]

def Utilities.Tricycle.cycleSlot : Fin 3 → Fin 2 → Fin 15

The two parallel slots of the cycle Cᵢ.

Equations

• Utilities.Tricycle.cycleSlot = ![![6, 7], ![8, 9], ![10, 11]]

def Utilities.Tricycle.transitionSlot : Fin 3 → Fin 15

The transition slot leaving vᵢ⁺.

Equations

• Utilities.Tricycle.transitionSlot = ![12, 13, 14]

def Utilities.Tricycle.spokeSlots : Finset (Fin 15)

The six spoke slots.

Equations

• Utilities.Tricycle.spokeSlots = {0, 1, 2, 3, 4, 5}

def Utilities.Tricycle.transitionVertices : Finset (Fin 7)

The six transition vertices.

Equations

• Utilities.Tricycle.transitionVertices = {1, 2, 3, 4, 5, 6}

The slot dictionary, verified

theorem Utilities.Tricycle.spokeMinus_ends (i : Fin 3) : tricycleCore.tail (spokeMinus i) = centre ∧ tricycleCore.head (spokeMinus i) = vMinus i

theorem Utilities.Tricycle.spokePlus_ends (i : Fin 3) : tricycleCore.tail (spokePlus i) = centre ∧ tricycleCore.head (spokePlus i) = vPlus i

theorem Utilities.Tricycle.cycleSlot_ends (i : Fin 3) (j : Fin 2) : tricycleCore.tail (cycleSlot i j) = vMinus i ∧ tricycleCore.head (cycleSlot i j) = vPlus i

theorem Utilities.Tricycle.transitionSlot_ends (i : Fin 3) : tricycleCore.tail (transitionSlot i) = vPlus i ∧ tricycleCore.head (transitionSlot i) = vMinus (i + 1)

theorem Utilities.Tricycle.mem_spokeSlots_iff (e : Fin 15) : e ∈ spokeSlots ↔ ∃ (i : Fin 3), e = spokeMinus i ∨ e = spokePlus i

theorem Utilities.Tricycle.mem_transitionVertices_iff (v : Fin 7) : v ∈ transitionVertices ↔ ∃ (i : Fin 3), v = vMinus i ∨ v = vPlus i

theorem Utilities.Tricycle.slot_classification (e : Fin 15) : (∃ (i : Fin 3), e = spokeMinus i ∨ e = spokePlus i) ∨ (∃ (i : Fin 3) (j : Fin 2), e = cycleSlot i j) ∨ ∃ (i : Fin 3), e = transitionSlot i

The fifteen slots are exactly the six spokes, the six cycle slots and the three transition slots.

Subdivisions of the tricycle core

def Utilities.Tricycle.tricycleSpec (length : Fin 15 → ℕ) (hpos : ∀ (e : Fin 15), 0 < length e) : Certificate.SubdivisionGraph.Spec 7 15

A subdivision H of the minimal tricycle, at an arbitrary positive length vector.

Equations

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

@[simp]

theorem Utilities.Tricycle.tricycleSpec_core (length : Fin 15 → ℕ) (hpos : ∀ (e : Fin 15), 0 < length e) : (tricycleSpec length hpos).core = tricycleCore

@[simp]

theorem Utilities.Tricycle.tricycleSpec_length (length : Fin 15 → ℕ) (hpos : ∀ (e : Fin 15), 0 < length e) (e : Fin 15) : (tricycleSpec length hpos).length e = length e

theorem Utilities.Tricycle.tricycleSpec_connected (length : Fin 15 → ℕ) (hpos : ∀ (e : Fin 15), 0 < length e) : graphConnected (tricycleSpec length hpos).graph

theorem Utilities.Tricycle.tricycleSpec_genus (length : Fin 15 → ℕ) (hpos : ∀ (e : Fin 15), 0 < length e) : (tricycleSpec length hpos).graph.genus = 9

Every subdivision of the minimal tricycle has genus nine; in particular the tricycle attains the Brill--Noether bound ⌊(g+3)/2⌋ = 6 with equality.

def Utilities.Tricycle.IsTricycle (length : Fin 15 → ℕ) : Prop

A tricycle graph: the transition slots are not subdivided. This is the characterisation at line 537 of the source's TeX, not Definition 3.1.

Equations

• Utilities.Tricycle.IsTricycle length = ∀ (i : Fin 3), length (Utilities.Tricycle.transitionSlot i) = 1