Documentation

TauCeti.Combinatorics.Network.Hoffman

Hoffman's feasibility theorem #

An assignment between signed lower and upper bounds with prescribed excess exists precisely when the prescribed excess is balanced and every vertex set satisfies the corresponding cut inequality. The result includes additive-subgroup integrality and strict cut certificates of infeasibility.

The auxiliary-terminal reduction first subtracts the lower bound. For nonnegative capacities and prescribed excess b, the fresh source supplies max (-b v) 0 to each vertex and each vertex sends max (b v) 0 to the fresh sink. A flow of the required value saturates both families of new arrows. The construction retains every original arrow, including parallel arrows and loops.

References #

source
def TauCeti.excessCapacity {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [AddCommGroup K] [LinearOrder K] (cap : Assignment Q K) (b : V → K) :
Assignment (AuxTerminalHom Q Finset.univ Finset.univ) K

Capacities for the auxiliary-terminal reduction of prescribed excess with zero lower bounds. The source supplies the negative part of b, and the sink receives its positive part.

Instances For
    source
    theorem TauCeti.excessCapacity_nonneg {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [AddCommGroup K] [LinearOrder K] {cap : Assignment Q K} (hcap : 0 ≤ cap) (b : V → K) :
    0 ≤ excessCapacity cap b

    The auxiliary capacities are nonnegative when the original capacities are.

    source
    @[simp]
    theorem TauCeti.excessCapacity_original {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [AddCommGroup K] [LinearOrder K] (cap : Assignment Q K) (b : V → K) {x y : V} (e : Q x y) :
    excessCapacity cap b (AuxTerminalHom.original e) = cap e
    source
    @[simp]
    theorem TauCeti.excessCapacity_source {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [AddCommGroup K] [LinearOrder K] (cap : Assignment Q K) (b : V → K) (x : V) :
    excessCapacity cap b (AuxTerminalHom.source ⋯) = max (-b x) 0
    source
    @[simp]
    theorem TauCeti.excessCapacity_sink {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [AddCommGroup K] [LinearOrder K] (cap : Assignment Q K) (b : V → K) (x : V) :
    excessCapacity cap b (AuxTerminalHom.sink ⋯) = max (b x) 0
    source
    theorem TauCeti.excessCapacity_mem {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [AddCommGroup K] [LinearOrder K] {cap : Assignment Q K} {b : V → K} (H : AddSubgroup K) (hcap : ∀ ⦃x y : V⦄ (e : Q x y), cap e ∈ H) (hb : ∀ (v : V), b v ∈ H) ⦃x y : V ⊕ Bool⦄ (e : AuxTerminalHom Q Finset.univ Finset.univ x y) :
    excessCapacity cap b e ∈ H

    The auxiliary capacities preserve an additive subgroup containing capacities and excesses.

    source
    def TauCeti.ExcessFlow.toAuxFlow {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] [DecidableEq V] {cap : Assignment Q K} {b : V → K} (f : ExcessFlow 0 cap b) :
    Flow (excessCapacity cap b) (Sum.inr false) (Sum.inr true)

    Extend a zero-lower-bound prescribed-excess assignment to an ordinary auxiliary flow. Both auxiliary arrows at each original vertex are saturated.

    Instances For
      source
      @[simp]
      theorem TauCeti.ExcessFlow.toAuxFlow_original {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] [DecidableEq V] {cap : Assignment Q K} {b : V → K} (f : ExcessFlow 0 cap b) {x y : V} (e : Q x y) :
      f.toAuxFlow.toFun (AuxTerminalHom.original e) = ↑f e
      source
      @[simp]
      theorem TauCeti.ExcessFlow.toAuxFlow_source {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] [DecidableEq V] {cap : Assignment Q K} {b : V → K} (f : ExcessFlow 0 cap b) (x : V) :
      f.toAuxFlow.toFun (AuxTerminalHom.source ⋯) = max (-b x) 0
      source
      @[simp]
      theorem TauCeti.ExcessFlow.toAuxFlow_sink {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] [DecidableEq V] {cap : Assignment Q K} {b : V → K} (f : ExcessFlow 0 cap b) (x : V) :
      f.toAuxFlow.toFun (AuxTerminalHom.sink ⋯) = max (b x) 0
      source
      @[simp]
      theorem TauCeti.ExcessFlow.val_toAuxFlow {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] [DecidableEq V] {cap : Assignment Q K} {b : V → K} (f : ExcessFlow 0 cap b) :
      f.toAuxFlow.val = ∑ v : V, max (b v) 0

      The auxiliary flow has the total positive prescribed excess as its value.

      source
      theorem TauCeti.ExcessFlow.toAuxFlow_mem_iff {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] [DecidableEq V] {cap : Assignment Q K} {b : V → K} (f : ExcessFlow 0 cap b) (H : AddSubgroup K) (hb : ∀ (v : V), b v ∈ H) :
      (∀ ⦃x y : V ⊕ Bool⦄ (e : AuxTerminalHom Q Finset.univ Finset.univ x y), f.toAuxFlow.toFun e ∈ H) ↔ ∀ ⦃x y : V⦄ (e : Q x y), ↑f e ∈ H

      Extending a prescribed-excess assignment preserves subgroup values in both directions.

      source
      theorem TauCeti.Flow.val_le_sum_max {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] [DecidableEq V] {cap : Assignment Q K} {b : V → K} (g : Flow (excessCapacity cap b) (Sum.inr false) (Sum.inr true)) :
      g.val ≤ ∑ v : V, max (b v) 0

      The value of an auxiliary flow is bounded by the total positive prescribed excess.

      source
      theorem TauCeti.Flow.sink_eq_of_val_eq_sum_max {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] [DecidableEq V] {cap : Assignment Q K} {b : V → K} (g : Flow (excessCapacity cap b) (Sum.inr false) (Sum.inr true)) (hg : g.val = ∑ v : V, max (b v) 0) (v : V) :
      g.toFun (AuxTerminalHom.sink ⋯) = max (b v) 0

      At the required value every arrow to the fresh sink is saturated.

      source
      theorem TauCeti.Flow.source_eq_of_val_eq_sum_max {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] [DecidableEq V] {cap : Assignment Q K} {b : V → K} (g : Flow (excessCapacity cap b) (Sum.inr false) (Sum.inr true)) (hb : ∑ v : V, b v = 0) (hg : g.val = ∑ v : V, max (b v) 0) (v : V) :
      g.toFun (AuxTerminalHom.source ⋯) = max (-b v) 0

      For balanced excess, the required value saturates every arrow from the fresh source.

      source
      theorem TauCeti.Flow.val_eq_sum_max_iff {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] [DecidableEq V] {cap : Assignment Q K} {b : V → K} (g : Flow (excessCapacity cap b) (Sum.inr false) (Sum.inr true)) (hb : ∑ v : V, b v = 0) :
      g.val = ∑ v : V, max (b v) 0 ↔ (∀ (v : V), g.toFun (AuxTerminalHom.source ⋯) = max (-b v) 0) ∧ ∀ (v : V), g.toFun (AuxTerminalHom.sink ⋯) = max (b v) 0

      For balanced excess, an auxiliary flow has the required value exactly when both families of auxiliary arrows are saturated.

      source
      def TauCeti.Flow.toExcessFlow {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] [DecidableEq V] {cap : Assignment Q K} {b : V → K} (g : Flow (excessCapacity cap b) (Sum.inr false) (Sum.inr true)) (hb : ∑ v : V, b v = 0) (hg : g.val = ∑ v : V, max (b v) 0) :
      ExcessFlow 0 cap b

      Restricting a balanced auxiliary flow of the required value realizes its prescribed excess.

      Instances For
        source
        @[simp]
        theorem TauCeti.Flow.toExcessFlow_apply {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] [DecidableEq V] {cap : Assignment Q K} {b : V → K} (g : Flow (excessCapacity cap b) (Sum.inr false) (Sum.inr true)) (hb : ∑ v : V, b v = 0) (hg : g.val = ∑ v : V, max (b v) 0) {x y : V} (e : Q x y) :
        ↑(g.toExcessFlow hb hg) e = g.toFun (AuxTerminalHom.original e)
        source
        def TauCeti.ExcessFlow.zeroAuxFlowEquiv {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] [DecidableEq V] {b : V → K} {cap : Assignment Q K} (hb : ∑ v : V, b v = 0) :
        ExcessFlow 0 cap b ≃ { g : Flow (excessCapacity cap b) (Sum.inr false) (Sum.inr true) // g.val = ∑ v : V, max (b v) 0 }

        Realizing prescribed excess is equivalent to an ordinary auxiliary flow of the required value. Restriction and extension preserve all original arrow values.

        Instances For
          source
          @[simp]
          theorem TauCeti.ExcessFlow.zeroAuxFlowEquiv_apply_val {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] [DecidableEq V] {b : V → K} {cap : Assignment Q K} (hb : ∑ v : V, b v = 0) (f : ExcessFlow 0 cap b) :
          ↑((zeroAuxFlowEquiv hb) f) = f.toAuxFlow
          source
          @[simp]
          theorem TauCeti.ExcessFlow.zeroAuxFlowEquiv_symm_apply {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] [DecidableEq V] {b : V → K} {cap : Assignment Q K} (hb : ∑ v : V, b v = 0) (g : { g : Flow (excessCapacity cap b) (Sum.inr false) (Sum.inr true) // g.val = ∑ v : V, max (b v) 0 }) :
          (zeroAuxFlowEquiv hb).symm g = (↑g).toExcessFlow hb ⋯
          source
          @[simp]
          theorem TauCeti.ExcessFlow.toAuxFlow_toExcessFlow {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] [DecidableEq V] {b : V → K} {cap : Assignment Q K} (hb : ∑ v : V, b v = 0) (f : ExcessFlow 0 cap b) :
          f.toAuxFlow.toExcessFlow hb ⋯ = f

          Restriction after extension recovers the original prescribed-excess assignment.

          source
          def TauCeti.ExcessFlow.auxFlowEquiv {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] [DecidableEq V] (lo hi : Assignment Q K) (b : V → K) (hb : ∑ v : V, b v = 0) :
          ExcessFlow lo hi b ≃ { g : Flow (excessCapacity (hi - lo) (b - excessAt lo)) (Sum.inr false) (Sum.inr true) // g.val = ∑ v : V, max ((b - excessAt lo) v) 0 }

          Subtracting the lower bound gives an equivalence with ordinary auxiliary flows of the required value for the shifted excess. The lower bound need not itself be feasible.

          Instances For
            source
            @[simp]
            theorem TauCeti.ExcessFlow.auxFlowEquiv_apply_original {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] [DecidableEq V] {lo hi : Assignment Q K} {b : V → K} (hb : ∑ v : V, b v = 0) (f : ExcessFlow lo hi b) {x y : V} (e : Q x y) :
            (↑((auxFlowEquiv lo hi b hb) f)).toFun (AuxTerminalHom.original e) = ↑f e - lo e
            source
            @[simp]
            theorem TauCeti.ExcessFlow.auxFlowEquiv_symm_apply_original {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] [DecidableEq V] {lo hi : Assignment Q K} {b : V → K} (hb : ∑ v : V, b v = 0) (g : { g : Flow (excessCapacity (hi - lo) (b - excessAt lo)) (Sum.inr false) (Sum.inr true) // g.val = ∑ v : V, max ((b - excessAt lo) v) 0 }) {x y : V} (e : Q x y) :
            ↑((auxFlowEquiv lo hi b hb).symm g) e = (↑g).toFun (AuxTerminalHom.original e) + lo e
            source
            @[simp]
            theorem TauCeti.ExcessFlow.auxFlowEquiv_apply_source {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] [DecidableEq V] {lo hi : Assignment Q K} {b : V → K} (hb : ∑ v : V, b v = 0) (f : ExcessFlow lo hi b) (x : V) :
            (↑((auxFlowEquiv lo hi b hb) f)).toFun (AuxTerminalHom.source ⋯) = max (-(b - excessAt lo) x) 0
            source
            @[simp]
            theorem TauCeti.ExcessFlow.auxFlowEquiv_apply_sink {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] [DecidableEq V] {lo hi : Assignment Q K} {b : V → K} (hb : ∑ v : V, b v = 0) (f : ExcessFlow lo hi b) (x : V) :
            (↑((auxFlowEquiv lo hi b hb) f)).toFun (AuxTerminalHom.sink ⋯) = max ((b - excessAt lo) x) 0
            source
            theorem TauCeti.ExcessFlow.auxFlowEquiv_mem_iff {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] [DecidableEq V] {lo hi : Assignment Q K} {b : V → K} (hb : ∑ v : V, b v = 0) (f : ExcessFlow lo hi b) (H : AddSubgroup K) (hloH : ∀ ⦃x y : V⦄ (e : Q x y), lo e ∈ H) (hbH : ∀ (v : V), b v ∈ H) :
            (∀ ⦃x y : V ⊕ Bool⦄ (e : AuxTerminalHom Q Finset.univ Finset.univ x y), (↑((auxFlowEquiv lo hi b hb) f)).toFun e ∈ H) ↔ ∀ ⦃x y : V⦄ (e : Q x y), ↑f e ∈ H

            The signed auxiliary reduction preserves subgroup values in both directions.

            source
            @[simp]
            theorem TauCeti.Flow.toExcessFlow_toAuxFlow {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] [DecidableEq V] {cap : Assignment Q K} {b : V → K} (g : Flow (excessCapacity cap b) (Sum.inr false) (Sum.inr true)) (hb : ∑ v : V, b v = 0) (hg : g.val = ∑ v : V, max (b v) 0) :
            (g.toExcessFlow hb hg).toAuxFlow = g

            Extension after restriction recovers an auxiliary flow of the required value.

            source
            theorem TauCeti.sum_max_le_arrowSum_excessCapacity {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] [DecidableEq V] {cap : Assignment Q K} {b : V → K} (hb : ∑ v : V, b v = 0) (hcut : ∀ (S : Finset V), ∑ v ∈ S, b v ≤ arrowSum cap Sᶜ S) {S : Finset (V ⊕ Bool)} (hσ : Sum.inr false ∈ S) (hτ : Sum.inr true ∉ S) :
            ∑ v : V, max (b v) 0 ≤ arrowSum (excessCapacity cap b) S Sᶜ

            Every auxiliary terminal cut has at least the required value when every original cut satisfies the prescribed-excess inequality.

            source
            theorem TauCeti.ExcessFlow.exists_mem_of_forall_cut_zero {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] [DecidableEq V] {cap : Assignment Q K} {b : V → K} (hcap : 0 ≤ cap) (hb : ∑ v : V, b v = 0) (hcut : ∀ (S : Finset V), ∑ v ∈ S, b v ≤ arrowSum cap Sᶜ S) (H : AddSubgroup K) (hcapH : ∀ ⦃x y : V⦄ (e : Q x y), cap e ∈ H) (hbH : ∀ (v : V), b v ∈ H) :
            ∃ (f : ExcessFlow 0 cap b), ∀ ⦃x y : V⦄ (e : Q x y), ↑f e ∈ H

            Nonnegative capacities and balanced prescribed excess admit a subgroup-valued realization whenever every cut can supply its prescribed demand.

            source
            theorem TauCeti.ExcessFlow.exists_mem_of_forall_cut {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] [DecidableEq V] {lo hi : Assignment Q K} {b : V → K} (hlo : lo ≤ hi) (hb : ∑ v : V, b v = 0) (hcut : ∀ (S : Finset V), ∑ v ∈ S, b v + arrowSum lo S Sᶜ ≤ arrowSum hi Sᶜ S) (H : AddSubgroup K) (hloH : ∀ ⦃x y : V⦄ (e : Q x y), lo e ∈ H) (hhiH : ∀ ⦃x y : V⦄ (e : Q x y), hi e ∈ H) (hbH : ∀ (v : V), b v ∈ H) :
            ∃ (f : ExcessFlow lo hi b), ∀ ⦃x y : V⦄ (e : Q x y), ↑f e ∈ H

            Integrality of prescribed-excess feasibility. Signed bounds and prescribed excess in an additive subgroup have a realization in that subgroup if the balance and cut conditions hold.

            source
            theorem TauCeti.ExcessFlow.nonempty_iff {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] [DecidableEq V] {lo hi : Assignment Q K} {b : V → K} (hlo : lo ≤ hi) :
            Nonempty (ExcessFlow lo hi b) ↔ ∑ v : V, b v = 0 ∧ ∀ (S : Finset V), ∑ v ∈ S, b v + arrowSum lo S Sᶜ ≤ arrowSum hi Sᶜ S

            Generalized Hoffman's theorem. Ordered signed bounds admit an assignment of prescribed excess exactly when that excess is balanced and every cut can supply its demand.

            source
            theorem TauCeti.ExcessFlow.exists_mem_iff {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] [DecidableEq V] {lo hi : Assignment Q K} {b : V → K} (hlo : lo ≤ hi) (H : AddSubgroup K) (hloH : ∀ ⦃x y : V⦄ (e : Q x y), lo e ∈ H) (hhiH : ∀ ⦃x y : V⦄ (e : Q x y), hi e ∈ H) (hbH : ∀ (v : V), b v ∈ H) :
            (∃ (f : ExcessFlow lo hi b), ∀ ⦃x y : V⦄ (e : Q x y), ↑f e ∈ H) ↔ ∑ v : V, b v = 0 ∧ ∀ (S : Finset V), ∑ v ∈ S, b v + arrowSum lo S Sᶜ ≤ arrowSum hi Sᶜ S

            Subgroup-valued feasibility has the same balance and cut criterion as unrestricted feasibility when both bounds and prescribed excess take values in the subgroup.

            source
            theorem TauCeti.ExcessFlow.not_nonempty_iff {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] [DecidableEq V] {lo hi : Assignment Q K} {b : V → K} (hlo : lo ≤ hi) :
            ¬Nonempty (ExcessFlow lo hi b) ↔ ∑ v : V, b v ≠ 0 ∨ ∃ (S : Finset V), arrowSum hi Sᶜ S < ∑ v ∈ S, b v + arrowSum lo S Sᶜ

            An infeasible prescribed-excess problem has either nonzero total excess or a strictly violating vertex set. Conversely, either certificate rules out every feasible assignment.

            source
            theorem TauCeti.ExcessFlow.nonempty_or_certificate {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] [DecidableEq V] {lo hi : Assignment Q K} {b : V → K} (hlo : lo ≤ hi) :
            Nonempty (ExcessFlow lo hi b) ∨ ∑ v : V, b v ≠ 0 ∨ ∃ (S : Finset V), arrowSum hi Sᶜ S < ∑ v ∈ S, b v + arrowSum lo S Sᶜ

            Either the prescribed excess is realized, or its total is nonzero, or a vertex set strictly violates the feasibility inequality.

            source
            theorem TauCeti.exists_isCirculation_iff {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] [DecidableEq V] {lo hi : Assignment Q K} (hlo : lo ≤ hi) :
            (∃ f ∈ Set.Icc lo hi, IsCirculation f) ↔ ∀ (S : Finset V), arrowSum lo Sᶜ S ≤ arrowSum hi S Sᶜ

            Hoffman's circulation theorem. A bounded circulation exists exactly when every vertex set has total lower bound entering it at most the total upper bound leaving it.

            source
            theorem TauCeti.exists_isCirculation_mem_iff {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] [DecidableEq V] {lo hi : Assignment Q K} (hlo : lo ≤ hi) (H : AddSubgroup K) (hloH : ∀ ⦃x y : V⦄ (e : Q x y), lo e ∈ H) (hhiH : ∀ ⦃x y : V⦄ (e : Q x y), hi e ∈ H) :
            (∃ f ∈ Set.Icc lo hi, IsCirculation f ∧ ∀ ⦃x y : V⦄ (e : Q x y), f e ∈ H) ↔ ∀ (S : Finset V), arrowSum lo Sᶜ S ≤ arrowSum hi S Sᶜ

            Hoffman's cut criterion also characterizes subgroup-valued circulations when both bounds lie in the additive subgroup.

            source
            theorem TauCeti.not_exists_isCirculation_iff {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] [DecidableEq V] {lo hi : Assignment Q K} (hlo : lo ≤ hi) :
            (¬∃ f ∈ Set.Icc lo hi, IsCirculation f) ↔ ∃ (S : Finset V), arrowSum hi S Sᶜ < arrowSum lo Sᶜ S

            Infeasibility of a circulation is witnessed by a strict Hoffman cut.

            source
            theorem TauCeti.exists_isCirculation_or_cut {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] [DecidableEq V] {lo hi : Assignment Q K} (hlo : lo ≤ hi) :
            (∃ f ∈ Set.Icc lo hi, IsCirculation f) ∨ ∃ (S : Finset V), arrowSum hi S Sᶜ < arrowSum lo Sᶜ S

            Either a bounded circulation exists or a strict Hoffman cut certifies infeasibility.

            Signed feasibility and obstruction examples #