Reference · Signed rationals

rainbow.math.rational.signed.lp-certificate-reflect

Signed rationalssrc/rainbow/math/rational/signed/lp_certificate_reflect.clj2 definitions, 2 theorems

LP optimality certificates by reflection over finite row and column lists. The Boolean checker decides primal feasibility, dual feasibility, both nonnegativity conditions and the signed-equivalence objective gap. Its native, axiom-free soundness theorem applies the existing list-quantified LP theorem. A concrete certificate needs one theorem application and a true-reflexivity witness; the kernel computes the checker on the supplied data. The application still contains that data, so total proof size is not independent of the input.

Depends onmath.rational.signed.lp-duality-onmath.rational.signed.decide-equivalence

lp/all-at-most-decide.{u} :
  (A : Type u) (f g : A → ℚ) (x₁ : List A)
  → data/Bool

lp/certificate-check.{u} :
  (A B : Type u) (M : A → B → ℚ) (b : A → ℚ) (c x : B → ℚ) (y : A → ℚ) (rows : List A)
  (cols : List B)
  → data/Bool

lp/all-at-most-decide-sound.{u} :
  (A : Type u) (f g : A → ℚ) (xs : List A)
  (h₁ : lp/all-at-most-decide A f g xs = data/true)
  → ∀ i ∈ xs, f i ≤ g i

lp/certificate-check-sound.{u} :
  (A B : Type u) (M : A → B → ℚ) (b : A → ℚ) (c x : B → ℚ) (y : A → ℚ) (rows : List A)
  (cols : List B)
  (checked : lp/certificate-check A B M b c x y rows cols = data/true)
  (candidate : B → ℚ)
  (candidate-feasible : ∀ i ∈ rows, Σ j∈cols, M i j · candidate j ≤ b i)
  (candidate-nonnegative : ∀ i ∈ cols, 0 ≤ candidate i)
  → Σ j∈cols, c j · candidate j ≤ Σ j∈cols, c j · x j