Highlights of the Tricycle library

A public interface, in one file. Every main theorem of this library is restated below as an example whose type is written out in full and whose proof is the real theorem. There is not a single new definition or theorem here.

• For a reader. The complete statement of the discrete/metric gonality counterexample, as formalized, is visible here in one screen.
• For the build. Each example is checked by the kernel against the real declaration, so a change to a statement is detected in this file.

The library formalizes van Dobben de Bruyn–Smit–van der Wegen, Discrete and metric divisorial gonality can be different, JCTA 189 (2022) 105619 (arXiv:2106.12568): the minimal tricycle T_m, a connected loopless multigraph on seven vertices with fifteen edges and cyclomatic genus nine, satisfies min_{k ≥ 1} dgon(σ_k(T_m)) = 5 < 6 = dgon(T_m). Baker's Conjecture 3.14(a) is therefore false, already at r = 1 and k = 2.

Thus a proof for metric gonality alone does not imply the corresponding result for discrete divisorial gonality.

The key definitions

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

The tricycle core: the seven-vertex, fifteen-slot core whose subdivisions are the tricycle graphs. (Tricycle/Core.lean)

Equations

• Tricycle.Highlights.tricycleCore = Utilities.Tricycle.tricycleCore

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

A subdivision is a tricycle graph when its three transition slots are unsubdivided. (Tricycle/Core.lean)

Equations

• Tricycle.Highlights.IsTricycle = Utilities.Tricycle.IsTricycle

def Tricycle.Highlights.Tm : Utilities.Certificate.SubdivisionGraph.Spec 7 15

The minimal tricycle T_m: the tricycle core at all-ones lengths. (Tricycle/UpperBounds.lean)

Equations

• Tricycle.Highlights.Tm = Utilities.Tricycle.Tm

def Tricycle.Highlights.divisorialGonality (G : CFGraph) : ℕ

Divisorial gonality: the least degree of an effective divisor of rank at least one. (Utilities/Gonality/DivisorialGonality.lean)

Equations

• Tricycle.Highlights.divisorialGonality = Utilities.Gonality.divisorialGonality

def Tricycle.Highlights.regularSubdivisionGonality (G : CFGraph) : ℕ

min_{k ≥ 1} dgon(σ_k(G)), with σ_k the k-fold regular subdivision built on the occurrence presentation of G. Deliberately not called metricGonality: the identification with the metric invariant is the source's Theorem 1.5, which is not formalized here. (Utilities/Gonality/GonalityTransport.lean)

Equations

• Tricycle.Highlights.regularSubdivisionGonality = Utilities.Gonality.regularSubdivisionGonality

The headline statements

The two sides of the gap

The two reusable ingredients

Both are more general than the headline, and both are stated for an arbitrary subdivision specification rather than for one graph.