Orientability of degree g - 1 divisor classes

An–Baker–Kuperberg–Shokrieh, Canonical representatives for divisor classes on tropical curves and the matrix–tree theorem, calls a divisor D orientable when D(p) = indeg_𝒪(p) - 1 for some orientation 𝒪, and proves in Theorem 4.10 of arXiv:1304.4259v2 that every divisor of degree g - 1 on a finite graph is linearly equivalent to an orientable one. This file proves the finite-multigraph form in orientable_of_deg_eq and orientable_iff_deg_eq.

Parallel edges

CFOrientation is a count_preserving flow-count vector representing an arbitrary edge-level orientation. Parallel edges may therefore be oriented independently, and no simplicity hypothesis is required.

The two halves, and how each is proved

The classes split by winnability, and the two halves are proved by unrelated arguments:

• Unwinnable classes are orientable — by an acyclic orientation. This is orientable_of_not_winnable below, a corollary of unwinnable_iff_exists_acyclic_ordiv (Foundations/AcyclicOrientation.lean). It was the one statement here that never needed simplicity even under the old model, because two parallel edges pointing opposite ways are themselves a directed 2-cycle, so no_bidirectional discarded no acyclic orientation.
• Winnable classes need a cyclic orientation, and are reached by the ABKS route of §3. orientable_of_forall_winnable records the reduction to them, but it is no longer needed for the main theorem: §3 proves all degree-(g−1) classes at once.

The ABKS route, as formalized in §3

The source's argument has two steps, and both are proved here.

1. Hakimi's criterion (\label{thm:orient}, line 744): a divisor of degree g − 1 with χ(S, D) ≥ 0 for every nonempty S is an orientation divisor, where χ(S,D) = deg(D|_S) + |S| − e(S). Here exists_ordiv_eq_of_chi_nonneg.

   ABKS obtain this from max-flow/min-cut. Section 3c takes an elementary route instead: with d v = D v + 1 the target in-degree, orient the edges one at a time (exists_isOrientationOf, induction on the edge multiset), decrementing d at the head. Some direction of the chosen edge always keeps Hakimi's inequality e(S) ≤ ∑_{v ∈ S} d v alive, because a tight set separating b from a and a tight set separating a from b would make the cross term e(S∖T, T∖S) of the submodularity refinement both zero and at least one — the edge ab sits inside it. No flow theory, and no simplicity: CFOrientation is now the edge-level orientation type, so an orientation built edge by edge packages directly.

2. The submodularity descent (\label{thm:eqiv_orient}, line 758): every degree-(g−1) divisor is linearly equivalent to one satisfying (1). Here exists_linear_equiv_chi_nonneg.

   χ(·, D) is submodular, with the quantitative refinement χ(S,D) + χ(T,D) = χ(S∪T,D) + χ(S∩T,D) + e(S∖T, T∖S) (eulerChi_add_eulerChi), so its minimizers are closed under ∩ and ∪ (eulerChi_inter_union_eq_chiMin) and there is a minimal one, chiMinimizer G D (chiMinimizer_subset). Firing its complement raises every χ(S, ·) above χ_D, with equality only for S ⊋ S₀ (chiMin_le_eulerChi_set_firing).

   ABKS then argue that the loop terminates. The formalization replaces the loop by its fixed point: chiPotential = χ_D · (|V| + 1) + |S₀| is bounded above by |V| and strictly increases at each step, so the divisor of greatest potential in the class — which exists by Int.exists_greatest_of_bdd — must already have χ_D ≥ 0. No well-founded recursion is needed.

Everything in §3a–§3b (edgesWithinOf, edgesBetweenOf, numEdgesOf, edgesBetween and their identities) is stated for an arbitrary edge multiset, because step (1) removes edges; G.edges is substituted only at the end.

1. Orientable, and the trivial facts

def Utilities.Orientable (G : CFGraph) (D : CFDiv G) : Prop

A divisor class is orientable when it contains the divisor of some orientation.

This is An–Baker–Kuperberg–Shokrieh's "linearly equivalent to an orientable divisor"; the linear equivalence is built into the predicate because that is the form every consumer wants. Since CFOrientation lost its no_bidirectional field it is the set of edge-level orientations of G, multigraphs included, so this predicate now agrees with ABKS's everywhere and not merely on simple graphs.

Equations

• Utilities.Orientable G D = ∃ (O : CFOrientation G), linearEquiv G D (ordiv G O)

def Utilities.AcyclicallyOrientable (G : CFGraph) (D : CFDiv G) : Prop

The acyclic refinement: the class contains the divisor of an acyclic orientation. By unwinnable_iff_exists_acyclic_ordiv this is exactly unwinnability at degree genus G - 1 (acyclicallyOrientable_iff_not_winnable).

Equations

• Utilities.AcyclicallyOrientable G D = ∃ (O : CFOrientation G), isAcyclic G O ∧ linearEquiv G D (ordiv G O)

theorem Utilities.orientable_ordiv {G : CFGraph} (O : CFOrientation G) : Orientable G (ordiv G O)

An orientation divisor is orientable, tautologically.

theorem Utilities.Orientable.of_linear_equiv {G : CFGraph} {D D' : CFDiv G} (h : linearEquiv G D D') (hD' : Orientable G D') : Orientable G D

Orientability is a property of the linear equivalence class.

theorem Utilities.Orientable.congr {G : CFGraph} {D D' : CFDiv G} (h : linearEquiv G D D') : Orientable G D ↔ Orientable G D'

Orientability transported the other way, so that Orientable is genuinely class-invariant.

theorem Utilities.Orientable.deg_eq {G : CFGraph} {D : CFDiv G} (h : Orientable G D) : CFDiv.degree D = G.genus - 1

An orientable divisor has degree genus G - 1. This is the converse half of the main theorem, and unlike the forward half it is unconditional: it needs neither connectivity nor simplicity, only degree_ordiv.

theorem Utilities.AcyclicallyOrientable.orientable {G : CFGraph} {D : CFDiv G} (h : AcyclicallyOrientable G D) : Orientable G D

An acyclically orientable divisor is orientable.

theorem Utilities.AcyclicallyOrientable.deg_eq {G : CFGraph} {D : CFDiv G} (h : AcyclicallyOrientable G D) : CFDiv.degree D = G.genus - 1

An acyclically orientable divisor has degree genus G - 1.

2. The unwinnable half, which is already done

This section never needed a simplicity hypothesis, even under the old restricted model: no_bidirectional discarded no acyclic orientation, because two parallel edges pointing opposite ways form a directed 2-cycle.

theorem Utilities.acyclicallyOrientable_iff_not_winnable {G : CFGraph} (h_conn : graphConnected G) (D : CFDiv G) (hDeg : CFDiv.degree D = G.genus - 1) : AcyclicallyOrientable G D ↔ ¬winnable G D

Acyclic orientability is unwinnability, at degree genus G - 1. A restatement of unwinnable_iff_exists_acyclic_ordiv (Foundations/AcyclicOrientation.lean, sorry-free) in the vocabulary of this file.

theorem Utilities.orientable_of_not_winnable {G : CFGraph} (h_conn : graphConnected G) (D : CFDiv G) (hDeg : CFDiv.degree D = G.genus - 1) (hUnwin : ¬winnable G D) : Orientable G D

Every unwinnable class of degree genus G - 1 is orientable, by an acyclic orientation.

This is the unwinnable case of ABKS Theorem 4.10, for which a cyclic orientation is never needed. It predates the ABKS route of §3, which now proves every degree-(g−1) class. It is kept because it says more than orientable_of_deg_eq does on unwinnable classes: the witnessing orientation is acyclic.

theorem Utilities.orientable_of_forall_winnable {G : CFGraph} (h_conn : graphConnected G) (hwin : ∀ (D : CFDiv G), CFDiv.degree D = G.genus - 1 → winnable G D → Orientable G D) (D : CFDiv G) (hDeg : CFDiv.degree D = G.genus - 1) : Orientable G D

The decomposition, made explicit. To orient every degree-(g−1) class it suffices to orient the winnable ones; the unwinnable ones are already done by orientable_of_not_winnable.

This was the reduction §2c was attacked through while the winnable case was open; §3 has since closed that case, so the lemma is no longer on the path to orientable_of_deg_eq. It still records why the winnable case was the hard one: such a class is by isAcyclic_iff_not_winnable_ordiv (Foundations/OrientationReversal.lean) never the divisor of an acyclic orientation, so any witness for it must be cyclic, and cyclic orientations were precisely what CFOrientation.no_bidirectional failed to represent on a multigraph.

3. The ABKS route: the Euler characteristic of an induced subgraph

def Utilities.edgesWithin (G : CFGraph) (S : Finset G.V) : ℕ

e(S): the number of edges of G with both endpoints in S, parallel edges counted with multiplicity.

Equations

• Utilities.edgesWithin G S = (Multiset.filter (fun (e : G.V × G.V) => e.1 ∈ S ∧ e.2 ∈ S) G.edges).card

def Utilities.eulerChi (G : CFGraph) (S : Finset G.V) (D : CFDiv G) : ℤ

χ(S, D) = deg(D|_S) + |S| - e(S) — the Euler characteristic of the induced subgraph G[S] shifted by the degree of D restricted to S.

This is An–Baker–Kuperberg–Shokrieh's χ(S,D) (An--Baker--Kuperberg--Shokrieh, arXiv:1304.4259), the function whose submodularity drives the whole proof of §2c.

Equations

• Utilities.eulerChi G S D = ∑ v ∈ S, D v + ↑S.card - ↑(Utilities.edgesWithin G S)

theorem Utilities.eulerChi_univ {G : CFGraph} (D : CFDiv G) : eulerChi G Finset.univ D = CFDiv.degree D - (G.genus - 1)

Sanity check on the definitions, and the reason χ(V,D) = 0 ↔ deg D = g - 1: on the full vertex set, χ measures the deviation of deg D from genus G - 1.

3a. Edge counts, on an arbitrary edge multiset

Hakimi's criterion is proved below by induction on the edge multiset, so both counting functions are introduced for an arbitrary M : Multiset (G.V × G.V) and specialised to G.edges afterwards (edgesWithin_eq, numEdgesOf_edges). Multiset.countP rather than Multiset.card ∘ Multiset.filter is the working form: countP_cons is exactly the induction step, and the whole layer is then arithmetic.

def Utilities.edgesWithinOf {G : CFGraph} (M : Multiset (G.V × G.V)) (S : Finset G.V) : ℕ

e_M(S): the number of edges of the multiset M with both endpoints in S.

Equations

• Utilities.edgesWithinOf M S = Multiset.countP (fun (e : G.V × G.V) => e.1 ∈ S ∧ e.2 ∈ S) M

def Utilities.edgesBetweenOf {G : CFGraph} (M : Multiset (G.V × G.V)) (S T : Finset G.V) : ℕ

e_M(S, T): the number of edges of M with one endpoint in S and the other in T.

Equations

• Utilities.edgesBetweenOf M S T = Multiset.countP (fun (e : G.V × G.V) => e.1 ∈ S ∧ e.2 ∈ T ∨ e.1 ∈ T ∧ e.2 ∈ S) M

def Utilities.numEdgesOf {G : CFGraph} (M : Multiset (G.V × G.V)) (v w : G.V) : ℕ

numEdges on an arbitrary edge multiset.

Equations

• Utilities.numEdgesOf M v w = Multiset.countP (fun (e : G.V × G.V) => e = (v, w) ∨ e = (w, v)) M

theorem Utilities.edgesWithin_eq {G : CFGraph} (S : Finset G.V) : edgesWithin G S = edgesWithinOf G.edges S

e(S) is e_{E(G)}(S).

theorem Utilities.numEdgesOf_edges {G : CFGraph} (v w : G.V) : numEdgesOf G.edges v w = numEdges G v w

numEdges G v w is numEdgesOf G.edges v w.

theorem Utilities.edgesWithinOf_add_edgesWithinOf {G : CFGraph} (M : Multiset (G.V × G.V)) (S T : Finset G.V) : edgesWithinOf M S + edgesWithinOf M T + edgesBetweenOf M (S \ T) (T \ S) = edgesWithinOf M (S ∩ T) + edgesWithinOf M (S ∪ T)

The quantitative refinement of the submodularity of e(·) (Picg_revised.tex:706): e(S) + e(T) + e(S∖T, T∖S) = e(S∩T) + e(S∪T). Proved by induction on the edge multiset; the induction step is a sixteen-case check on which of S, T each endpoint lies in.

theorem Utilities.edgesWithinOf_submodular {G : CFGraph} (M : Multiset (G.V × G.V)) (S T : Finset G.V) : edgesWithinOf M S + edgesWithinOf M T ≤ edgesWithinOf M (S ∩ T) + edgesWithinOf M (S ∪ T)

Submodularity of e_M(·), the inequality form.

theorem Utilities.edgesBetweenOf_comm {G : CFGraph} (M : Multiset (G.V × G.V)) (S T : Finset G.V) : edgesBetweenOf M S T = edgesBetweenOf M T S

e_M(S, T) counts pairs, so it is symmetric.

theorem Utilities.edgesBetweenOf_eq_sum {G : CFGraph} (M : Multiset (G.V × G.V)) {S T : Finset G.V} (hST : Disjoint S T) : edgesBetweenOf M S T = ∑ v ∈ S, ∑ w ∈ T, numEdgesOf M v w

e_M(S,T) as a double sum of edge multiplicities, for disjoint S and T. This is the bridge between the countP form, in which submodularity is proved, and the numEdges form, in which the effect of a set firing is computed.

def Utilities.edgesBetween (G : CFGraph) (S T : Finset G.V) : ℕ

e(S, T), as the double sum of edge multiplicities over S × T. For disjoint S and T this is the number of edges with one end in each (edgesBetweenOf_eq_sum), which is what makes it the right bookkeeping device for a set firing.

Equations

• Utilities.edgesBetween G S T = ∑ v ∈ S, ∑ w ∈ T, numEdges G v w

theorem Utilities.edgesBetween_comm {G : CFGraph} (S T : Finset G.V) : edgesBetween G S T = edgesBetween G T S

edgesBetween is symmetric.

theorem Utilities.edgesBetween_mono_right {G : CFGraph} {S T T' : Finset G.V} (h : T ⊆ T') : edgesBetween G S T ≤ edgesBetween G S T'

edgesBetween is monotone in its second argument.

theorem Utilities.edgesBetweenOf_edges {G : CFGraph} (S T : Finset G.V) (hST : Disjoint S T) : edgesBetweenOf G.edges S T = edgesBetween G S T

The two forms of e(S,T) agree on disjoint sets.

3b. eulerChi is submodular

χ(S,D) = deg(D|_S) + |S| - e(S) with the first two terms modular and -e(·) submodular: ABKS's Lemmas lem:SubmodularLem and lem:EulerLem (Picg_revised.tex:694,704). Everything here is edgesWithinOf_add_edgesWithinOf plus Finset.sum_union_inter and Finset.card_union_add_card_inter.

@[simp]

theorem Utilities.eulerChi_empty {G : CFGraph} (D : CFDiv G) : eulerChi G ∅ D = 0

χ(∅, D) = 0.

theorem Utilities.eulerChi_add_eulerChi {G : CFGraph} (D : CFDiv G) (S T : Finset G.V) : eulerChi G S D + eulerChi G T D = eulerChi G (S ∪ T) D + eulerChi G (S ∩ T) D + ↑(edgesBetweenOf G.edges (S \ T) (T \ S))

The quantitative refinement of submodularity (Picg_revised.tex:706, \label{lem:EulerLem}): χ(S,D) + χ(T,D) = χ(S∪T,D) + χ(S∩T,D) + e(S∖T, T∖S).

theorem Utilities.eulerChi_submodular {G : CFGraph} (D : CFDiv G) (S T : Finset G.V) : eulerChi G (S ∪ T) D + eulerChi G (S ∩ T) D ≤ eulerChi G S D + eulerChi G T D

Submodularity of χ(·, D) (Picg_revised.tex:694, \label{lem:SubmodularLem}).

theorem Utilities.eulerChi_union_of_disjoint {G : CFGraph} (D : CFDiv G) {S T : Finset G.V} (h : Disjoint S T) : eulerChi G (S ∪ T) D = eulerChi G S D + eulerChi G T D - ↑(edgesBetween G S T)

χ on a disjoint union (Picg_revised.tex:710, \eqref{eq:EulerUnion}): χ(S ∪ T, D) = χ(S,D) + χ(T,D) - e(S,T).

3c. Hakimi's criterion, by induction on the edge multiset

The classical proof of \label{thm:orient} goes through max-flow/min-cut. The route taken here is elementary: orient the edges one at a time, maintaining Hakimi's inequality for the remaining multiset. The only thing that has to be checked is that some direction of the chosen edge keeps the inequality, and that is exactly edgesWithinOf_add_edgesWithinOf: if a tight set separated b from a and another tight set separated a from b, the cross term e(S∖T, T∖S) would be both 0 and ≥ 1, the edge ab itself sitting inside it.

Because the induction removes edges, everything is stated for an arbitrary edge multiset; G.edges is substituted only at the very end.

def Utilities.IsOrientationOf {G : CFGraph} (M N : Multiset (G.V × G.V)) (d : G.V → ℕ) : Prop

N orients the edge multiset M with in-degree function d: every parallel class of M is split between the two directions, and d v edges of N point at v. Unfolded, this is exactly CFOrientation.count_preserving together with indeg = d.

Equations

• One or more equations did not get rendered due to their size.

theorem Utilities.edgesWithinOf_singleton {G : CFGraph} {M : Multiset (G.V × G.V)} (hloop : ∀ (v : G.V), (v, v) ∉ M) (v : G.V) : edgesWithinOf M {v} = 0

A loopless multiset has no edge inside a singleton.

theorem Utilities.exists_isOrientationOf {G : CFGraph} (n : ℕ) (M : Multiset (G.V × G.V)) : M.card = n → (∀ (v : G.V), (v, v) ∉ M) → ∀ (d : G.V → ℕ), ∑ v : G.V, d v = M.card → (∀ (S : Finset G.V), edgesWithinOf M S ≤ ∑ v ∈ S, d v) → ∃ (N : Multiset (G.V × G.V)), IsOrientationOf M N d

Hakimi's criterion for an arbitrary edge multiset. If d sums to the number of edges and dominates e_M(S) on every vertex set, then M has an orientation with in-degree function d. The induction is on the number of edges.

theorem Utilities.exists_ordiv_eq_of_chi_nonneg {G : CFGraph} (D : CFDiv G) (hDeg : CFDiv.degree D = G.genus - 1) (hchi : ∀ (S : Finset G.V), S.Nonempty → 0 ≤ eulerChi G S D) : ∃ (O : CFOrientation G), D = ordiv G O

Hakimi's criterion (Picg_revised.tex:744, \label{thm:orient}): a divisor of degree genus G - 1 all of whose χ(S, ·) are nonnegative is an orientation divisor — on the nose, not merely up to linear equivalence.

No simplicity hypothesis, since 2026-08-20. This is where the old model defect lived and where the hypothesis was consumed: the classical statement produces an edge-level orientation, and packaging one as a CFOrientation used to require that no parallel class be split — on the 5-banana the divisor (1, 2) satisfies the criterion and was not ordiv of any CFOrientation. With no_bidirectional removed, CFOrientation is the edge-level orientation type, (1, 2) is realised, and the classical statement transcribes verbatim.

ABKS cite Hakimi, Schrijver Thm 61.1 and Backman Thm 7.3, and note that the statement is equivalent to max-flow/min-cut; no flow theory is used here. The proof is exists_isOrientationOf, the edge-by-edge greedy orientation, applied to G.edges with target in-degree d v = D v + 1. The hypothesis enters twice: at S = {v} it says D v + 1 ≥ 0, so d is a well-defined natural number, and at general S it is exactly Hakimi's inequality e(S) ≤ ∑_{v ∈ S} d v. deg D = genus G - 1 is what makes ∑ d the number of edges.

3d. Firing a set of vertices, seen by eulerChi

Two formulas, both instances of "chips cross the boundary of the fired set once per edge": firing A adds e(A, T) to χ(T, ·) when T misses A, and subtracts e(Aᶜ, T) when T sits inside A. Everything below uses only these two.

theorem Utilities.linear_equiv_set_firing {G : CFGraph} (D : CFDiv G) (A : Finset G.V) : linearEquiv G D (setFiring G D A)

Firing a set is a linear equivalence: setFiring G D A - D is the sum of the firing vectors of the members of A, hence principal.

theorem Utilities.sum_set_firing_of_disjoint {G : CFGraph} (D : CFDiv G) {A T : Finset G.V} (h : Disjoint T A) : ∑ w ∈ T, setFiring G D A w = ∑ w ∈ T, D w + ↑(edgesBetween G A T)

Firing A seen from outside A: every edge from A to T sends one chip.

theorem Utilities.sum_set_firing_of_subset {G : CFGraph} (D : CFDiv G) {A T : Finset G.V} (h : T ⊆ A) : ∑ w ∈ T, setFiring G D A w = ∑ w ∈ T, D w - ↑(edgesBetween G Aᶜ T)

Firing A seen from inside A: every edge from T to the outside of A loses one chip.

theorem Utilities.eulerChi_set_firing_of_disjoint {G : CFGraph} (D : CFDiv G) {A T : Finset G.V} (h : Disjoint T A) : eulerChi G T (setFiring G D A) = eulerChi G T D + ↑(edgesBetween G A T)

χ(T, ·) after firing A, for T disjoint from A.

theorem Utilities.eulerChi_set_firing_of_subset {G : CFGraph} (D : CFDiv G) {A T : Finset G.V} (h : T ⊆ A) : eulerChi G T (setFiring G D A) = eulerChi G T D - ↑(edgesBetween G Aᶜ T)

χ(T, ·) after firing A, for T inside A.

3e. The minimum of χ(·, D) and its minimal minimizer

noncomputable def Utilities.chiMin (G : CFGraph) (D : CFDiv G) : ℤ

χ_D, the minimum of χ(S, D) over all vertex sets. Including ∅ (where χ = 0) and V costs nothing and removes a side condition: χ_D ≤ 0 always, and at degree genus G - 1 both of those sets have χ = 0, so a negative minimum is automatically attained at a proper nonempty set.

Equations

• Utilities.chiMin G D = Finset.univ.inf' ⋯ fun (S : Finset G.V) => Utilities.eulerChi G S D

theorem Utilities.chiMin_le {G : CFGraph} (D : CFDiv G) (S : Finset G.V) : chiMin G D ≤ eulerChi G S D

χ_D is a lower bound.

theorem Utilities.exists_eulerChi_eq_chiMin {G : CFGraph} (D : CFDiv G) : ∃ (S : Finset G.V), eulerChi G S D = chiMin G D

χ_D is attained.

theorem Utilities.chiMin_nonpos {G : CFGraph} (D : CFDiv G) : chiMin G D ≤ 0

χ_D ≤ 0, because χ(∅, D) = 0.

theorem Utilities.eulerChi_inter_union_eq_chiMin {G : CFGraph} (D : CFDiv G) {S T : Finset G.V} (hS : eulerChi G S D = chiMin G D) (hT : eulerChi G T D = chiMin G D) : eulerChi G (S ∩ T) D = chiMin G D ∧ eulerChi G (S ∪ T) D = chiMin G D

The minimizers of χ(·, D) are closed under ∩ and ∪ (Picg_revised.tex:696, \label{lem:intersection}), by the quantitative refinement: the cross term is a nonnegative integer and both new values are ≥ χ_D, so all three inequalities are equalities.

noncomputable def Utilities.chiMinimizer (G : CFGraph) (D : CFDiv G) : Finset G.V

S₀(D), the minimal minimizer of χ(·, D) (Picg_revised.tex:730, \label{cor:minimal1}). Defined as a minimizer of least cardinality; chiMinimizer_subset shows it is contained in every other minimizer, which is what makes it the minimal one.

Equations

• Utilities.chiMinimizer G D = Classical.choose ⋯

theorem Utilities.chiMinimizer_eq {G : CFGraph} (D : CFDiv G) : eulerChi G (chiMinimizer G D) D = chiMin G D

S₀(D) is a minimizer.

theorem Utilities.chiMinimizer_subset {G : CFGraph} (D : CFDiv G) {T : Finset G.V} (hT : eulerChi G T D = chiMin G D) : chiMinimizer G D ⊆ T

S₀(D) is contained in every minimizer.

3f. One descent step

ABKS's Claim (Picg_revised.tex:772): firing the complement of S₀(D) produces a divisor whose χ is everywhere ≥ χ_D, with equality only on sets strictly containing S₀(D). The proof below merges their four cases into two — S ⊆ S₀ and S ⊄ S₀ — which is legitimate because the empty intersection is not a special case once χ(∅, ·) = 0 ≥ χ_D is available.

noncomputable def Utilities.chiPotential (G : CFGraph) (D : CFDiv G) : ℤ

The termination measure: χ_D weighted so that a unit gain in the minimum beats any change in |S₀(D)|, plus |S₀(D)| itself. It is bounded above by |V| (as χ_D ≤ 0 and |S₀| ≤ |V|) and strictly increases at every descent step, which is why the descent stops.

Equations

• Utilities.chiPotential G D = Utilities.chiMin G D * (↑(Fintype.card G.V) + 1) + ↑(Utilities.chiMinimizer G D).card

theorem Utilities.chiPotential_le {G : CFGraph} (D : CFDiv G) : chiPotential G D ≤ ↑(Fintype.card G.V)

The potential is bounded above by |V|.

theorem Utilities.exists_linear_equiv_chi_nonneg {G : CFGraph} (h_conn : graphConnected G) (D : CFDiv G) (hDeg : CFDiv.degree D = G.genus - 1) : ∃ (D' : CFDiv G), linearEquiv G D D' ∧ ∀ (S : Finset G.V), S.Nonempty → 0 ≤ eulerChi G S D'

The submodularity descent (Picg_revised.tex:758, \label{thm:eqiv_orient}): every divisor of degree genus G - 1 is linearly equivalent to one satisfying Hakimi's criterion.

No simplicity hypothesis: this step never mentions orientations, only eulerChi and set firing.

ABKS run the descent as a loop and argue that it terminates. Here the loop is replaced by its fixed point: chiPotential is bounded above by |V|, so among all divisors in the class there is one of greatest potential (Int.exists_greatest_of_bdd), and chiPotential_lt says that a divisor with χ_D < 0 is never of greatest potential. Hence the maximiser has χ_D ≥ 0, which is Hakimi's criterion.

4. The main statement

theorem Utilities.orientable_of_deg_eq {G : CFGraph} (h_conn : graphConnected G) (D : CFDiv G) (hDeg : CFDiv.degree D = G.genus - 1) : Orientable G D

ABKS Theorem 4.10 (arXiv:1304.4259v2). On a connected graph, simple or not, every divisor of degree genus G - 1 is linearly equivalent to ordiv G O for some orientation O.

The simplicity hypothesis this theorem used to carry (it was called orientable_of_deg_eq_of_simple) was an artefact of CFOrientation.no_bidirectional and has been deleted with it; see the module docstring.

Proved by composing the two halves of the ABKS route: exists_linear_equiv_chi_nonneg (the submodularity descent) moves the class to a representative satisfying Hakimi's criterion, and exists_ordiv_eq_of_chi_nonneg (Hakimi) turns that representative into an orientation on the nose. The unwinnable case also has an independent proof with an acyclic witness — see orientable_of_not_winnable.

theorem Utilities.orientable_iff_deg_eq {G : CFGraph} (h_conn : graphConnected G) (D : CFDiv G) : Orientable G D ↔ CFDiv.degree D = G.genus - 1

§2c as a biconditional. On a connected graph the orientable divisors are exactly the divisors of degree genus G - 1. The → direction is unconditional (Orientable.deg_eq); only ← needs connectivity.