Standalone graph and banana vocabulary

Basic graph, divisor, and banana path data used by the paper-facing statements. These declarations keep their independent TMB meanings and storage conventions.

Standalone mathematical vocabulary

The declarations in this section deliberately use only Mathlib. They give the reader-facing meanings of the graph, divisor, banana, marking, and transmission notation appearing below; none aliases the implementation library. Everything lives in the namespace TMB, which no library declaration inhabits, so that a solution file importing the implementation library can repeat this block verbatim without any name collision.

The definitions are written to follow the implementation library's own definitions as closely as possible (so that a solution can bridge them by unfolding), but they are independent declarations. Small proof fields needed to construct structures (for example, the additivity fields of deg) are ordinary definitional well-formedness proofs written with deterministic tactics, not solutions to any of the paper's theorem statements.

Graphs and divisors

structure TMB.CFGraph : Type (u + 1)

A finite, nonempty, loopless undirected multigraph. Each edge occurrence is stored once, using either ordering of its endpoints.

• 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 unoriented edge occurrences, each stored once as an ordered endpoint pair; repeated pairs represent parallel edges.

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

def TMB.numEdges (G : CFGraph) (x y : G.V) : ℕ

Number of edge occurrences joining two vertices.

Equations

• TMB.numEdges G x y = (Multiset.filter (fun (e : G.V × G.V) => e = (x, y) ∨ e = (y, x)) G.edges).card

def TMB.graphConnected (G : CFGraph) : Prop

Connectivity in cut form.

Equations

• TMB.graphConnected G = ∀ (S : Finset G.V), (∃ (x : G.V) (y : G.V), x ∈ S ∧ y ∉ S) → ∃ x ∈ S, ∃ y ∉ S, TMB.numEdges G x y > 0

def TMB.genus (G : CFGraph) : ℤ

Cyclomatic genus |E| - |V| + 1.

Equations

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

def TMB.vertexDegree (G : CFGraph) (x : G.V) : ℤ

Valence of a vertex.

Equations

• TMB.vertexDegree G x = ∑ y : G.V, ↑(TMB.numEdges G x y)

@[reducible, inline]

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

An integral divisor on a graph.

Equations

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

def TMB.oneChip {G : CFGraph} (x : G.V) : CFDiv G

One chip at x.

Equations

• TMB.oneChip x y = if y = x then 1 else 0

def TMB.outdegreeSet (G : CFGraph) (S : Finset G.V) (x : G.V) : ℤ

Edges leaving x towards the complement of S, with multiplicity.

Equations

• TMB.outdegreeSet G S x = ∑ y ∈ Finset.univ \ S, ↑(TMB.numEdges G x y)

def TMB.firingVector (G : CFGraph) (x : G.V) : CFDiv G

The principal divisor obtained by firing x once.

Equations

• TMB.firingVector G x y = if y = x then -TMB.vertexDegree G x else ↑(TMB.numEdges G x y)

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

The subgroup generated by vertex firings.

Equations

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

def TMB.linearEquiv (G : CFGraph) (D E : CFDiv G) : Prop

Linear equivalence of divisors.

Equations

• TMB.linearEquiv G D E = (E - D ∈ TMB.principalDivisors G)

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

An effective divisor has nonnegative coefficients.

Equations

• TMB.effective D = ∀ (x : G.V), D x ≥ 0

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

Effective divisors as an additive submonoid.

Equations

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

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

A divisor is winnable if its class has an effective representative.

Equations

• TMB.winnable G D = ∃ E ∈ TMB.Eff G, TMB.linearEquiv G D E

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

Divisor degree. The short proofs certify that summation is additive.

Equations

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

def TMB.effOfDegree (G : CFGraph) (d : ℤ) : Set (CFDiv G)

Effective divisors of a prescribed degree.

Equations

• TMB.effOfDegree G d = {E : TMB.CFDiv G | TMB.effective E ∧ TMB.deg E = d}

def TMB.rankGeq (G : CFGraph) (D : CFDiv G) (r : ℤ) : Prop

Baker--Norine rank at least r, in subtraction-test form.

Equations

• TMB.rankGeq G D r = ∀ E ∈ TMB.effOfDegree G r, TMB.winnable G (D - E)

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

Exact rank as adjacent lower-bound tests.

Equations

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

noncomputable def TMB.rank (G : CFGraph) (D : CFDiv G) : ℤ

The unique exact rank when it exists, and -1 as a fallback.

Equations

• TMB.rank G D = if h : ∃ (r : ℤ), TMB.rankEq G D r then Classical.choose h else -1

def TMB.canonicalDivisor (G : CFGraph) : CFDiv G

The canonical divisor K(x) = val(x) - 2.

Equations

• TMB.canonicalDivisor G x = TMB.vertexDegree G x - 2

def TMB.qEffective {G : CFGraph} (q : G.V) (D : CFDiv G) : Prop

Effective away from q.

Equations

• TMB.qEffective q D = ∀ (x : G.V), x ≠ q → D x ≥ 0

def TMB.legalSet (G : CFGraph) (D : CFDiv G) (S : Finset G.V) : Prop

Firing S keeps every vertex of S out of debt.

Equations

• TMB.legalSet G D S = ∀ x ∈ S, TMB.outdegreeSet G S x ≤ D x

def TMB.qReduced (G : CFGraph) (q : G.V) (D : CFDiv G) : Prop

A q-reduced divisor: effective away from q, and no nonempty set avoiding q can be fired legally.

Equations

• TMB.qReduced G q D = (TMB.qEffective q D ∧ ∀ (S : Finset G.V), q ∉ S → S.Nonempty → ¬TMB.legalSet G D S)

Brill--Noether parameters

def TMB.rectangleWidth (G : CFGraph) (r d : ℤ) : ℤ

The width g - d + r of the Brill--Noether rectangle.

Equations

• TMB.rectangleWidth G r d = TMB.genus G - d + r

def TMB.bnNumber (G : CFGraph) (r d : ℤ) : ℤ

The Brill--Noether number.

Equations

• TMB.bnNumber G r d = TMB.genus G - (r + 1) * TMB.rectangleWidth G r d

def TMB.BNExists (G : CFGraph) (r d : ℤ) : Prop

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

Equations

• TMB.BNExists G r d = ∃ (D : TMB.CFDiv G), TMB.deg D = d ∧ TMB.rank G D ≥ r

Graph isomorphisms and vertex gluing

structure TMB.CFGraphIso (G : CFGraph) (H : CFGraph) : Type (max u v)

A graph isomorphism is a vertex equivalence preserving multiplicities.

• vertexEquiv : G.V ≃ H.V

  The bijection of vertices whose edge-multiplicity preservation makes this a graph isomorphism.

• map_num_edges (x y : G.V) : numEdges H (self.vertexEquiv x) (self.vertexEquiv y) = numEdges G x y

def TMB.CFGraphIso.mapDiv {G : CFGraph} {H : CFGraph} (φ : CFGraphIso G H) (D : CFDiv G) : CFDiv H

Push a divisor forward along a graph isomorphism.

Equations

• φ.mapDiv D y = D (φ.vertexEquiv.symm y)

def TMB.wedgeRightVertex (G : CFGraph) (H : CFGraph) (x : G.V) (y a✝ : H.V) : G.V ⊕ { b : H.V // b ≠ y }

Embed a right-factor vertex into a vertex wedge.

Equations

• TMB.wedgeRightVertex G H x y b = if h : b = y then Sum.inl x else Sum.inr ⟨b, h⟩

def TMB.vertexWedge (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) : CFGraph

Identify x and y in the disjoint union of two graphs.

Equations

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

def TMB.wedgeAddDivisor (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (E : CFDiv H) : CFDiv (vertexWedge G H x y)

Add factor divisors on their vertex wedge.

Equations

• TMB.wedgeAddDivisor G H x y D E = Sum.elim (fun (a : G.V) => D a + if a = x then E y else 0) fun (b : { b : H.V // b ≠ y }) => E ↑b

structure TMB.MarkedGraph : Type 1

A graph with ordered outside marks.

• graph : CFGraph

  The underlying graph on which the two ordered outside marks lie.

• left : self.graph.V

  The left outside mark, retained as the left mark when another factor is glued on the right.

• right : self.graph.V

  The right outside mark, identified with the next factor's left mark in a chain.

@[reducible, inline]

abbrev TMB.MarkedGraph.wedge (M N : MarkedGraph) : MarkedGraph

Glue the right mark of M to the left mark of N.

Equations

• M.wedge N = { graph := TMB.vertexWedge M.graph N.graph M.right N.left, left := Sum.inl M.left, right := TMB.wedgeRightVertex M.graph N.graph M.right N.left N.right }

def TMB.MarkedGraph.chain (M : MarkedGraph) : List MarkedGraph → MarkedGraph

Left-associated iterated vertex gluing.

Equations

• M.chain [] = M
• M.chain (N :: rest) = (M.wedge N).chain rest

def TMB.cutMultiplicity (G : CFGraph) (S : Finset G.V) : ℤ

Total multiplicity of the edges leaving S.

Equations

• TMB.cutMultiplicity G S = ∑ x ∈ S, TMB.outdegreeSet G S x

def TMB.TwoEdgeCutCondition (G : CFGraph) : Prop

Every nonempty proper cut has at least two crossing edges.

Equations

• TMB.TwoEdgeCutCondition G = ∀ (S : Finset G.V), S.Nonempty → S ≠ Finset.univ → 2 ≤ TMB.cutMultiplicity G S

structure TMB.PointedGenusOneRigid (H : CFGraph) (y : H.V) : Prop

A pointed genus-one graph whose marked point is the unique vertex in its degree-zero linear-equivalence class.

• connected : graphConnected H
• genus_one : genus H = 1
• exists_ne : ∃ (p : H.V), p ≠ y
• nontrivial (p : H.V) : p ≠ y → ¬linearEquiv H (oneChip y - oneChip p) 0

Banana graphs

structure TMB.Banana (g : ℕ) : Type

A positive integral banana graph with g + 1 labelled strands between two multivalent vertices 0 and 1. Each strand records which multivalent vertex is its tail and which is its head (a storage orientation only; the graph below is undirected), together with its positive length.

• tail : Fin (g + 1) → Fin 2

  The chosen tail pole of each of the g + 1 banana strands.

• head : Fin (g + 1) → Fin 2

  The chosen head pole of each banana strand, required to differ from its tail.

• length : Fin (g + 1) → ℕ

  The number of edges in each subdivided banana strand, required to be positive.

• core_loopless (α : Fin (g + 1)) : self.tail α ≠ self.head α
• length_pos (α : Fin (g + 1)) : 0 < self.length α

@[reducible, inline]

abbrev TMB.Banana.Interior {g : ℕ} (B : Banana g) : Type

Interior vertices remember their strand and offset; offset j denotes path position j + 1 from the tail.

Equations

• B.Interior = ((α : Fin (g + 1)) × Fin (B.length α - 1))

@[reducible, inline]

abbrev TMB.Banana.Vertex {g : ℕ} (B : Banana g) : Type

Vertices are the two multivalent vertices and all strand interiors.

Equations

• B.Vertex = (Fin 2 ⊕ B.Interior)

@[reducible, inline]

abbrev TMB.Banana.Step {g : ℕ} (B : Banana g) : Type

Unit steps along all strands.

Equations

• B.Step = ((α : Fin (g + 1)) × Fin (B.length α))

@[reducible, inline]

abbrev TMB.Banana.PathPosition {g : ℕ} (B : Banana g) (α : Fin (g + 1)) : Type

Positions 0, ..., length along a strand, measured from its tail.

Equations

• B.PathPosition α = Fin (B.length α + 1)

def TMB.Banana.coreVertex {g : ℕ} (B : Banana g) (i : Fin 2) : B.Vertex

A multivalent vertex.

Equations

• B.coreVertex i = Sum.inl i

def TMB.Banana.interiorVertex {g : ℕ} (B : Banana g) (α : Fin (g + 1)) (offset : Fin (B.length α - 1)) : B.Vertex

An interior vertex.

Equations

• B.interiorVertex α offset = Sum.inr ⟨α, offset⟩

def TMB.Banana.stepLeft {g : ℕ} (B : Banana g) (α : Fin (g + 1)) (offset : Fin (B.length α)) : B.Vertex

The left endpoint of a unit step.

Equations

• B.stepLeft α offset = if hzero : ↑offset = 0 then B.coreVertex (B.tail α) else B.interiorVertex α ⟨↑offset - 1, ⋯⟩

def TMB.Banana.stepRight {g : ℕ} (B : Banana g) (α : Fin (g + 1)) (offset : Fin (B.length α)) : B.Vertex

The right endpoint of a unit step.

Equations

• B.stepRight α offset = if hlast : ↑offset + 1 = B.length α then B.coreVertex (B.head α) else B.interiorVertex α ⟨↑offset, ⋯⟩

def TMB.Banana.unitEdge {g : ℕ} (B : Banana g) (step : B.Step) : B.Vertex × B.Vertex

The ordered pair emitted by one unit step.

Equations

• B.unitEdge step = (B.stepLeft step.fst step.snd, B.stepRight step.fst step.snd)

theorem TMB.Banana.stepLeft_ne_stepRight {g : ℕ} (B : Banana g) (α : Fin (g + 1)) (offset : Fin (B.length α)) : B.stepLeft α offset ≠ B.stepRight α offset