Decoding the actual registered LP solver output
Lax263307.RegisteredLP · concepts/Lax263307/RegisteredLP.lean · lax-263307
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
Read the tagged rational certificate returned by the registered exact LP solver. The decoded certificate is valid for the supplied program, in all dimensions and for all three outcomes. This provides the concrete solver function used by the projection branch of the round-or-cut algorithm.
Concept map
Evidence
Each proof establishes this claim relative to its assumptions.
Lean source view on GitHub
| 1 | import Lax109476.PolynomialTimeSolver |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: Decoding the actual registered LP solver output |
| 6 | type: theorem |
| 7 | --- |
| 8 | Read the tagged rational certificate returned by the registered exact LP |
| 9 | solver. The decoded certificate is valid for the supplied program, in all |
| 10 | dimensions and for all three outcomes. This provides the concrete solver |
| 11 | function used by the projection branch of the round-or-cut algorithm. |
| 12 | |
| 13 | # Formalization notes |
| 14 | |
| 15 | The parser and fallback are total and computable. The fallback is never used |
| 16 | on the registered solver's output. The parser matches the verified parser |
| 17 | in the registered Leighton–Rao proof package; an induction identifies the |
| 18 | parsers and reuses its encoding theorem. The surrounding RAM invocation remains a separate |
| 19 | implementation obligation. |
| 20 | -/ |
| 21 | |
| 22 | namespace Lax263307.RegisteredLP |
| 23 | |
| 24 | open Lax109476.LinearProgram Lax109476.RationalCertificates Lax109476.RationalEncoding |
| 25 | |
| 26 | def value (sign num den : ℕ) : ℚ := |
| 27 | if sign = 1 then -(num : ℚ) / den else (num : ℚ) / den |
| 28 | |
| 29 | def rational : List ℕ → Option (ℚ × List ℕ) |
| 30 | | sign :: num :: den :: rest => some (value sign num den, rest) |
| 31 | | _ => none |
| 32 | |
| 33 | def vector : ℕ → List ℕ → Option (List ℚ × List ℕ) |
| 34 | | 0, input => some ([], input) |
| 35 | | n + 1, input => (rational input).bind fun qr => |
| 36 | (vector n qr.2).map fun tail => (qr.1 :: tail.1, tail.2) |
| 37 | |
| 38 | def vectorFunction (n : ℕ) (input : List ℕ) : Option ((Fin n → ℚ) × List ℕ) := |
| 39 | (vector n input).map fun result => (fun i => result.1.getD i.val 0, result.2) |
| 40 | |
| 41 | def parse (m n : ℕ) : List ℕ → Option (Certificate m n × List ℕ) |
| 42 | | 0 :: rest => (vectorFunction n rest).bind fun zr => |
| 43 | (vectorFunction m zr.2).map fun yr => (.optimal zr.1 yr.1, yr.2) |
| 44 | | 1 :: rest => (vectorFunction m rest).map fun yr => (.infeasible yr.1, yr.2) |
| 45 | | 2 :: rest => (vectorFunction n rest).bind fun zr => |
| 46 | (vectorFunction n zr.2).map fun dr => (.unbounded zr.1 dr.1, dr.2) |
| 47 | | _ => none |
| 48 | |
| 49 | def certificate {m n : ℕ} (solve : List ℕ → List ℕ) (P : Program ℚ m n) : Certificate m n := |
| 50 | ((parse m n (solve (encodeProgram P))).map Prod.fst).getD (.infeasible 0) |
| 51 | |
| 52 | axiom exists_solver : ∃ solve : List ℕ → List ℕ, Lax759944.RamPolytime.RamPolytime solve ∧ |
| 53 | ∀ (m n : ℕ) (P : Program ℚ m n), IsValidCertificate P (certificate solve P) |
| 54 | |
| 55 | end Lax263307.RegisteredLP |
| 56 |
Formalization notes
The parser and fallback are total and computable. The fallback is never used on the registered solver's output. The parser matches the verified parser in the registered Leighton–Rao proof package; an induction identifies the parsers and reuses its encoding theorem. The surrounding RAM invocation remains a separate implementation obligation.
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments