Burning along a subdivided slot #
The burned-set layer of Utilities/Gonality/BurnedSet.lean is stated for an
arbitrary CFGraph. On a subdivision the fire propagates along slots, and the
moves used over and over by van Dobben de Bruyn–Smit–van der Wegen's §3 are:
- chip-free stretches burn (
mem_burned_slotVertex_of_chipFree_upand its downward twin) — from a burned position the fire runs to the end of a chip-free stretch of the slot; - a burned/unburned split costs a chip (
exists_chip_up,exists_chip_down) — the first unburned vertex past the fire front is adjacent to a burned one, so it can afford that edge, so it carries a chip; - cycle blocking (
two_le_chips_of_cycle) — two distinct slots with the same endpoints form a cycle; if one endpoint burns and the other does not, the cycle carries at least two chips.
The cycle lemma is stated via two internally disjoint arcs rather than via
distinct interior vertices, which is what makes it cover the banana case (both
slots of length one, so the cycle has only two vertices). There the two
witnesses coincide at the unburned endpoint, whose two edges to the burned
endpoint are parallel, and the edge multiplicity supplies the second chip
(two_le_num_edges_of_parallel_unit). Getting this case right is what makes
the minimal tricycle T_m itself tractable, not merely its simple refinements.
Numerical slot positions #
spec.slotVertex e k is the vertex at position k along slot e, clamped to
the slot so that no proof obligation rides along. Position 0 is the core
tail, position spec.length e the core head, and the positions strictly
between are the slot interior. Statements carry explicit
k ≤ spec.length e hypotheses wherever clamping would otherwise silently
change the meaning.
Two distinct chipped vertices of a set carry at least two chips between them, when the divisor is effective elsewhere.
Two distinct burned neighbours of an unburned vertex cost it two chips.
Numerical positions along a slot #
The vertex at numerical position k along slot e, clamped to the slot.
Equations
- spec.slotVertex edge k = spec.pathVertex edge ⟨min k (spec.length edge), ⋯⟩
Instances For
The vertices of the closed subdivided slot edge.
Equations
- spec.slotClosed edge = Finset.image (spec.slotVertex edge) (Finset.range (spec.length edge + 1))
Instances For
Distinct positions in one slot are distinct vertices.
Parallel unit slots double an edge multiplicity. This is the ingredient
that makes the banana case of two_le_chips_of_cycle work.
Chips, counted slot by slot #
Every chip count in the tricycle argument is a linear combination of the n
core-vertex values and the p slot-interior totals, so the bookkeeping of
Lemma 3.6 never needs a Finset union. This is the mitigation of blueprint
risk R1, one step further than the blueprint's own suggestion: not merely a
disjoint partition, but a coordinate system.
The chips on the interior of slot edge.
Equations
- sp.slotInteriorChips D edge = ∑ j : Fin (sp.length edge - 1), D (sp.interiorVertex edge j)
Instances For
The coordinate system. Total degree splits as the core-vertex values plus the slot-interior totals.
Chip-free stretches burn #
The fire runs up a chip-free stretch of a slot.
The fire runs down a chip-free stretch of a slot.
A burned/unburned split costs a chip #
Between a burned position and a later unburned one there is a boundary: an unburned position whose predecessor is burned.
The downward boundary.
Going up: a burned/unburned split costs a chip.
Going down: a burned/unburned split costs a chip.
Cycle blocking #
Cycle blocking, tail burned. Two distinct slots with the same endpoints
form a cycle. If the common tail is burned and the common head is not, the
cycle carries at least two chips — counted in the slot coordinate system, so
the statement is a linear inequality ready for omega.
The coincidence branch — both boundary witnesses landing on the unburned head —
is exactly the banana case (length e₁ = length e₂ = 1), and is where the
parallel-edge multiplicity supplies the second chip.
Cycle blocking, head burned. The mirror image of
two_le_chips_of_cycle_tail_burned.