Exact gonality of common-period chains #
This file transports the transmission-theoretic gonality theorem across the
reader-facing bridge-chain model. The mathematical chain theorem is proved on
the vertex-wedge chain, where common-period k-general transmission composes;
contracting every displayed bridge preserves degree and rank.
theorem
Bananas.graph_connected_bridgeChain
(M : Utilities.MarkedGraph)
(L : List Utilities.MarkedGraph)
(hMconn : _root_.graphConnected M.graph)
(hLconn : ∀ N ∈ L, _root_.graphConnected N.graph)
:
Connectivity is preserved by the displayed bridge-chain construction.
theorem
Bananas.exact_gonality_of_leftRankTransport
{source target : Utilities.MarkedGraph}
(transport : LeftRankTransport source target)
{k : ℕ}
(hTargetConn : _root_.graphConnected target.graph)
(hTargetK : KGeneralTransmission (mark target.graph target.left target.right) k)
(hsmall : k ≤ (source.graph.genus.toNat + 3) / 2)
:
Exact gonality transports from the target of a rank-preserving contraction
back to its source. The upper-bound divisor is written explicitly as k
chips at the preserved left mark, so no surjectivity of the divisor map is
needed.
theorem
Bananas.exact_gonality_bridgeChain_of_commonPeriod
(M : Utilities.MarkedGraph)
(L : List Utilities.MarkedGraph)
(k : ℕ)
(hMconn : _root_.graphConnected M.graph)
(hMK : KGeneralTransmission (mark M.graph M.left M.right) k)
(hLconn : ∀ N ∈ L, _root_.graphConnected N.graph)
(hLK : ∀ N ∈ L, KGeneralTransmission (mark N.graph N.left N.right) k)
(hsmall : k ≤ ((M.bridgeChain L).graph.genus.toNat + 3) / 2)
:
Utilities.BNExists (M.bridgeChain L).graph 1 ↑k ∧ ∀ d < ↑k, ¬Utilities.BNExists (M.bridgeChain L).graph 1 d
A bridge-chain of connected factors with common k-general transmission
has gonality exactly k, whenever k is at most the generic gonality of the
total genus.