Lax Lean Archive

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

Soundness of exact rational LP certificates

Lax109476.CertificateSoundness · concepts/Lax109476/CertificateSoundness.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 valid rational certificate establishes its claimed outcome for the linear program over real variables. Matching primal and dual objectives certify optimality, Farkas multipliers certify infeasibility, and a feasible point with an improving recession direction certifies unboundedness.

    Concept map
    5 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.RationalCertificates
    2
    3/-!
    4---
    5title: Soundness of exact rational LP certificates
    6type: theorem
    7---
    8Every valid rational certificate establishes its claimed outcome for the
    9linear program over real variables. Matching primal and dual objectives
    10certify optimality, Farkas multipliers certify infeasibility, and a feasible
    11point with an improving recession direction certifies unboundedness.
    12
    13# Formalization notes
    14
    15Rational arithmetic is transferred exactly to the real interpretation.
    16Optimality uses weak duality; infeasibility uses certificate soundness;
    17unboundedness follows by taking arbitrarily large nonnegative multiples
    18of the certified recession direction. No solver or certificate-existence
    19theorem is needed to check a supplied certificate.
    20-/
    21
    22namespace Lax109476.CertificateSoundness
    23
    24open Lax109476.LinearProgram Lax109476.RationalCertificates
    25
    26/-- Exact rational certificate checks imply the asserted real LP outcome. -/
    27axiom valid_certificate_correct :
    28 ∀ (m n : ℕ) (P : Program ℚ m n) (certificate : Certificate m n),
    29 IsValidCertificate P certificate → IsCorrectOutcome P certificate
    30
    31end Lax109476.CertificateSoundness
    32
    Show Proof
    Formalization notes

    Rational arithmetic is transferred exactly to the real interpretation. Optimality uses weak duality; infeasibility uses certificate soundness; unboundedness follows by taking arbitrarily large nonnegative multiples of the certified recession direction. No solver or certificate-existence theorem is needed to check a supplied certificate.

    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…