Theorem 3.9 and the tricycle gap #
The lower half of van Dobben de Bruyn–Smit–van der Wegen's Theorem 3.9 —
dgon(G) ≥ 6 for every tricycle graph, i.e. every subdivision of T_m whose
three transition edges are not subdivided — and the assembly of the
counterexample.
Given Lemma 3.6, the argument is short. On a tricycle a chip on a transition path must sit on a transition vertex, so the outer ring carries exactly three chips, all on transition vertices, and each cycle carries at most two. Three is odd, so some cycle carries exactly one; firing at that cycle's chip-free transition vertex burns the whole cycle and then leaks one step along the adjacent transition edge, giving three burned transition vertices. Lemma 3.5(b) charges three chips to the centre and three spoke interiors, but the centre has two and the spoke interiors have none.
What is and is not claimed #
baker_subdivision_conjecture_false refutes Baker, Specialization of linear
systems from curves to graphs, Conjecture 3.14(a) at r = 1 and k = 2:
dgon(σ_k(G)) = dgon(G) for all k ≥ 1. Conjecture 3.14(b),
dgon(Γ(G)) = dgon(G), follows from (a) by the source's Theorem 1.5
(dgon(Γ(G)) = min_k dgon(σ_k(G))), which is not formalized here; see
Utilities/Gonality/GonalityTransport.lean for why the invariant is named
regularSubdivisionGonality rather than metricGonality.
An unsubdivided slot has no interior chips #
Chip-free propagation with explicit hypotheses #
The fire runs up a chip-free transition path.
The fire runs down a chip-free transition path.
Three burned transition vertices #
Three burned transition vertices cost three chips on the centre and their three spoke interiors.
The two burning cases of Theorem 3.9 #
The cycle Cᵢ's single chip sits on vᵢ⁺: firing at vᵢ⁻ burns vᵢ⁻,
vᵢ⁺ and vᵢ₊₁⁻.
The cycle Cᵢ's single chip sits on vᵢ⁻: firing at vᵢ⁺ burns vᵢ⁺,
vᵢ⁻ and vᵢ₊₂⁺.
Theorem 3.9, lower half #
The fifteen slot-interior totals, written out.
The parity step of Theorem 3.9: the outer ring's three chips sit on the six transition vertices, one per transition path, so some cycle carries exactly one chip — and then one of its two transition vertices is chip-free.
Theorem 3.9, lower half. Every tricycle graph — every subdivision of the minimal tricycle whose three transition edges are unsubdivided — has divisorial gonality at least six.
Two specifications with the same core and the same lengths #
Two subdivision specifications over the same core with the same slot lengths
present the same graph. (Spec is a structure, so this is not rfl: the two
length functions are only pointwise equal.)
Equations
- One or more equations did not get rendered due to their size.
Instances For
The minimal tricycle and its 2-subdivision #
dgon(T_m) = 6. Theorem 3.9 for the minimal tricycle.
dgon(σ₂(T_m)) = 5. Proposition 3.3 together with Corollary 3.7.
Scaling T_m by two is σ₂(T_m).
Every σ_k(T_m) is a subdivision of the tricycle core, hence connected.
The gap #
min_{k ≥ 1} dgon(σ_k(T_m)) = 5. The upper bound is k = 2
(Proposition 3.3); the lower bound is Corollary 3.7, which holds at every k
— and must, since k ↦ dgon(σ_k(T_m)) is not monotone (dgon(σ₃) = 6).
The tricycle gap. 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 false. Baker, Specialization of linear
systems from curves to graphs, Conjecture 3.14(a) asserts
dgon_r(σ_k(G)) = dgon_r(G) for every connected loopless multigraph G, every
r ≥ 1 and every k ≥ 1. It already fails at r = 1 and k = 2, on the
minimal tricycle.
Conjecture 3.14(b), dgon_r(Γ(G)) = dgon_r(G), follows from (a) through the
source's Theorem 1.5, dgon_r(Γ(G)) = min_k dgon_r(σ_k(G)), which is deliberately
not formalized here — see Utilities/Gonality/GonalityTransport.lean.
The gap at the level of an arbitrary CFGraph #
regularSubdivisionGonality : CFGraph → ℕ builds σ_k on the occurrence
presentation of its argument, which labels vertices and edge occurrences by
arbitrary bijections. Tricycle/RegularSubdivisionBridge.lean
identifies that construction with slot scaling for a unit-length specification,
which lets the whole statement be made without mentioning Spec.
min_{k ≥ 1} dgon(σ_k(T_m)) = 5, with σ_k built on the occurrence
presentation of T_m rather than on the tricycle core.
The tricycle gap, with both sides invariants of the bare graph.
Baker's Conjecture 3.14(a) is false, stated for an arbitrary connected
loopless multigraph and the canonical σ_k construction.
Baker, Specialization of linear systems from curves to graphs,
Conjecture 3.14(a): dgon_r(σ_k(G)) = dgon_r(G) for every connected loopless
multigraph G, every r ≥ 1 and every k ≥ 1. It fails already at r = 1
and k = 2, on the minimal tricycle.