Reference · Non-negative rationals

rainbow.math.rational.nnrat.lp-example

Non-negative rationalssrc/rainbow/math/rational/nnrat/lp_example.clj0 definitions, 1 theorems

A concrete, fully worked LP with a machine-checked optimality certificate -- the tangible 'sellable' artifact: a real optimization instance whose proposed solution is PROVEN optimal by the kernel, with no trust in any solver. Instance (indices = Bool, so 2 constraints and 2 variables; rows=cols=[true,false]): maximize c.x = x_0 + x_1 s.t. x_0 + x_1 <= 2 (both constraints identical, A = all ones) x >= 0 Proposed primal x = (1, 1) (objective 2); dual y = (1, 0) (objective 2). y is dual feasible (A^T y = (1,1) >= c = (1,1)) and the objectives match (c.x = 2 = b.y), a zero duality gap -- so by lp-optimality-certificate x is a maximizer. nnrat/lp-example-x-optimal : forall x' : Bool -> nnrat, (forall i, (A x')_i <= b_i) -> c.x' <= 2 i.e. no feasible point beats x's objective of 2. Numbers are chosen so every feasibility/gap check reduces to reflexivity (y=(1,0) keeps arithmetic integral). Native and axiom-free; instantiates nnrat/lp-optimality-certificate.

Depends onmath.rational.nnrat.lp-optimality

nnrat/lp-example-x-optimal :
  (x-alt : data/Bool → ℚ≥0)
  (hp-alt : ∀ (i : data/Bool), nnrat/map-sum data/Bool (fun j => (fun x₁ => fun x₂ => 1) i j · x-alt j) [data/true, data/false] ≤ (fun x₃ => 2) i)
  → nnrat/map-sum data/Bool (fun j => (fun x₆ => 1) j · x-alt j) [data/true, data/false] ≤ 2