Unconditional transmission gluing for Section 6

ChainGluing.lean predates the proof of bounded Demazure factorizations and therefore exposes its chain result with an explicit factorization hypothesis. DemazureFactorization.lean now proves precisely that input for all nonnegative genus budgets. This file records the resulting unconditional version, which is the transmission-existence backbone of the Section 6 chain arguments.

theorem Bananas.chainTransmissionExistence_unconditional (M : Utilities.MarkedGraph) (L : List Utilities.MarkedGraph) (hM : Utilities.TransmissionExistence M.graph M.left M.right) (hL : ∀ N ∈ L, Utilities.TransmissionExistence N.graph N.left N.right) (hGenus : ∀ N ∈ M :: L, 0 ≤ N.graph.genus) : Utilities.TransmissionExistence (M.chain L).graph (M.chain L).left (M.chain L).right

The outer marks of an iterated vertex-gluing chain have transmission existence whenever every factor does. No additional Demazure-factorization hypothesis remains: it is discharged by transmissionExistence_vertexWedge_opposite.

theorem Bananas.onceMarkedBNExists_chain_unconditional (M : Utilities.MarkedGraph) (L : List Utilities.MarkedGraph) (hM : Utilities.TransmissionExistence M.graph M.left M.right) (hL : ∀ N ∈ L, Utilities.TransmissionExistence N.graph N.left N.right) (hGenus : ∀ N ∈ M :: L, 0 ≤ N.graph.genus) (hconn : graphConnected (M.chain L).graph) (tau : AspPerm) (lambda : YoungDiagram) (hProfile : Utilities.GrassmannianPartitionProfile tau lambda) (hFinite : Utilities.FiniteTransmissionPerm tau) (hLength : ↑(invSet tau.func).ncard ≤ (M.chain L).graph.genus) : Utilities.OnceMarkedBNExists (M.chain L).graph (M.chain L).left lambda

The once-marked existence consequence of the unconditional chain gluing. This is the currently formal transmission counterpart of the first conclusion of the paper's chain theorem; the remaining Section 6 work is to prove the paper's upper Weierstrass-size Brill--Noether generality conclusions.