Degree-one rigidity from two-edge-connected cuts

For the pointed genus-one wedge argument, the remaining cycle input is that distinct vertices determine distinct degree-one divisor classes. This file proves a graph-level sufficient condition: every nonempty proper vertex cut has total outgoing multiplicity at least two.

If (y) - (p) were principal, choose the maximum level set of a firing script with principal divisor (p) - (y). The vertex p cannot lie in that set. At every other maximum except possibly y, the level-set inequality forces out-degree zero; at y it forces out-degree at most one. Thus the whole cut has size at most one, contradicting the hypothesis.

def Utilities.cutMultiplicity (H : CFGraph) (S : Finset H.V) : ℤ

Total edge multiplicity crossing from S to its complement, counted at the endpoint in S.

Equations

• Utilities.cutMultiplicity H S = ∑ v ∈ S, outdegreeSet H S v

def Utilities.TwoEdgeCutCondition (H : CFGraph) : Prop

Every nonempty proper vertex set has at least two outgoing edges, counted with multiplicity. For a connected loopless multigraph this is the usual absence of bridges.

Equations

• Utilities.TwoEdgeCutCondition H = ∀ (S : Finset H.V), S.Nonempty → S ≠ Finset.univ → 2 ≤ Utilities.cutMultiplicity H S

@[simp]

theorem Utilities.cutMultiplicity_singleton (H : CFGraph) (v : H.V) : cutMultiplicity H {v} = vertexDegree H v

The cut leaving a singleton has multiplicity equal to the valence of its unique vertex.

theorem Utilities.vertex_degree_ne_one_of_twoEdgeCutCondition {H : CFGraph} (hCut : TwoEdgeCutCondition H) (v : H.V) : vertexDegree H v ≠ 1

A graph satisfying the two-edge cut condition has no degree-one vertices.

theorem Utilities.cutMultiplicity_nonneg (H : CFGraph) (S : Finset H.V) : 0 ≤ cutMultiplicity H S

theorem Utilities.outdeg_S_topSet_eq_zero_of_prin_eq_zero {H : CFGraph} {g : firingScript H} {v : H.V} (hv : v ∈ topSet g) (hPrin : (prin H) g v = 0) : outdegreeSet H (topSet g) v = 0

A maximum-level vertex whose principal coefficient is zero has no edge leaving the maximum-level set.

theorem Utilities.outdeg_S_topSet_le_one_of_prin_eq_neg_one {H : CFGraph} {g : firingScript H} {v : H.V} (hv : v ∈ topSet g) (hPrin : (prin H) g v = -1) : outdegreeSet H (topSet g) v ≤ 1

A maximum-level vertex with principal coefficient -1 has at most one edge leaving the maximum-level set.

theorem Utilities.not_linear_equiv_one_chip_sub_of_twoEdgeCutCondition {H : CFGraph} (_hConnected : graphConnected H) (hCut : TwoEdgeCutCondition H) {p y : H.V} (hpy : p ≠ y) : ¬linearEquiv H (oneChip y - oneChip p) 0

Distinct vertices cannot be linearly equivalent in degree one when every proper cut has multiplicity at least two. Connectedness is retained in the interface expected by the genus-one application; the cut hypothesis already contains the part of connectedness used by this extremal-set proof.

theorem Utilities.pointedGenusOneRigid_of_twoEdgeCutCondition {H : CFGraph} (y : H.V) (hConnected : graphConnected H) (hGenus : H.genus = 1) (hExists : ∃ (p : H.V), p ≠ y) (hCut : TwoEdgeCutCondition H) : PointedGenusOneRigid H y

A connected genus-one graph with a second vertex and no one-edge cut is a pointed rigid genus-one block.