Keyboard shortcuts

Press ← or β†’ to navigate between chapters

Press ? to show this help

Press Esc to hide this help

SupplierDual

Abstract

The finite path-potential and normalized real dual-certificate interface retains the necessary live upstream proofs. The finite incompatibility adapter directly applies the repository frozen inequality_farkas result instead of copying a second Farkas proof. Source: https://github.com/elazarg/multitubes/tree/20d22aa7ca67f9843e5adf9edf173403a2f4033a. These are necessary reusable prerequisites of the circuit supplier.

Generic declarations use these source contexts: universe uV uE variable {π•œ : Type*} [AddCommMonoid π•œ] [LinearOrder π•œ] [IsOrderedAddMonoid π•œ] variable {V : Type uV} {E : Type uE} {G : EdgeGraph V E} variable {π•œg : Type*} [AddCommGroup π•œg] variable {π•œg : Type*} [AddCommGroup π•œg] variable {π•œp : Type*} [Add π•œp] [LE π•œp] variable {π•œg : Type*} [AddCommGroup π•œg] [Preorder π•œg] [IsOrderedAddMonoid π•œg] variable {π•œo : Type*} [AddCommMonoid π•œo] [Preorder π•œo] [IsOrderedAddMonoid π•œo] variable [IsOrderedCancelAddMonoid π•œo] variable [Finite E] variable [IsOrderedCancelAddMonoid π•œ] universe uS uR variable {State : Type uS} {Row Action : Type uR} variable [Fintype State] [Fintype Row] universe uV uE variable {V : Type uV} {E : Type uE}

Definition 1.1 (walkWeight).

Lean statement: D5/S3/Combinatorics/Graph/LayeredCirculation/SupplierDual.walkWeight

Formalization. D5/S3/Combinatorics/Graph/LayeredCirculation/SupplierDual.walkWeight (βœ“ std3).

Source. Repository-derived.

Commentary.

Exact source telescope, in the module declared generic contexts: def walkWeight (weight : E β†’ π•œ) {start finish : V} (walk : G.Walk start finish) : π•œ := (walk.edges.map weight).sum omit [LinearOrder π•œ] in

Theorem 1.2 (walkWeight concat).

Lean statement: D5/S3/Combinatorics/Graph/LayeredCirculation/SupplierDual.walkWeight_concat

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/LayeredCirculation/SupplierDual.walkWeight_concat (βœ“ std3). ∎

Source. Repository-derived.

Commentary.

Exact source telescope, in the module declared generic contexts: @[simp] theorem walkWeight_concat (weight : E β†’ π•œ) {start finish : V} (walk : G.Walk start finish) (edge : E) (legal : G.source edge = finish) : walkWeight weight (walk.concat edge legal) = walkWeight weight walk + weight edge

Theorem 1.3 (walkWeight castFinish).

Lean statement: D5/S3/Combinatorics/Graph/LayeredCirculation/SupplierDual.walkWeight_castFinish

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/LayeredCirculation/SupplierDual.walkWeight_castFinish (βœ“ std3). ∎

Source. Repository-derived.

Commentary.

Exact source telescope, in the module declared generic contexts: @[simp] theorem walkWeight_castFinish (weight : E β†’ π•œ) {start finish finish’ : V} (walk : G.Walk start finish) (hfinish : finish = finish’) : walkWeight weight (walk.castFinish hfinish) = walkWeight weight walk

Definition 1.4 (IsPotential).

Lean statement: D5/S3/Combinatorics/Graph/LayeredCirculation/SupplierDual.IsPotential

Formalization. D5/S3/Combinatorics/Graph/LayeredCirculation/SupplierDual.IsPotential (βœ“ std3).

Source. Repository-derived.

Commentary.

Exact source telescope, in the module declared generic contexts: def IsPotential (G : EdgeGraph V E) (weight : E β†’ π•œp) (Ο† : V β†’ π•œp) : Prop := βˆ€ e : E, Ο† (G.source e) + weight e ≀ Ο† (G.target e)

Definition 1.5 (defect).

Lean statement: D5/S3/Combinatorics/Graph/LayeredCirculation/SupplierDual.defect

Formalization. D5/S3/Combinatorics/Graph/LayeredCirculation/SupplierDual.defect (βœ“ std3).

Source. Repository-derived.

Commentary.

Exact source telescope, in the module declared generic contexts: def defect (G : EdgeGraph V E) (weight : E β†’ π•œg) (Ο† : V β†’ π•œg) (e : E) : π•œg := Ο† (G.source e) + weight e - Ο† (G.target e)

Definition 1.6 (nodupIncomingWeights).

Lean statement: D5/S3/Combinatorics/Graph/LayeredCirculation/SupplierDual.nodupIncomingWeights

Formalization. D5/S3/Combinatorics/Graph/LayeredCirculation/SupplierDual.nodupIncomingWeights (βœ“ std3).

Source. Repository-derived.

Commentary.

Exact source telescope, in the module declared generic contexts: def nodupIncomingWeights (G : EdgeGraph V E) (weight : E β†’ π•œ) (vertex : V) : Set π•œ := {r | βˆƒ (start : V) (walk : G.Walk start vertex), walk.edges.Nodup ∧ walkWeight weight walk = r} omit [LinearOrder π•œ] in

Theorem 1.7 (Nonpositive cycle deletion preserves endpoints and increases weight).

Lean statement: D5/S3/Combinatorics/Graph/LayeredCirculation/SupplierDual.exists_nodup_visited_walkWeight_le

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/LayeredCirculation/SupplierDual.exists_nodup_visited_walkWeight_le (βœ“ std3). ∎

Source. Repository-derived.

Commentary.

If every closed walk has nonpositive weight, every walk of length at most a supplied natural bound has a walk with the same endpoints, no repeated visited vertex, and at least the original weight. Deleting a nonempty closed subwalk decreases length and cannot decrease weight; induction on the bound terminates. In a graph with finitely many vertices the resulting walk has fewer edges than vertices, supplying the finite bound for max-plus relaxation.

Definition 1.8 (maxIncomingWeight).

Lean statement: D5/S3/Combinatorics/Graph/LayeredCirculation/SupplierDual.maxIncomingWeight

Formalization. D5/S3/Combinatorics/Graph/LayeredCirculation/SupplierDual.maxIncomingWeight (βœ“ std3).

Source. Repository-derived.

Commentary.

Exact source telescope, in the module declared generic contexts: def maxIncomingWeight (G : EdgeGraph V E) (weight : E β†’ π•œ) (vertex : V) : π•œ := Finset.max’ (Set.Finite.toFinset (finite_nodupIncomingWeights (G := G) weight vertex)) ((Set.Finite.toFinset_nonempty (finite_nodupIncomingWeights (G := G) weight vertex)).2 ⟨0, zero_mem_nodupIncomingWeights (G := G) weight vertex⟩) omit [IsOrderedAddMonoid π•œ] in

Definition 1.9 (IsNormalizedCertificate).

Lean statement: D5/S3/Combinatorics/Graph/LayeredCirculation/SupplierDual.IsNormalizedCertificate

Formalization. D5/S3/Combinatorics/Graph/LayeredCirculation/SupplierDual.IsNormalizedCertificate (βœ“ std3).

Source. Repository-derived.

Commentary.

Exact source telescope, in the module declared generic contexts: def IsNormalizedCertificate (delta : Row β†’ State β†’ ℝ) (coefficient : Row β†’ ℝ) : Prop := (βˆ€ row, 0 ≀ coefficient row) ∧ (βˆ‘ row, coefficient row = 1) ∧ βˆ€ state, βˆ‘ row, coefficient row * delta row state = 0

Definition 1.10 (certificateValue).

Lean statement: D5/S3/Combinatorics/Graph/LayeredCirculation/SupplierDual.certificateValue

Formalization. D5/S3/Combinatorics/Graph/LayeredCirculation/SupplierDual.certificateValue (βœ“ std3).

Source. Repository-derived.

Commentary.

Exact source telescope, in the module declared generic contexts: def certificateValue (base : Row β†’ ℝ) (coefficient : Row β†’ ℝ) : ℝ := βˆ‘ row, coefficient row * base row

Definition 1.11 (WorstResidualAtMost).

Lean statement: D5/S3/Combinatorics/Graph/LayeredCirculation/SupplierDual.WorstResidualAtMost

Formalization. D5/S3/Combinatorics/Graph/LayeredCirculation/SupplierDual.WorstResidualAtMost (βœ“ std3).

Source. Repository-derived.

Commentary.

Exact source telescope, in the module declared generic contexts: def WorstResidualAtMost (delta : Row β†’ State β†’ ℝ) (base : Row β†’ ℝ) (level : ℝ) : Prop := βˆƒ potential : State β†’ ℝ, βˆ€ row, base row - dotProduct (delta row) potential ≀ level

Theorem 1.12 (worstResidualAtMost iff normalizedDual le).

Lean statement: D5/S3/Combinatorics/Graph/LayeredCirculation/SupplierDual.worstResidualAtMost_iff_normalizedDual_le

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/LayeredCirculation/SupplierDual.worstResidualAtMost_iff_normalizedDual_le (βœ“ std3). ∎

Source. Repository-derived.

Commentary.

Exact source telescope, in the module declared generic contexts: theorem worstResidualAtMost_iff_normalizedDual_le (delta : Row β†’ State β†’ ℝ) (base : Row β†’ ℝ) (level : ℝ) : WorstResidualAtMost delta base level ↔ βˆ€ coefficient : Row β†’ ℝ, IsNormalizedCertificate delta coefficient β†’ certificateValue base coefficient ≀ level

Definition 1.13 (WorstDirectedResidualAtMost).

Lean statement: D5/S3/Combinatorics/Graph/LayeredCirculation/SupplierDual.WorstDirectedResidualAtMost

Formalization. D5/S3/Combinatorics/Graph/LayeredCirculation/SupplierDual.WorstDirectedResidualAtMost (βœ“ std3).

Source. Repository-derived.

Commentary.

Exact source telescope, in the module declared generic contexts: def WorstDirectedResidualAtMost (G : EdgeGraph V E) (weight : E β†’ ℝ) (level : ℝ) : Prop := βˆƒ potential : V β†’ ℝ, βˆ€ edge, MaxPlusPotential.defect G weight potential edge ≀ level

Theorem 1.14 (worstDirectedResidualAtMost iff closedWalk le).

Lean statement: D5/S3/Combinatorics/Graph/LayeredCirculation/SupplierDual.worstDirectedResidualAtMost_iff_closedWalk_le

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/LayeredCirculation/SupplierDual.worstDirectedResidualAtMost_iff_closedWalk_le (βœ“ std3). ∎

Source. Repository-derived.

Commentary.

Exact source telescope, in the module declared generic contexts: theorem worstDirectedResidualAtMost_iff_closedWalk_le [Finite E] (G : EdgeGraph V E) (weight : E β†’ ℝ) (level : ℝ) : WorstDirectedResidualAtMost G weight level ↔ βˆ€ (vertex : V) (cycle : G.Walk vertex vertex), MaxPlusPotential.walkWeight weight cycle ≀ cycle.length * level

Definition 1.15 (SignedEdge).

Lean statement: D5/S3/Combinatorics/Graph/LayeredCirculation/SupplierDual.SignedEdge

Formalization. D5/S3/Combinatorics/Graph/LayeredCirculation/SupplierDual.SignedEdge (βœ“ std3).

Source. Repository-derived.

Commentary.

Exact source telescope, in the module declared generic contexts: abbrev SignedEdge (E : Type uE) := E Γ— Bool

Definition 1.16 (signedDelta).

Lean statement: D5/S3/Combinatorics/Graph/LayeredCirculation/SupplierDual.signedDelta

Formalization. D5/S3/Combinatorics/Graph/LayeredCirculation/SupplierDual.signedDelta (βœ“ std3).

Source. Repository-derived.

Commentary.

Exact source telescope, in the module declared generic contexts: def signedDelta [DecidableEq V] (G : EdgeGraph V E) : SignedEdge E β†’ V β†’ ℝ | (edge, false) => fun vertex => (if vertex = G.target edge then 1 else 0) - (if vertex = G.source edge then 1 else 0) | (edge, true) => fun vertex => (if vertex = G.source edge then 1 else 0) - (if vertex = G.target edge then 1 else 0)

Theorem 1.17 (dotProduct signedDelta false).

Lean statement: D5/S3/Combinatorics/Graph/LayeredCirculation/SupplierDual.dotProduct_signedDelta_false

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/LayeredCirculation/SupplierDual.dotProduct_signedDelta_false (βœ“ std3). ∎

Source. Repository-derived.

Commentary.

Exact source telescope, in the module declared generic contexts: theorem dotProduct_signedDelta_false [Fintype V] [DecidableEq V] (G : EdgeGraph V E) (edge : E) (potential : V β†’ ℝ) : dotProduct (signedDelta G (edge, false)) potential = potential (G.target edge) - potential (G.source edge)

Theorem 1.18 (dotProduct signedDelta true).

Lean statement: D5/S3/Combinatorics/Graph/LayeredCirculation/SupplierDual.dotProduct_signedDelta_true

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/LayeredCirculation/SupplierDual.dotProduct_signedDelta_true (βœ“ std3). ∎

Source. Repository-derived.

Commentary.

Exact source telescope, in the module declared generic contexts: theorem dotProduct_signedDelta_true [Fintype V] [DecidableEq V] (G : EdgeGraph V E) (edge : E) (potential : V β†’ ℝ) : dotProduct (signedDelta G (edge, true)) potential = potential (G.source edge) - potential (G.target edge)

References