Lax Lean Archive

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

Improving directions certify unboundedness

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

    A feasible point xx and an improving recession direction dd certify that the objective is unbounded above. For every t≥0t\ge0, the point x+tdx+td is feasible and has objective cTx+tcTdc^T x+t c^T d, which tends to infinity.

    Concept map
    3 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.RecessionDirection
    2
    3/-!
    4---
    5title: Improving directions certify unboundedness
    6type: theorem
    7---
    8A feasible point xx and an improving recession direction dd certify that
    9the objective is unbounded above. For every t≥0t\ge0, the point x+tdx+td is
    10feasible and has objective cTx+tcTdc^T x+t c^T d, which tends to infinity.
    11
    12# Formalization notes
    13
    14The feasible base point is essential: an improving direction by itself
    15does not imply that the program has any feasible points. This is certificate
    16soundness and does not assert existence of a rational recession certificate.
    17-/
    18
    19namespace Lax109476.RecessionSoundness
    20
    21open Lax109476.LinearProgram Lax109476.RecessionDirection
    22
    23/-- A feasible base point and an improving direction rule out any objective bound. -/
    24axiom direction_not_bounded :
    25 ∀ (m n : ℕ) (P : Program ℝ m n) (x d : Fin n → ℝ),
    26 PrimalFeasible P x → IsImprovingDirection P d → ¬ IsBoundedAbove P
    27
    28end Lax109476.RecessionSoundness
    29
    Show Proof
    Formalization notes

    The feasible base point is essential: an improving direction by itself does not imply that the program has any feasible points. This is certificate soundness and does not assert existence of a rational recession 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…