Arithmetic balancing cuts for mixed-torsion chains

The prefix genus of a chain is nondecreasing and its suffix genus is nonincreasing. For a chain with at least two positive-genus factors, the prefix is strictly smaller than the suffix at the first factor, while the reverse strict inequality holds at the last factor. The first crossing therefore gives a nonempty split satisfying ChainDominatesAtSplit.

This is the finite arithmetic step used in the proof of Corollary 6.16(2). Genus-zero factors are deliberately handled separately by ZeroGenusWedge: strict positivity is used here only to keep both sides of the balancing cut nonempty.

Monotonicity of prefix and suffix genus

theorem Bananas.chainFactorGenus_nonneg (L : List KGeneralChainFactor) : 0 ≤ chainFactorGenus L

@[simp]

theorem Bananas.chainFactorGenus_append (L R : List KGeneralChainFactor) : chainFactorGenus (L ++ R) = chainFactorGenus L + chainFactorGenus R

theorem Bananas.chainFactorGenus_take_mono (L : List KGeneralChainFactor) {i j : ℕ} (hij : i ≤ j) : chainFactorGenus (List.take i L) ≤ chainFactorGenus (List.take j L)

Prefix genus is monotone in the prefix length.

theorem Bananas.chainFactorGenus_drop_anti (L : List KGeneralChainFactor) {i j : ℕ} (hij : i ≤ j) : chainFactorGenus (List.drop j L) ≤ chainFactorGenus (List.drop i L)

Suffix genus is antitone in the number of discarded factors.

The first crossing

theorem Bananas.chain_last_suffix_le_prefix (L : List KGeneralChainFactor) (hL : L ≠ []) : chainFactorGenus (List.drop (L.length - 1) L) ≤ chainFactorGenus (List.take (L.length - 1 + 1) L)

At the last factor, suffix genus is at most prefix genus.

theorem Bananas.first_prefix_lt_suffix_of_positive_tail (F next : KGeneralChainFactor) (rest : List KGeneralChainFactor) (hPositive : ∀ Q ∈ next :: rest, 0 < Q.marked.graph.genus) : chainFactorGenus (List.take 1 (F :: next :: rest)) < chainFactorGenus (List.drop 0 (F :: next :: rest))

The first factor's prefix genus is strictly smaller than its suffix genus when a positive-genus tail is present.

def Bananas.GenusCrossed (L : List KGeneralChainFactor) (i : ℕ) : Prop

The prefix and suffix genus functions have crossed at i.

Equations

• Bananas.GenusCrossed L i = (Bananas.chainFactorGenus (List.drop i L) ≤ Bananas.chainFactorGenus (List.take (i + 1) L))

theorem Bananas.exists_genusCrossed (L : List KGeneralChainFactor) (hL : L ≠ []) : ∃ (i : ℕ), GenusCrossed L i

noncomputable def Bananas.firstGenusCrossing (L : List KGeneralChainFactor) (hL : L ≠ []) : ℕ

The first index at which suffix genus is no larger than prefix genus. It exists for every nonempty chain by the last-factor inequality.

Equations

• Bananas.firstGenusCrossing L hL = Nat.find ⋯

theorem Bananas.firstGenusCrossing_spec (L : List KGeneralChainFactor) (hL : L ≠ []) : chainFactorGenus (List.drop (firstGenusCrossing L hL) L) ≤ chainFactorGenus (List.take (firstGenusCrossing L hL + 1) L)

theorem Bananas.firstGenusCrossing_lt_length (L : List KGeneralChainFactor) (hL : L ≠ []) : firstGenusCrossing L hL < L.length

theorem Bananas.prefix_le_suffix_before_firstGenusCrossing (L : List KGeneralChainFactor) (hL : L ≠ []) {i : ℕ} (hi : i < firstGenusCrossing L hL) : chainFactorGenus (List.take (i + 1) L) ≤ chainFactorGenus (List.drop i L)

Before the first crossing, prefix genus is no larger than suffix genus.

theorem Bananas.suffix_le_prefix_from_firstGenusCrossing (L : List KGeneralChainFactor) (hL : L ≠ []) {i : ℕ} (hi : firstGenusCrossing L hL ≤ i) : chainFactorGenus (List.drop i L) ≤ chainFactorGenus (List.take (i + 1) L)

From the first crossing onward, suffix genus remains no larger than prefix genus.

theorem Bananas.firstGenusCrossing_pos_of_positive_tail (F next : KGeneralChainFactor) (rest : List KGeneralChainFactor) (hPositive : ∀ Q ∈ next :: rest, 0 < Q.marked.graph.genus) : 0 < firstGenusCrossing (F :: next :: rest) ⋯

Positivity forces the first crossing to occur after the initial factor.

A nonempty dominating split

theorem Bananas.exists_chainDominatesAtSplit_of_positive (F next : KGeneralChainFactor) (rest : List KGeneralChainFactor) (hPositive : ∀ Q ∈ F :: next :: rest, 0 < Q.marked.graph.genus) : ∃ (leftHead : KGeneralChainFactor) (leftTail : List KGeneralChainFactor) (rightHead : KGeneralChainFactor) (rightTail : List KGeneralChainFactor), F :: next :: rest = leftHead :: leftTail ++ rightHead :: rightTail ∧ ChainDominatesAtSplit (leftHead :: leftTail) (rightHead :: rightTail)

Every chain of at least two positive-genus factors admits a nonempty crossing split. The split is canonical: take the first genus crossing.

theorem Bananas.exists_chainDominatesAtSplit_of_firstCrossing_pos (F next : KGeneralChainFactor) (rest : List KGeneralChainFactor) (hCrossingPos : 0 < firstGenusCrossing (F :: next :: rest) ⋯) : ∃ (leftHead : KGeneralChainFactor) (leftTail : List KGeneralChainFactor) (rightHead : KGeneralChainFactor) (rightTail : List KGeneralChainFactor), F :: next :: rest = leftHead :: leftTail ++ rightHead :: rightTail ∧ ChainDominatesAtSplit (leftHead :: leftTail) (rightHead :: rightTail)

If the canonical first crossing is nonzero, it gives a nonempty dominating split without any positivity assumption on the individual factors. Positivity above is only one sufficient condition for the crossing to be nonzero; the zero-crossing case is handled separately in the final form of Corollary 6.16(2).

theorem Bananas.exists_chainBalancedAtSplit_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)) : ∃ (leftHead : KGeneralChainFactor) (leftTail : List KGeneralChainFactor) (rightHead : KGeneralChainFactor) (rightTail : List KGeneralChainFactor), F :: next :: rest = leftHead :: leftTail ++ rightHead :: rightTail ∧ ChainBalancedAtSplit (leftHead :: leftTail) (rightHead :: rightTail)

The paper's minimum budget therefore yields a nonempty balanced split for every chain of at least two positive-genus factors.

Removing a zero-genus leading factor

theorem Bananas.chainMinBudget_tail_of_head_genus_zero (F next : KGeneralChainFactor) (rest : List KGeneralChainFactor) (hZero : F.marked.graph.genus = 0) (hMin : ChainMinBudget (F :: next :: rest)) : ChainMinBudget (next :: rest)

If the first factor has genus zero, the paper's minimum-budget condition restricts to the remaining nonempty tail without change.

theorem Bananas.genus_eq_zero_of_mem_of_chainFactorGenus_eq_zero (L : List KGeneralChainFactor) (hSum : chainFactorGenus L = 0) (F : KGeneralChainFactor) (hMem : F ∈ L) : F.marked.graph.genus = 0

If the total genus of a factor list is zero, every member has genus zero. Connectivity of each bundled factor supplies nonnegativity.