Unwinnability at degree g - 1 and acyclic orientations

For a connected graph G and a divisor D of degree genus G - 1, the main result unwinnable_iff_exists_acyclic_ordiv identifies unwinnability with linear equivalence to ordiv G O for an acyclic orientation O.

The proof assembles the following results from chip-firing-with-lean:

• ordiv, isAcyclic, acyclicWithUniqueSource, orientationToConfig (Orientation.lean:402,221,357,431) — the definitions.
• ordiv_unwinnable (Orientation.lean:666) — acyclic ⟹ ordiv unwinnable. This alone is the reverse implication, after transporting along linearEquiv with winnable_equiv_winnable (Rank.lean:32).
• config_and_divisor_from_O (Orientation.lean:449) and div_of_config_of_div (Config.lean:161) — together they give, for any acyclic O with unique source q, (orientationToConfig G O q hO).chips - oneChip q = ordiv G O (orientation_config_sub_one_chip_eq_ordiv below). This is the bridge from the configuration side back to the orientation divisor.
• maximal_superstable_orientation (Orientation.lean:1186) — every maximal superstable configuration comes from an acyclic orientation with unique source q (Dhar's algorithm, via superstable_dhar at Orientation.lean:1118).
• maximal_unwinnable_char (RRGHelpers.lean:329) — a divisor is maximal unwinnable iff its q-reduced representative has the shape c - q for c the (maximal superstable) q-reduced configuration.
• winnable_of_deg_ge_genus (RRGHelpers.lean:223) — an unwinnable divisor of degree g - 1 is maximal unwinnable, since adding one chip gives degree g and therefore a winnable divisor.
• unique_q_reduced (Basic.lean:1497) — existence and uniqueness of the q-reduced representative, used to recover linearEquiv G D (qReducedRep h_conn q D) (the spec lemma for qReducedRep is private to RRGHelpers.lean, so it is re-derived here in one line from the public unique_q_reduced).

theorem Utilities.exists_acyclic_ordiv_of_unwinnable {G : CFGraph} (h_conn : graphConnected G) (D : CFDiv G) (hUnwin : ¬winnable G D) (hDeg : CFDiv.degree D = G.genus - 1) : ∃ (O : CFOrientation G), isAcyclic G O ∧ linearEquiv G D (ordiv G O)

The hard direction, assembled. An unwinnable divisor of degree genus G - 1 is linearly equivalent to the orientation divisor of some acyclic orientation.

Chain: unwinnable of degree g-1 is maximal unwinnable (winnable_of_deg_ge_genus, the one new step); maximal_unwinnable_char reads off that the q-reduced representative is c - q for c the maximal superstable q-reduced configuration; maximal_superstable_orientation produces an acyclic O with unique source q realizing c; orientation_config_sub_one_chip_eq_ordiv identifies c - q with ordiv G O.

theorem Utilities.unwinnable_of_exists_acyclic_ordiv {G : CFGraph} (D : CFDiv G) (O : CFOrientation G) (hAcyc : isAcyclic G O) (hEquiv : linearEquiv G D (ordiv G O)) : ¬winnable G D

The easy direction. If D is linearly equivalent to the orientation divisor of an acyclic orientation, D is unwinnable. This is ordiv_unwinnable (Orientation.lean:666) transported along linearEquiv by winnable_equiv_winnable (Rank.lean:32).

theorem Utilities.unwinnable_iff_exists_acyclic_ordiv {G : CFGraph} (h_conn : graphConnected G) (D : CFDiv G) (hDeg : CFDiv.degree D = G.genus - 1) : ¬winnable G D ↔ ∃ (O : CFOrientation G), isAcyclic G O ∧ linearEquiv G D (ordiv G O)

T3, combinatorial half. For a connected graph G and a divisor D of degree genus G - 1, D is unwinnable if and only if D is linearly equivalent to ordiv G O for some acyclic orientation O.

Pairs with Utilities.Certificate.ExplicitPotential.onFacet_flipPoint_iff_runsAgainst in OrientationPoint.lean, which reads the same equivalence off the geometric side: a circuit is tight at the orientation's theta witness exactly when the orientation has a directed cycle, i.e. is not acyclic.