Highlights of the `TreewidthGonality` library #

A public interface, in one file. Every main theorem of this library is restated below as an example whose type is written out in full and whose proof is the real theorem. There is not a single new definition or theorem here.

For a reader. The complete statement of each headline result is visible here, with all of its binders and hypotheses.
For the build. Because each example is checked by the kernel against the real declaration, a change to a statement is detected in this file.

The headline theorem of the library is treewidth ≤ gonality (van Dobben de Bruyn–Gijswijt, arXiv:1407.7055), assembled from two independent halves: the divisor-theoretic bound bramble_order_le_gonality_succ, and Seymour–Thomas bramble/treewidth duality exists_bramble_of_treewidth. Both are unconditional; #print axioms on either reports exactly [propext, Classical.choice, Quot.sound]. The Seymour–Thomas half follows the Bellenbaum–Diestel proof.

The key definitions #

Re-exported here so that the statements below read without qualification.

source

def TreewidthGonality.Highlights.underlyingSimpleGraph (G : CFGraph) :

SimpleGraph G.V

The simple graph underlying a chip-firing multigraph: v and w are adjacent when numEdges G v w > 0. "The treewidth of a multigraph" means the treewidth of this graph — parallel edges do not change it. (Utilities/Foundations/UnderlyingSimpleGraph.lean)

Equations

TreewidthGonality.Highlights.underlyingSimpleGraph = Utilities.underlyingSimpleGraph

Instances For

source

def TreewidthGonality.Highlights.divisorialGonality (G : CFGraph) :

ℕ

Divisorial gonality: the least degree of an effective divisor of rank at least one, as a natural number. (Utilities/Gonality/DivisorialGonality.lean)

Equations

TreewidthGonality.Highlights.divisorialGonality = Utilities.Gonality.divisorialGonality

Instances For

source

def TreewidthGonality.Highlights.Bramble {V : Type u} [DecidableEq V] (H : SimpleGraph V) :

Type u

A bramble of a simple graph: a family of vertex sets, each inducing a connected subgraph, any two of which touch. (TreewidthGonality/Treewidth/Bramble.lean)

Equations