A cut criterion for reduced divisors

The paper's SameStrand argument is a reduced-divisor argument. This lemma packages the only finite-set calculation it needs: a strict total chip versus boundary inequality produces the pointwise witness required by qReduced.

theorem Bananas.q_reduced_of_sum_lt_cut (G : CFGraph) (q : G.V) (D : CFDiv G) (hEff : qEffective q D) (hCut : ∀ S ⊆ {x : G.V | x ≠ q}, S.Nonempty → ∑ v ∈ S, D v < ∑ v ∈ S, ∑ w : G.V with w ∉ S, ↑(numEdges G v w)) : qReduced G q D

A q-effective divisor is q-reduced if every nonempty set avoiding q carries strictly fewer total chips than its outgoing edge multiplicity.

theorem Bananas.q_reduced_two_chip_sub_of_cut_bounds (G : CFGraph) (q x y : G.V) (hqx : q ≠ x) (hqy : q ≠ y) (hTwo : ∀ S ⊆ {x : G.V | x ≠ q}, S.Nonempty → 2 ≤ ∑ v ∈ S, ∑ w : G.V with w ∉ S, ↑(numEdges G v w)) (hThree : ∀ S ⊆ {x : G.V | x ≠ q}, x ∈ S → y ∈ S → 3 ≤ ∑ v ∈ S, ∑ w : G.V with w ∉ S, ↑(numEdges G v w)) : qReduced G q (oneChip x + oneChip y - oneChip q)

A two-chip divisor with one chip of debt at q is reduced as soon as all cuts have size at least two and the only cuts which contain both chips have size at least three. This is the exact cut-theoretic form of the remaining case split in the paper's SameStrand lemma.

theorem Bananas.q_reduced_two_chip_sub_of_twoEdgeCutCondition (G : CFGraph) (q x y : G.V) (hqx : q ≠ x) (hqy : q ≠ y) (hTwoEdge : Utilities.TwoEdgeCutCondition G) (hThree : ∀ S ⊆ {x : G.V | x ≠ q}, x ∈ S → y ∈ S → 3 ≤ ∑ v ∈ S, ∑ w : G.V with w ∉ S, ↑(numEdges G v w)) : qReduced G q (oneChip x + oneChip y - oneChip q)

The uniform part of the preceding cut hypothesis is automatic on a bridgeless graph. This wrapper is useful for banana graphs, where TwoEdgeCutCondition is inherited from their parallel-edge core and only the exceptional cuts containing both chips require further geometric analysis.