Genus-one rigid wedges

This module isolates the cycle-ready consequence of the exact wedge winnability convolution. The rigidity condition is deliberately explicit: it is not asserted for every genus-one graph.

structure Utilities.PointedGenusOneRigid (H : CFGraph) (y : H.V) : Prop

A pointed genus-one graph for which no other vertex is linearly equivalent to the marked point in degree zero.

• connected : graphConnected H
• genus_one : H.genus = 1
• exists_ne : ∃ (p : H.V), p ≠ y
• nontrivial (p : H.V) : p ≠ y → ¬linearEquiv H (oneChip y - oneChip p) 0

theorem Utilities.linear_equiv_zero_of_winnable_deg_zero (K : CFGraph) (A : CFDiv K) (hWin : winnable K A) (hDeg : CFDiv.degree A = 0) : linearEquiv K A 0

A winnable divisor of degree zero is linearly equivalent to zero.

@[simp]

theorem Utilities.wedgeLiftLeftDivisor_eq_wedgeAdd (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) : wedgeLiftLeftDivisor G H x y D = wedgeAddDivisor G H x y D 0

The left-supported divisor is definitionally the wedge sum with zero on the right factor.

theorem Utilities.deg_nonneg_of_winnable (K : CFGraph) (A : CFDiv K) (hWin : winnable K A) : 0 ≤ CFDiv.degree A

Winnability forces nonnegative degree.

theorem Utilities.effective_marked_pile_of_nonneg (K : CFGraph) (q : K.V) (t : ℤ) (ht : 0 ≤ t) : effective (t • oneChip q)

A nonnegative integral pile of chips at one vertex is effective.

theorem Utilities.winnable_chipShift_mono (K : CFGraph) (A : CFDiv K) (q : K.V) {s t : ℤ} (hst : s ≤ t) (hWin : winnable K (chipShift K A q s)) : winnable K (chipShift K A q t)

Adding chips at one marked vertex preserves winnability.

theorem Utilities.wedgeLiftLeft_sub_left (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (a : G.V) : wedgeLiftLeftDivisor G H x y D - oneChip (Sum.inl a) = wedgeAddDivisor G H x y (D - oneChip a) 0

Subtracting a left-factor chip from a left-supported wedge divisor stays entirely on the left factor.

theorem Utilities.wedgeLiftLeft_sub_right (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (p : { z : H.V // z ≠ y }) : wedgeLiftLeftDivisor G H x y D - oneChip (Sum.inr p) = wedgeAddDivisor G H x y D (-oneChip ↑p)

Subtracting a non-marked right-factor chip from a left-supported wedge divisor puts exactly its negative on the right factor.

theorem Utilities.rank_wedgeLiftLeft_ge_one_iff (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (hH : PointedGenusOneRigid H y) (D : CFDiv G) : rank (vertexWedge G H x y) (wedgeLiftLeftDivisor G H x y D) ≥ 1 ↔ rank G D ≥ 1 ∧ winnable G (D - 2 • oneChip x)

Exact rank-one criterion for attaching a pointed rigid genus-one block. For a genuine subdivided cycle, the remaining input is precisely the familiar fact that distinct vertices have distinct degree-one divisor classes.