Chains with a common general-transmission period

The corollary following Proposition 6.1 cites Theorem A of Pflueger 2022: vertex-gluing twice-marked graphs with the same k-general transmission period preserves k-general transmission. This file proves the required affine Coxeter-length inequality directly from the periodic simple-reflection reduction already developed for Proposition 6.13, then records the two-factor and iterated graph statements and the resulting Brill--Noether generality criterion.

Affine Coxeter length and the Demazure product

theorem Bananas.IsKAffine.aspPerm_mul {k : ℕ} {α β : AspPerm} (hα : IsKAffine k α.func) (hβ : IsKAffine k β.func) : IsKAffine k (α * β).func

theorem Bananas.kInversionCount_aspPerm_inv {k : ℕ} (hk : 0 < k) (α : AspPerm) (hα : IsKAffine k α.func) : kInversionCount k α⁻¹.func = kInversionCount k α.func

theorem Bananas.affineReflection_star_affine_and_count_le {k : ℕ} {α : AspPerm} (hα : IsKAffine k α.func) (i : ℤ) (hk : 2 ≤ k) : IsKAffine k (α ⋆ affineReflection k i hk).func ∧ kInversionCount k (α ⋆ affineReflection k i hk).func ≤ kInversionCount k α.func + 1

Right Demazure multiplication by one periodic simple reflection preserves k-affinity and raises affine inversion length by at most one.

theorem Bananas.kInversionCount_star_le (k : ℕ) (α β : AspPerm) (hα : IsKAffine k α.func) (hβ : IsKAffine k β.func) : IsKAffine k (α ⋆ β).func ∧ kInversionCount k (α ⋆ β).func ≤ kInversionCount k α.func + kInversionCount k β.func

Affine Coxeter length is subadditive under the Demazure product. This is the combinatorial content of the same-period gluing theorem cited from Pflueger 2022.

Common-period general transmission across wedges and chains

theorem Bananas.torsionWitness_vertexWedge_opposite (G H : CFGraph) (x : G.V) (y : H.V) (u : G.V) (v : H.V) (k : ℕ) (hG : TorsionWitness (mark G u x) k) (hH : TorsionWitness (mark H y v) k) : TorsionWitness (mark (Utilities.vertexWedge G H x y) (Sum.inl u) (Utilities.wedgeRightVertex G H x y v)) k

A common torsion witness glues across an opposite-side vertex wedge.

theorem Bananas.kGeneralTransmission_vertexWedge_opposite (G H : CFGraph) (x : G.V) (y : H.V) (u : G.V) (v : H.V) (k : ℕ) (hGconn : _root_.graphConnected G) (hHconn : _root_.graphConnected H) (hG : KGeneralTransmission (mark G u x) k) (hH : KGeneralTransmission (mark H y v) k) : KGeneralTransmission (mark (Utilities.vertexWedge G H x y) (Sum.inl u) (Utilities.wedgeRightVertex G H x y v)) k

Two opposite-side marked graphs with the same k-general transmission period have k-general transmission after vertex gluing.

theorem Bananas.kGeneralTransmission_markedChain_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) : KGeneralTransmission (mark (M.chain L).graph (M.chain L).left (M.chain L).right) k

Common-period general transmission is preserved by a left-associated marked chain.

theorem Bananas.graph_connected_markedChain (M : Utilities.MarkedGraph) (L : List Utilities.MarkedGraph) (hMconn : _root_.graphConnected M.graph) (hLconn : ∀ N ∈ L, _root_.graphConnected N.graph) : _root_.graphConnected (M.chain L).graph

Connectivity is preserved along a marked chain.

theorem Bananas.brillNoetherGeneral_markedChain_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) (hthreshold : (M.chain L).graph.genus.toNat + 2 ≤ 2 * k) : BrillNoetherGeneral (M.chain L).graph

The equal-period chain corollary following Proposition 6.1. A chain of connected graphs with common k-general transmission is Brill--Noether general whenever its total genus satisfies the corrected natural threshold g + 2 ≤ 2k.