Rational flow instances and certificates
Lax455465.RationalEncoding · concepts/Lax455465/RationalEncoding.lean · lax-455465
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
Finite algorithms receive nonnegative rational capacities and vertex weights. Each rational is encoded by its reduced numerator and positive denominator. An instance contains its edge model, number of vertices, vertex weights in vertex order, and full capacity matrix in row order. A cut is encoded by its length- membership word. An ordinary flow certificate contains its claimed value and the commodity/arc amounts. A short-path certificate instead contains its value and a list of paths with rational flow amounts.
Concept map
Lean source view on GitHub
| 1 | import Lax455465.ConcurrentFlow |
| 2 | import Lax759944.RamPolytime |
| 3 | import Mathlib.Data.NNRat.Lemmas |
| 4 | |
| 5 | /-! |
| 6 | --- |
| 7 | title: Rational flow instances and certificates |
| 8 | type: definition |
| 9 | --- |
| 10 | Finite algorithms receive nonnegative rational capacities and vertex weights. |
| 11 | Each rational is encoded by its reduced numerator and positive denominator. |
| 12 | An instance contains its edge model, number of vertices, vertex weights in |
| 13 | vertex order, and full capacity matrix in row order. A cut is encoded by |
| 14 | its length- membership word. An ordinary flow certificate contains its claimed value and the |
| 15 | commodity/arc amounts. A short-path certificate instead contains its value |
| 16 | and a list of paths with rational flow amounts. |
| 17 | |
| 18 | # Formalization notes |
| 19 | |
| 20 | The dense encoding covers arbitrary rational capacities and weights, including |
| 21 | zero weights and absent edges. The first entry distinguishes directed from |
| 22 | undirected instances. Cut entries are exactly zero or one. A flow certificate |
| 23 | starts with the numerator and denominator of its value and the number of |
| 24 | path records; each record contains its vertex-count, vertex list, numerator, |
| 25 | and denominator. Repeated path records contribute their summed amount. |
| 26 | |
| 27 | Algorithms use `Lax759944.RamPolytime.RamPolytime` directly. It quantifies |
| 28 | one actual program, polynomial word and instruction bounds in the binary |
| 29 | input size, and exact execution at every sufficiently large word length on |
| 30 | Lax808846's registered word RAM. The physical tape has the length prefix |
| 31 | specified by that predicate. No new machine or abstract cost oracle is used. |
| 32 | The algorithm's function is total; its output on malformed inputs is unconstrained. |
| 33 | -/ |
| 34 | |
| 35 | open scoped NNReal NNRat |
| 36 | |
| 37 | namespace Lax455465.RationalEncoding |
| 38 | |
| 39 | open Lax455465.ProductNetwork Lax455465.ConcurrentFlow |
| 40 | |
| 41 | /-- A product instance with nonnegative rational capacities and weights. -/ |
| 42 | structure RationalInstance (n : ℕ) where |
| 43 | /-- The rational capacity of each edge or directed arc. -/ |
| 44 | capacity : Fin n → Fin n → ℚ≥0 |
| 45 | /-- Loops have zero capacity. -/ |
| 46 | loopless : ∀ v, capacity v v = 0 |
| 47 | /-- The rational weights specifying product demands. -/ |
| 48 | weight : Fin n → ℚ≥0 |
| 49 | |
| 50 | /-- Interpret rational capacities as exact nonnegative real capacities. -/ |
| 51 | def RationalInstance.network {n : ℕ} (I : RationalInstance n) : Network n where |
| 52 | capacity u v := (I.capacity u v : ℝ≥0) |
| 53 | loopless v := by simpa using congrArg (fun q : ℚ≥0 => (q : ℝ≥0)) (I.loopless v) |
| 54 | |
| 55 | /-- Interpret rational vertex weights as exact nonnegative real weights. -/ |
| 56 | def RationalInstance.weights {n : ℕ} (I : RationalInstance n) : VertexWeight n := |
| 57 | fun v => (I.weight v : ℝ≥0) |
| 58 | |
| 59 | /-- Encode a nonnegative rational by its canonical numerator and denominator. -/ |
| 60 | def encodeRational (q : ℚ≥0) : List ℕ := [q.num, q.den] |
| 61 | |
| 62 | /-- Encode the edge model, order, weights, and row-major capacity matrix. -/ |
| 63 | def encodeInput {n : ℕ} (kind : EdgeKind) (I : RationalInstance n) : List ℕ := |
| 64 | [match kind with | .undirected => 0 | .directed => 1, n] ++ |
| 65 | (List.ofFn I.weight).flatMap encodeRational ++ |
| 66 | (List.ofFn fun u => List.ofFn (I.capacity u)).flatten.flatMap encodeRational |
| 67 | |
| 68 | /-- Encode a shore as its length-`n` membership word. -/ |
| 69 | def encodeCut {n : ℕ} (S : Finset (Fin n)) : List ℕ := |
| 70 | List.ofFn fun v => if v ∈ S then 1 else 0 |
| 71 | |
| 72 | /-- A finite rational flow certificate, with its claimed concurrent value. -/ |
| 73 | structure FlowCertificate (n : ℕ) where |
| 74 | /-- The common fraction of demand claimed by the certificate. -/ |
| 75 | value : ℚ≥0 |
| 76 | /-- Paths and their flow amounts; duplicate records are added together. -/ |
| 77 | paths : List (List (Fin n) × ℚ≥0) |
| 78 | |
| 79 | /-- The exact fractional path flow represented by a certificate. -/ |
| 80 | noncomputable def FlowCertificate.flow {n : ℕ} (certificate : FlowCertificate n) : |
| 81 | PathFlow n := |
| 82 | certificate.paths.foldl |
| 83 | (fun F record => F + Finsupp.single record.1 (record.2 : ℝ≥0)) 0 |
| 84 | |
| 85 | /-- Encode a certificate's value and its length-prefixed rational path records. -/ |
| 86 | def encodeFlow {n : ℕ} (certificate : FlowCertificate n) : List ℕ := |
| 87 | encodeRational certificate.value ++ [certificate.paths.length] ++ |
| 88 | certificate.paths.flatMap fun record => |
| 89 | [record.1.length] ++ record.1.map Fin.val ++ encodeRational record.2 |
| 90 | |
| 91 | /-- A polynomial-size rational arc-flow certificate for the ordinary theorem. -/ |
| 92 | structure ArcCertificate (n : ℕ) where |
| 93 | /-- The common demand fraction. -/ |
| 94 | value : ℚ≥0 |
| 95 | /-- The amount assigned to each commodity and directed arc. -/ |
| 96 | arcs : Fin n → Fin n → Fin n → Fin n → ℚ≥0 |
| 97 | |
| 98 | /-- Exact real interpretation of rational commodity/arc amounts. -/ |
| 99 | def ArcCertificate.flow {n : ℕ} (certificate : ArcCertificate n) : ArcFlow n := |
| 100 | fun s t u v => (certificate.arcs s t u v : ℝ≥0) |
| 101 | |
| 102 | /-- The value followed by all n⁴ arc coordinates in index order. -/ |
| 103 | def encodeArcs {n : ℕ} (certificate : ArcCertificate n) : List ℕ := |
| 104 | encodeRational certificate.value ++ |
| 105 | (List.ofFn fun s => List.ofFn fun t => List.ofFn fun u => List.ofFn fun v => |
| 106 | encodeRational (certificate.arcs s t u v)).flatten.flatten.flatten.flatten |
| 107 | |
| 108 | end Lax455465.RationalEncoding |
| 109 |
Formalization notes
The dense encoding covers arbitrary rational capacities and weights, including zero weights and absent edges. The first entry distinguishes directed from undirected instances. Cut entries are exactly zero or one. A flow certificate starts with the numerator and denominator of its value and the number of path records; each record contains its vertex-count, vertex list, numerator, and denominator. Repeated path records contribute their summed amount.
Algorithms use directly. It quantifies one actual program, polynomial word and instruction bounds in the binary input size, and exact execution at every sufficiently large word length on Lax808846's registered word RAM. The physical tape has the length prefix specified by that predicate. No new machine or abstract cost oracle is used. The algorithm's function is total; its output on malformed inputs is unconstrained.
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments