Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Soundness of infeasibility certificates

Lax109476.FarkasSoundness · concepts/Lax109476/FarkasSoundness.lean · lax-109476

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    If y≥0y\ge0, ATy≥0A^T y\ge0, and bTy<0b^T y<0, the system Ax≤bAx\le b, x≥0x\ge0 has no solution. This is the elementary soundness direction of the alternative expressed by Farkas' lemma.

    Concept map
    3 concepts; 2 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax109476.FarkasCertificate
    2
    3/-!
    4---
    5title: Soundness of infeasibility certificates
    6type: theorem
    7---
    8If y≥0y\ge0, ATy≥0A^T y\ge0, and bTy<0b^T y<0, the system Ax≤bAx\le b, x≥0x\ge0
    9has no solution. This is the elementary soundness direction of the
    10alternative expressed by Farkas' lemma.
    11
    12# Formalization notes
    13
    14The proof rearranges finite sums and uses nonnegative multipliers. It
    15does not assume the existence direction of Farkas' lemma.
    16-/
    17
    18namespace Lax109476.FarkasSoundness
    19
    20open Lax109476.LinearProgram Lax109476.FarkasCertificate
    21
    22/-- A negative certified upper bound is incompatible with primal feasibility. -/
    23axiom certificate_not_feasible :
    24 ∀ (m n : ℕ) (P : Program ℝ m n) (y : Fin m → ℝ),
    25 IsInfeasibilityCertificate P y → ¬ IsFeasible P
    26
    27end Lax109476.FarkasSoundness
    28
    Show Proof
    Formalization notes

    The proof rearranges finite sums and uses nonnegative multipliers. It does not assume the existence direction of Farkas' lemma.

    Builds on
    Used by
    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…