Reference · Non-negative rationals
rainbow.math.rational.nnrat.lp-strong-duality
Concrete textbook strong duality for a verified Bool-indexed 2x2 LP. Instance (rows and columns enumerate [true,false]): maximize x_0 + x_1 subject to x_0 + x_1 <= 2 in each row, x >= 0. The exhibited primal point is x=(1,1), and the exhibited dual point is y=(1,0). The named theorem bundles all five facts that make this a genuine strong-duality witness: x is primal feasible, y is dual feasible, their objectives are equivalent, x bounds every primal-feasible alternative from above, and y bounds every dual-feasible alternative from below. nnrat/lp-example-strong-duality : primal-feasible(x) /\ dual-feasible(y) /\ c.x ~ b.y /\ (forall x', primal-feasible(x') -> c.x' <= c.x) /\ (forall y', dual-feasible(y') -> b.y <= b.y') The two optimality components instantiate the general primal and dual LP optimality certificates. All evidence is native proof data and axiom-free.
nnrat/lp-example-strong-duality
nnrat/lp-example-strong-duality : → proposition/conjunction (∀ (i : data/Bool), nnrat/map-sum data/Bool (fun j => (fun x₂₉₇ => fun x₂₉₈ => 1) i j · (fun x₂₉₉ => 1) j) [data/true, data/false] ≤ (fun x₃₀₀ => 2) i) (proposition/conjunction (∀ (j : data/Bool), (fun x₄₄₇ => 1) j ≤ nnrat/map-sum data/Bool (fun i => (fun x₄₄₈ => fun x₄₄₉ => 1) i j · (fun i₁ => data/Bool.rec (fun x₄₅₂ => ℚ≥0) 0 1 i₁) i) [data/true, data/false]) (proposition/conjunction (nnrat/map-sum data/Bool (fun j => (fun x₅₂₇ => 1) j · (fun x₅₂₈ => 1) j) [data/true, data/false] = nnrat/map-sum data/Bool (fun i => (fun x₅₃₇ => 2) i · (fun i₁ => data/Bool.rec (fun x₅₄₀ => ℚ≥0) 0 1 i₁) i) [data/true, data/false]) (proposition/conjunction (∀ (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] ≤ nnrat/map-sum data/Bool (fun j => (fun x₅₇₅ => 1) j · (fun x₅₇₆ => 1) j) [data/true, data/false]) (∀ (y-alt : data/Bool → ℚ≥0), ∀ (hd-alt : ∀ (j : data/Bool), (fun x₅₇₇ => 1) j ≤ nnrat/map-sum data/Bool (fun i => (fun x₅₇₈ => fun x₅₇₉ => 1) i j · y-alt i) [data/true, data/false]), nnrat/map-sum data/Bool (fun i => (fun x₅₈₈ => 2) i · (fun i₁ => data/Bool.rec (fun x₅₉₁ => ℚ≥0) 0 1 i₁) i) [data/true, data/false] ≤ nnrat/map-sum data/Bool (fun i => (fun x₅₉₂ => 2) i · y-alt i) [data/true, data/false]))))
0 = nnrat/zero1 = nnrat/one= = nnrat/equivalent: equality of rational values· = nnrat/multiplyℚ≥0 = nnrat/NonnegativeRational≤ = nnrat/at-most