Documentation

LeanPool.BrillNoetherGraphs.Tricycle.HelperLemma

Lemma 3.5 of van Dobben de Bruyn–Smit–van der Wegen #

Part (a) is proved in full generality in Utilities/Gonality/BurnedSet.lean (not_mem_burned_of_qReduced): a positive-rank q-reduced divisor's own base point is never burned by a fire started at a chip-free vertex.

Part (b) is the counting half, here specialised to the spokes of the tricycle core:

if I is a set of spokes whose transition vertices are all burned, then {v₀} ∪ ⋃_{i ∈ I} (interior of spoke i) carries at least |I| chips.

The split is the source's own I = I₀ ⊔ I₁. For i ∈ I₀ the first vertex up the spoke is burned; those vertices are distinct across spokes, so v₀ — which is not burned — pays for all of them at once, giving |I₀| ≤ D(v₀). For i ∈ I₁ the first vertex up the spoke is unburned while the far end is burned, so the slot has a burned/unburned split and therefore a chip in its interior.

Indexing the six spokes #

source
def Utilities.Tricycle.spokeOf :
Fin 6 → Fin 15

The six spoke slots, indexed by Fin 6.

Equations
Instances For
    source
    def Utilities.Tricycle.transitionOf :
    Fin 6 → Fin 7

    The transition vertex at the far end of spoke i.

    Equations
    Instances For
      source
      theorem Utilities.Tricycle.spokeOf_injective :
      Function.Injective spokeOf
      source
      theorem Utilities.Tricycle.transitionOf_injective :
      Function.Injective transitionOf
      source
      theorem Utilities.Tricycle.tricycleCore_spoke_tail (i : Fin 6) :
      tricycleCore.tail (spokeOf i) = centre
      source
      theorem Utilities.Tricycle.tricycleCore_spoke_head (i : Fin 6) :
      tricycleCore.head (spokeOf i) = transitionOf i

      Lemma 3.5(b) #

      source
      theorem Utilities.Tricycle.spoke_tail {spec : Certificate.SubdivisionGraph.Spec 7 15} (hcore : spec.core = tricycleCore) (i : Fin 6) :
      spec.core.tail (spokeOf i) = centre
      source
      theorem Utilities.Tricycle.spoke_head {spec : Certificate.SubdivisionGraph.Spec 7 15} (hcore : spec.core = tricycleCore) (i : Fin 6) :
      spec.core.head (spokeOf i) = transitionOf i
      source
      def Utilities.Tricycle.spokeStep (spec : Certificate.SubdivisionGraph.Spec 7 15) (i : Fin 6) :
      spec.Vertex

      The first vertex up spoke i from the centre.

      Equations
      Instances For
        source
        theorem Utilities.Tricycle.spokeStep_of_length_one {spec : Certificate.SubdivisionGraph.Spec 7 15} (hcore : spec.core = tricycleCore) {i : Fin 6} (h : spec.length (spokeOf i) = 1) :
        spokeStep spec i = spec.coreVertex (transitionOf i)
        source
        theorem Utilities.Tricycle.num_edges_centre_spokeStep {spec : Certificate.SubdivisionGraph.Spec 7 15} (hcore : spec.core = tricycleCore) (i : Fin 6) :
        0 < numEdges spec.graph (spec.coreVertex centre) (spokeStep spec i)

        The centre is adjacent to the first vertex up each spoke.

        source
        theorem Utilities.Tricycle.spokeStep_injective {spec : Certificate.SubdivisionGraph.Spec 7 15} (hcore : spec.core = tricycleCore) :
        Function.Injective (spokeStep spec)

        The six first-steps are distinct vertices.

        source
        theorem Utilities.Tricycle.helper_lemma_b {spec : Certificate.SubdivisionGraph.Spec 7 15} (hcore : spec.core = tricycleCore) {D : CFDiv spec.graph} (hEff : effective D) (hred : qReduced spec.graph (spec.coreVertex centre) D) (hrank : rank spec.graph D ≥ 1) {w : spec.Vertex} (hw : D w = 0) (I : Finset (Fin 6)) (hI : ∀ i ∈ I, spec.coreVertex (transitionOf i) ∈ Gonality.burned spec.graph D w) :
        ↑I.card ≤ D (spec.coreVertex centre) + ∑ i ∈ I, spec.slotInteriorChips D (spokeOf i)

        Lemma 3.5(b). A set of spokes whose transition vertices are all burned costs its cardinality in chips, counted on the centre and the spoke interiors.