Lax Lean Archive

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

Exact rational certificates exist for all linear-programming outcomes

Lax109476.CertificateExistence · concepts/Lax109476/CertificateExistence.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

    Every rational linear program has an exact rational certificate: a matching primal–dual pair, nonnegative Farkas multipliers, or a feasible point and an improving recession direction.

    Concept map
    11 concepts
    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.RationalFeasibility
    2import Lax109476.StrongDuality
    3import Lax109476.RecessionExistence
    4
    5/-!
    6---
    7title: Exact rational certificates exist for all linear-programming outcomes
    8type: theorem
    9---
    10Every rational linear program has an exact rational certificate: a matching
    11primal–dual pair, nonnegative Farkas multipliers, or a feasible point and
    12an improving recession direction.
    13
    14# Formalization notes
    15
    16The certificate conditions are checked in the rationals and describe
    17optimization over real variables. This is an existence theorem independent
    18of polynomial-time solvability. It does not assert a size or runtime bound.
    19-/
    20
    21namespace Lax109476.CertificateExistence
    22
    23open Lax109476.LinearProgram Lax109476.RationalCertificates
    24
    25/-- Every rational coefficient input has an exact valid outcome certificate. -/
    26axiom exists_valid_certificate :
    27 ∀ (m n : ℕ) (P : Program ℚ m n), ∃ certificate : Certificate m n,
    28 IsValidCertificate P certificate
    29
    30end Lax109476.CertificateExistence
    31
    Show Proof
    Formalization notes

    The certificate conditions are checked in the rationals and describe optimization over real variables. This is an existence theorem independent of polynomial-time solvability. It does not assert a size or runtime bound.

    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

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

    Loading discussion…