Chains with mixed torsion orders

This file formalizes the first half of Corollary 6.16 (thm:bngChain). The factors are bundled with their individual periods and k-general transmission hypotheses. ChainPrefixBudget g L is the recursive form of the paper's condition

k_i > g₁ + ... + gᵢ.

Starting from an accumulated graph of genus g, its first conjunct says that the next period is larger than g plus the genus of the next factor; its tail then uses that enlarged genus. This presentation follows the left-associated recursion in MarkedGraph.chain and avoids any indexing conventions.

structure Bananas.KGeneralChainFactor : Type 1

One factor of a mixed-torsion chain, including precisely the hypotheses used by Corollary 6.16.

• marked : Utilities.MarkedGraph

  The graph and ordered boundary marks of this chain factor.

• period : ℕ

  The transmission period at which this marked factor is k-general.

• connected : _root_.graphConnected self.marked.graph
• kGeneral : KGeneralTransmission (mark self.marked.graph self.marked.left self.marked.right) self.period

def Bananas.ChainPrefixBudget : ℤ → List KGeneralChainFactor → Prop

The prefix-genus period inequalities for the factors still to be attached to a chain whose accumulated genus is g.

For factors F₂, ..., Fℓ and g = g₁, this unfolds to g₁ + g₂ < k₂, g₁ + g₂ + g₃ < k₃, and so on.

Equations

• Bananas.ChainPrefixBudget x✝ [] = True
• Bananas.ChainPrefixBudget x✝ (F :: rest) = (x✝ + F.marked.graph.genus < ↑F.period ∧ Bananas.ChainPrefixBudget (x✝ + F.marked.graph.genus) rest)

@[simp]

theorem Bananas.chainPrefixBudget_nil (g : ℤ) : ChainPrefixBudget g []

@[simp]

theorem Bananas.chainPrefixBudget_cons (g : ℤ) (F : KGeneralChainFactor) (rest : List KGeneralChainFactor) : ChainPrefixBudget g (F :: rest) ↔ g + F.marked.graph.genus < ↑F.period ∧ ChainPrefixBudget (g + F.marked.graph.genus) rest

theorem Bananas.onceMarkedBrillNoetherGeneral_chain_aux (M : Utilities.MarkedGraph) (hMconn : _root_.graphConnected M.graph) (hMsub : AllSubmodular (mark M.graph M.left M.right)) (hMgeneral : OnceMarkedBrillNoetherGeneral M.graph M.right) (L : List KGeneralChainFactor) (hBudget : ChainPrefixBudget M.graph.genus L) : OnceMarkedBrillNoetherGeneral (M.chain (List.map KGeneralChainFactor.marked L)).graph (M.chain (List.map KGeneralChainFactor.marked L)).right

Inductive engine for Corollary 6.16(1). The accumulated twice-marked graph is already once-marked Brill--Noether general at its right mark; attaching factors whose periods satisfy the successive prefix bounds preserves that property.

The extra left mark is retained only because Theorem 6.6 uses it to compose the exact transmission permutations.

theorem Bananas.onceMarkedBrillNoetherGeneral_mixedTorsionChain (head : KGeneralChainFactor) (tail : List KGeneralChainFactor) (hHeadBudget : head.marked.graph.genus < ↑head.period) (hTailBudget : ChainPrefixBudget head.marked.graph.genus tail) : OnceMarkedBrillNoetherGeneral (head.marked.chain (List.map KGeneralChainFactor.marked tail)).graph (head.marked.chain (List.map KGeneralChainFactor.marked tail)).right

Corollary 6.16(1), the once-marked mixed-torsion chain theorem.

The head inequality is the i = 1 case of the paper's hypothesis, and hTailBudget contains all later prefix inequalities. Every factor has its own period and k-general transmission; no common torsion order is assumed.