Exact flow–cut output certificates
Lax455465.FlowCutCertificate · concepts/Lax455465/FlowCutCertificate.lean · lax-455465
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
The output contains both a cut and a rational concurrent flow. For a product instance with positive-weight vertices, the cut has positive demand, the flow is feasible, and their values satisfy
The same output witnesses both sides of the algorithmic flow–cut guarantee. A zero-capacity cut and the zero flow are valid when the instance has no positive concurrent flow.
Concept map
Lean source view on GitHub
| 1 | import Lax455465.RationalEncoding |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: Exact flow–cut output certificates |
| 6 | type: definition |
| 7 | --- |
| 8 | The output contains both a cut and a rational concurrent flow. For a product |
| 9 | instance with positive-weight vertices, the cut has positive demand, the |
| 10 | flow is feasible, and their values satisfy |
| 11 | |
| 12 | The same output witnesses both sides of the algorithmic flow–cut guarantee. |
| 13 | A zero-capacity cut and the zero flow are valid when the instance has no |
| 14 | positive concurrent flow. |
| 15 | |
| 16 | # Formalization notes |
| 17 | |
| 18 | The output starts with the length- cut membership word, followed by the |
| 19 | existing rational arc-flow encoding. Validity is checked against the input; |
| 20 | an output annotation about its approximation ratio is never trusted. |
| 21 | -/ |
| 22 | |
| 23 | open scoped NNReal |
| 24 | |
| 25 | namespace Lax455465.FlowCutCertificate |
| 26 | |
| 27 | open Lax455465.ProductNetwork Lax455465.ConcurrentFlow Lax455465.RationalEncoding |
| 28 | |
| 29 | /-- The cut and rational path flow returned by a flow–cut algorithm. -/ |
| 30 | structure Certificate (n : ℕ) where |
| 31 | /-- One shore of the cut. -/ |
| 32 | cut : Finset (Fin n) |
| 33 | /-- A concurrent flow with an explicitly claimed value. -/ |
| 34 | flow : ArcCertificate n |
| 35 | |
| 36 | /-- The exact output contains the cut followed by the flow certificate. -/ |
| 37 | def encodeCertificate {n : ℕ} (certificate : Certificate n) : List ℕ := |
| 38 | encodeCut certificate.cut ++ encodeArcs certificate.flow |
| 39 | |
| 40 | /-- The joint guarantee for directed and undirected product demands. -/ |
| 41 | def IsValid {n : ℕ} (kind : EdgeKind) (I : RationalInstance n) (C : ℝ) |
| 42 | (certificate : Certificate n) : Prop := |
| 43 | AdmissibleCut I.weights certificate.cut ∧ |
| 44 | IsArcConcurrentFlow kind I.network I.weights |
| 45 | (certificate.flow.value : ℝ≥0) certificate.flow.flow ∧ |
| 46 | (ratioCost I.network I.weights certificate.cut : ℝ) ≤ |
| 47 | C * logFactor (supportCount I.weights) * (certificate.flow.value : ℝ) |
| 48 | |
| 49 | end Lax455465.FlowCutCertificate |
| 50 |
Formalization notes
The output starts with the length- cut membership word, followed by the existing rational arc-flow encoding. Validity is checked against the input; an output annotation about its approximation ratio is never trusted.
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments