The canonical mixed-torsion chain conclusion

This file transports the centered-wedge form of Corollary 6.16(2) to the left-associated MarkedGraph.chain used in the statement of the paper.

The right half of a centered chain is assembled from the outside inward, so the transport uses both commutativity and associativity of vertex wedges. The generic commutativity isomorphism is recorded here; associativity is in VertexWedgeAssociativity.

@[simp]

theorem Bananas.markedChain_append (M : Utilities.MarkedGraph) (L R : List Utilities.MarkedGraph) : M.chain (L ++ R) = (M.chain L).chain R

Commuting a vertex wedge

noncomputable def Bananas.vertexWedgeCommPresentation (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) : Utilities.VertexWedgePresentation (Utilities.vertexWedge H G y x) G H x y

The wedge with its two factors exchanged, presented by the original ordered pair of factors.

Equations

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

noncomputable def Bananas.vertexWedgeComm (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) : Utilities.CFGraphIso (Utilities.vertexWedge G H x y) (Utilities.vertexWedge H G y x)

Vertex wedges are commutative up to graph isomorphism.

Equations

• Bananas.vertexWedgeComm G H x y = (Bananas.vertexWedgeCommPresentation G H x y).graphIso

@[simp]

theorem Bananas.vertexWedge_comm_apply_left (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (a : G.V) : (vertexWedgeComm G H x y).vertexEquiv (Sum.inl a) = Utilities.wedgeRightVertex H G y x a

@[simp]

theorem Bananas.vertexWedge_comm_apply_right (G : CFGraph) (H : CFGraph) (x : G.V) (y b : H.V) : (vertexWedgeComm G H x y).vertexEquiv (Utilities.wedgeRightVertex G H x y b) = Sum.inl b

Reassociating a marked chain

noncomputable def Bananas.vertexWedgeCongrRight {G : CFGraph} {H : CFGraph} {H' : CFGraph} (phi : Utilities.CFGraphIso H H') (x : G.V) (y : H.V) (y' : H'.V) (hy : phi.vertexEquiv y = y') : Utilities.CFGraphIso (Utilities.vertexWedge G H x y) (Utilities.vertexWedge G H' x y')

Transport a right wedge attachment along an isomorphism that sends the old attachment vertex to the specified new one. Binding the target vertex separately lets Lean eliminate the equality before the dependent wedge type is formed.

Equations

• Bananas.vertexWedgeCongrRight phi x y y' hy = hy ▸ (Utilities.CFGraphIso.refl G).vertexWedgeCongr phi x y

@[simp]

theorem Bananas.vertexWedgeCongrRight_apply_left {G : CFGraph} {H : CFGraph} {H' : CFGraph} (phi : Utilities.CFGraphIso H H') (x : G.V) (y : H.V) (y' : H'.V) (hy : phi.vertexEquiv y = y') (a : G.V) : (vertexWedgeCongrRight phi x y y' hy).vertexEquiv (Sum.inl a) = Sum.inl a

structure Bananas.MarkedChainReassocData (M F : Utilities.MarkedGraph) (rest : List Utilities.MarkedGraph) : Type u_1

Reassociation data, including the endpoint fact needed to use the isomorphism beneath a further vertex wedge.

• iso : Utilities.CFGraphIso ((M.wedge F).chain rest).graph (M.wedge (F.chain rest)).graph

  The graph isomorphism moving the first wedge outside the remaining chain.

• map_left : self.iso.vertexEquiv ((M.wedge F).chain rest).left = (M.wedge (F.chain rest)).left

noncomputable def Bananas.markedChainReassocData (M F : Utilities.MarkedGraph) (rest : List Utilities.MarkedGraph) : MarkedChainReassocData M F rest

Reassociate a left-associated marked chain so that its first factor is glued to the chain of all remaining factors.

Equations

• One or more equations did not get rendered due to their size.
• Bananas.markedChainReassocData M F [] = { iso := Utilities.CFGraphIso.refl (M.wedge F).graph, map_left := ⋯ }

noncomputable def Bananas.markedChainReassocIso (M F : Utilities.MarkedGraph) (rest : List Utilities.MarkedGraph) : Utilities.CFGraphIso ((M.wedge F).chain rest).graph (M.wedge (F.chain rest)).graph

The graph isomorphism underlying markedChainReassocData.

Equations

• Bananas.markedChainReassocIso M F rest = (Bananas.markedChainReassocData M F rest).iso

@[simp]

theorem Bananas.markedChainReassocIso_apply_left (M F : Utilities.MarkedGraph) (rest : List Utilities.MarkedGraph) : (markedChainReassocIso M F rest).vertexEquiv ((M.wedge F).chain rest).left = (M.wedge (F.chain rest)).left

Reversing the right half of a chain

structure Bananas.ReversedFactorChainIsoData (F : KGeneralChainFactor) (rest : List KGeneralChainFactor) : Type

Data for reversing a nonempty marked factor chain. The isomorphism sends the chain's left endpoint to the right endpoint of the outside-in presentation, which is the central attachment vertex.

• iso : Utilities.CFGraphIso (F.marked.chain (List.map KGeneralChainFactor.marked rest)).graph (reversedMarkedChain F rest).graph

  The graph isomorphism from the original chain to its reversed presentation.

• map_left : self.iso.vertexEquiv (F.marked.chain (List.map KGeneralChainFactor.marked rest)).left = (reversedMarkedChain F rest).right

noncomputable def Bananas.reversedFactorChainIsoData (F : KGeneralChainFactor) (rest : List KGeneralChainFactor) : ReversedFactorChainIsoData F rest

The canonical chain of a list of factors is graph-isomorphic to its outside-in reversed presentation with all marks swapped.

Equations

• One or more equations did not get rendered due to their size.
• Bananas.reversedFactorChainIsoData F [] = { iso := Utilities.CFGraphIso.refl F.marked.graph, map_left := ⋯ }

noncomputable def Bananas.reversedFactorChainIso (F : KGeneralChainFactor) (rest : List KGeneralChainFactor) : Utilities.CFGraphIso (F.marked.chain (List.map KGeneralChainFactor.marked rest)).graph (reversedMarkedChain F rest).graph

The underlying graph isomorphism reversing the factor chain and interchanging its outer marks.

Equations

• Bananas.reversedFactorChainIso F rest = (Bananas.reversedFactorChainIsoData F rest).iso

@[simp]

theorem Bananas.reversedFactorChainIso_apply_left (F : KGeneralChainFactor) (rest : List KGeneralChainFactor) : (reversedFactorChainIso F rest).vertexEquiv (F.marked.chain (List.map KGeneralChainFactor.marked rest)).left = (reversedMarkedChain F rest).right

Corollary 6.16(2) for positive-genus chains

noncomputable def Bananas.balancedChainGraphIso (leftHead : KGeneralChainFactor) (leftTail : List KGeneralChainFactor) (rightHead : KGeneralChainFactor) (rightTail : List KGeneralChainFactor) : Utilities.CFGraphIso ((leftHead.marked.chain (List.map KGeneralChainFactor.marked leftTail)).chain (List.map KGeneralChainFactor.marked (rightHead :: rightTail))).graph (balancedChainGraph leftHead leftTail rightHead rightTail)

The graph in the centered presentation of a balanced split is the canonical left-associated chain, up to the explicit reassociation and reversal isomorphisms above.

Equations

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

theorem Bananas.brillNoetherGeneral_mixedTorsionChain_of_minBudget_of_positive (F next : KGeneralChainFactor) (rest : List KGeneralChainFactor) (hPositive : ∀ Q ∈ F :: next :: rest, 0 < Q.marked.graph.genus) (hMin : ChainMinBudget (F :: next :: rest)) : BrillNoetherGeneral (F.marked.chain (List.map KGeneralChainFactor.marked (next :: rest))).graph

Corollary 6.16(2) for chains of at least two positive-genus factors.

The paper's minimum prefix/suffix period bound chooses a nonempty balancing cut. The two once-marked halves are Brill--Noether general by the preceding chain theorems; the centered wedge is general by Proposition 6.14, and the explicit graph isomorphism transports that conclusion to the canonical chain.

Absorbing genus-zero factors

theorem Bananas.brillNoetherGeneral_factorChain_cons_genus_zero_of_tail (F next : KGeneralChainFactor) (rest : List KGeneralChainFactor) (hZero : F.marked.graph.genus = 0) (hTail : BrillNoetherGeneral (next.marked.chain (List.map KGeneralChainFactor.marked rest)).graph) : BrillNoetherGeneral (F.marked.chain (List.map KGeneralChainFactor.marked (next :: rest))).graph

A genus-zero factor at the head of a canonical chain can be moved to the right of the remaining chain and absorbed. This is the graph-theoretic reduction needed to extend Corollary 6.16(2) from positive-genus factors to the paper's full graph convention.

theorem Bananas.brillNoetherGeneral_markedChain_of_tail_genus_zero (M : Utilities.MarkedGraph) (tail : List KGeneralChainFactor) (hGeneral : BrillNoetherGeneral M.graph) (hZero : ∀ F ∈ tail, F.marked.graph.genus = 0) : BrillNoetherGeneral (M.chain (List.map KGeneralChainFactor.marked tail)).graph

Once a marked accumulator is Brill--Noether general, appending only connected genus-zero factors preserves Brill--Noether generality.

theorem Bananas.brillNoetherGeneral_mixedTorsionChain_of_minBudget (F : KGeneralChainFactor) (tail : List KGeneralChainFactor) (hMin : ChainMinBudget (F :: tail)) : BrillNoetherGeneral (F.marked.chain (List.map KGeneralChainFactor.marked tail)).graph

Corollary 6.16(2) in the paper's full graph convention, allowing connected genus-zero factors in arbitrary positions.

At a nonzero first genus crossing, the canonical balancing argument applies without any factorwise positivity assumption. If the first crossing is zero, nonnegativity forces the entire suffix to have genus zero; the minimum budget makes the head factor general, and the suffix is absorbed one tree factor at a time.