Exact rational solution certificates
Lax109476.RationalCertificates · concepts/Lax109476/RationalCertificates.lean · lax-109476
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
A rational linear program is a linear program with rational coefficients, still optimized over real variables. Its outcomes have three certificate forms:
- an optimal primal point and matching dual multipliers;
- nonnegative Farkas multipliers certifying infeasibility;
- a feasible primal point and an improving recession direction certifying unboundedness.
Every coordinate in these certificates is rational, and all certificate conditions can be checked by exact rational arithmetic.
Concept map
Lean source view on GitHub
| 1 | import Lax109476.FarkasCertificate |
| 2 | import Lax109476.RecessionDirection |
| 3 | import Mathlib.Data.Rat.Cast.Order |
| 4 | |
| 5 | /-! |
| 6 | --- |
| 7 | title: Exact rational solution certificates |
| 8 | type: definition |
| 9 | --- |
| 10 | A rational linear program is a linear program with rational coefficients, |
| 11 | still optimized over real variables. Its outcomes have three certificate forms: |
| 12 | |
| 13 | * an optimal primal point and matching dual multipliers; |
| 14 | * nonnegative Farkas multipliers certifying infeasibility; |
| 15 | * a feasible primal point and an improving recession direction certifying |
| 16 | unboundedness. |
| 17 | |
| 18 | Every coordinate in these certificates is rational, and all certificate |
| 19 | conditions can be checked by exact rational arithmetic. |
| 20 | |
| 21 | # Formalization notes |
| 22 | |
| 23 | The three constructors carry precisely the witnesses needed for their |
| 24 | claims. The predicates use the same row, column, and objective formulas |
| 25 | as the real program. The real interpretation casts the coefficient data |
| 26 | and witness coordinates exactly. No outcome or correctness proof is |
| 27 | assumed as part of the input. |
| 28 | -/ |
| 29 | |
| 30 | namespace Lax109476.RationalCertificates |
| 31 | |
| 32 | open Lax109476.LinearProgram Lax109476.FarkasCertificate Lax109476.RecessionDirection |
| 33 | |
| 34 | /-- Interpret rational coefficient data as a real linear program. -/ |
| 35 | def toReal {m n : ℕ} (P : Program ℚ m n) : Program ℝ m n where |
| 36 | A i j := P.A i j |
| 37 | b i := P.b i |
| 38 | c j := P.c j |
| 39 | |
| 40 | /-- The exact real interpretation of a rational vector. -/ |
| 41 | def realVector {n : ℕ} (x : Fin n → ℚ) : Fin n → ℝ := fun j => x j |
| 42 | |
| 43 | /-- A rational certificate for one of the three possible LP outcomes. -/ |
| 44 | inductive Certificate (m n : ℕ) |
| 45 | /-- Primal and dual points with matching objectives. -/ |
| 46 | | optimal (x : Fin n → ℚ) (y : Fin m → ℚ) |
| 47 | /-- Separating nonnegative multipliers for an infeasible primal system. -/ |
| 48 | | infeasible (y : Fin m → ℚ) |
| 49 | /-- A feasible base point and an improving recession direction. -/ |
| 50 | | unbounded (x d : Fin n → ℚ) |
| 51 | |
| 52 | /-- The exact rational inequalities and equalities validating a certificate. -/ |
| 53 | def IsValidCertificate {m n : ℕ} (P : Program ℚ m n) : Certificate m n → Prop |
| 54 | | .optimal x y => PrimalFeasible P x ∧ DualFeasible P y ∧ primalValue P x = dualValue P y |
| 55 | | .infeasible y => IsInfeasibilityCertificate P y |
| 56 | | .unbounded x d => PrimalFeasible P x ∧ IsImprovingDirection P d |
| 57 | |
| 58 | /-- The real mathematical claim made by each certificate constructor. -/ |
| 59 | def IsCorrectOutcome {m n : ℕ} (P : Program ℚ m n) : Certificate m n → Prop |
| 60 | | .optimal x _ => IsPrimalOptimal (toReal P) (realVector x) |
| 61 | | .infeasible _ => ¬ IsFeasible (toReal P) |
| 62 | | .unbounded _ _ => IsFeasible (toReal P) ∧ ¬ IsBoundedAbove (toReal P) |
| 63 | |
| 64 | end Lax109476.RationalCertificates |
| 65 |
Formalization notes
The three constructors carry precisely the witnesses needed for their claims. The predicates use the same row, column, and objective formulas as the real program. The real interpretation casts the coefficient data and witness coordinates exactly. No outcome or correctness proof is assumed as part of the input.
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments