Lemma 3.6 and Corollary 3.7 #
Van Dobben de Bruyn–Smit–van der Wegen, Lemma 3.6: on any subdivision H of
the minimal tricycle, a positive-rank v₀-reduced divisor of degree at most 5
carries exactly two chips on v₀ and exactly one chip on each transition path.
Corollary 3.7, dgon(H) ≥ 5, is then immediate, and holds for every length
vector — which is what makes the left-hand side of the tricycle gap a minimum
over all σ_k rather than a bound at one k.
How the bookkeeping is kept linear #
The source's regions Cᵢ and its closed transition paths overlap. To keep the
chip counting explicit, every count is expressed in the slot coordinate system of
Utilities/Subdivision/SpecBurning.lean — the seven core-vertex values
D (coreVertex v) and the fifteen slot-interior totals slotInteriorChips D e.
Each geometric conclusion is then a linear inequality in those twenty-two
integers, the degree identity is one more, and linarith finishes. No Finset
union, no inclusion–exclusion.
Aggregates #
The chips on the closed transition path i, from vᵢ⁺ to vᵢ₊₁⁻.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The chips on the cycle Cᵢ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The chips on the interiors of the two spokes meeting Cᵢ.
Equations
- Utilities.Tricycle.spokePairChips spec D i = spec.slotInteriorChips D (Utilities.Tricycle.spokeMinus i) + spec.slotInteriorChips D (Utilities.Tricycle.spokePlus i)
Instances For
Transporting the slot dictionary to an arbitrary subdivision #
Cycle blocking on the tricycle #
If vᵢ⁻ burns and vᵢ⁺ does not, the cycle Cᵢ carries two chips.
If vᵢ⁺ burns and vᵢ⁻ does not, the cycle Cᵢ carries two chips.
Chips on a transition path from a burned/unburned split #
The fire enters transition path i at vᵢ⁺ and is stopped before
vᵢ₊₁⁻: the path carries a chip strictly past vᵢ⁺.
The fire enters transition path i at vᵢ₊₁⁻ and is stopped before
vᵢ⁺.
A chip-free transition path conducts the fire from vᵢ⁺ to vᵢ₊₁⁻.
Evaluating the slot dictionary at concrete indices #
The degree identity in slot coordinates #
Total degree, written out in the twenty-two slot coordinates.
The burned-transition-vertex indicator #
1 if the transition vertex v is burned, 0 otherwise.
Equations
- Utilities.Tricycle.burnedInd spec D w v = if spec.coreVertex v ∈ Utilities.Gonality.burned spec.graph D w then 1 else 0
Instances For
Lemma 3.5(b) in slot coordinates #
The two half-counts of Lemma 3.6's first paragraph #
Forward half-count. If vⱼ⁻ is burned, then Cⱼ together with the
closed transition path leaving vⱼ⁺ carries three, counting each burned
transition vertex in it as one.
Backward half-count. If vⱼ⁺ is burned, then Cⱼ together with the
closed transition path entering vⱼ⁻ carries three, counting each burned
transition vertex in it as one.
Lemma 3.6, first paragraph: every transition path carries a chip #
Lemma 3.6, second paragraph: two chips on the centre #
A cycle with at most one chip is entirely burned by the fire started at one of its own chip-free transition vertices, so both of its spokes' transition vertices are burned, and Lemma 3.5(b) charges two chips to the centre and those two spokes.
The disjunctive form fed to the eight-way case split below.
Lemma 3.6 #
Lemma 3.6. On any subdivision of the minimal tricycle, a positive-rank
v₀-reduced divisor of degree at most five has exactly two chips on v₀ and
exactly one chip on each of the three transition paths.
Corollary 3.7 #
Corollary 3.7. Every subdivision of the minimal tricycle has
divisorial gonality at least five — for every length vector, hence for every
σ_k. This is what makes the left-hand side of the tricycle gap a minimum
rather than a bound at one k.