Reference · Signed rationals

rainbow.math.rational.signed.lp-certificate

Signed rationalssrc/rainbow/math/rational/signed/lp_certificate.clj0 definitions, 3 theorems

A worked LP optimality certificate on concrete numbers, including a NEGATIVE cost -- the per-instance end of the verified-optimization pipeline. The program is a two-product mix where the second product carries a penalty rather than a margin: maximize 2*x0 - 1*x1 subject to x0 + x1 <= 4 (shared capacity) x0 <= 3 (a line limit) x >= 0 The proposed decision is x = (3, 0) and the proposed dual price vector is y = (0, 2): capacity is not binding so it prices at zero, the line limit is binding so it carries the whole margin. Both objectives evaluate to 6, so the duality gap is closed and the pair is a certificate. What the kernel then checks is `optimization/signed-lp-worked-optimal` : no feasible plan scores above 6. Two things make this the shape a buyer can use. First, the cost -1 is not expressible in the nnrat LP stack at all, so this instance is only checkable through the signed theorems. Real programs have penalties, and a checker that cannot represent them checks nothing that matters. Second, EVERY hypothesis is discharged by computation. Feasibility, dual feasibility and nonnegativity are each `signed/decide-at-most-true-sound` applied to a reflexivity witness: the comparison reduces, reflexivity records that it reduced to `true`, soundness converts it. No inequality here was proved by hand. That is what makes the pattern cheap enough to run per instance while the expensive theorem -- `optimization/signed-lp-optimality-certificate`, proved once for every matrix, cost vector and dual vector -- is reused unchanged. Native and axiom-free on D63; chains the signed LP duality theorems and the decidable signed order.

Depends onmath.rational.signed.lp-dualitymath.rational.signed.decide-order

optimization/signed-lp-worked-dual-bound :
  → Σ j∈[data/false, data/true], (fun index => data/Bool.rec (fun x₃ => ℚ) 2 -1 index) j · (fun index => data/Bool.rec (fun x₆ => ℚ) 3 0 index) j ≤ Σ i∈[data/false, data/true], (fun index => data/Bool.rec (fun x₉ => ℚ) 4 3 index) i · (fun index => data/Bool.rec (fun x₁₂ => ℚ) 0 2 index) i

optimization/signed-lp-worked-value :
  → Σ j∈[data/false, data/true], (fun index => data/Bool.rec (fun x₃ => ℚ) 2 -1 index) j · (fun index => data/Bool.rec (fun x₆ => ℚ) 3 0 index) j = 6

optimization/signed-lp-worked-optimal :
  (candidate : data/Bool → ℚ)
  (candidate-feasible : ∀ (i : data/Bool), Σ j∈[data/false, data/true], (fun row => data/Bool.rec (fun x₁₂ => data/Bool → ℚ) (fun index => data/Bool.rec (fun x₁₅ => ℚ) 1 1 index) (fun index => data/Bool.rec (fun x₁₈ => ℚ) 1 0 index) row) i j · candidate j ≤ (fun index => data/Bool.rec (fun x₂₁ => ℚ) 4 3 index) i)
  (candidate-nonnegative : ∀ (j : data/Bool), 0 ≤ candidate j)
  → Σ j∈[data/false, data/true], (fun index => data/Bool.rec (fun x₂₄ => ℚ) 2 -1 index) j · candidate j ≤ Σ j∈[data/false, data/true], (fun index => data/Bool.rec (fun x₂₇ => ℚ) 2 -1 index) j · (fun index => data/Bool.rec (fun x₃₀ => ℚ) 3 0 index) j