Twice-marked banana graphs: definitions

This is the paper-specific vocabulary for the twice-marked banana paper. A banana of genus g is represented by the existing positive subdivision model with two core vertices and g + 1 distinct edge slots. Thus parallel strands are retained by construction, rather than identified as a simple graph.

@[reducible, inline]

abbrev Bananas.Banana (g : ℕ) : Type

A genus-g banana graph: g + 1 positive-length strands between two core vertices.

Equations

• Bananas.Banana g = Utilities.Certificate.SubdivisionGraph.Spec 2 (g + 1)

def Bananas.bananaOfLengths (g : ℕ) (length : Fin (g + 1) → ℕ) (hpos : ∀ (i : Fin (g + 1)), 0 < length i) : Banana g

A concrete banana with prescribed positive strand lengths: the two-vertex core with g + 1 parallel strands, none of which is a loop. This is the coordinate-first constructor behind the notation B_{n₀,…,nₑ} and, at g = 2, θ_{a,b,c}.

Equations

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

def Bananas.strandVertex {g : ℕ} (B : Banana g) (α : Fin (g + 1)) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) : (Utilities.Certificate.SubdivisionGraph.Spec.graph B).V

The vertex at position i along strand α, measured from core vertex 0. SubdivisionGraph.Spec allows an individual slot to be stored in either orientation, so this deliberately reverses its coordinate when necessary.

Equations

• Bananas.strandVertex B α i = Utilities.Certificate.SubdivisionGraph.Spec.pathVertex B α (if B.core.tail α = 0 then i else ⟨B.length α - ↑i, ⋯⟩)

def Bananas.strandMirror {g : ℕ} (B : Banana g) (α : Fin (g + 1)) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α

Reflection of a normalized strand coordinate about its midpoint.

Equations

• Bananas.strandMirror B α i = ⟨B.length α - ↑i, ⋯⟩

def Bananas.leftEndpoint {g : ℕ} (B : Banana g) : (Utilities.Certificate.SubdivisionGraph.Spec.graph B).V

The two multivalent vertices of a banana.

Equations

• Bananas.leftEndpoint B = Utilities.Certificate.SubdivisionGraph.Spec.coreVertex B 0

def Bananas.rightEndpoint {g : ℕ} (B : Banana g) : (Utilities.Certificate.SubdivisionGraph.Spec.graph B).V

The right multivalent endpoint of the banana graph.

Equations

• Bananas.rightEndpoint B = Utilities.Certificate.SubdivisionGraph.Spec.coreVertex B 1

structure Bananas.TwiceMarked : Type 1

A graph with an ordered pair of marked vertices.

• graph : CFGraph

  The underlying graph carrying the two marked vertices.

• u : self.graph.V

  The first vertex in the ordered pair of marks.

• v : self.graph.V

  The second vertex in the ordered pair of marks.

@[reducible, inline]

abbrev Bananas.mark (G : CFGraph) (u v : G.V) : TwiceMarked

Bundle a graph and an ordered pair of its vertices as a twice-marked graph.

Equations

• Bananas.mark G u v = { graph := G, u := u, v := v }

noncomputable def Bananas.rankDelta (M : TwiceMarked) (D : CFDiv M.graph) : ℤ

Paper source: def-Delt (Definition 2.8), the function Δ(D).

The paper's second rank difference, relative to the two marks.

Equations

• Bananas.rankDelta M D = rank M.graph D - rank M.graph (D - oneChip M.u) - rank M.graph (D - oneChip M.v) + rank M.graph (D - oneChip M.u - oneChip M.v)

def Bananas.twist (M : TwiceMarked) (D : CFDiv M.graph) (a b : ℤ) : CFDiv M.graph

Paper source: def-Twist (Definition 2.7).

Equations

• Bananas.twist M D a b = D + a • oneChip M.u + b • oneChip M.v

def Bananas.Submodular (M : TwiceMarked) (D : CFDiv M.graph) : Prop

Paper source: def-submod (Definition 2.9).

Submodularity of a divisor, including all of its marked twists.

Equations

• Bananas.Submodular M D = ∀ (a b : ℤ), 0 ≤ Bananas.rankDelta M (Bananas.twist M D a b)

def Bananas.AllSubmodular (M : TwiceMarked) : Prop

Every divisor is submodular for this marked graph.

Equations

• Bananas.AllSubmodular M = ∀ (D : CFDiv M.graph), Bananas.Submodular M D

def Bananas.TorsionWitness (M : TwiceMarked) (k : ℕ) : Prop

Paper source: the hypothesis ku ∼ kv of the k-general transmission definition (Definition 1.10), not the torsion order of def-TwMkGraph.

A positive k kills the degree-zero class of the marked-point difference.

Equations

• Bananas.TorsionWitness M k = (0 < k ∧ linearEquiv M.graph (↑k • (oneChip M.u - oneChip M.v)) 0)

def Bananas.IsTorsionOrder (M : TwiceMarked) (k : ℕ) : Prop

Paper source: def-TwMkGraph (Definition 2.6), the torsion order.

The torsion order is the least positive k killing the marked difference.

Equations

• Bananas.IsTorsionOrder M k = (Bananas.TorsionWitness M k ∧ ∀ (m : ℕ), Bananas.TorsionWitness M m → k ≤ m)

def Bananas.IsTransmissionPermutation (M : TwiceMarked) (D : CFDiv M.graph) (τ : ℤ → ℤ) : Prop

Paper source: def-tauD (Definition 2.11), the transmission permutation τ^{u,v}_D characterised by δ(τ(b) = a) = Δ(D + au - bv).

We keep the permutation as an integer function; bijectivity is stated here instead of using a separate affine-permutation structure. Note that the main library models the same notion by AspPerm together with Utilities.SatisfiesTransmission; the two presentations are not yet connected by any lemma.

Equations

• Bananas.IsTransmissionPermutation M D τ = (Function.Bijective τ ∧ ∀ (a b : ℤ), (if τ b = a then 1 else 0) = Bananas.rankDelta M (D + a • oneChip M.u - b • oneChip M.v))

def Bananas.IsKAffine (k : ℕ) (τ : ℤ → ℤ) : Prop

Paper source: def-EA (Definition 2.10), membership in the extended affine symmetric group \widetilde{Sigma}_k.

Equations

• Bananas.IsKAffine k τ = ∀ (n : ℤ), τ (n + ↑k) = τ n + ↑k

def Bananas.kInversions (k : ℕ) (τ : ℤ → ℤ) : Set (ℤ × ℤ)

Paper source: def-inv (Definition 2.13), the set Inv_k(τ).

The paper's k-inversions are k-equivalence classes of inversions, where (a,b) ∼ (a',b') iff a - a' = b - b' and a ≡ a' (mod k). Each class has a unique representative with 0 ≤ a < k, and this set of representatives is what is recorded here.

Equations

• Bananas.kInversions k τ = {p : ℤ × ℤ | p.1 < p.2 ∧ τ p.1 > τ p.2 ∧ 0 ≤ p.1 ∧ p.1 < ↑k}

noncomputable def Bananas.kInversionCount (k : ℕ) (τ : ℤ → ℤ) : ℕ

Paper source: def-inv (Definition 2.13), the number inv_k(τ).

Equations

• Bananas.kInversionCount k τ = (Bananas.kInversions k τ).ncard

def Bananas.KGeneralTransmission (M : TwiceMarked) (k : ℕ) : Prop

Paper source: Definition 1.10, k-general transmission.

Stated directly in terms of transmission permutations and their k-inversion counts. The (kInversions k τ).Finite conjunct is not redundant decoration: Set.ncard is 0 on an infinite set, so without it the count bound would be satisfied vacuously by a permutation with infinitely many k-inversions. (Finiteness is in fact automatic here — see kInversions_finite_of_isKAffine — but only because of the other conjuncts.)

Equations

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

def Bananas.BrillNoetherGeneral (G : CFGraph) : Prop

Paper source: Definition 1.3, i.e. part 2 of Conjecture 1.2. Every pair in the divisor census satisfies ρ(g,r,d) ≥ 0.

This is deliberately an implication and not an equivalence. The converse inclusion (every pair with ρ ≥ 0 occurs) is part 1 of Conjecture 1.2, which the paper records as open outside small genus. Building it into the definition would silently strengthen every hypothesis BrillNoetherGeneral G and, more importantly, weaken every conclusion of the form ¬ BrillNoetherGeneral G.

Equations

• Bananas.BrillNoetherGeneral G = ∀ (r d : ℤ), 0 ≤ r → Utilities.BNExists G r d → 0 ≤ Utilities.bnNumber G r d

def Bananas.thetaExceptionalPositions {g : ℕ} (B : Banana g) (α : Fin (g + 1)) (i j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) : Set (Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α)

Paper source: the set N_(G,u,v) of thm-NonSubmodGenus2 (Theorem 3.4), for two marks u = v_{α,i}, v = v_{α,j} on one strand: { v_{α,q} : q ≠ n_α - i, q ≠ j, j - i ≤ q ≤ j - i + n_α }.

The bounds are stated over ℤ. The paper places no order relation on i and j, and with truncated ℕ subtraction the constraint j - i ≤ q would collapse to 0 ≤ q whenever j < i; the ℕ reading therefore only agrees with the paper's set when i ≤ j.

Equations

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

def Bananas.EvenlyMarkedTheta (B : Banana 2) (α β : Fin 3) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B β) : Prop

Paper source: defn:evenlyMarked (Definition 4.14).

Two interior marks on distinct theta strands divide their strands in the same rational ratio. Cross multiplication avoids a division convention.

Equations

• Bananas.EvenlyMarkedTheta B α β i j = (α ≠ β ∧ 0 < ↑i ∧ ↑i < B.length α ∧ 0 < ↑j ∧ ↑j < B.length β ∧ ↑i * B.length β = ↑j * B.length α)