The tricycle upper bounds

Two explicit divisors, both certified through the core vertices are rank-determining theorem Spec.rank_ge_one_of_forall_mem_coreVertices (Utilities/Foundations/RankDeterminingSet.lean), which is the repository's metric-free form of Luo's Theorem 1.6 and is exactly the source's Corollary 2.13. Only seven obligations arise — one per core vertex — and each is a single explicit firing set, checked by decide.

• Proposition 3.3 of van Dobben de Bruyn–Smit–van der Wegen: D₀ = 2·v₀ + Σᵢ (midpoint of transition slot i) has positive rank on σ₂(T_m), so dgon(σ₂(T_m)) ≤ 5. Firing Sᵢᶜ moves exactly four chips: two off v₀ — which is why the coefficient is 2, and why k = 2 and not k = 1 — and one off each of the two transition midpoints bounding the component Sᵢ of σ₂(T_m) ∖ supp D₀ containing the cycle Cᵢ. At k = 2 a transition midpoint is adjacent to both of its transition vertices, so those two chips land exactly on vᵢ⁻ and vᵢ⁺.
• Theorem 3.9, upper half: one chip on each of the six transition vertices has positive rank on T_m, so dgon(T_m) ≤ 6.

The firing sets and residual divisors are checked directly by the Lean kernel.

Winnability from an explicit script

@[instance_reducible]

instance Utilities.Tricycle.decidableEffective {G : CFGraph} (D : CFDiv G) : Decidable (effective D)

effective is a bounded quantifier over a Fintype; make that visible to instance search so the concrete checks below are decide-shaped.

Equations

• Utilities.Tricycle.decidableEffective D = id inferInstance

theorem Utilities.Tricycle.winnable_of_effective_add_prin {G : CFGraph} (D : CFDiv G) (x : firingScript G) (h : effective (D + (prin G) x)) : winnable G D

An explicit firing script witnessing winnability.

The two concrete subdivisions

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

The minimal tricycle T_m itself.

Equations

• Utilities.Tricycle.Tm = Utilities.Tricycle.tricycleSpec (fun (x : Fin 15) => 1) ⋯

def Utilities.Tricycle.Tm2 : Certificate.SubdivisionGraph.Spec 7 15

Its 2-subdivision σ₂(T_m).

Equations

• Utilities.Tricycle.Tm2 = Utilities.Tricycle.tricycleSpec (fun (x : Fin 15) => 2) ⋯

theorem Utilities.Tricycle.Tm_connected : graphConnected Tm.graph

theorem Utilities.Tricycle.Tm2_connected : graphConnected Tm2.graph

Theorem 3.9, upper half: dgon(T_m) ≤ 6

def Utilities.Tricycle.sixChips : CFDiv Tm.graph

One chip on each of the six transition vertices.

Equations

• Utilities.Tricycle.sixChips v = if v = Utilities.Tricycle.Tm.coreVertex 0 then 0 else 1

def Utilities.Tricycle.TmOuterRing : Finset Tm.graph.V

The outer ring of T_m: everything but the centre. Firing it once is legal (each transition vertex has exactly one spoke edge and exactly one chip) and delivers six chips to v₀.

Equations

• Utilities.Tricycle.TmOuterRing = {v : Utilities.Tricycle.Tm.graph.V | v ≠ Utilities.Tricycle.Tm.coreVertex 0}

theorem Utilities.Tricycle.sixChips_effective : effective sixChips

theorem Utilities.Tricycle.sixChips_deg : CFDiv.degree sixChips = 6

theorem Utilities.Tricycle.sixChips_rank : rank Tm.graph sixChips ≥ 1

theorem Utilities.Tricycle.divisorialGonality_Tm_le_six : Gonality.divisorialGonality Tm.graph ≤ 6

Theorem 3.9, upper half. The minimal tricycle has divisorial gonality at most six.

Proposition 3.3: dgon(σ₂(T_m)) ≤ 5

def Utilities.Tricycle.transitionMidpoint (i : Fin 3) : Tm2.graph.V

The midpoint of transition slot i in σ₂.

Equations

• Utilities.Tricycle.transitionMidpoint i = Utilities.Tricycle.Tm2.interiorVertex (Utilities.Tricycle.transitionSlot i) ⟨0, ⋯⟩

def Utilities.Tricycle.specialDivisor : CFDiv Tm2.graph

The special divisor D₀ = 2·v₀ + Σᵢ (midpoint of transition slot i).

Equations

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

def Utilities.Tricycle.cycleComponent (i : Fin 3) : Finset Tm2.graph.V

The component of σ₂(T_m) ∖ supp D₀ containing the cycle Cᵢ: the cycle itself together with the interiors of the two spokes at vᵢ⁻ and vᵢ⁺.

Equations

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

def Utilities.Tricycle.cycleComponentCompl (i : Fin 3) : Finset Tm2.graph.V

The set actually fired: the complement of Sᵢ.

Equations

• Utilities.Tricycle.cycleComponentCompl i = {v : Utilities.Tricycle.Tm2.graph.V | v ∉ Utilities.Tricycle.cycleComponent i}

theorem Utilities.Tricycle.specialDivisor_effective : effective specialDivisor

theorem Utilities.Tricycle.specialDivisor_deg : CFDiv.degree specialDivisor = 5

theorem Utilities.Tricycle.specialDivisor_rank : rank Tm2.graph specialDivisor ≥ 1

theorem Utilities.Tricycle.divisorialGonality_Tm2_le_five : Gonality.divisorialGonality Tm2.graph ≤ 5

Proposition 3.3. The 2-subdivision of the minimal tricycle has divisorial gonality at most five.