Balanced chains with mixed torsion orders

This file formalizes the second half of Corollary 6.16 (thm:bngChain). A chain is split at one of its separating vertices. The factors on the left obey the prefix-genus bounds of part (1), while the factors on the right obey the corresponding suffix-genus bounds. The right half is built from the outside inward after swapping both marks of every factor. Thus the suffix bounds become the prefix bounds needed by Theorem 6.6.

The final graph is presented by its central vertex wedge. This is a literal iterated vertex gluing of the factors in their original order; choosing this parenthesization avoids identifying the different nested Sum vertex types of left- and right-associated MarkedGraph.chain constructions.

Reversing a chain factor

def Bananas.KGeneralChainFactor.swapMarks (F : KGeneralChainFactor) : KGeneralChainFactor

Reverse the orientation of a twice-marked chain factor.

Equations

• F.swapMarks = { marked := { graph := F.marked.graph, left := F.marked.right, right := F.marked.left }, period := F.period, connected := ⋯, kGeneral := ⋯ }

@[simp]

theorem Bananas.KGeneralChainFactor.swapMarks_graph (F : KGeneralChainFactor) : F.swapMarks.marked.graph = F.marked.graph

@[simp]

theorem Bananas.KGeneralChainFactor.swapMarks_left (F : KGeneralChainFactor) : F.swapMarks.marked.left = F.marked.right

@[simp]

theorem Bananas.KGeneralChainFactor.swapMarks_right (F : KGeneralChainFactor) : F.swapMarks.marked.right = F.marked.left

@[simp]

theorem Bananas.KGeneralChainFactor.swapMarks_period (F : KGeneralChainFactor) : F.swapMarks.period = F.period

Genus budgets from the right

def Bananas.chainFactorGenus (L : List KGeneralChainFactor) : ℤ

The sum of the genera of a list of chain factors.

Equations

• Bananas.chainFactorGenus L = (List.map (fun (F : Bananas.KGeneralChainFactor) => F.marked.graph.genus) L).sum

@[simp]

theorem Bananas.chainFactorGenus_nil : chainFactorGenus [] = 0

@[simp]

theorem Bananas.chainFactorGenus_cons (F : KGeneralChainFactor) (rest : List KGeneralChainFactor) : chainFactorGenus (F :: rest) = F.marked.graph.genus + chainFactorGenus rest

def Bananas.ChainSuffixBudget : List KGeneralChainFactor → Prop

The paper's suffix-genus inequalities.

For Fᵢ, Fᵢ₊₁, ..., Fℓ, the first conjunct says gᵢ + gᵢ₊₁ + ... + gℓ < kᵢ; the recursive tail records the same inequality at every later factor.

Equations

• Bananas.ChainSuffixBudget [] = True
• Bananas.ChainSuffixBudget (F :: rest) = (Bananas.chainFactorGenus (F :: rest) < ↑F.period ∧ Bananas.ChainSuffixBudget rest)

@[simp]

theorem Bananas.chainSuffixBudget_nil : ChainSuffixBudget []

@[simp]

theorem Bananas.chainSuffixBudget_cons (F : KGeneralChainFactor) (rest : List KGeneralChainFactor) : ChainSuffixBudget (F :: rest) ↔ chainFactorGenus (F :: rest) < ↑F.period ∧ ChainSuffixBudget rest

theorem Bananas.chainPrefixBudget_iff_indexed (g : ℤ) (L : List KGeneralChainFactor) : ChainPrefixBudget g L ↔ ∀ (i : ℕ) (hi : i < L.length), g + chainFactorGenus (List.take (i + 1) L) < ↑(L.get ⟨i, hi⟩).period

Indexed form of the recursive prefix budget.

theorem Bananas.chainSuffixBudget_iff_indexed (L : List KGeneralChainFactor) : ChainSuffixBudget L ↔ ∀ (i : ℕ) (hi : i < L.length), chainFactorGenus (List.drop i L) < ↑(L.get ⟨i, hi⟩).period

Indexed form of the recursive suffix budget.

def Bananas.ChainMinBudget (L : List KGeneralChainFactor) : Prop

The literal minimum hypothesis in Corollary 6.16(2), indexed from zero.

Equations

• Bananas.ChainMinBudget L = ∀ (i : ℕ) (hi : i < L.length), min (Bananas.chainFactorGenus (List.take (i + 1) L)) (Bananas.chainFactorGenus (List.drop i L)) < ↑(L.get ⟨i, hi⟩).period

def Bananas.ChainDominatesAtSplit (left right : List KGeneralChainFactor) : Prop

A cut lies at the crossing of the prefix- and suffix-genus functions.

Before the cut, each prefix is no larger than the corresponding suffix; after the cut, each suffix is no larger than the corresponding prefix. The maximal index used in the paper's proof has exactly this property.

Equations

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

def Bananas.ChainBalancedAtSplit (left right : List KGeneralChainFactor) : Prop

The split form of the minimum condition in Corollary 6.16(2): on the left side the minimum is the prefix genus, and on the right side it is the suffix genus.

Equations

• Bananas.ChainBalancedAtSplit left right = (Bananas.ChainPrefixBudget 0 left ∧ Bananas.ChainSuffixBudget right)

theorem Bananas.chainBalancedAtSplit_of_minBudget (left right : List KGeneralChainFactor) (hMin : ChainMinBudget (left ++ right)) (hCross : ChainDominatesAtSplit left right) : ChainBalancedAtSplit left right

The paper's minimum hypothesis gives the two recursive budgets at any crossing cut of the prefix- and suffix-genus functions.

The reversed right-hand chain

def Bananas.reversedMarkedChain (F : KGeneralChainFactor) : List KGeneralChainFactor → Utilities.MarkedGraph

Build a nonempty suffix from the outside inward.

For the original order F :: next :: rest, this is the chain whose factor order is reverse (F :: next :: rest) and whose factor marks are all swapped. Its right mark is therefore the original left mark of F, namely the vertex at which this suffix is attached to the left half of the chain.

Equations

• Bananas.reversedMarkedChain F [] = F.swapMarks.marked
• Bananas.reversedMarkedChain F (F_1 :: rest) = (Bananas.reversedMarkedChain F_1 rest).wedge F.swapMarks.marked

@[simp]

theorem Bananas.reversedMarkedChain_nil (F : KGeneralChainFactor) : reversedMarkedChain F [] = F.swapMarks.marked

@[simp]

theorem Bananas.reversedMarkedChain_cons (F next : KGeneralChainFactor) (rest : List KGeneralChainFactor) : reversedMarkedChain F (next :: rest) = (reversedMarkedChain next rest).wedge F.swapMarks.marked

theorem Bananas.genus_reversedMarkedChain (F : KGeneralChainFactor) (rest : List KGeneralChainFactor) : (reversedMarkedChain F rest).graph.genus = chainFactorGenus (F :: rest)

The reversed chain has the sum of the original factor genera.

theorem Bananas.graph_connected_reversedMarkedChain (F : KGeneralChainFactor) (rest : List KGeneralChainFactor) : _root_.graphConnected (reversedMarkedChain F rest).graph

Connectivity is preserved while the suffix is assembled from the right.

theorem Bananas.allSubmodular_reversedMarkedChain (F : KGeneralChainFactor) (rest : List KGeneralChainFactor) : AllSubmodular (mark (reversedMarkedChain F rest).graph (reversedMarkedChain F rest).left (reversedMarkedChain F rest).right)

Every divisor on the reversed chain is submodular at its two outer marks.

theorem Bananas.onceMarkedBrillNoetherGeneral_reversedMixedTorsionChain (F : KGeneralChainFactor) (rest : List KGeneralChainFactor) (hBudget : ChainSuffixBudget (F :: rest)) : OnceMarkedBrillNoetherGeneral (reversedMarkedChain F rest).graph (reversedMarkedChain F rest).right

The right-hand analogue of Corollary 6.16(1).

Under suffix-genus period bounds, the reversed chain is Brill--Noether general as a once-marked graph at its central (right) mark.

The central split and Corollary 6.16(2)

theorem Bananas.graph_connected_factorChain (F : KGeneralChainFactor) (rest : List KGeneralChainFactor) : _root_.graphConnected (F.marked.chain (List.map KGeneralChainFactor.marked rest)).graph

Connectivity of a left-associated nonempty factor chain.

def Bananas.balancedChainGraph (leftHead : KGeneralChainFactor) (leftTail : List KGeneralChainFactor) (rightHead : KGeneralChainFactor) (rightTail : List KGeneralChainFactor) : CFGraph

The graph obtained by gluing the two nonempty halves at their central marks. The right half is presented from the outside inward.

Equations

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

theorem Bananas.brillNoetherGeneral_mixedTorsionChain_of_balancedSplit (leftHead : KGeneralChainFactor) (leftTail : List KGeneralChainFactor) (rightHead : KGeneralChainFactor) (rightTail : List KGeneralChainFactor) (hBalanced : ChainBalancedAtSplit (leftHead :: leftTail) (rightHead :: rightTail)) : BrillNoetherGeneral (balancedChainGraph leftHead leftTail rightHead rightTail)

Paper Corollary 6.16(2), at a balancing split.

If the factors to the left of a separating vertex satisfy their prefix-genus bounds, while the factors to its right satisfy their suffix-genus bounds, then the unmarked chain is Brill--Noether general. Under the paper's global kᵢ > min(prefix genus, suffix genus) hypothesis, its maximal balancing index is exactly a split with these two properties.

theorem Bananas.brillNoetherGeneral_mixedTorsionChain_of_minBudget_at_crossing (leftHead : KGeneralChainFactor) (leftTail : List KGeneralChainFactor) (rightHead : KGeneralChainFactor) (rightTail : List KGeneralChainFactor) (hMin : ChainMinBudget (leftHead :: leftTail ++ rightHead :: rightTail)) (hCross : ChainDominatesAtSplit (leftHead :: leftTail) (rightHead :: rightTail)) : BrillNoetherGeneral (balancedChainGraph leftHead leftTail rightHead rightTail)

Corollary 6.16(2) in the paper's literal minimum-budget language, once the crossing cut selected in its proof is supplied.