Highlights

This is the repository's auditable, reader-facing statement layer. The definitions used in theorem statements are repeated here in full: they do not alias or invoke the implementation library. Proof bodies, below the statement vocabulary, explicitly cross from these local definitions to the repository's proved API.

The current installments record Brill--Noether existence through genus five, CDPR and its sharp mixed-chain extensions, the tricycle counterexample to invariance of divisorial gonality under regular subdivision, and the treewidth lower bound on divisorial gonality. Further headline theorems can be added one at a time in the same style.

Self-contained statement vocabulary

structure Highlights.CFGraph : Type (u + 1)

A finite, nonempty, loopless undirected multigraph. An undirected edge is stored by either ordering of its endpoints; numEdges below forgets that ordering.

• V : Type u

  The finite nonempty vertex type of the loopless multigraph.

• instDecidableEq : DecidableEq self.V
• instFintype : Fintype self.V
• instNonempty : Nonempty self.V
• edges : Multiset (self.V × self.V)

  The multiset of edges, retaining parallel-edge multiplicities through ordered endpoint pairs.

• loopless (v : self.V) : (v, v) ∉ self.edges

def Highlights.numEdges (G : CFGraph) (v w : G.V) : ℕ

The number of edges between two vertices, counted with multiplicity.

Equations

• Highlights.numEdges G v w = (Multiset.filter (fun (e : G.V × G.V) => e = (v, w) ∨ e = (w, v)) G.edges).card

def Highlights.graphConnected (G : CFGraph) : Prop

A graph is connected when every nontrivial vertex cut has a crossing edge.

Equations

• Highlights.graphConnected G = ∀ (S : Finset G.V), (∃ (v : G.V) (w : G.V), v ∈ S ∧ w ∉ S) → ∃ v ∈ S, ∃ w ∉ S, Highlights.numEdges G v w > 0

def Highlights.genus (G : CFGraph) : ℤ

The genus (cyclomatic number) |E| - |V| + 1.

Equations

• Highlights.genus G = ↑G.edges.card - ↑(Fintype.card G.V) + 1

def Highlights.vertexDegree (G : CFGraph) (v : G.V) : ℤ

The degree (valence) of a vertex.

Equations

• Highlights.vertexDegree G v = ∑ u : G.V, ↑(Highlights.numEdges G v u)

@[reducible, inline]

abbrev Highlights.CFDiv (G : CFGraph) : Type u_1

A divisor is an integer-valued function on the vertices.

Equations

• Highlights.CFDiv G = (G.V → ℤ)

def Highlights.firingVector (G : CFGraph) (v : G.V) : CFDiv G

The principal divisor obtained by firing one vertex once.

Equations

• Highlights.firingVector G v w = if w = v then -Highlights.vertexDegree G v else ↑(Highlights.numEdges G v w)

def Highlights.principalDivisors (G : CFGraph) : AddSubgroup (CFDiv G)

The subgroup generated by all vertex firings.

Equations

• Highlights.principalDivisors G = AddSubgroup.closure (Set.range (Highlights.firingVector G))

def Highlights.linearEquiv (G : CFGraph) (D D' : CFDiv G) : Prop

Two divisors are linearly equivalent when their difference is principal.

Equations

• Highlights.linearEquiv G D D' = (D' - D ∈ Highlights.principalDivisors G)

def Highlights.effective {G : CFGraph} (D : CFDiv G) : Prop

A divisor is effective when it has no negative coefficient.

Equations

• Highlights.effective D = ∀ (v : G.V), D v ≥ 0

def Highlights.Eff (G : CFGraph) : AddSubmonoid (CFDiv G)

The additive monoid of effective divisors.

Equations

• Highlights.Eff G = { carrier := {D : Highlights.CFDiv G | Highlights.effective D}, add_mem' := ⋯, zero_mem' := ⋯ }

def Highlights.winnable (G : CFGraph) (D : CFDiv G) : Prop

A divisor is winnable when it is linearly equivalent to an effective divisor.

Equations

• Highlights.winnable G D = ∃ D' ∈ Highlights.Eff G, Highlights.linearEquiv G D D'

def Highlights.deg {G : CFGraph} : CFDiv G →+ ℤ

The degree of a divisor, i.e. its total number of chips.

Equations

• Highlights.deg = { toFun := fun (D : Highlights.CFDiv G) => ∑ v : G.V, D v, map_zero' := ⋯, map_add' := ⋯ }

def Highlights.effOfDegree (G : CFGraph) (k : ℤ) : Set (CFDiv G)

The effective divisors of a prescribed degree.

Equations

• Highlights.effOfDegree G k = {E : Highlights.CFDiv G | Highlights.effective E ∧ Highlights.deg E = k}

def Highlights.rankGeq (G : CFGraph) (D : CFDiv G) (k : ℤ) : Prop

rankGeq G D k means that removing any effective divisor of degree k from D leaves a winnable divisor.

Equations

• Highlights.rankGeq G D k = ∀ E ∈ Highlights.effOfDegree G k, Highlights.winnable G (D - E)

def Highlights.rankEq (G : CFGraph) (D : CFDiv G) (r : ℤ) : Prop

rankEq G D r means that the Baker--Norine rank of D is exactly r.

Equations

• Highlights.rankEq G D r = (Highlights.rankGeq G D r ∧ ¬Highlights.rankGeq G D (r + 1))

def Highlights.gonalityLeq (G : CFGraph) (k : ℤ) : Prop

gonalityLeq G k means that G has a degree-k divisor of rank at least one. This deliberately states the witness property directly, without introducing a minimum or an infimum.

Equations

• Highlights.gonalityLeq G k = ∃ (D : Highlights.CFDiv G), Highlights.deg D = k ∧ Highlights.rankGeq G D 1

def Highlights.gonalityEq (G : CFGraph) (k : ℤ) : Prop

gonalityEq G k means that degree k supports a rank-one divisor and no smaller degree does. This witness formulation avoids hiding the statement behind an infimum.

Equations

• Highlights.gonalityEq G k = (Highlights.gonalityLeq G k ∧ ∀ d < k, ¬Highlights.gonalityLeq G d)

Brill--Noether generality and twice-marked graphs

def Highlights.oneChip {G : CFGraph} (v : G.V) : CFDiv G

The divisor consisting of one chip at v.

Equations

• Highlights.oneChip v w = if w = v then 1 else 0

def Highlights.brillNoetherNumber (G : CFGraph) (r d : ℤ) : ℤ

The Brill--Noether number rho(g,r,d).

Equations

• Highlights.brillNoetherNumber G r d = Highlights.genus G - (r + 1) * (Highlights.genus G - d + r)

def Highlights.brillNoetherExists (G : CFGraph) (r d : ℤ) : Prop

Existence of a degree-d divisor of rank at least r.

Equations

• Highlights.brillNoetherExists G r d = ∃ (D : Highlights.CFDiv G), Highlights.deg D = d ∧ Highlights.rankGeq G D r

def Highlights.brillNoetherGeneral (G : CFGraph) : Prop

The nonexistence half of Brill--Noether generality: every divisor that exists lies in the range predicted by the Brill--Noether number.

Equations

• Highlights.brillNoetherGeneral G = ∀ (r d : ℤ), 0 ≤ r → Highlights.brillNoetherExists G r d → 0 ≤ Highlights.brillNoetherNumber G r d

structure Highlights.TwiceMarkedGraph : Type 1

A graph with an ordered left and right marked vertex. The graph is packaged existentially so twice-marked graphs with different vertex types can occur in one list.

• graph : CFGraph

  The underlying finite loopless multigraph with two distinguished vertices.

• u : self.graph.V

  The first distinguished vertex, used as the incoming mark when joining a chain.

• v : self.graph.V

  The second distinguished vertex, used as the outgoing mark when joining a chain.

def Highlights.trivialTwiceMarkedGraph : TwiceMarkedGraph

A harmless one-vertex value, used for an empty chain and for malformed path-length data.

Equations

• One or more equations did not get rendered due to their size.

def Highlights.bridgeGlue (G₁ G₂ : TwiceMarkedGraph) : TwiceMarkedGraph

Join two twice-marked graphs by taking their disjoint union and adding one bridge from the right mark of the first to the left mark of the second. The new marks are the two outside marks.

This deliberately uses a bridge rather than identifying the two vertices; it is the most literal finite-graph presentation of a chain.

Equations

• One or more equations did not get rendered due to their size.

def Highlights.glueChain : List TwiceMarkedGraph → TwiceMarkedGraph

Glue a list from left to right. The empty list has the harmless one-vertex value above.

Equations

• Highlights.glueChain [] = Highlights.trivialTwiceMarkedGraph
• Highlights.glueChain (G :: rest) = List.foldl Highlights.bridgeGlue G rest

def Highlights.twiceMarkedCycleLength (m n : ℕ) : Fin 2 → ℕ

The two complementary arc lengths of a twice-marked cycle.

Equations

• Highlights.twiceMarkedCycleLength m n = ![m, n]

@[reducible, inline]

abbrev Highlights.TwiceMarkedCycleVertex (m n : ℕ) : Type

Vertices of the cycle: the two marked endpoints and the disjoint interior vertices of its top and bottom arcs.

Equations

• Highlights.TwiceMarkedCycleVertex m n = (Fin 2 ⊕ (arc : Fin 2) × Fin (Highlights.twiceMarkedCycleLength m n arc - 1))

@[reducible, inline]

abbrev Highlights.TwiceMarkedCycleStep (m n : ℕ) : Type

Unit steps along the two arcs.

Equations

• Highlights.TwiceMarkedCycleStep m n = ((arc : Fin 2) × Fin (Highlights.twiceMarkedCycleLength m n arc))

def Highlights.twiceMarkedCycleStepLeft (m n : ℕ) (step : TwiceMarkedCycleStep m n) : TwiceMarkedCycleVertex m n

Left endpoint of a unit step along a cycle arc.

Equations

• Highlights.twiceMarkedCycleStepLeft m n step = if hzero : ↑step.snd = 0 then Sum.inl 0 else Sum.inr ⟨step.fst, ⟨↑step.snd - 1, ⋯⟩⟩

def Highlights.twiceMarkedCycleStepRight (m n : ℕ) (step : TwiceMarkedCycleStep m n) : TwiceMarkedCycleVertex m n

Right endpoint of a unit step along a cycle arc.

Equations

• Highlights.twiceMarkedCycleStepRight m n step = if hlast : ↑step.snd + 1 = Highlights.twiceMarkedCycleLength m n step.fst then Sum.inl 1 else Sum.inr ⟨step.fst, ⟨↑step.snd, ⋯⟩⟩

def Highlights.twiceMarkedCycle (m n : ℕ) : TwiceMarkedGraph

A cycle marked at the endpoints of two complementary arcs of lengths m and n. If either length is zero, the value is the documented junk graph trivialTwiceMarkedGraph.

Equations

• One or more equations did not get rendered due to their size.

def Highlights.torsionGt (M : TwiceMarkedGraph) (n : ℕ) : Prop

torsionGt M n says that no positive multiple k ≤ n of the two marked points is linearly equivalent. Equivalently, the order of [u-v] in the Jacobian is greater than n (including the infinite-order convention).

Equations

• Highlights.torsionGt M n = ∀ (k : ℕ), 1 ≤ k → k ≤ n → ¬Highlights.linearEquiv M.graph (↑k • Highlights.oneChip M.u) (↑k • Highlights.oneChip M.v)

def Highlights.cdprGeneral (lengths : List (ℕ × ℕ)) : Prop

CDPR genericity for integer cycle lengths. There are at least two loops; all arc lengths are positive, ruling out the junk branch of twiceMarkedCycle; and no two arc lengths have a ratio of positive numerator-plus-denominator at most 2g-2, where g is the number of cycles.

Equations

• One or more equations did not get rendered due to their size.

def Highlights.chainOfCycles (lengths : List (ℕ × ℕ)) : TwiceMarkedGraph

The bridge-chain built from a list of pairs of cycle arc lengths.

Equations

• Highlights.chainOfCycles lengths = Highlights.glueChain (List.map (fun (mn : ℕ × ℕ) => Highlights.twiceMarkedCycle mn.1 mn.2) lengths)

def Highlights.thetaLength (a b c : ℕ) : Fin 3 → ℕ

The three strand lengths, in order.

Equations

• Highlights.thetaLength a b c = ![a, b, c]

@[reducible, inline]

abbrev Highlights.ThetaVertex (a b c : ℕ) : Type

Vertices of Theta a b c: the top and bottom vertices, together with three disjoint sets of a - 1, b - 1, and c - 1 interior vertices.

Equations

• Highlights.ThetaVertex a b c = (Fin 2 ⊕ (strand : Fin 3) × Fin (Highlights.thetaLength a b c strand - 1))

@[reducible, inline]

abbrev Highlights.ThetaStep (a b c : ℕ) : Type

Unit steps along the three strands of Theta a b c.

Equations

• Highlights.ThetaStep a b c = ((strand : Fin 3) × Fin (Highlights.thetaLength a b c strand))

def Highlights.thetaStepLeft (a b c : ℕ) (step : ThetaStep a b c) : ThetaVertex a b c

Left endpoint of one unit step along a theta strand.

Equations

• Highlights.thetaStepLeft a b c step = if hzero : ↑step.snd = 0 then Sum.inl 0 else Sum.inr ⟨step.fst, ⟨↑step.snd - 1, ⋯⟩⟩

def Highlights.thetaStepRight (a b c : ℕ) (step : ThetaStep a b c) : ThetaVertex a b c

Right endpoint of one unit step along a theta strand.

Equations

• Highlights.thetaStepRight a b c step = if hlast : ↑step.snd + 1 = Highlights.thetaLength a b c step.fst then Sum.inl 1 else Sum.inr ⟨step.fst, ⟨↑step.snd, ⋯⟩⟩

def Highlights.Theta (a b c : ℕ) : CFGraph

Theta a b c is the graph made from three internally disjoint paths of lengths a, b, and c joining a common top vertex to a common bottom vertex.

Equations

• One or more equations did not get rendered due to their size.

def Highlights.TMTheta (a b c u v : ℕ) : TwiceMarkedGraph

TMTheta a b c u v marks position u on the first (a-) strand and position v on the third (c-) strand. Invalid positions receive the same documented junk value used by twiceMarkedCycle; evenlyMarkedK below contains the guards used by every theorem.

Equations

• One or more equations did not get rendered due to their size.

def Highlights.evenlyMarkedK (a b c u v k : ℕ) : Prop

The numerical condition that TMTheta a b c u v is evenly marked and has torsion order exactly k. The equal-ratio condition u / a = v / c is written without division as u * c = v * a; exactness of the order is recorded on both marked strands.

Equations

• Highlights.evenlyMarkedK a b c u v k = (0 < a ∧ 0 < b ∧ 0 < c ∧ 1 ≤ u ∧ u < a ∧ 1 ≤ v ∧ v < c ∧ u * c = v * a ∧ a / u.gcd a = k ∧ c / v.gcd c = k)

inductive Highlights.CycleThetaFactor : Type

The two kinds of factor admitted in the mixed-chain highlight.

• cycle (m n : ℕ) : CycleThetaFactor
• theta (a b c u v k : ℕ) : CycleThetaFactor

def Highlights.CycleThetaFactor.markedGraph : CycleThetaFactor → TwiceMarkedGraph

Forget the readable factor tag and retain its twice-marked graph.

Equations

• (Highlights.CycleThetaFactor.cycle m n).markedGraph = Highlights.twiceMarkedCycle m n
• (Highlights.CycleThetaFactor.theta a b c u v _k).markedGraph = Highlights.TMTheta a b c u v

def Highlights.CycleThetaFactor.factorGenus : CycleThetaFactor → ℕ

The genus contribution of a factor: one for a cycle and two for a theta graph.

Equations

• (Highlights.CycleThetaFactor.cycle m n).factorGenus = 1
• (Highlights.CycleThetaFactor.theta a b c u v _k).factorGenus = 2

def Highlights.CycleThetaFactor.period : CycleThetaFactor → ℕ

The exact torsion period supplied by the numerical factor data.

Equations

• (Highlights.CycleThetaFactor.cycle m n).period = (m + n) / m.gcd n
• (Highlights.CycleThetaFactor.theta a b c u v _k).period = _k

def Highlights.CycleThetaFactor.totalGenus (factors : List CycleThetaFactor) : ℕ

The total genus contributed by a list of cycle/theta factors.

Equations

• Highlights.CycleThetaFactor.totalGenus factors = (List.map Highlights.CycleThetaFactor.factorGenus factors).sum

def Highlights.mixedChainTorsionBudget (factors : List CycleThetaFactor) : Prop

Corollary 6.16's sharp torsion budget for a mixed chain: the exact period of a factor exceeds the smaller of the genera accumulated on its two sides, counting the factor on both sides.

Equations

• One or more equations did not get rendered due to their size.

def Highlights.mixedChainLeftTorsionBudget (factors : List CycleThetaFactor) : Prop

The one-sided torsion budget for marked generality at the left endpoint of a mixed chain. At factor i, its period exceeds the total genus of the suffix beginning there.

Equations

• Highlights.mixedChainLeftTorsionBudget factors = ∀ (i : ℕ) (hi : i < factors.length), Highlights.CycleThetaFactor.totalGenus (List.drop i factors) < (factors.get ⟨i, hi⟩).period

def Highlights.chainOfCyclesAndThetas (factors : List CycleThetaFactor) : TwiceMarkedGraph

The twice-marked bridge-chain represented by mixed readable factors.

Equations

• Highlights.chainOfCyclesAndThetas factors = Highlights.glueChain (List.map Highlights.CycleThetaFactor.markedGraph factors)

A canonical, reader-facing regular subdivision

Every occurrence of an edge gets its own slot, so parallel edges remain distinct. In the nth regular subdivision that slot is replaced by a path of n unit edges. Its n - 1 new vertices remember the edge occurrence and their position along that path. The implementation below spells these counts as n * 1 only to make the later bridge to “scale a unit edge by n” exact; this reduces definitionally to n.

noncomputable def Highlights.subdivisionEdgeEquiv (G : CFGraph) : G.edges.ToType ≃ Fin G.edges.card

A canonical enumeration of the occurrences in the edge multiset. The subtype G.edges distinguishes repeated copies of the same endpoint pair.

Equations

• Highlights.subdivisionEdgeEquiv G = ⋯.mp (Fintype.equivFin G.edges.ToType)

noncomputable def Highlights.subdivisionEdgeAt (G : CFGraph) (edge : Fin G.edges.card) : G.V × G.V

The endpoint pair occupying a canonical edge-occurrence slot.

Equations

• Highlights.subdivisionEdgeAt G edge = ((Highlights.subdivisionEdgeEquiv G).symm edge).fst

@[reducible, inline]

abbrev Highlights.SubdivisionVertex (G : CFGraph) (n : ℕ) : Type

Vertices in the nth regular subdivision: relabelled original vertices, together with an edge occurrence and an interior position 0, ..., n - 2. The harmless relabelling by Fin makes the construction canonical.

Equations

• Highlights.SubdivisionVertex G n = (Fin (Fintype.card G.V) ⊕ (_ : Fin G.edges.card) × Fin (n * 1 - 1))

@[reducible, inline]

abbrev Highlights.SubdivisionStep (G : CFGraph) (n : ℕ) : Type

Unit steps in the subdivided paths.

Equations

• Highlights.SubdivisionStep G n = ((_ : Fin G.edges.card) × Fin (n * 1))

noncomputable def Highlights.subdivisionStepLeft (G : CFGraph) (n : ℕ) (edge : Fin G.edges.card) (offset : Fin (n * 1)) : SubdivisionVertex G n

The left endpoint of one unit step in a subdivided edge.

Equations

• Highlights.subdivisionStepLeft G n edge offset = if hzero : ↑offset = 0 then Sum.inl ((Fintype.equivFin G.V) (Highlights.subdivisionEdgeAt G edge).1) else Sum.inr ⟨edge, ⟨↑offset - 1, ⋯⟩⟩

noncomputable def Highlights.subdivisionStepRight (G : CFGraph) (n : ℕ) (edge : Fin G.edges.card) (offset : Fin (n * 1)) : SubdivisionVertex G n

The right endpoint of one unit step in a subdivided edge.

Equations

• Highlights.subdivisionStepRight G n edge offset = if hlast : ↑offset + 1 = n * 1 then Sum.inl ((Fintype.equivFin G.V) (Highlights.subdivisionEdgeAt G edge).2) else Sum.inr ⟨edge, ⟨↑offset, ⋯⟩⟩

noncomputable def Highlights.regularSubdivision (G : CFGraph) (n : ℕ) (_hn : 0 < n) : CFGraph

The nth regular subdivision of G: every edge occurrence is replaced by a path of exactly n edges.

Equations

• One or more equations did not get rendered due to their size.

The minimal tricycle

Number the centre 0, the three minus vertices 1, 3, 5, and the three plus vertices 2, 4, 6. There are six centre spokes; two parallel edges join each minus/plus pair; and three transition edges join each plus vertex to the next minus vertex around the ring.

def Highlights.tricycle : CFGraph

The minimal tricycle, displayed directly as its seven vertices and fifteen edges. The repeated pairs are the three doubled minus/plus edges.

Equations

• One or more equations did not get rendered due to their size.

Tree decompositions and treewidth

def Highlights.underlyingSimpleGraph (G : CFGraph) : SimpleGraph G.V

The simple graph underlying a multigraph: two vertices are adjacent when at least one edge occurrence joins them. Parallel edges therefore do not affect treewidth.

Equations

• Highlights.underlyingSimpleGraph G = { Adj := fun (v w : G.V) => Highlights.numEdges G v w > 0, symm := ⋯, loopless := ⋯ }

structure Highlights.TreeDecomposition {V : Type u} (H : SimpleGraph V) : Type (max 1 u)

A tree decomposition of a simple graph consists of a finite tree and a bag of graph vertices at each tree node. Every vertex and edge is covered, and the bags containing any fixed vertex form a connected subtree.

• Node : Type

  Nodes of the decomposition tree.

• nodeFintype : Fintype self.Node
• nodeDecidableEq : DecidableEq self.Node
• tree : SimpleGraph self.Node

  The finite decomposition tree.

• isTree : self.tree.IsTree

  The decomposition graph is connected and acyclic.

• bag : self.Node → Finset V

  The bag at each tree node.

• cover_vertex (v : V) : ∃ (t : self.Node), v ∈ self.bag t

  Every graph vertex occurs in a bag.

• cover_edge (v w : V) : H.Adj v w → ∃ (t : self.Node), v ∈ self.bag t ∧ w ∈ self.bag t

  The endpoints of every graph edge occur together in a bag.

• coherent (v : V) : (SimpleGraph.induce {t : self.Node | v ∈ self.bag t} self.tree).Connected

  The nodes whose bags contain a fixed vertex form a connected subtree.

def Highlights.TreeDecomposition.width {V : Type u} {H : SimpleGraph V} (D : TreeDecomposition H) : ℕ

The width of a tree decomposition: one less than its largest bag size.

Equations

• D.width = (Finset.univ.sup fun (t : D.Node) => (D.bag t).card) - 1

def Highlights.treewidthSet {V : Type u} (H : SimpleGraph V) : Set ℕ

Widths realized by tree decompositions of H.

Equations

• Highlights.treewidthSet H = {w : ℕ | ∃ (D : Highlights.TreeDecomposition H), D.width = w}

noncomputable def Highlights.treewidth {V : Type u} (H : SimpleGraph V) : ℕ

Treewidth is the least width of a tree decomposition.

Equations

• Highlights.treewidth H = sInf (Highlights.treewidthSet H)

Proof bridges

Everything above this point is statement vocabulary. The following public conversion is where the file deliberately crosses into the implementation library.

def Highlights.libraryGraph (G : CFGraph) : _root_.CFGraph

View a public graph in the chip-firing implementation model.

Equations

• Highlights.libraryGraph G = { V := G.V, instDecidableEq := G.instDecidableEq, instFintype := G.instFintype, instNonempty := ⋯, edges := G.edges, loopless := ⋯ }

def Highlights.libraryMarkedGraph (M : TwiceMarkedGraph) : Utilities.MarkedGraph

Cross a reader-facing twice-marked graph into the library's marked-graph bundle without changing any graph data.

Equations

• Highlights.libraryMarkedGraph M = { graph := Highlights.libraryGraph M.graph, left := M.u, right := M.v }

def Highlights.ofLibraryGraph (G : _root_.CFGraph) : CFGraph

Convert a library graph to the auditable statement vocabulary.

Equations

• Highlights.ofLibraryGraph G = { V := G.V, instDecidableEq := G.instDecidableEq, instFintype := G.instFintype, instNonempty := ⋯, edges := G.edges, loopless := ⋯ }

@[simp]

theorem Highlights.libraryGraph_ofLibraryGraph (G : _root_.CFGraph) : libraryGraph (ofLibraryGraph G) = G

@[simp]

theorem Highlights.ofLibraryGraph_libraryGraph (G : CFGraph) : ofLibraryGraph (libraryGraph G) = G

theorem Highlights.brill_noether_general_library_iff (G : CFGraph) : brillNoetherGeneral G ↔ Bananas.BrillNoetherGeneral (libraryGraph G)

The copied local definition of Brill--Noether generality agrees with the library predicate after crossing the graph boundary.

Explicit cycle factors versus the Bananas implementation

Explicit theta factors versus the Bananas implementation

theorem Highlights.libraryGraph_regularSubdivision (G : CFGraph) (n : ℕ) (hn : 0 < n) : libraryGraph (regularSubdivision G n hn) = Utilities.Gonality.regularSubdivision (libraryGraph G) n hn

The readable construction above agrees exactly with the occurrence-safe regular subdivision used by the library.

theorem Highlights.gonality_leq_library_iff (G : CFGraph) (k : ℤ) : gonalityLeq G k ↔ _root_.gonalityLeq (libraryGraph G) k

The local witness-based gonality predicate is exactly the library's predicate after crossing the graph-structure boundary.

def Highlights.libraryTreeDecomposition {V : Type u} {H : SimpleGraph V} (D : TreeDecomposition H) : Utilities.Treewidth.TreeDecomposition H

Convert a local tree decomposition to the implementation structure.

Equations

• One or more equations did not get rendered due to their size.

theorem Highlights.treewidthSet_eq_library {V : Type u} (H : SimpleGraph V) : treewidthSet H = Utilities.Treewidth.widthSet H

The local and implementation definitions realize exactly the same widths.

theorem Highlights.treewidth_eq_library {V : Type u} (H : SimpleGraph V) : treewidth H = Utilities.Treewidth.treewidth H

Consequently the copied reader-facing definition of treewidth agrees with the load-bearing implementation definition.

theorem Highlights.underlyingSimpleGraph_eq_library (G : CFGraph) : underlyingSimpleGraph G = Utilities.underlyingSimpleGraph (libraryGraph G)

The locally defined underlying simple graph agrees with the library's.

Brill--Noether existence through genus five

theorem Highlights.brill_noether_existence_through_five (G : CFGraph) (h_connected : graphConnected G) (g r d : ℤ) (h_genus : genus G = g) (h_genus_le_five : g ≤ 5) (h_brill_noether : (r + 1) * (g - d + r) ≤ g) : ∃ (D : CFDiv G), deg D = d ∧ rankGeq G D r

Every connected finite graph of genus at most five satisfies Brill--Noether existence.

Chains of loops: the CDPR theorem and its sharp extensions

theorem Highlights.cdpr_marked_no_high_multiplicity (lengths : List (ℕ × ℕ)) (h_general : cdprGeneral lengths) (D : CFDiv (chainOfCycles lengths).graph) (r d : ℤ) (h_rank_nonnegative : 0 ≤ r) (h_rank_below_genus : r < genus (chainOfCycles lengths).graph) (h_degree : deg D = d) (h_rank : rankGeq (chainOfCycles lengths).graph D r) (h_rho : 0 ≤ brillNoetherNumber (chainOfCycles lengths).graph r d) : ¬rankGeq (chainOfCycles lengths).graph (D - (r + brillNoetherNumber (chainOfCycles lengths).graph r d + 1) • oneChip (chainOfCycles lengths).u) 0

Marked CDPR theorem. At the left endpoint of a generic chain of g loops, a degree-d, rank-at-least-r divisor cannot retain rank zero after removing r + rho + 1 chips.

theorem Highlights.cdpr_chain_brill_noether_general (lengths : List (ℕ × ℕ)) (h_general : cdprGeneral lengths) : brillNoetherGeneral (chainOfCycles lengths).graph

CDPR Theorem 1.1(1), discrete form. A generic chain of cycles is Brill--Noether general in the nonexistence sense.

theorem Highlights.cycle_chain_brill_noether_general_of_torsion (lengths : List (ℕ × ℕ)) (h_positive : ∀ mn ∈ lengths, 0 < mn.1 ∧ 0 < mn.2) (h_torsion : ∀ (i : ℕ) (hi : i < lengths.length), torsionGt (twiceMarkedCycle (lengths.get ⟨i, hi⟩).1 (lengths.get ⟨i, hi⟩).2) (min (i + 1) (lengths.length - i))) : brillNoetherGeneral (chainOfCycles lengths).graph

The sharp cycle-chain form behind CDPR. Numbering the g cycles from 1 to g, the torsion order of cycle i need only exceed min(i, g + 1 - i).

theorem Highlights.cycle_theta_chain_marked_no_high_multiplicity (factors : List CycleThetaFactor) (h_cycles_positive : ∀ (m n : ℕ), CycleThetaFactor.cycle m n ∈ factors → 0 < m ∧ 0 < n) (h_thetas_evenly_marked : ∀ (a b c u v k : ℕ), CycleThetaFactor.theta a b c u v k ∈ factors → evenlyMarkedK a b c u v k) (h_torsion : mixedChainLeftTorsionBudget factors) (D : CFDiv (chainOfCyclesAndThetas factors).graph) (r d : ℤ) (h_rank_nonnegative : 0 ≤ r) (h_rank_below_genus : r < genus (chainOfCyclesAndThetas factors).graph) (h_degree : deg D = d) (h_rank : rankGeq (chainOfCyclesAndThetas factors).graph D r) (h_rho : 0 ≤ brillNoetherNumber (chainOfCyclesAndThetas factors).graph r d) : ¬rankGeq (chainOfCyclesAndThetas factors).graph (D - (r + brillNoetherNumber (chainOfCyclesAndThetas factors).graph r d + 1) • oneChip (chainOfCyclesAndThetas factors).u) 0

Marked mixed cycle/theta chain theorem. Under the sharp one-sided torsion budget, a degree-d, rank-at-least-r divisor cannot retain rank zero after removing r + rho + 1 chips at the left endpoint of the chain.

theorem Highlights.cycle_theta_chain_brill_noether_general (factors : List CycleThetaFactor) (h_cycles_positive : ∀ (m n : ℕ), CycleThetaFactor.cycle m n ∈ factors → 0 < m ∧ 0 < n) (h_thetas_evenly_marked : ∀ (a b c u v k : ℕ), CycleThetaFactor.theta a b c u v k ∈ factors → evenlyMarkedK a b c u v k) (h_torsion : mixedChainTorsionBudget factors) : brillNoetherGeneral (chainOfCyclesAndThetas factors).graph

Mixed cycle/theta chain theorem. A chain whose factors are cycles or evenly marked theta graphs is Brill--Noether general whenever every cycle is nondegenerate and each factor satisfies the sharp minimum genus/torsion budget. This is the existential/unmarked conclusion of Corollary 6.16.

Exact gonality of common-torsion chains

theorem Highlights.cycle_theta_chain_gonality_eq_common_torsion (factors : List CycleThetaFactor) (k : ℕ) (h_nonempty : factors ≠ []) (h_cycles_positive : ∀ (m n : ℕ), CycleThetaFactor.cycle m n ∈ factors → 0 < m ∧ 0 < n) (h_thetas_evenly_marked : ∀ (a b c u v period : ℕ), CycleThetaFactor.theta a b c u v period ∈ factors → evenlyMarkedK a b c u v period) (h_common_torsion : ∀ F ∈ factors, F.period = k) (h_small : k ≤ (CycleThetaFactor.totalGenus factors + 3) / 2) : gonalityEq (chainOfCyclesAndThetas factors).graph ↑k

Exact gonality of a common-torsion cycle/theta chain. If every factor has the same torsion order k, then the bridge-chain has gonality exactly k whenever k is at most the generic gonality floor((g+3)/2) of its total genus g.

The theta factors are allowed because the proof uses the common k-general-transmission package, not a factorwise gonality assertion.

theorem Highlights.exists_graph_of_genus_and_gonality (g k : ℕ) (hk : 2 ≤ k) (hkg : k ≤ (g + 3) / 2) : ∃ (G : CFGraph), graphConnected G ∧ genus G = ↑g ∧ gonalityEq G ↑k

Every gonality between two and the generic gonality occurs. More precisely, for every genus g and 2 ≤ k ≤ floor((g+3)/2) = ceil(g/2)+1, there is a connected finite graph of genus g and divisorial gonality exactly k.

Divisorial gonality can drop under regular subdivision

theorem Highlights.gonality_drops_under_regular_subdivision : ∃ (G : CFGraph) (k : ℤ) (n : ℕ) (hn : 0 < n), graphConnected G ∧ gonalityLeq (regularSubdivision G n hn) k ∧ ¬gonalityLeq G k

There is a connected graph with no degree-k, rank-one divisor, although one of its regular subdivisions does have such a divisor. The witness is the minimal tricycle, with k = 5 and subdivision factor n = 2.

This is the direction that yields the divisorial/metric gonality gap: the minimal tricycle has divisorial gonality six, while its second regular subdivision has divisorial gonality five.

Treewidth is at most divisorial gonality

theorem Highlights.treewidth_le_gonality (G : CFGraph) (h_connected : graphConnected G) (k : ℕ) (h_gonality : gonalityLeq G ↑k) : treewidth (underlyingSimpleGraph G) ≤ k

Treewidth is at most divisorial gonality (van Dobben de Bruyn--Gijswijt). In witness form: on a connected graph, any degree-k divisor of rank at least one bounds the treewidth by k.